Next: , Previous: Configuration information, Up: Interpreting the output

4.2 Test round messages

In verbosity modes 1 and 2, lbtt reports numeric statistics on the generated automata in tabular form. Each row of this table contains the following information (in this order):

The following example shows a fragment of the output that lbtt might produce during a test round when running in the default verbosity mode 3. 

1. Round 6 of 10

2.     Generating random state space

3.     Random LTL formula:
         formula:                   ((p1 <-> p0) U (p0 \/ ! p3))
         negated formula:           ! ((p1 <-> p0) U (p0 \/ ! p3))

       0: `Implementation 0'
         Positive formula:
4.         Büchi automaton:
             number of states:      6
             number of transitions: 15
             acceptance sets:       1
             computation time:      0.03      seconds (user time)
5.         Product automaton:
             number of states:      582       [97.00% of worst case (600)]
             number of transitions: 7188
6.         Accepting cycles:
             cycle reachable from   0         states
             not reachable from     100       states
7.       Negated formula:
           Büchi automaton:
             number of states:      4
             number of transitions: 6
             acceptance sets:       0
             computation time:      0.04      seconds (user time)
           Product automaton:
             number of states:      363       [90.75% of worst case (400)]
             number of transitions: 2581
           Accepting cycles:
             cycle reachable from   25        states
             not reachable from     75        states
8.       Result consistency check:
           result:                  failed    [75 (75.00%) of 100 test cases]

The numbered parts of the output are:

  1. Number of the test round.
  2. lbtt generates a new random state space for model checking tests. (In this case the size of the state spaces was fixed in the configuration; if the state space size is allowed to vary in an interval, lbtt would also show here the actual size of the generated state space.)
  3. Information about a random LTL formula and its negation. To simplify the notation, it is assumed that all unary formula operators have higher precedence than binary operators.
  4. Information about the Büchi automaton that `Implementation 0' generated from the positive LTL formula (number of states, transitions and acceptance conditions, and the amount of user time elapsed in generating the automaton).
  5. Information about the synchronous product of the state space and the Büchi automaton constructed from the positive formula.
  6. Model checking result information. In this case, the automaton cannot reach an “accepting cycle” regardless of the state of the state space in which the automaton could begin its execution. In other words, the random state space contains no states with an infinite path beginning from the state such that the Büchi automaton accepts the temporal interpretation of the path (the infinite sequence of state labels on the path).
  7. The model checking process is repeated using the negated formula as input for the LTL-to-Büchi translator `Implementation 0'.
  8. lbtt performs the model checking result consistency check (see Model checking result consistency check) using the model checking results computed for the positive and the negative formula. In this example, the result consistency check fails in 75 states of the state space. This implies that `Implementation 0' failed to translate one (or both) of the formulas into a Büchi automaton correctly.

The output of phases 4—8 will be repeated for each implementation included in the tests. After this lbtt proceeds to the model checking result cross-comparison test (see Model checking result cross-comparison test) and the Büchi automata intersection emptiness test (see Automata intersection emptiness check).

The model checking result cross-comparison test might result in the following output (shown in verbosity modes greater than 1): 

    Model checking result cross-comparison:
      result:
        failed (+)  0: `Implementation 0', 1: `Implementation 1'

Throughout all test failure reports, lbtt refers to the positive and negated formulas with the symbols `+' and `-', respectively. Therefore, the above message indicates that the model checking results obtained using `Implementation 0' and `Implementation 1' for the positive formula do not agree. A similar line will be shown for all pairs of implementations for which the test failed.

lbtt also reports if the model checking result cross-comparison could not be performed between a pair of implementations (for example, if one of the implementations failed to generate an automaton); in this case, the result of the test is `N/A'.

If using enumerated or randomly generated paths as state spaces, the model checking results are also compared against those given by lbtt's internal model checking algorithm.

A similar convention is used to report failures in the Büchi automata intersection emptiness check. However, because this test is always performed on Büchi automata constructed from two complementary LTL formulas, a test failure report shows LTL formula information beside the name of the implementation used for generating the Büchi automaton from that formula. Note that the Büchi automata intersection emptiness check may fail on the automata constructed by the same implementation; in the following example, the check failed between the automata constructed by `Implementation 0', and the automata constructed by `Implementation 0' and `Implementation 1' from the positive and negative formulas, respectively. 

    Büchi automata intersection emptiness check:
      result:
        failed      0: `Implementation 0'
        failed (+)  0: `Implementation 0', (-) 1: `Implementation 1'

If using a log file (see `--logfile' command line option), a summary of all testing errors will be written to the file using the output format specified above.