Internal functions and data structures of the dag package.

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:

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:

Side Effects none

Defined in dagVertex.c

void 
Dag_Dfs(
  Dag_Vertex_t* dfsRoot, 
  Dag_DfsFunctions_t* dfsFun, 
  char* dfsData 
)
The parameters are: 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:

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: 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: 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: 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

Last updated on 2012/11/18 14h:37