Previous: Test round messages, Up: Interpreting the output
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:
Note that the pairwise inconsistency results form a symmetric matrix (possibly shown in several parts), which means that the same information is repeated on both sides of the matrix diagonal.
Where applicable, the statistics are shown separately for positive, negative and all LTL formulas used in the tests.