CommandBuildTrans()
driver for building transition relation
CommandComputeInitSet()
driver for building initial state
CommandComputePostSet()
compute the post set of a given set
CommandComputeReachSet()
driver for building reached set
CommandComputeUnion()
compute the union of two regions
CommandDynamicVarOrdering()
Implements the dynamic_var_ordering command.
CommandPrintRegion()
Print the given region
CommandReadOrder()
Order the MDD variables of a module as specified by a file
CommandWriteOrder()
Write the current ordering of the module into a file
DynOrderTypeConvertToString()
Converts a dynamic ordering method type to a string.
IntegersCompare()
Used to sort an array of integers in ascending order.
MddGroupVariables()
Group all bdd vars corresponding to mdd vars initMddId to initMddId + (blockSize-1) in a block which will not be split in reordering.
ModuleAssignMddIdsToVariables()
Create MDD variables according to the specified total ordering
ModuleTotalOrderVariables()
Convert an ordering of a subset of variables to a total ordering
StringConvertToDynOrderType()
Converts a string to a dynamic ordering method type.
SymAssignmentBuildMddBoolean()
Build MDD for boolean assignment with LHS and RHS of type boolean
SymAssignmentBuildMddStandard()
build MDD for a standard asssignment
SymBitVectorBuildAssignmentMdd()
build MDD for bit vector assignment
SymBitVectorBuildBooleanExpressionMdd()
build MDD for a boolean expression of bit vectors
SymBitVectorBuildMddArrayForVar()
return and mdd array for a bitvector variable
SymBitVectorBuildMddArray()
build MDD array for bit vector expression
SymCreateMddVariable()
utility to create an MDD variable
SymExprBuildExprConstMdd()
build MDD for an expression-constant equality
SymExprBuildMvf()
Given a parse tree for a multivalued expression compute its mvf
SymGetArrayElementVar()
required
SymGetArrayId()
required
SymGetArrayNvals()
required
SymGetConstant()
utility to get a constant value from an expression
SymGetMddLiteral()
utility to get and MDD literal
SymGetNvals()
utility to get the number of possible values of a multi valued variable
SymGetRelExprMdd()
required
SymGetTopMddId()
get top mdd id
SymGetVariableIdConstantAndPlus()
utility to get the components of an expression of the form v + c or v - c
SymGetVariableId()
utility to get the mdd variable id corresponding to the expression
SymInfoReadModule()
required
SymIsMultiValuedVariable()
is the given expression a multi-valued variable?
SymIsNumEnumRangeConstant()
utility to check if a given expression is a num or enum or range constant
SymIsUnprimedId()
does this id belong to a primed or unprimed variable
SymMVBuildAssignmentMdd()
Build MDD for multi valued assignment
SymMVBuildBooleanExpressionMdd()
Given a boolean expression involving multivalued variables, build mdd for it
SymMddArrayAndComponents()
do "and" of all MDD array components
SymMddArrayAndMddArray()
do "and" on two MDD arrays
SymMddArrayAndMdd()
Does "and" on all components of MDD array with given mdd
SymMddArrayCompareEqual()
do equality check on two MDD arrays
SymMddArrayCompareGreaterEqual()
do greater than or equal check on two MDD arrays
SymMddArrayCompareGreater()
do greater than check on two MDD arrays
SymMddArrayCompareLesserEqual()
do lesser than or equal check on two MDD arrays
SymMddArrayCompareLesser()
do lesser than check on two MDD arrays
SymMddArrayFree()
free MDD array
SymMddArrayImpliesMddArray()
do "implies" on two MDD arrays
SymMddArrayMinusMddArray()
do "subtract" on two MDD arrays
SymMddArrayNot()
do "not" on MDD array
SymMddArrayObtainConstant()
Obtain constant MDD array
SymMddArrayOrMddArray()
do "or" on two MDD arrays
SymMddArrayOrMdd()
Door "or" on all components of MDD array with given mdd
SymMddArrayPlusMddArray()
do "add" on two MDD arrays
SymMddArrayPrint()
print MDD array
SymMddArrayXnorMddArray()
do "xnor" on two MDD arrays
SymMddInTrueSupport()
Check if the given variable is in the true support of the given mdd
SymModuleSearch()
do reachability + invariant checking
SymRangeReadDummyId()
Utility to access a dummyId for a range
SymReadOrder()
Read variable order for module from a file
SymWriteOrder()
Write variable order for symInfo into a file
Sym_AssignmentBuildMdd()
build MDD for an assignment
Sym_AtomBuildInitialRegion()
build initial region for an atom
Sym_AtomBuildTransitionRelation()
build transition relation for an atom
Sym_AtomsBuildPartialInitialRegion()
build mdd for partial initial region
Sym_AtomsComputePartialImage()
Compute partial image with respect to a set of atoms
Sym_DebugTracePrint()
print debug trace for an invariant
Sym_End()
Termination function for sym package
Sym_ExprBuildMdd()
build MDD for an expression
Sym_Init()
Initilization function for sym package
Sym_MddPickMinterm()
utility to pick a minterm form a MDD
Sym_MddPrintCubesImplSpec()
Utility to dump mdds
Sym_MddPrintCubes()
Utility to dump mdds
Sym_MddPrintRawCubes()
Utility to dump mdds - in terms of raw mdd ids
Sym_MddPrintStateForErrorTrace()
Utility to generate a state string for Tcl/Tk error trace display
Sym_ModuleBuildInitialRegion()
build mdd for initial region of module
Sym_ModuleBuildTransitionRelation()
build symbolic transtion relation for a module
Sym_ModuleMatchMddIds()
match mdd ids of two modules
Sym_ModulePerformBFS()
do invariant checking
Sym_RegionAlloc()
Allocate a region struct
Sym_RegionFree()
required
Sym_RegionManagerAddModuleToSymInfo()
Add a module and symInfo pair to the moduleToSymInfo table
Sym_RegionManagerAlloc()
Allocate a region manager
Sym_RegionManagerDeleteModuleToSymInfo()
Delete a module-syminfo pair from moduleToSymInfo table
Sym_RegionManagerFree()
required
Sym_RegionManagerIncrementCounter()
Increment region manager's region counter
Sym_RegionManagerReadCounter()
Read region manager's region counter
Sym_RegionManagerReadRegionTable()
Read region manager's region table
Sym_RegionManagerReadSymInfo()
Find the symInfo for the given module
Sym_Reinit()
Re-initialization function for sym package
Sym_SymInfoAlloc()
Allocate and return a symInfo struct
Sym_SymInfoBuildFlatTrans()
Utility to build a flat transition relation
Sym_SymInfoFree()
Utility to free symInfo
Sym_SymInfoLookupPrimedVariableId()
lookup primed mdd id for a variable
Sym_SymInfoLookupUnprimedVariableId()
lookup unprimed mdd id for a variable
Sym_SymInfoReadConjunctForAtom()
read the conjunct (transtion relation) for the given atom
Sym_SymInfoReadConjuncts()
read the conjuncts from symInfo
Sym_SymInfoReadIdToVar()
read the idToVar table from symInfo
Sym_SymInfoReadImgInfo()
read the image info from symInfo
Sym_SymInfoReadManager()
read the mdd manager from symInfo
Sym_SymInfoReadPrimedIdArray()
read the primedIdArray array
Sym_SymInfoReadQuantifyIdArray()
read the quantifyIdArray array
Sym_SymInfoReadUnprimedIdArray()
read the unprimedIdArray array
Sym_SymInfoReadVarToPrimedId()
read the varToPrimedId st_table
Sym_SymInfoReadVarToUnprimedId()
read the varToUnprimedId st_table
Sym_SymInfoSetConjunctForAtom()
set the conjunct (transtion relation) for the given atom
Sym_SymInfoSetImgInfo()
read the image info from symInfo
VarBuildBddIdArray()
Gets the levels of the BDD variables corresponding to the MDD variable of a node.
VarOrderIsInArray()
check if a variable is in a varOrderArray
VarOrdersCompareBddIdArray()
Used to sort an array of nodes in ascending order of lowest BDD level.

Last updated on 980624 22h11