Go to the first, previous, next, last section, table of contents.

4.2 Commands for Checking Specifications

Command: compute_reachable [-h]

Computes the set of reachable states. The result is then used to simplify image and preimage computations. This can result in improved performances for models with sparse state spaces. Sometimes this option may slow down the performance because the computation of reachable states may be very expensive. The environment variable forward_search is set.

Command: print_reachable_states [-h]

Prints the number of reachable states of the read model. The reachable states are computed if needed.

Command: check_spec [-h] [-m | -o output-file] [ctl-expression]

Evaluates SPEC statements. If no ctl-expression is given at command line, then the command evaluates the previously parsed SPEC statements, if any. If a formula is false, a path witnessing its falsity is printed. Infinite paths are represented by a finite sequence of states leading to a cycle.

-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 "more" command.

-o output-file

Writes the output generated by the command in processing SPECs to the file output-file.

ctl-expression

A real time CTL formula to be checked.

If the ag_only_search environment variable has been set, and the set of reachable states has been already computed, then a specialized algorithm to check AG formulas is used instead of the standard model checking algorithms.

Environment Variable: ag_only_search

Enables the use of an ad hoc algorithm for checking AG formulas. The algorithm, given a formula of the form AG alpha, computes the set of states satisfying alpha, and checks whether it contains the reachable states is the empty set. If this is the case, then the property is verified, else a counterexample is printed.

Command: check_invar [-h] [-m | -o output-file] [invar-expression]

Evaluates invariants. If no invar-expression is given at command line, then the command evaluates the previously parsed INVARSPEC statements, if any. If a formula is false, a path witnessing its falsity is printed.

-m

Pipes the output generated by the program in processing INVARSPECs to the program specified by the PAGER shell variable if defined, else through the UNIX "more" command.

-o output-file

Writes the output generated by the command in processing INVARSPECs to the file output-file.

invar-expression

An invariant to be verified.

Command: check_ltlspec [-h] [-m | -o output-file] [ltl-expression]

Performs model checking of LTL formulas. If no ltl-expression is given at command line, then the previously parsed LTLSPEC, if any, are considered. LTL model checking is reduced to CTL model checking as described in [CGH97].

-m

Pipes the output generated by the program in processing LTLSPECs to the program specified by the PAGER shell variable if defined, else through the UNIX "more" command.

-o output_file

Writes the output generated by the command in processing LTLSPECs to the file output-file.

ltl-expression

A LTL formula to be checked.

Command: compute [-h] [-m | -o output-file] [compute-expression]

Performs quantitative analysis. If no compute-expression is given at command line, then the previously parsed COMPUTE statements, if any, are considered.

-m

Pipes the output generated by the program in processing COMPUTEs to the program specified by the PAGER shell variable if defined, else through the UNIX "more" command.

-o output-file

Writes the output generated by the command in processing COMPUTEs to the file output-file.

compute-expression

A quantitative characteristic to be computed.