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 2010/05/19 22h:25