ref.h
External header file
refInt.h
Internal header file
ref.c
Routines to check if one module is a refinement of another
refSym1.c
Routines to check if one module simulates another using naive approach
refUtil.c
Routines to check if one module is a refinement of another

ref.h

External header file

By: Sriram Rajamani

See Alsooptional


refInt.h

Internal header file

By: Sriram Rajamani

See Alsooptional


ref.c

Routines to check if one module is a refinement of another

By: Sriram K. Rajamani

This package has routines that check if one module refines another. 1. refinement check is provided via the check_refine command. It requires that all history dependent variables of the specification be witnessed in the implementation 2. simulation check is provided via the check_simulate command. 3. compositonal refinement facility is provided by the check_refine_atom command. This command helps the user carry out one proof oligation in a compositional proof.

See Alsosym

Ref_Init()
Init function for tcl.
Ref_Reinit()
Reinit function
Ref_End()
End function
Ref_CheckAtomRefinement()
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
RefCheckTransitionInvariant()
Check refinement using transition invariant check on the implementation
RefCheckNohiddenRefinement()
driver for checking refinement with no hidden variables in the specification
RefCheckCompositionalRefinementOneAtom()
driver for checking one step in the compositional refinement proof
RefDumpIds()
dump and array of mdd Ids for debugging
RefGetFlatSpecTransRelation()
get flattened transition relation for specification in terms of variables of implementation
Ref_VariableReadControlAtom()
Ref_VariableReadControlAtom

refSym1.c

Routines to check if one module simulates another using naive approach

By: Sriram K. Rajamani

optional

See Alsooptional

Ref_CheckSimulationUsingPre()
Check if specModule is a simulates of implModule
RefUnprimedIdsMerge()
merge unprimed ids of two modules
RefPrimedIdsMerge()
merge primed ids of two modules
RefMddBuildNoChange()
Build MDD for no variables changing
RefMddBuildObseq()
Build MDD for observational equivalence between two modules
RefConjunctsAddExtra()
Add one mdd to the conjuncts array and return a new conjuncts array
RefCheckSimulation()
driver for checking simulation

refUtil.c

Routines to check if one module is a refinement of another

By: Sriram K. Rajamani

optional

See Alsooptional

Ref_CheckImplCompatibility()
check implementation compatibility between spec and impl
Ref_LookupVarList()
Lookup variable by name from a list of variables
Ref_IsMemberOfAtomList()
test for membership in list of atoms
Ref_IsMemberOfNameList()
test for membership in list of names
RefMddArrayFree()
free MDD array

Last updated on 980624 22h11