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

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

Side Effects none

See Also Sym_AtomBuildTransitionRelation

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

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

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

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

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

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

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

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

Side Effects none


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

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

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

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

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

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

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


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

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

void 
Sym_RegionFree(
  Sym_Region_t * region 
)
optional

Side Effects required

See Also optional

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

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


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

void 
Sym_RegionManagerFree(
  Sym_RegionManager_t * regionManager 
)
optional

Side Effects required

See Also optional

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

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

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

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


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

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

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


void 
Sym_SymInfoFree(
  Sym_Info_t * symInfo 
)
Utility to free symInfo

Side Effects none

See Also Sym_SymInfoAlloc

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

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

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

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

Side Effects none

See Also Sum_SymInfoReadImgInfo

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

Side Effects none


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

Side Effects none

See Also Sym_SymInfoReadUnprimedArray

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

Side Effects none

See Also Sym_SymInfoReadConjuncts

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

Side Effects none

See Also Sym_SymInfoReadUnprimedIdArray

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

Side Effects none

See Also Sym_SymInfoReadUnprimedIdArray

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

Side Effects none

See Also Sym_SymInfoReadPrimedIdArray

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

Side Effects none

See Also Sym_SymInfoReadVarToUnprimedId

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

Side Effects none

See Also Sym_SymInfoReadVarToPrimedId

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

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

Side Effects none

See Also Sym_SymInfoReadUnprimedArray

Last updated on 980624 22h11