optional

int 
RefCheckCompositionalRefinementOneAtom(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
optional

Side Effects trnasition relations for new modules will be built if -r option is used

See Also optional
Defined in ref.c

int 
RefCheckNohiddenRefinement(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
optional

Side Effects required

See Also optional
Defined in ref.c

int 
RefCheckSimulation(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
optional

See Also optional
Defined in refSym1.c

boolean 
RefCheckTransitionInvariant(
  Mdl_Module_t * module, 
  Sym_Info_t * symInfo, 
  mdd_t * transInv, 
  mdd_t * initSet, 
  array_t * eventIdArray, 
  array_t * histFreeIdArray, 
  array_t * histDependIdArray, 
  array_t * transQuanIdArr, 
  boolean  verbose, 
  boolean  checkAtEnd 
)
optional

Side Effects required

See Also optional
Defined in ref.c

array_t * 
RefConjunctsAddExtra(
  Sym_Info_t * symInfo, 
  mdd_t * extra 
)
Add one mdd to the conjuncts array and return a new conjuncts array. The user is responsible for freeing the new array and all the mdds in the new array

Side Effects none

See Also RefUnprimedIdsMerge
Defined in refSym1.c

void 
RefDumpIds(
  array_t * a 
)
optional

Side Effects required

See Also optional
Defined in ref.c

mdd_t * 
RefGetFlatSpecTransRelation(
  Mdl_Module_t * specModule, 
  Sym_Info_t * specSymInfo, 
  Mdl_Module_t * implModule, 
  Sym_Info_t * implSymInfo, 
  array_t * specIdArray, 
  array_t * implIdArray 
)
optional

Side Effects specIdArray and implId array will be filled with matching mddIds from specification and implementation

See Also optional
Defined in ref.c

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

Side Effects none

Defined in refUtil.c

mdd_t * 
RefMddBuildNoChange(
  Sym_Info_t * symInfo 
)
Build one conjunct for each variable x, saying that (x' = x), and take conjunction of all these

Side Effects none

See Also RefMddBuildObseq
Defined in refSym1.c

mdd_t * 
RefMddBuildObseq(
  Mdl_Module_t * impl, 
  Sym_Info_t * implSymInfo, 
  Mdl_Module_t * spec, 
  Sym_Info_t * specSymInfo 
)
Preconditions: 1. Each interface variable of the specification needs to be an interface variable of the implementation. 2. Each external variable of the specification needs to be an interface or external variable of the implementation. If these conditions are met, this routine returns an MDD that forces equality for corresponding UNPRIMED variables of specification and implementation.

See Also RefMddBuildNoChange
Defined in refSym1.c

array_t * 
RefPrimedIdsMerge(
  Sym_Info_t * symInfo1, 
  Sym_Info_t * symInfo2 
)
merge primed ids of two modules and return the result in a new array. It is the caller's responsibility to free this array

Side Effects none

See Also RefUnprimedIdsMerge
Defined in refSym1.c

array_t * 
RefUnprimedIdsMerge(
  Sym_Info_t * symInfo1, 
  Sym_Info_t * symInfo2 
)
merge unprimed ids of two modules and return the result in a new array. It is the caller's responsibility to free this array

Side Effects none

See Also RefPrimedIdsMerge
Defined in refSym1.c

boolean 
Ref_CheckAtomRefinement(
  Mdl_Manager_t * mdlManager, 
  Mdl_Module_t * spec, 
  Atm_Atom_t * specAtom, 
  Mdl_Module_t * impl, 
  lsList  varNameList, 
  lsList  forceVarNameList, 
  Tcl_Interp * interp, 
  boolean  checkRef, 
  boolean  verbose, 
  boolean  keepIntermediate, 
  int  impBoundary, 
  boolean  checkAtEnd, 
  char * orderFileName 
)
Given implementation, specification and and atom atom1 in implementation, construct new modules newimplementation and newspecification such that 1. new implementation contains atom1 only 2. new specification contains heuristically chosen atoms from specification and implementation that control variables controlled by atom1, but do not include atom1 itself

Side Effects required

See Also optional
Defined in ref.c

boolean 
Ref_CheckImplCompatibility(
  Mdl_Module_t * spec, 
  Mdl_Module_t * impl 
)
optional

Side Effects none

See Also optional
Defined in refUtil.c

boolean 
Ref_CheckNohiddenRefinement(
  Mdl_Module_t * implModule, 
  Sym_Info_t * implSymInfo, 
  Mdl_Module_t * specModule, 
  Sym_Info_t * specSymInfo, 
  boolean  verbose, 
  boolean  checkAtEnd 
)
Currently all variables of specModule need to be present in implModule The algorithm for doing this is as follows: -- First check if the initial states of specModule are contained in implModule If not FAIL -- do reachability of implModule During each stage of reachability 1. restrict trans relation of implModule to states in the frontier (ie build (frontier & implTrans)) 2. If restricted implementation trans does NOT imply specification trans, then FAIL and print error trace -- If reachability completes, PASS

Side Effects required

See Also optional
Defined in ref.c

boolean 
Ref_CheckSimulationUsingPre(
  Mdl_Module_t * implModule, 
  Sym_Info_t * implSymInfo, 
  Mdl_Module_t * specModule, 
  Sym_Info_t * specSymInfo, 
  boolean  verbose 
)
Check if specModule is a simulates of implModule

Side Effects required

See Also optional
Defined in refSym1.c

int 
Ref_End(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
optional

Side Effects required

See Also optional
Defined in ref.c

int 
Ref_Init(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
optional

Side Effects required

See Also optional
Defined in ref.c

boolean 
Ref_IsMemberOfAtomList(
  lsList  atomList, 
  Atm_Atom_t * atom 
)
optional

Side Effects none

See Also optional
Defined in refUtil.c

boolean 
Ref_IsMemberOfNameList(
  lsList  nameList, 
  char * name 
)
optional

Side Effects none

See Also optional
Defined in refUtil.c

Var_Variable_t * 
Ref_LookupVarList(
  lsList  varList, 
  char * name 
)
optional

Side Effects none

See Also optional
Defined in refUtil.c

int 
Ref_Reinit(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
optional

Side Effects required

See Also optional
Defined in ref.c

Atm_Atom_t * 
Ref_VariableReadControlAtom(
  Var_Variable_t * var 
)
Given a variable, get its controlling atom. This differs from Var_VariableReadControllingAtom in that it also works for array and bit-vector variables. In the case of arrays and bit-vectors (or arrays of bit vectors) the atom controlling the first element is returned.

See Also Var_VariableReadControlAtom
Defined in ref.c

Last updated on 980624 22h11