Previous: Data display commands, Up: Analyzing test results


5.5 Failure analysis commands

The first part of this section introduces the commands available for identifying an LTL-to-Büchi translator that caused a failure in one of the automata correctness tests. The second part describes the conventions that lbtt uses for justifying the result of the analysis.

5.5.1 Alphabetical list of failure analysis commands

`buchianalysis <implementation-id> <implementation-id>'
Analyze a failure in the Büchi automata intersection emptiness check (see Automata intersection emptiness check). The two implementation identifiers select the Büchi automata for which to perform the analysis. The Büchi automata intersection emptiness check always involves automata constructed from the positive and the negative formulas used in the current test round. The first implementation identifier chooses an implementation that constructed an automaton from the positive formula, and the second identifier selects an implementation used for translating the negative formula into an automaton. (The identifiers can also be equal if one of the tested implementations failed the check against itself.)

A failure in the Büchi automata intersection emptiness check implies that there exists an input sequence over subsets of atomic propositions that is accepted by both automata included in the analysis. lbtt examines the intersection of the automata to find a witness of such an input, checks whether this witness is a model of the positive formula, and tells which one of the automata is likely to be incorrect according to the following rules:


`consistencyanalysis <implementation-id> [state-id]'
Analyze a failure in the model checking result consistency check (see Model checking result consistency check). The implementation-id parameter chooses the implementation to analyze. In addition, the optional state-id parameter can be used to specify a state (in the state space) in which to perform the analysis (use the `inconsistencies' command, Data display commands, to see a list of all states in which the check failed). If the state identifier is omitted, lbtt will try to find a state where the check failed.

A failure in the model checking result consistency check implies the existence of a witness (i.e., a path in the state space used for the tests in the current test round) whose temporal interpretation is not accepted by either of two automata constructed from two complementary LTL formulas. In the analysis, lbtt finds such a witness, checks separately whether it is a model of the positive formula, and then tells which one of the automata seems to reject the witness incorrectly.

`resultanalysis [``+'' | ``-''] <implementation-id> <implementation-id> [state-id]'
Analyze a failure in the model checking result cross-comparison test (see Model checking result cross-comparison test) between two implementations on either the positive (`+') or the negative (`-') LTL formula used in the current test round. The implementation identifiers can be optionally followed by an identifier of a state in the state space to specify a state in which the analysis should be performed. (Suitable state identifiers can be found by looking for inconsistencies in the model checking results accessible with the `evaluate' command, Data display commands; by omitting the state identifier, lbtt will try to find a state in which the model checking result comparison failed between the implementations.)

If using randomly generated or enumerated paths as state spaces, lbtt also accepts the identifier `lbtt' in place of either of the implementation identifiers. This instructs lbtt to perform the analysis against lbtt's internal model checking algorithm.

A failure in the model checking result cross-comparison test suggests that the state space used in the current test round contains a path which is accepted by one, but rejected by another automaton constructed from the same LTL formula. To determine which one of these automata accepts or rejects the input incorrectly, lbtt finds a witness path giving contradictory model checking results, model checks the formula separately in the witness, and tells which one of the automata seems to accept or reject the witness incorrectly.

5.5.2 Witnesses, proofs and refutations

All of the above analysis commands use lbtt's internal model checking algorithm to determine which one of the two automata involved in each test is incorrect by checking whether an LTL formula holds in a witness path extracted from the state space used in the current test round or from the intersection of two Büchi automata. The witness path is a sequence of consecutive states that ends in a loop, and is represented in two parts as an initial “prefix” (which may be empty) and a “cycle” that is considered to repeat itself indefinitely. The witness might, for example, look as follows:

         Execution M:
           prefix:
             s3 {p0,p2,p4} --> s4
           cycle:
             s4 {p1,p3} --> s5
             s5 {p3} --> s6
             s6 {p1,p2,p3} --> s7
             s7 {p3,p4} --> s8
             s8 {p1} --> s9
             s9 {} --> s2
             s2 {} --> s3
             s3 {p0,p2,p4} --> s4

In this case, the witness (or “execution” as displayed in the output) M consists of a single-state prefix followed by a cycle of eight states. The atomic propositions that hold in each state are also shown in the output.

(The witness can be considered a small state space M = <S, R, L> following the definition in State spaces; in the example above, S = {s2, s3, s4, s5, s6, s7, s8, s9}, R = {(s2, s3), (s3, s4), (s4, s5), (s5, s6), (s6, s7), (s7, s8), (s8, s9), (s9, s2)}, L(s2) = L(s_9) = {}, L(s3) = {p0, p2, p4}, L(s4) = {p1, p3}, L(s5) = {p3}, L(s6) = {p1, p2, p3}, L(s7) = {p3, p4}, and L(s8) = {p1}.)

In the model checking result cross-comparison test and the model checking result consistency check, the witness is an actual path extracted from the state space used for the tests in the current test round. In this case, the state identifiers correspond to the states of the state space, and can be accessed with the `statespace [state-id]' command (see Data display commands).

To justify the result of the analysis, lbtt also displays a proof or a refutation for the LTL formula in the witness. The proof or refutation is constructed by a recursive examination of the subformulas of the (positive or negative) formula used in the current test round according to the semantics of LTL and might look as follows:

         Analysis of the formula in the execution:
           M,<s3, ...> |/= ((X p0 U ! p4) <-> p0) :
           +-> M,<s3, ...> |/= (X p0 U ! p4) :
           |   +-> M,<s3, ...> |/= X p0 :
           |   |   +-> s3 --> s4
           |   |   +-> M,<s4, ...> |/= p0
           |   +-> M,<s3, ...> |/= ! p4 :
           |       +-> M,<s3, ...> |== p4
           +-> M,<s3, ...> |== p0

The proof (or refutation) can be considered a tree of statements of the form `M,<s, ...> |== subformula' or `M,<s, ...> |/= subformula'. Here, the symbol `|==' is used to denote that the formula subformula holds in the (infinite) subsequence beginning at state `s' of the witness, and the relational symbol `|/=' denotes the opposite. The children of each proof tree node give justification for the claim in their parent node; the children might be further expanded if the claims in them do not directly follow from the definition of L. In the presence of temporal operators, the proofs may need to be based also on the structural properties of M. These are shown as statements of the form `sn --> sm' to indicate that M contains a transition from the state `sn' to the state `sm' (and, since the states in M are connected into a non-branching sequence, that this is the only transition originating from `sn').

In the above example, lbtt claims that the formula `((X p0 U ! p4) <-> p0)' does not hold in the witness presented earlier in this section, and that this follows (by the semantics of logical equivalence) from the claims that the subformula `(X p0 U ! p4)' does not hold, but the subformula `p0' holds in this witness. `(X p0 U ! p4)' does not hold in the witness, because neither `X p0' nor `! p4' holds in the first state of the witness (p4 is included in L(s3), and p0 is not included in L(s4), where s4 is the only successor of s3). On the other hand, `p0' holds in the witness because of the fact that p0 is included in L(s3).