NuSMV/code/nusmv/core/dag/dag.h File Reference

#include "nusmv/core/utils/utils.h"
#include "cudd/util.h"
#include "cudd/st.h"
#include "nusmv/core/utils/list.h"

Go to the source code of this file.

Data Structures

struct  Dag_DfsFunctions_t
 DFS function struct. More...
struct  Dag_Vertex_t
 DAG vertex. More...

Defines

#define DAG_ANNOTATION_BIT   ((nusmv_ptrint) 1)
#define DAG_DEFAULT_DENSITY   20
#define DAG_DEFAULT_GROWTH   1.5
#define DAG_DEFAULT_VERTICES_NO   65537
 Directed acyclic graphs with sharing.
#define DAG_GC_NO   (int) 1
#define DAG_MAX_STAT   (int) 2
#define DAG_NODE_NO   (int) 0
#define Dag_VertexClear(p)   (p = (Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT)))
 Clears (forces) a bit annotation to 0.
#define Dag_VertexGetRef(p)   ((Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT)))
 Filters a pointer from bit annotations.
#define Dag_VertexIsSet(p)   ((nusmv_ptrint)p & DAG_ANNOTATION_BIT)
 Tests if the edge is annotated.
#define Dag_VertexSet(p)   (p = (Dag_Vertex_t*)((nusmv_ptrint)p | DAG_ANNOTATION_BIT))
 Sets (forces) a bit annotation to 1.
#define DagId(r, s)   (Dag_Vertex_t*)((nusmv_ptrint)s ^ (nusmv_ptrint)r)
 Controls the sign of a dag.

Typedefs

typedef int(* PF_IVPCPI )(void *, char *, nusmv_ptrint)
typedef void(* PF_VPCP )(char *)
typedef void(* PF_VPVPCPI )(void *, char *, nusmv_ptrint)

Functions

void Dag_Dfs (Dag_Vertex_t *dfsRoot, Dag_DfsFunctions_t *dfsFun, char *dfsData)
Dag_Manager_t * Dag_ManagerAlloc (void)
 Creates a new DAG manager.
Dag_Manager_t * Dag_ManagerAllocWithParams (int dagInitVerticesNo, int maxDensity, int growthFactor)
void Dag_ManagerFree (Dag_Manager_t *dagManager, PF_VPCP freeData, PF_VPCP freeGen)
 Deallocates a DAG manager.
void Dag_ManagerGC (Dag_Manager_t *dagManager, PF_VPCP freeData, PF_VPCP freeGen)
 Garbage collects the DAG manager.
Dag_DfsFunctions_t * Dag_ManagerGetDfsCleanFun (Dag_Manager_t *dagManager)
void Dag_PrintStats (Dag_Manager_t *dagManager, int clustSz, FILE *outFile)
 Prints various statistics.
Dag_Vertex_t * Dag_VertexInsert (Dag_Manager_t *dagManager, int vSymb, char *vData, Dag_Vertex_t **vSons, unsigned numSons)
 Vertex insert.
Dag_Vertex_t * Dag_VertexLookup (Dag_Manager_t *dagManager, int vSymb, char *vData, Dag_Vertex_t **vSons, unsigned numSons)
 Vertex lookup.
void Dag_VertexMark (Dag_Vertex_t *v)
 Marks a vertex as permanent.
void Dag_VertexUnmark (Dag_Vertex_t *v)
 Unmarks a vertex (makes it volatile).
void PrintStat (Dag_Vertex_t *dfsRoot, FILE *statFile, char *prefix)
 Visit a DAG to compute some statistics.

Define Documentation

#define DAG_ANNOTATION_BIT   ((nusmv_ptrint) 1)
#define DAG_DEFAULT_DENSITY   20
Todo:
Missing synopsis
Todo:
Missing description
#define DAG_DEFAULT_GROWTH   1.5
Todo:
Missing synopsis
Todo:
Missing description
#define DAG_DEFAULT_VERTICES_NO   65537

Directed acyclic graphs with sharing.

Author:
Armando Tacchella External functions and data strucures of the dag package.
Todo:
Missing synopsis
Todo:
Missing description
#define DAG_GC_NO   (int) 1
Todo:
Missing synopsis
Todo:
Missing description
#define DAG_MAX_STAT   (int) 2
Todo:
Missing synopsis
Todo:
Missing description
#define DAG_NODE_NO   (int) 0
Todo:
Missing synopsis
Todo:
Missing description
#define Dag_VertexClear (  )     (p = (Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT)))

