Previous: Test round messages, Up: Interpreting the output


4.3 Test statistics

At the end of testing, lbtt outputs some simple statistics computed over all tests in verbosity modes 2 and above. If using an error log file (see `--logfile' command line option), the statistics will be stored also in the log file. These statistics can be also accessed during interactive testing by using the internal command `statistics' (see `statistics' command). In brief, the statistics include:

Where applicable, the statistics are shown separately for positive, negative and all LTL formulas used in the tests.