RefCheckCompositionalRefinementOneAtom()
driver for checking one step in the compositional refinement proof
RefCheckNohiddenRefinement()
driver for checking refinement with no hidden variables in the specification
RefCheckSimulation()
driver for checking simulation
RefCheckTransitionInvariant()
Check refinement using transition invariant check on the implementation
RefConjunctsAddExtra()
Add one mdd to the conjuncts array and return a new conjuncts array
RefDumpIds()
dump and array of mdd Ids for debugging
RefGetFlatSpecTransRelation()
get flattened transition relation for specification in terms of variables of implementation
RefMddArrayFree()
free MDD array
RefMddBuildNoChange()
Build MDD for no variables changing
RefMddBuildObseq()
Build MDD for observational equivalence between two modules
RefPrimedIdsMerge()
merge primed ids of two modules
RefUnprimedIdsMerge()
merge unprimed ids of two modules
Ref_CheckAtomRefinement()
Ref_CheckImplCompatibility()
check implementation compatibility between spec and impl
Ref_CheckNohiddenRefinement()
Check if implModule is a refinement of specModule with the assumption that all history dependent variables of specModule are also present in implModule
Ref_CheckSimulationUsingPre()
Check if specModule is a simulates of implModule
Ref_End()
End function
Ref_Init()
Init function for tcl.
Ref_IsMemberOfAtomList()
test for membership in list of atoms
Ref_IsMemberOfNameList()
test for membership in list of names
Ref_LookupVarList()
Lookup variable by name from a list of variables
Ref_Reinit()
Reinit function
Ref_VariableReadControlAtom()
Ref_VariableReadControlAtom

Last updated on 980624 22h11