check_refine - Performs symbolic (mdd based) refinement check. Assumes that all history dependent variables of specModule are present in implModule

check_refine [-e] [-h] [-o <fname>] [-v] <module_name1> <module_name2>

Command Options:

do transition invariant check only at the end (after completing reachability)

print usage

write out the mdd variable ordering in file specified by

verbose mode - prints MDDs associated with each intermediate step

Last updated on 980624 22h11