Next: , Previous: Command line options, Up: Command line options


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 configuration file.

`--configfile=FILE-NAME'
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.
`--formulafile=FILE-NAME'
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.

`--h'
`--help'
These options list all the available command line parameters.
`--logfile=FILE-NAME'
This option instructs lbtt to create a log of all errors encountered during testing. By default no log will be created.
`--profile'
This option can be used as a shorthand for disabling all Büchi automata correctness tests. 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.
`--quiet'
`--silent'
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.
`--showconfig'
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 any tests.
`--showoperatordistribution'
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.
`--skip=NUMBER-OF-ROUNDS'
This option can be used to skip the first NUMBER-OF-ROUNDS test rounds, i.e., begin testing from round NUMBER-OF-ROUNDS+1.
`-V'
`--version'
This option displays the version of the lbtt executable.