3.2.1 Special options
The following list presents all command line options for which there is
no (directly) corresponding option that may be set in the program
- This option can be used to instruct lbtt to read program
configuration from another file instead of the default configuration
file `config' in the current working directory.
- This option instructs lbtt to read the LTL formulas used in the tests
from a file (or standard input) instead of generating them randomly. The
special filename `-' refers to standard input. Each
input formula should be followed by a newline. The formulas can be specified
either in lbtt's own prefix notation
(see Format for LTL formulas; also the infix notation used in output
messages is supported) or in a variety of formats found in
some LTL-to-Büchi translator implementations (Spin, LTL2BA, LTL2AUT,
Temporal Massage Parlor, Wring, Spot, LBT), however with the restriction that
all atomic propositions should have names of the form
`pN' for some nonnegative integer N.
(When using one of the alternative
formats, it is recommended to use parentheses to avoid possible ambiguities in
the precedence and associativity of the various operators; in lbtt,
the unary operators have the highest precedence, `/\' has higher
precedence than `\/', which in turn has higher precedence than any of
`->', `<->' or `xor', and the binary temporal operators have
the lowest precedence. All binary logical operators are left-associative;
all binary temporal operators are nonassociative.)
If this option is used, all command line or configuration file parameters
affecting the generation of random LTL formulas (excluding their mode of
output) are ignored.
- These options list all the available command line parameters.
- This option instructs lbtt to create a log of all errors
encountered during testing. By default no log will be created.
- This option can be used as a shorthand for disabling all Büchi automata
The test report generated at the end of testing then shows
only the running times of each tested LTL-to-Büchi translator and the sizes
of the generated automata.
- These options suppress any messages that are normally displayed during
testing. Use the `--logfile' option (see
above) with these options to save a test failure report into a log file.
- If this option is present on the command line, lbtt will
write the current configuration to standard output
(see Configuration information) and then exit.
This option can be used together with the `--configfile' option to
test the settings defined in a configuration file without actually performing
- With this option lbtt uses the priorities defined for the
LTL formula operators available for random LTL formula generation to compute
the expected number of occurrences of each operator in a single randomly
generated formula. The distribution is then displayed along with other
configuration information when the program starts.
- This option can be used to skip the first NUMBER-OF-ROUNDS test rounds,
i.e., begin testing from round NUMBER-OF-ROUNDS+1.
- This option displays the version of the lbtt executable.