static void
ComputeDepth(
Dag_Vertex_t* v,
int p_depth,
Statistics_t* stat
)
- Dfs function
- Defined in
dagEnStat.c
static int
ComputeFatherAndSonNum(
Dag_Vertex_t* f,
char * visData,
nusmv_ptrint sign
)
- Dfs function
- Defined in
dagEnStat.c
static void
DFS(
Dag_Vertex_t * v,
Dag_DfsFunctions_t * dfsFun,
char * dfsData,
nusmv_ptrint vBit
)
- The parameters are:
- v, the current dag vertex
- dfsFun, the functions to perform the DFS
- dfsData, a reference to generic data
- vBit, the incoming link annotation (0 or not-0)
- Side Effects none
- Defined in
dagDfs.c
int
DagVertexComp(
const char * v1,
const char * v2
)
- Gets two vertex pointers v1, v2, (as char pointers) and
compares the symbol, the generic data reference and the
pointers to the sons. Returns -1 if v1 < v2, 0 if v1 =
v2 and 1 if v1 > v2, in lexicographic order of fields.
- Side Effects None
- Defined in
dagVertex.c
int
DagVertexHash(
char* v,
int modulus
)
- Calculate a preliminary index as follows:
v -> symbol +
8 low order bits of (int) (v -> data) +
16 low order bits of each son up to MAXSON +
1 for each son whose edge is annotated
Return the modulus of the index and the actual hash size.
- Side Effects None
- Defined in
dagVertex.c
void
DagVertexInit(
Dag_Manager_t * dagManager,
Dag_Vertex_t * v
)
- Performs several tasks:
- connects the vertex to the sons by increasing the sons'
marks
- removes sons from the free list if their mark
is increased to one for the first time;
- clears the vertex mark and stores the vertex in the
free list;
- clears other internal fields.
- Side Effects none
- Defined in
dagVertex.c
void
Dag_Dfs(
Dag_Vertex_t* dfsRoot,
Dag_DfsFunctions_t* dfsFun,
char* dfsData
)
- The parameters are:
- dfsRoot, the dag vertex where to start the DFS
- dfsFun, the functions to perform the DFS steps
- dfsData, a reference to generic data
The function increments the DFS code for the dag
manager owning dfsRoot and starts the DFS. Increment of
the code guarantees that each node is visited once and
only once. dfsFun -> Set() may change the default behaviour by
forcing to DFS to visit nodes more than once, or by preventing
DFS to do a complete visit.
- Side Effects none
- Defined in
dagDfs.c
Dag_Manager_t *
Dag_ManagerAlloc(
)
- Allocates the unique table (vTable) and the free list (gcList).
Initializes the counters for various statistics (stats).
Returns the pointer to the dag manager.
- Side Effects none
- See Also
Dag_ManagerAllocWithParams
Dag_ManagerFree
- Defined in
dagManager.c
void
Dag_ManagerFree(
Dag_Manager_t * dagManager,
Dag_ProcPtr_t freeData,
Dag_ProcPtr_t freeGen
)
- Forces a total garbage collection and then deallocates the
dag manager. `freeData' can be used to deallocate `data'
fields (user data pointers) in the nodes, while `freeGen'
is applied to `gRef' fields (user generic pointers).
`freeData' and `freeGen' are in the form `void f(char * r)'.
- Side Effects none
- See Also
Dag_ManagerGC
- Defined in
dagManager.c
void
Dag_ManagerGC(
Dag_Manager_t * dagManager,
Dag_ProcPtr_t freeData,
Dag_ProcPtr_t freeGen
)
- Sweeps out useless vertices, i.e., vertices that are not
marked as permanent, that are not descendants
of permanent vertices, or whose brother (if any) is neither
permanent nor descendant of a permanent vertex.
The search starts from vertices that are in the garbage
bin and whose mark is 0.
`freeData' can be used to deallocate `data'
fields (user data pointers) in the nodes, while `freeGen'
is applied to `gRef' fields (user generic pointers).
`freeData' and `freeGen' are in the form `void f(char * r)'.
- Side Effects none
- See Also
Dag_ManagerFree
- Defined in
dagManager.c
void
Dag_PrintStats(
Dag_Manager_t * dagManager,
int clustSz,
FILE * outFile
)
- Prints the following:
- the number of entries found in every chunk of
`clustSz' bins (if `clustSz' is 1 then the number
of entries per bin is given, if `clustSz' is 0 no
such information is displayed);
- the number of shared vertices, i.e., the number
of v's such that v -> mark > 1;
- the average entries per bin and the variance;
- min and max entries per bin.
- Side Effects none
- Defined in
dagStat.c
Dag_Vertex_t *
Dag_VertexInsert(
Dag_Manager_t * dagManager,
int vSymb,
char * vData,
Dag_Vertex_t ** vSons,
unsigned numSons
)
- Adds a vertex into the DAG and returns a
reference to it:
- vSymb is an integer code (vertex label);
- vData is a generic annotation;
- vSons must be a list of vertices (the intended sons).
Returns NIL(Dag_vertex_t) if there is no dagManager and
if vSymb is negative.
- Side Effects none
- Defined in
dagVertex.c
Dag_Vertex_t *
Dag_VertexLookup(
Dag_Manager_t * dagManager,
int vSymb,
char * vData,
Dag_Vertex_t** vSons,
unsigned numSons
)
- Uniquely adds a new vertex into the DAG and returns a
reference to it:
- vSymb is a NON-NEGATIVE integer (vertex label);
- vData is a pointer to generic user data;
- vSons is a list of vertices (possibly NULL).
Returns NIL(Dag_vertex_t) if there is no dagManager and
if vSymb is negative.
- Side Effects none
- Defined in
dagVertex.c
void
Dag_VertexMark(
Dag_Vertex_t * v
)
- Increments the vertex mark by one, so it cannot be
deleted by garbage collection unless unmarked.
- Side Effects none
- Defined in
dagVertex.c
void
Dag_VertexUnmark(
Dag_Vertex_t * v
)
- Decrements the vertex mark by one, so it can be
deleted by garbage collection when fatherless.
- Side Effects none
- Defined in
dagVertex.c
static void
GC(
Dag_Vertex_t * v,
Dag_ProcPtr_t freeData,
Dag_ProcPtr_t freeGen
)
- Gets a vertex to be freed. If the vertex has permanent or
non-orphan brothers it is rescued. Otherwise the brother is
unconnected and the sons marks are updated. GC is then
propagated to each fatherless son.
- Side Effects none
- Defined in
dagManager.c
void
PrintStat(
Dag_Vertex_t* dfsRoot,
FILE* statFile,
char* prefix
)
- Calls Depth First Search on the DAG dfsRoot to populate
the struct Statistics.
Then calls _PrintStat to print out them.
- Defined in
dagEnStat.c
static void
ResetStat(
Statistics_t* stat
)
- Reset the statistics data
- Defined in
dagEnStat.c
static void
_PrintStat(
Statistics_t* stat,
FILE* statFile,
char* prefix
)
- Print these data:
1. Total nodes per number of children;
2. Total nodes and total leaves per depth.
- Side Effects data are appended to statFile
- See Also
PrintStat()
- Defined in
dagEnStat.c
static void
clean_first(
Dag_Vertex_t* f,
char* cleanData,
nusmv_ptrint sign
)
- Dfs FirstVisit for cleaning.
- Side Effects None
- Defined in
dagDfs.c
static void
doNothingAndReturnVoid(
Dag_Vertex_t* f,
char* visData,
nusmv_ptrint sign
)
- Dfs function doing nothing
- Defined in
dagEnStat.c
static int
doNothingAndReturnZero(
Dag_Vertex_t* f,
char * visData,
nusmv_ptrint sign
)
- Dfs function returning zero
- Defined in
dagEnStat.c
static void
do_nothing(
Dag_Vertex_t* f,
char* cleanData,
nusmv_ptrint sign
)
- Dfs Back & Last visit for cleaning.
- Side Effects None
- Defined in
dagDfs.c
static int
return_zero(
Dag_Vertex_t* f,
char* cleanData,
nusmv_ptrint sign
)
- Dfs SetVisit for cleaning.
- Side Effects None
- Defined in
dagDfs.c
(
)
- Check if a vertex is a leaf
- Defined in
dagDfs.c
(
)
- The annotation bit is forced to 0 by a bitwise-and with
complement of DAG_ANNOTATION_BIT mask.
- Side Effects The value of p changes to the purified value.
- Defined in
dag.h
(
)
- The pointer is filtered by a bitwise-xor with either
DAG_ANNOTATION_BIT or !DAG_ANNOTATION_BIT. The pointer is not
altered, but the leftmost bit is complemented when
s==DAG_ANNOTATION_BIT and goes unchanged when
s!=DAG_ANNOTATION_BIT.
- Side Effects none
- Defined in
dag.h
(
)
- The annotation bit is filtered to 0. The result is the pointer
purified from the bit annotation.
- Side Effects none
- Defined in
dag.h
(
)
- Makes the code more readable
- Defined in
dagEnStat.c
(
)
- The parameters are:
- current, the dag vertex where to start the DFS
- dfs_fun, the functions to perform the DFS steps
- dfs_data, a reference to generic data
The function increments the DFS code for the dag manager owning
dfsRoot. Increment of the code guarantees that each node is
visited once and only once. dfs_fun->Set() may change the default
behaviour by forcing the DFS to visit nodes more than once
(by returning -1), or by preventing DFS to do a complete visit
(by returning 1).
- Side Effects node->dag->dfsCode: is incremented by one.
- Defined in
dagDfs.c
(
)
- The annotation bit is forced to 1 by a bitwise-or with
DAG_ANNOTATION_BIT mask.
- Side Effects The value of p changes to the purified value.
- Defined in
dag.h
(
)
- Uses a bitwise-and with DAG_ANNOTATION_BIT to test the
annotation bit of p. The result is either 0(false) or
not 0(true)
- Side Effects none
- Defined in
dag.h