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

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

Side Effects none

See Also optional

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

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

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

Side Effects required

See Also optional

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

Side Effects required

See Also optional

boolean 
Ref_IsMemberOfAtomList(
  lsList  atomList, 
  Atm_Atom_t * atom 
)
optional

Side Effects none

See Also optional

boolean 
Ref_IsMemberOfNameList(
  lsList  nameList, 
  char * name 
)
optional

Side Effects none

See Also optional

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

Side Effects none

See Also optional

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

Side Effects required

See Also optional

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

Last updated on 980624 22h11