Clears (forces) a bit annotation to 0.

The annotation bit is forced to 0 by a bitwise-and with complement of DAG_ANNOTATION_BIT mask.

The value of p changes to the purified value.

#define Dag_VertexGetRef (  )     ((Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT)))

Filters a pointer from bit annotations.

The annotation bit is filtered to 0. The result is the pointer purified from the bit annotation.

none

#define Dag_VertexIsSet (  )     ((nusmv_ptrint)p & DAG_ANNOTATION_BIT)

Tests if the edge is annotated.

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)

none

#define Dag_VertexSet (  )     (p = (Dag_Vertex_t*)((nusmv_ptrint)p | DAG_ANNOTATION_BIT))

Sets (forces) a bit annotation to 1.

The annotation bit is forced to 1 by a bitwise-or with DAG_ANNOTATION_BIT mask.

The value of p changes to the purified value.

#define DagId ( r,
 )     (Dag_Vertex_t*)((nusmv_ptrint)s ^ (nusmv_ptrint)r)

Controls the sign of a dag.

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.

none


Typedef Documentation

typedef int(* PF_IVPCPI)(void *, char *, nusmv_ptrint)
Todo:
Missing synopsis
Todo:
Missing description
typedef void(* PF_VPCP)(char *)
typedef void(* PF_VPVPCPI)(void *, char *, nusmv_ptrint)
Todo:
Missing synopsis
Todo:
Missing description

Function Documentation

void Dag_Dfs ( Dag_Vertex_t *  dfsRoot,
Dag_DfsFunctions_t *  dfsFun,
char *  dfsData 
)

AutomaticStart

Todo:
Missing synopsis
Todo:
Missing description
Dag_Manager_t* Dag_ManagerAlloc ( void   ) 

Creates a new DAG manager.

Allocates the unique table (vTable) and the free list (gcList). Initializes the counters for various statistics (stats). Returns the pointer to the dag manager.

none

See also:
Dag_ManagerAllocWithParams Dag_ManagerFree
Dag_Manager_t* Dag_ManagerAllocWithParams ( int  dagInitVerticesNo,
int  maxDensity,
int  growthFactor 
)
Todo:
Missing synopsis
Todo:
Missing description
void Dag_ManagerFree ( Dag_Manager_t *  dagManager,
PF_VPCP  freeData,
PF_VPCP  freeGen 
)

Deallocates a DAG manager.

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)'.

none

See also:
Dag_ManagerGC
void Dag_ManagerGC ( Dag_Manager_t *  dagManager,
PF_VPCP  freeData,
PF_VPCP  freeGen 
)

Garbage collects the DAG manager.

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)'.

none

See also:
Dag_ManagerFree
Dag_DfsFunctions_t* Dag_ManagerGetDfsCleanFun ( Dag_Manager_t *  dagManager  ) 
void Dag_PrintStats ( Dag_Manager_t *  dagManager,
int  clustSz,
FILE *  outFile 
)

Prints various statistics.

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.

none

Dag_Vertex_t* Dag_VertexInsert ( Dag_Manager_t *  dagManager,
int  vSymb,
char *  vData,
Dag_Vertex_t **  vSons,
unsigned  numSons 
)

Vertex insert.

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.

none

Dag_Vertex_t* Dag_VertexLookup ( Dag_Manager_t *  dagManager,
int  vSymb,
char *  vData,
Dag_Vertex_t **  vSons,
unsigned  numSons 
)

Vertex lookup.

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.

none

void Dag_VertexMark ( Dag_Vertex_t *  v  ) 

Marks a vertex as permanent.

Increments the vertex mark by one, so it cannot be deleted by garbage collection unless unmarked.

none

void Dag_VertexUnmark ( Dag_Vertex_t *  v  ) 

Unmarks a vertex (makes it volatile).

Decrements the vertex mark by one, so it can be deleted by garbage collection when fatherless.

none

void PrintStat ( Dag_Vertex_t *  dfsRoot,
FILE *  statFile,
char *  prefix 
)

Visit a DAG to compute some statistics.

Calls Depth First Search on the DAG dfsRoot to populate the struct Statistics. Then calls _PrintStat to print out them.

All Data Structures Files Functions Variables Typedefs Enumerations Enumerator Defines

Generated on 14 Oct 2015 for NuSMV Developers Manual by  doxygen 1.6.1