Next: Testing procedure, Previous: Test methods, Up: Test methods
By default, all tests lbtt makes are based on randomly generated input. However, the LTL formulas used as input for the LTL-to-Büchi translators can be optionally given by the user by telling lbtt to read LTL formulas from a file or from standard input (see `--formulafile' command line option).
Additionally, some of the tests make use of randomly generated “state spaces”, which are basically directed labeled graphs with labels on nodes with the additional requirement of having at least one arc leaving each node. The label of each node is a subset of a finite collection of atomic propositions (an uninterpreted set of assertions which may or may not hold in a state), which occur also in the LTL formulas used in the tests.
The following sections describe how lbtt generates input for the tests and list the parameters which can be used to adjust the behavior of the input generation algorithms.