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

4.1 Configuration information

Before starting tests, lbtt outputs (in verbosity modes 2 and above) a summary of the current program configuration as obtained by reading the program configuration file and interpreting the command line parameters. The same summary can be obtained without running any tests by using the `--showconfig' command line option (see `--showconfig' option). The information will be written also to the error log file if one was specified in the command line with the `--logfile' option (see `--logfile' option). The summary consists of the following information:


     Program configuration:
       1000 test rounds.
       Testing will be interrupted in case of an error.
       Signalling a break will interrupt testing.
       Using global model checking for tests.
       Writing error log to `error.log'.
         0: `Implementation 0'
         1: `Implementation 1'
       Timeout for translators is set to 30 seconds.
       Enabled tests:
         Model checking result cross-comparison test
         Model checking result consistency check
         Büchi automata intersection emptiness check
       Random state spaces:
         Random graphs (50 states, 5 atomic propositions)
         New state space will be generated after every 5th round.
         Random seed: 98
         Random edge probability: 0.10
         Propositional truth probability: 0.50
       Random LTL formulas:
         5 parse tree nodes, 5 atomic propositions
         New LTL formula will be generated after every round.
         Random seed: 17991
         Atomic symbols in use (priority):
           false (5); propositions (90); true (5)
         Operators used for random LTL formula generation:
           operator  !        /\       U        V        X        \/
           priority  10       10       20       20       10       20