2.2 Testing procedure

The following figure illustrates the first two tests in lbtt's testing procedure:

After obtaining an LTL formula f (either by reading it from a file or by calling the random formula generation algorithm), lbtt invokes each LTL-to-Büchi translator participating in the tests in turn to construct a collection of Büchi automata for the formula f and the negated formula ! f. Each of these automata is then composed with the randomly generated state space, whereafter lbtt performs the model checking result cross-comparison test (see Model checking result cross-comparison test) and the model checking result consistency check (see Model checking result consistency check) on the model checking results, and reports all detected failures.

The Büchi automata intersection emptiness check (see Automata intersection emptiness check) operates as follows (note that the LTL-to-Büchi translation phase is repeated in this figure only for completeness; in reality, lbtt performs this phase only once):

The test procedure can then be repeated using a different LTL formula and/or a different state space.