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: