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

Last updated on 980624 22h11