5.4 Data display commands

The following commands can be used to access test result information and to inspect the LTL formulas, Büchi automata and the state space used in the current test round.

`algorithms'

`implementations'

`translators'

Show a list of implementations declared in the program configuration file and tell whether they are currently enabled for testing. The list also shows the numeric identifiers of the implementations.

`buchi [``+'' | ``-''] <implementation-id> [state-id-list | ``dot'']'

Display information about the structure of the Büchi automaton generated by the implementation implementation-id from the positive (`+') or negative (`-') LTL formula used in the current test round. The implementation identifier may be optionally followed by a list of state identifiers to display specific states of the automaton (see Command conventions, for details on how the list should be formatted), or the keyword `dot' to display the automaton in a format that can be given as input for the `dot' tool of the GraphViz graph visualization package [GViz] to obtain a graphical representation of the automaton.

`evaluate [``+'' | ``-''] [implementation-id-list] [state-id-list]'

Display the model checking results for the positive (`+') or the negative (`-') formula computed using a given set of implementations for constructing a Büchi automaton from the formula. If no implementation list is specified, show the results for all implementations. The implementation identifier list may optionally be followed by a list of (state space) state identifiers to restrict the output to only a subset of all states. (See Command conventions, for more information about the format used for the lists.)

This command can be used to look for states in which the model checking result cross-comparison test (see Model checking result cross-comparison test) failed for a pair of implementations. These state identifiers can then be used as input for the `resultanalysis' command (see Failure analysis commands).

Note 1: Observe that the model checking results shown do not follow the “universal” semantics of LTL (common in model checking), by which a formula is usually considered to hold in a set of infinite paths beginning from a state only if all paths in the set are accepted by the Büchi automaton constructed from the formula to be model checked. Instead, lbtt will mark the result true if any of these paths is accepted by the automaton.

Note 2: If using random or enumerated paths as state spaces, lbtt accepts also the identifier `lbtt' in the implementation identifier list. This identifier can be used for accessing the model checking results computed using lbtt's internal model checking algorithm for paths.

`formula [``+'' | ``-''] [``normal'' | ``nnf'']'

Display the positive (`+') or the negative (`-') LTL formula used for tests in the current test round either in the form in which it was generated (`normal' – the default) or in negation normal form (`nnf').

`inconsistencies [implementation-id-list]'

List the state space states in which the model checking result consistency check (see Model checking result consistency check) failed for each implementation in the list (or all implementations if the list is omitted). See Command conventions, for information on formatting the list. The state identifiers can then be used as input for the `consistencyanalysis' command (see Failure analysis commands).

`results [implementation-id-list]'

Display test results (in the current test round) for each implementation in the list (or all implementations if the list is omitted). For more information about the output, see Test round messages; see Command conventions, for information on how to specify the implementations.

`statespace [state-id-list | ``dot'']'

Display information about the structure of the state space used for model checking tests in the current test round. The optional state-id-list can be used to display only a part of the whole state space (see Command conventions, for information on formatting the state list). Alternatively, the `dot' keyword can be used to output the state space description in a format recognized by the `dot' tool of the GraphViz graph visualization package [GViz] that can be used to obtain a graphical representation of the state space.

`statistics'

Display statistics computed over all test rounds performed since the program was started. This is the same information that lbtt normally outputs at the end of testing; see Test statistics, for more information about the output that is displayed.