static int 
CommandBuildTrans(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Build transition relation for the given module. The transtion relation is conjunctively decomposed - one conjunct per atom and stored as part of the symInfo for the module

Side Effects 1. transition relation is stored as part of modules's SymInfo 2. If there is no symInfo, one is creared by executing the sym_static_order command.

See Also CommandComputeInitSet CommandComputeReachSet
Defined in symIntf.c

static int 
CommandComputeInitSet(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Compute the mdd representing initial states of a module

Side Effects The initial region computed is added to the region manager's region table

See Also CommandComputeReachedSet
Defined in symIntf.c

static int 
CommandComputePostSet(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
driver for one step image computation

Side Effects the image is stored in the region manager's region table

See Also CommandBuildTrans
Defined in symIntf.c

static int 
CommandComputeReachSet(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Do symbolic reachability for a module. A transition relation must exist before thie function is called

Side Effects 1. The command could modify the status of the invariants associated with the module on which it is executed. 2. The mdd represnting all reached states is added to the region table (of the region manager)

See Also CommandComputeInitSet
Defined in symIntf.c

static int 
CommandComputeUnion(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
typical usage is to union an image with an existing region

Side Effects The result of the union is added to the region manager's region table

See Also CommandComputePostSet
Defined in symIntf.c

static int 
CommandDynamicVarOrdering(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Implements the dynamic_var_ordering command.

Defined in symIntf.c

static int 
CommandPrintRegion(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Print the given region

Side Effects none

See Also CommandComputePostSet
Defined in symIntf.c

static int 
CommandReadOrder(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Read an ordering of MDD variables into a file, and order the MDD variables of a module accordingly

Side Effects none

See Also CommandWriteOrder
Defined in symIntf.c

static int 
CommandWriteOrder(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Write the current ordering of MDD variables into a file

Side Effects none

See Also CommandReadOrder
Defined in symIntf.c

static char * 
DynOrderTypeConvertToString(
  bdd_reorder_type_t  method 
)
Converts a dynamic ordering method type to a string. This string must NOT be freed by the caller.

Defined in symIntf.c

static int 
IntegersCompare(
  char ** obj1, 
  char ** obj2 
)
Used to sort an array of integers in ascending order.

Defined in symIntf.c

void 
MddGroupVariables(
  mdd_manager * mddMgr, 
  int  initMddId, 
  int  blockSize 
)
Group all bdd vars corresponding to mdd vars initMddId to initMddId + (blockSize-1) in a block which will not be reordered internally. Ths bdd's corresponding to these mdd's should be contiguous; if not the function will fail.

Defined in sym.c

static void 
ModuleAssignMddIdsToVariables(
  Mdl_Module_t * module, 
  Sym_Info_t * symInfo, 
  array_t * totalVarArray 
)
Create MDD variables according to the specified total ordering

Side Effects MDD variables are created for each of the module variables, as specified by the total ordering SeeAlso [

Defined in symIntf.c

static array_t * 
ModuleTotalOrderVariables(
  Mdl_Module_t * module, 
  array_t * varOrderArray 
)
Given a module and an array of variables (the order in which the variables are present in the array), pad remaining variables to the end of the array

Side Effects Remaining variables are added to the end of the array

See Also SymReadOrder
Defined in symIntf.c

static bdd_reorder_type_t 
StringConvertToDynOrderType(
  char * string 
)
Converts a string to a dynamic ordering method type. If string is not "sift" or "window", then returns BDD_REORDER_NONE.

Defined in symIntf.c

mdd_t * 
SymAssignmentBuildMddBoolean(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  Atm_Expr_t * expr 
)
Simply build MDDs for LHS and RHS separately and xnor them

Side Effects none

See Also SymMVBuildAssignmentMdd
Defined in symAssignMdd.c

mdd_t * 
SymAssignmentBuildMddStandard(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  Atm_Expr_t * expr 
)
A standard assignment assigns a scalar value (RHS) to a scalar variable (LHS). Depending on whether the LHS is boolean or multivalued, different functions are called

Side Effects none

See Also SymAssignmentBuildMddBoolean
Defined in symAssignMdd.c

mdd_t * 
SymBitVectorBuildAssignmentMdd(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  Atm_Expr_t * expr 
)
This routine builds an MDD for a bit vector assignment

Side Effects none

See Also SymBitVectorBuildBooleanExpression
Defined in symBitvec.c

mdd_t * 
SymBitVectorBuildBooleanExpressionMdd(
  Sym_Info_t * symInfo, 
  Atm_Expr_t * expr 
)
Given an expression of the form e1 e2, where e1 and e2 are bit-vector expressions and relop is a comparision operator, this routne builds an MDD for the comparison

Side Effects none

See Also SymBitVetorBuildAssignmentMdd
Defined in symBitvec.c

array_t * 
SymBitVectorBuildMddArrayForVar(
  Sym_Info_t * symInfo, 
  Atm_ExprType  varType, 
  Var_Variable_t * var 
)
Given a bitvector variable and its variable type (primed or unprimed), return an array of MDDs corresponding to its variables

Side Effects none

See Also SymBitVectorBuildMddArray
Defined in symBitvec.c

array_t * 
SymBitVectorBuildMddArray(
  Sym_Info_t * symInfo, 
  Atm_Expr_t * expr 
)
This routine builds an MDD array for a bit vector expression. Valid bit vector expressions are 0. c, a bit vector constant 1. v,a bit vector variable 2. a[index

Side Effects none

See Also SymBitVectorBuildBooleanExpressionMdd
Defined in symBitvec.c

int 
SymCreateMddVariable(
  mdd_manager * manager, 
  int  range 
)
given a range create an MDD variable for that range

Side Effects required

See Also optional
Defined in symUtil.c

mdd_t * 
SymExprBuildExprConstMdd(
  Sym_Info_t * symInfo, 
  Atm_Expr_t * expr, 
  int  c, 
  int  nVals 
)
Given an expression e and a constant c, build MDD for the boolean expression e = c. Note that e and c are multivalued

Side Effects none

See Also Sym_ExprBuildMdd
Defined in symExprMdd.c

Mvf_Function_t * 
SymExprBuildMvf(
  Sym_Info_t * symInfo, 
  Atm_Expr_t * expr 
)
An mvf is an array of mdds. A multivalued function can be represented with such an array of size equal to the number of values that could be taken by the expression. We build such an mvf for the given expression. For information on mvf see the mvf package (borrowed, with thanks, from VIS)

Side Effects none

Defined in symMV.c

Var_Variable_t * 
SymGetArrayElementVar(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  int  value 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

int 
SymGetArrayId(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  Atm_ExprType  pOrUnp, 
  int  value 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

int 
SymGetArrayNvals(
  Var_Variable_t * var 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

int 
SymGetConstant(
  Atm_Expr_t * expr 
)
The key here is to return the "index" of the constant value in the case of enumerated data types

Side Effects required

See Also optional
Defined in symUtil.c

mdd_t * 
SymGetMddLiteral(
  mdd_manager * manager, 
  int  id, 
  int  value 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

int 
SymGetNvals(
  Sym_Info_t * symInfo, 
  int  id 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

mdd_t * 
SymGetRelExprMdd(
  Sym_Info_t * symInfo, 
  Atm_ExprType  exprType, 
  int  lvarid, 
  int  rvarid 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

int 
SymGetTopMddId(
  mdd_t * m, 
  Sym_Info_t * symInfo 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

void 
SymGetVariableIdConstantAndPlus(
  Atm_Expr_t * expr, 
  int * varId, 
  int * c, 
  boolean * isPlus, 
  Sym_Info_t * symInfo 
)
utility to get the components of an expression of the form v + c or v - c

Side Effects required

See Also optional
Defined in symUtil.c

int 
SymGetVariableId(
  Atm_Expr_t * expr, 
  Sym_Info_t * symInfo 
)
utility to get the mdd variable id corresponding to the expression

Side Effects required

See Also optional
Defined in symUtil.c

Mdl_Module_t * 
SymInfoReadModule(
  Sym_Info_t * symInfo 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

boolean 
SymIsMultiValuedVariable(
  Atm_Expr_t * expr 
)
is the given expression a multi-valued variable?

Side Effects required

See Also optional
Defined in symUtil.c

boolean 
SymIsNumEnumRangeConstant(
  Atm_Expr_t * expr 
)
utility to check if a given expression is a num or enum or range constant

Side Effects required

See Also optional
Defined in symUtil.c

boolean 
SymIsUnprimedId(
  Sym_Info_t * symInfo, 
  int  id 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

mdd_t * 
SymMVBuildAssignmentMdd(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  Atm_Expr_t * expr 
)
Build MDD for multi valued assignment

Side Effects none

Defined in symMV.c

mdd_t * 
SymMVBuildBooleanExpressionMdd(
  Sym_Info_t * symInfo, 
  Atm_Expr_t * expr 
)
Given a multivalued expression of the form e1 e2, where e1 and e2 are multivalued expressions and is a comparison operator, this routine builds an MDD for the comparison

Side Effects none

Defined in symMV.c

mdd_t * 
SymMddArrayAndComponents(
  Sym_Info_t * symInfo, 
  array_t * mddArray 
)
Given an mdd array, perform and-ing of all components and return the result as an MDD

Side Effects none

See Also SymMddArrayAndComponents
Defined in symMddArray.c

array_t * 
SymMddArrayAndMddArray(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise and-ing and return the result as and MDD array

Side Effects none

See Also SymMddArrayOrMddArray
Defined in symMddArray.c

array_t * 
SymMddArrayAndMdd(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  mdd_t * m 
)
Given an mdd array and an mdd, perform and on each element of the array with the given mdd, and return the result as and MDD array

Side Effects none

See Also SymMddArrayAndMddArray
Defined in symMddArray.c

mdd_t * 
SymMddArrayCompareEqual(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise equality checking and return the result as an MDD. One could interpret the result as a collection of conditions on the variables that make the MDD arrays equal

Side Effects none

See Also SymMddArrayCompareLesser
Defined in symMddArray.c

mdd_t * 
SymMddArrayCompareGreaterEqual(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform lexicograhic lesser than checking and return the result as an MDD. One could interpret the result as a collection of conditions on the variables that make the first MDD array greater than or equal to the second

Side Effects none

See Also SymMddArrayCompareGreater
Defined in symMddArray.c

mdd_t * 
SymMddArrayCompareGreater(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform lexicograhic greater than checking and return the result as an MDD. One could interpret the result as a collection of conditions on the variables that make the first MDD array greater than the second

Side Effects none

See Also SymMddArrayCompareLesser
Defined in symMddArray.c

mdd_t * 
SymMddArrayCompareLesserEqual(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform lexicograhic lesser than checking and return the result as an MDD. One could interpret the result as a collection of conditions on the variables that make the first MDD array lesser than or equal to the second

Side Effects none

See Also SymMddArrayCompareGreaterEqual
Defined in symMddArray.c

mdd_t * 
SymMddArrayCompareLesser(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform lexicograhic lesser than checking and return the result as an MDD. One could interpret the result as a collection of conditions on the variables that make the first MDD array lesser than the second

Side Effects none

See Also SymMddArrayCompareGreater
Defined in symMddArray.c

void 
SymMddArrayFree(
  array_t * mddArray 
)
Free the MDD array along with all MDDs contained in it

Side Effects none

See Also SymMddArrayObtainConstant
Defined in symMddArray.c

array_t * 
SymMddArrayImpliesMddArray(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise implication and return the result as and MDD array

Side Effects none

See Also SymMddArrayAndMddArray
Defined in symMddArray.c

array_t * 
SymMddArrayMinusMddArray(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise subtraction(propogating borrow from the 0th bit to the last bit) as and MDD array

Side Effects none

See Also SymMddArrayAddMddArray
Defined in symMddArray.c

array_t * 
SymMddArrayNot(
  Sym_Info_t * symInfo, 
  array_t * mddArray 
)
Given an mdd array perform component-wise negation and return the result as and MDD array

Side Effects none

See Also SymMddArrayNot
Defined in symMddArray.c

array_t * 
SymMddArrayObtainConstant(
  Sym_Info_t * symInfo, 
  int  n, 
  boolean  c 
)
Given a size n and a boolean c, create and return an MDD array of zeros or ones (as specified by c) It is the caller's responsibilty to free this array as well as the mdds in it

Side Effects none

See Also SymMddArrayFree
Defined in symMddArray.c

array_t * 
SymMddArrayOrMddArray(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise or-ing and return the result as and MDD array

Side Effects none

See Also SymMddArrayAndMddArray
Defined in symMddArray.c

array_t * 
SymMddArrayOrMdd(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  mdd_t * m 
)
Given an mdd array and an mdd, perform or on each element of the array with the given mdd, and return the result as and MDD array

Side Effects none

See Also SymMddArrayAndMddArray
Defined in symMddArray.c

array_t * 
SymMddArrayPlusMddArray(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise addition (propogating carry from the 0th bit to the last bit) as and MDD array

Side Effects none

See Also SymMddArrayOrMddArray
Defined in symMddArray.c

void 
SymMddArrayPrint(
  Sym_Info_t * symInfo, 
  array_t * array1 
)
print all MDDs in the MDD array

Side Effects none

See Also SymMddArrayPrint
Defined in symMddArray.c

array_t * 
SymMddArrayXnorMddArray(
  Sym_Info_t * symInfo, 
  array_t * array1, 
  array_t * array2 
)
Given two mdd arrays of equal length, perform component-wise xnor-ing and return the result as and MDD array

Side Effects none

See Also SymMddArrayOrMddArray
Defined in symMddArray.c

boolean 
SymMddInTrueSupport(
  mdd_t * m, 
  int  id, 
  Sym_Info_t * symInfo 
)
optional

Side Effects required

See Also optional
Defined in symUtil.c

mdd_t * 
SymModuleSearch(
  Mdl_Module_t * module, 
  Sym_Info_t * symInfo, 
  boolean  verbose, 
  boolean  checkInvariants, 
  array_t * invNameArray, 
  array_t * typedExprArray, 
  Tcl_Interp * interp, 
  int  maxNumSteps 
)
reachability + optionally invariant checking

Side Effects state of invariants may be changed

See Also Sym_ModuleBuildTransitionRelation
Defined in sym.c

int 
SymRangeReadDummyId(
  Sym_Info_t * symInfo, 
  int  range, 
  int  num 
)
We create twp dummy MDD ids for each value of range in a multi valued expression. These MDD ids are used while manipluating mvfs. This function looks up a dummy id given the range value

Side Effects If the desired dummy id is not found, it is created and inserted into the rangeToDummyId table

Defined in symUtil.c

array_t * 
SymReadOrder(
  FILE * fp, 
  Mdl_Module_t * module 
)
Write variable order for module from a file

Side Effects none

See Also SymWriteOrder
Defined in symIntf.c

void 
SymWriteOrder(
  FILE * fp, 
  Sym_Info_t * symInfo 
)
Write variable order for symInfo into a file

Side Effects none

See Also SymReadOrder
Defined in symIntf.c

mdd_t * 
Sym_AssignmentBuildMdd(
  Sym_Info_t * symInfo, 
  Atm_Assign_t * assign, 
  st_table * assignedVarTable 
)
Given an assignment, build an MDD for the assignment

Side Effects The variables that are assigned to, are added to the assignedVarTable that is passed in

See Also SymAssignmentBuildMddStandard
Defined in symAssignMdd.c

mdd_t * 
Sym_AtomBuildInitialRegion(
  Sym_Info_t * symInfo, 
  Atm_Atom_t * atom 
)
build intial region for atom

Side Effects none

See Also Sym_AtomBuildTransitionRelation
Defined in sym.c

mdd_t * 
Sym_AtomBuildTransitionRelation(
  Sym_Info_t * symInfo, 
  Atm_Atom_t * atom 
)
build transition relation for an atom

Side Effects none

See Also Sym_ModuleBuildTransitionRelation
Defined in sym.c

mdd_t * 
Sym_AtomsBuildPartialInitialRegion(
  Sym_Info_t * symInfo, 
  array_t * atomArray, 
  mdd_t * partialState 
)
build mdd for partial initial region

Side Effects none

See Also Sym_AtomsComputePartialImage
Defined in symUtil.c

mdd_t * 
Sym_AtomsComputePartialImage(
  Sym_Info_t * symInfo, 
  array_t * atomArray, 
  mdd_t * prevState, 
  mdd_t * partialState 
)
Compute partial image with respect to a set of atoms

Side Effects none

See Also Sym_AtomsBuildPartialInitialRegion
Defined in symUtil.c

void 
Sym_DebugTracePrint(
  Sym_Info_t * symInfo, 
  array_t * savedOnions, 
  int  step, 
  mdd_t * notInv, 
  array_t * eventIdArray, 
  array_t * histDependIdArray, 
  char * invName, 
  char * moduleName 
)
Given an array of MDDs (representing the onion ring), the step at which the error occured, the negation of the invariant that got violated, arrays of event and history free ids of the module, name of the invariant and module, this function prints the debug trace. It starts with the onion ring at the specified step and intersects it with the negation of the invariant. Then it successivey does pre-image computations and finds a path to an initial state. Then it reverses the path and and prints an error trace. It uses different displaying techniques if Tk interface is running

Side Effects none

See Also SymModuleSearch
Defined in sym.c

int 
Sym_End(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
Currently this function does nothing. During a subsequent cleanup this should be made to free all memeory allocated by sym

Side Effects none

See Also Sym_Init Sym_Reinit
Defined in symIntf.c

mdd_t * 
Sym_ExprBuildMdd(
  Sym_Info_t * symInfo, 
  Atm_Expr_t * expr 
)
This routined builds an MDD for an expression. Note that the expression *must* evaluate to a boolean valuse in order to be able to build an MDD. Otherwise an error message is printed, and the routine aborts

Side Effects none

See Also optional
Defined in symExprMdd.c

int 
Sym_Init(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
This function is called when Mocha comes up and does the following: 1. Create hooks to sym package's functions for the supported commands 2. Allocate memory for SymRegionManager and deposit it in the main manager

Side Effects none

See Also Sym_End Sym_Reinit
Defined in symIntf.c

mdd_t  * 
Sym_MddPickMinterm(
  Sym_Info_t * symInfo, 
  mdd_t * mdd 
)
utility to pick a minterm form a MDD

Side Effects none

Defined in symUtil.c

void 
Sym_MddPrintCubesImplSpec(
  Sym_Info_t * implSymInfo, 
  Sym_Info_t * specSymInfo, 
  mdd_t * mdd, 
  int  level 
)
Dump the given MDD as a sum of cubes. Using symInfo, the MDD ids are translated to variable names in the reactive module description

Side Effects none

See Also Sym_MddPrintRawCubes
Defined in symUtil.c

void 
Sym_MddPrintCubes(
  Sym_Info_t * symInfo, 
  mdd_t * mdd, 
  int  level 
)
Dump the given MDD as a sum of cubes. Using symInfo, the MDD ids are translated to variable names in the reactive module description

Side Effects none

See Also Sym_MddPrintRawCubes
Defined in symUtil.c

void 
Sym_MddPrintRawCubes(
  Sym_Info_t * symInfo, 
  mdd_t * mdd, 
  int  level 
)
Utility to dump mdds - in terms of raw mdd ids

Side Effects none

See Also Sym_MddPrintCubes
Defined in symUtil.c

void 
Sym_MddPrintStateForErrorTrace(
  Sym_Info_t * symInfo, 
  mdd_t * mdd, 
  char ** stateString 
)
Given an mdd representinga state, generate a string in the form x1=v1 x2=v2 ...

Side Effects desired sting is padded to the end of stateString

See Also Sym_MddPrintCubes
Defined in symUtil.c

mdd_t * 
Sym_ModuleBuildInitialRegion(
  Sym_Info_t * symInfo, 
  Mdl_Module_t * module 
)
build mdd for initial region of module

Side Effects none

See Also Sym_ModuleBuildTransitionRelation
Defined in sym.c

void 
Sym_ModuleBuildTransitionRelation(
  Sym_Info_t * symInfo, 
  Mdl_Module_t * module 
)
build symbloic transition relation for a module. A conjunct is created for each atom and all conjuncts are stored in an array

Side Effects transtion relation is build and stored inside symInfo

See Also SymSearchModule
Defined in sym.c

boolean 
Sym_ModuleMatchMddIds(
  Mdl_Module_t * module1, 
  Mdl_Module_t * module2, 
  Sym_Info_t * symInfo1, 
  Sym_Info_t * symInfo2, 
  array_t * idArray1, 
  array_t * idArray2 
)
returns arrays of matching mdd ids for unprimed vars of two modules (through the arguments). The return value is true if every variable of module2 is also present in module 1 (this is the no-hidden variable case)

Side Effects matching ids are returned in corresponding indices of idArray1 and idArray2

Defined in symUtil.c

void 
Sym_ModulePerformBFS(
  Tcl_Interp * interp, 
  Main_Manager_t * mainManager, 
  Mdl_Module_t * module, 
  array_t * invNameArray, 
  array_t * typedExprArray 
)
Do invariant checking. This is the entry point for the sym invariant engine to be called from the inv package

See Also Sym_ModuleBuildTransitionRelation
Defined in sym.c

Sym_Region_t * 
Sym_RegionAlloc(
  Mdl_Module_t * module, 
  mdd_t * regionMdd 
)
Allocate a region struct and set its module and image pointers to the arguments passed

Side Effects required

See Also optional
Defined in symIntf.c

void 
Sym_RegionFree(
  Sym_Region_t * region 
)
optional

Side Effects required

See Also optional
Defined in symIntf.c

void 
Sym_RegionManagerAddModuleToSymInfo(
  Sym_RegionManager_t * regionManager, 
  Mdl_Module_t * module, 
  Sym_Info_t * symInfo 
)
Given a module and its symInfo, add it to the region manager's moduleToSymInfo hash table

Side Effects none

See Also Sym_RegionManagerReadSymInfo Sym_RegionManagerDeleteModuleToSymInfo
Defined in symIntf.c

Sym_RegionManager_t * 
Sym_RegionManagerAlloc(
    
)
A region manager manintains: 1. mapping from modules to their symInfos and 2. region tables mapping region names to regions 3. region counter used to generate unique region names This routine allocates and returns a pointer to a region manager

Side Effects required

Defined in symIntf.c

void 
Sym_RegionManagerDeleteModuleToSymInfo(
  Sym_RegionManager_t * regionManager, 
  Mdl_Module_t * module 
)
Given a module, delete it (and it's symInfo) from the region manager's moduleToSymInfo table. If the module is not in the table, this is a no-op

Side Effects none

See Also Sym_RegionManagerAddModuleToSymInfo
Defined in symIntf.c

void 
Sym_RegionManagerFree(
  Sym_RegionManager_t * regionManager 
)
optional

Side Effects required

See Also optional
Defined in symIntf.c

void 
Sym_RegionManagerIncrementCounter(
  Sym_RegionManager_t * regionManager 
)
Given a pointer to the region manager, increment the value of the region counter

Side Effects none

See Also Sym_RegionManagerReadCounter
Defined in symIntf.c

unsigned long 
Sym_RegionManagerReadCounter(
  Sym_RegionManager_t * regionManager 
)
Given a pointer to the region manager, return the value of the region counter inside the manager

Side Effects none

See Also Sym_RegionManagerReadRegionTable Sym_RegionManagerIncrementCounter
Defined in symIntf.c

Tcl_HashTable * 
Sym_RegionManagerReadRegionTable(
  Sym_RegionManager_t * regionManager 
)
Given a pointer to the region manager, return the region table (a Tcl hash table) associated with it. The region table hashes region names to SymRegionStruct vlaues. The user should NOT free this table

Side Effects none

See Also Sym_RegionManagerReadCounter
Defined in symIntf.c

Sym_Info_t * 
Sym_RegionManagerReadSymInfo(
  Sym_RegionManager_t * regionManager, 
  Mdl_Module_t * module 
)
Given a region manager and a module pointer, this routine returns a pointer to the module's symInfo it it exists, and 0 otherwise. The caller should NOT free this pointer

Side Effects SymRegionManagerAddModuleToSymInfo

Defined in symIntf.c

int 
Sym_Reinit(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
This function is called when the user types a re-init command. Re-initialization is not yet supported by sym. Currently, this function does nothing

Side Effects none

See Also Sym_Init Sym_End
Defined in symIntf.c

Sym_Info_t * 
Sym_SymInfoAlloc(
  Tcl_Interp * interp, 
  Mdl_Module_t * module, 
  mdd_manager * manager 
)
Allocate and return a symInfo struct

Side Effects none

See Also Sym_SymInfoFree
Defined in symUtil.c

mdd_t * 
Sym_SymInfoBuildFlatTrans(
  Sym_Info_t * syminfo 
)
symInfo maintains a transition relation for a module as an array of conjuncts. This utility takes "and" of all the conjuncts and builds a flat transition relation

Side Effects none

Defined in symUtil.c

void 
Sym_SymInfoFree(
  Sym_Info_t * symInfo 
)
Utility to free symInfo

Side Effects none

See Also Sym_SymInfoAlloc
Defined in symUtil.c

boolean 
Sym_SymInfoLookupPrimedVariableId(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  int * id 
)
lookup primed mdd id for a variable

Side Effects none

See Also Sym_SymInfoLookupUnprimedVariableId
Defined in symUtil.c

boolean 
Sym_SymInfoLookupUnprimedVariableId(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  int * id 
)
lookup unprimed mdd id for a variable

Side Effects none

See Also Sym_SymInfoLookupPrimedVariableId
Defined in symUtil.c

mdd_t * 
Sym_SymInfoReadConjunctForAtom(
  Sym_Info_t * symInfo, 
  Atm_Atom_t * atom 
)
read the conjunct (transtion relation) for the given atom

Side Effects none

See Also Sym_SymInfoReadManager
Defined in symUtil.c

array_t * 
Sym_SymInfoReadConjuncts(
  Sym_Info_t * symInfo 
)
read the conjuncts from symInfo

Side Effects none

See Also Sum_SymInfoReadImgInfo
Defined in symUtil.c

st_table * 
Sym_SymInfoReadIdToVar(
  Sym_Info_t * symInfo 
)
read the idToVar table from symInfo

Side Effects none

Defined in symUtil.c

Img_ImageInfo_t * 
Sym_SymInfoReadImgInfo(
  Sym_Info_t * symInfo 
)
read the image info from symInfo

Side Effects none

See Also Sym_SymInfoReadUnprimedArray
Defined in symUtil.c

mdd_manager * 
Sym_SymInfoReadManager(
  Sym_Info_t * symInfo 
)
read the mdd manager from symInfo

Side Effects none

See Also Sym_SymInfoReadConjuncts
Defined in symUtil.c

array_t * 
Sym_SymInfoReadPrimedIdArray(
  Sym_Info_t * symInfo 
)
read the primedIdArray array

Side Effects none

See Also Sym_SymInfoReadUnprimedIdArray
Defined in symUtil.c

array_t * 
Sym_SymInfoReadQuantifyIdArray(
  Sym_Info_t * symInfo 
)
read the quantifyIdArray array

Side Effects none

See Also Sym_SymInfoReadUnprimedIdArray
Defined in symUtil.c

array_t * 
Sym_SymInfoReadUnprimedIdArray(
  Sym_Info_t * symInfo 
)
read the unprimedIdArray array

Side Effects none

See Also Sym_SymInfoReadPrimedIdArray
Defined in symUtil.c

st_table * 
Sym_SymInfoReadVarToPrimedId(
  Sym_Info_t * symInfo 
)
read the varToPrimedId st_table

Side Effects none

See Also Sym_SymInfoReadVarToUnprimedId
Defined in symUtil.c

st_table * 
Sym_SymInfoReadVarToUnprimedId(
  Sym_Info_t * symInfo 
)
read the varToUnprimedId st_table

Side Effects none

See Also Sym_SymInfoReadVarToPrimedId
Defined in symUtil.c

void 
Sym_SymInfoSetConjunctForAtom(
  Sym_Info_t * symInfo, 
  Atm_Atom_t * atom, 
  mdd_t * atomMdd 
)
set the conjunct (transtion relation) for the given atom

Side Effects none

See Also Sym_SymInfoReadManager
Defined in symUtil.c

void 
Sym_SymInfoSetImgInfo(
  Sym_Info_t * symInfo, 
  Img_ImageInfo_t * imgInfo 
)
read the image info from symInfo

Side Effects none

See Also Sym_SymInfoReadUnprimedArray
Defined in symUtil.c

static array_t * 
VarBuildBddIdArray(
  Sym_Info_t * symInfo, 
  Var_Variable_t * var, 
  boolean  primed 
)
Returns an array (of int's) of the levels of the BDD variables corresponding to the MDD variable of a node. The level of a BDD variable is it place in the current variable ordering of the BDD manager. The returned array is sorted in ascending order. It is the responsibility of the caller to free this array.

Defined in symIntf.c

static int 
VarOrderIsInArray(
  array_t * varOrderArray, 
  VarOrder_t * varOrder 
)
check if a variable is in a varOrderArray

Side Effects none

Defined in symIntf.c

static int 
VarOrdersCompareBddIdArray(
  lsGeneric  node1, 
  lsGeneric  node2 
)
Used to sort an array of nodes in ascending order of lowest BDD level.

Defined in symIntf.c

Last updated on 980624 22h11