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 2012/11/18 14h:37