check_ctlspec - Performs fair CTL model checking.
check_ctlspec [-h] [-m | -o output-file] [-n number | -p "ctl-expr [IN context]" | -P "name"]
Performs fair CTL model checking.
A ctl-expr to be checked can be specified at command line
using option -p. Alternatively, option -n or
-P can be used for checking a particular formula in the
property database. If neither -n nor -p are used,
all the SPEC formulas in the database are checked.
Command options:
- -m
- Pipes the output generated by the command in processing
SPECs 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
SPECs to the file output-file.
- -p "ctl-expr [IN context]"
- A CTL formula to be checked. context is the module
instance name which the variables in ctl-expr must
be evaluated in.
- -n number
- Checks the CTL property with index number in the property
database.
- -P name
- Checks the CTL property with name name in the property
database.
If the ag_only_search environment variable has been set, and
the set of reachable states has already been computed, then a
specialized algorithm to check AG formulas is used instead of the
standard model checking algorithms.
Last updated on 2011/04/06 21h:13