check_ltlspec - Performs LTL model checking


check_ltlspec [-h] [-m | -o output-file] [-n number | -p "ltl-expr [IN context]" | -P "name"]

Performs model checking of LTL formulas. LTL model checking is reduced to CTL model checking as described in the paper by [CGH97].

A ltl-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 LTLSPEC formulas in the database are checked.

Command options:

-m
Pipes the output generated by the command in processing LTLSPECs 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 LTLSPECs to the file output-file.
-p "ltl-expr [IN context]"
An LTL formula to be checked. context is the module instance name which the variables in ltl_expr must be evaluated in.
-n number
Checks the LTL property with index number in the property database.
-P name
Checks the LTL property named name in the property database.

Last updated on 2012/11/18 14h:37