static void
CleanBack(
Dag_Vertex_t * f,
char * cleanData,
nusmv_ptrint sign
)
- Dfs BackVisit for cleaning.
- Side Effects None
- Defined in
dagDfs.c
static void
CleanFirst(
Dag_Vertex_t * f,
char * cleanData,
nusmv_ptrint sign
)
- Dfs FirstVisit for cleaning.
- Side Effects None
- Defined in
dagDfs.c
static void
CleanLast(
Dag_Vertex_t * f,
char * cleanData,
nusmv_ptrint sign
)
- Dfs LastVisit for cleaning.
- Side Effects None
- Defined in
dagDfs.c
static int
CleanSet(
Dag_Vertex_t * f,
char * cleanData,
nusmv_ptrint sign
)
- Dfs Set for cleaning.
- Side Effects None
- Defined in
dagDfs.c
static int
Compare(
Dag_Vertex_t* v,
lsList list,
nusmv_ptrint vBit
)
- The parameters are:
- v, the current dag vertex
- list, the list of sons of the corrent dag vertex
- vBit, the incoming link annotation (0 or not-0)
- Side Effects None
- Defined in
dagEn.c
static Dag_Vertex_t*
DFS1(
Dag_Vertex_t* v,
nusmv_ptrint vBit
)
- The parameters are:
- v, the current dag vertex
- vBit, the incoming link annotation (0 or not-0)
- Side Effects none
- Defined in
dagEn.c
static void
DFS2(
Dag_Vertex_t * v,
nusmv_ptrint vBit,
lsList sons,
int father_symbol
)
- The parameters are:
- v, the current dag vertex
- vBit, the incoming link annotation (0 or not-0)
- sons, the list of sons of the corrent dag vertex
- father_symbol, the integer code of the father vertex
of the corrent dag vertex
- Side Effects None
- Defined in
dagEn.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_Vertex_t*
Dag_Ennarize(
Dag_Vertex_t* dfsRoot
)
- The parameters are:
- dfsRoot, the dag vertex of the binary dag to transform into
ennary dag
- Side Effects none
- Defined in
dagEn.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,
lsList vSons
)
- 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,
lsList vSons
)
- 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
static int
SetupSet(
Dag_Vertex_t* f,
char * visData,
nusmv_ptrint sign
)
- Dfs Set for ennarization.
- Side Effects None
- Defined in
dagEn.c
static lsList
getEnnarySons(
Dag_Vertex_t * v,
nusmv_ptrint sign
)
- The parameters are:
- v, the current dag vertex
- sign, the incoming link annotation (0 or not-0)
- Side Effects None
- Defined in
dagEn.c
(
)
- The leftmost bit is forced to 0 by a bitwise-and with
DAG_BIT_CLEAR == 0x7FFFFFFF mask.
- Side Effects The value of p changes to the purified value.
- Defined in
dag.h
(
)
- The leftmost bit is filtered to 0 by a bitwise-and with
DAG_BIT_CLEAR == 0x7FFFFFFF mask. The result is the pointer
purified from the bit annotation.
- Side Effects none
- Defined in
dag.h
(
)
- The leftmost bit is filtered to 0 by a bitwise-and with
DAG_BIT_CLEAR == 0x7FFFFFFF mask. The result is the pointer
purified from the bit annotation.The leftmost bit is forced
to 1 or 0 according to the result of bitwise-or with S.
- Side Effects none
- Defined in
dagEn.c
(
)
- Select a particular field of the struct associated via gRef
to each node
- Side Effects none
- Defined in
dagEn.c
(
)
- The leftmost bit is forced to 1 by a bitwise-or with
DAG_BIT_SET == 0x80000000 mask .
- Side Effects The value of p changes to the purified value.
- Defined in
dag.h
(
)
- Uses a bitwise-and with DAG_BIT_SET == 0x80000000 to test the
leftmost bit of p. The result is either 0x00000000 if the bit
is not set, or 0x80000000 if the bit is set.
- Side Effects none
- Defined in
dag.h