check_invar - Performs model checking of invariants


check_invar [-h] [-m | -o output-file] [-s "strategy"] [-e "heuristic"] [-t number] [-k number] [-j "heuristic"] [-n number | -p "invar-expr [IN context]" | -P "name"]

Performs invariant checking on the given model. An invariant is a set of states. Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant. Invariants to be verified can be provided as simple formulas (without any temporal operators) in the input file via the INVARSPEC keyword or directly at command line, using the option -p.

Option -n can be used for checking a particular invariant of the model. If neither -n nor -p are used, all the invariants are checked.

During checking of invariant all the fairness conditions associated with the model are ignored.

If an invariant does not hold, a proof of failure is demonstrated. This consists of a path starting from an initial state to a state lying outside the invariant. This path has the property that it is the shortest path leading to a state outside the invariant.

Command options:

-m
Pipes the output generated by the program in processing INVARSPECs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".
-o output-file
Writes the output generated by the command in processing INVARSPECs to the file output-file.
-s strategy
Force the analysis strategy.
-e heuristic
Force the search heuristic for the forward-backward strategy.
-t number
When using the mixed BDD and BMC approach specify the heuristic threshold.
-k number
When using the mixed BDD and BMC approach specify the BMC max k.
-j heuristic
Force the switch heuristic for the BDD-BMC strategy.
-p "invar-expr [IN context]"
The command line specified invariant formula to be verified. context is the module instance name which the variables in invar-expr must be evaluated in.
-P name
Checks the INVARSPEC with name name in the property database.

Last updated on 2010/05/19 15h:56