check_ctlspec [-h] [-m | -o output-file] [-n number | -p "ctl-expr [IN context]"]
Performs fair CTL model checking.
A ctl-expr to be checked can be specified at command line using option -p. Alternatively, option -n 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:
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.