Next: Test round messages, Previous: Interpreting the output, Up: Interpreting the output
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:
Example:
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'.
Implementations:
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