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


3.2.3 LTL formula options

The following command line options can be used to control the behavior of lbtt's random LTL formula generation algorithm. They correspond to the options available in the `FormulaOptions' section of the configuration file.

`--abbreviatedoperators[=yes | no]'
`--noabbreviatedoperators'
These options can be used to allow or prevent lbtt from using any of the “abbreviated” operators (`->', `<->', `xor', `W', `<>', `B', `M' and `[]') when generating random LTL formulas.
`--andpriority'
This option sets the priority for logical conjunction (the `/\' operator).
`--beforepriority'
This option sets the priority for the temporal “before” operator (`B').
`--defaultoperatorpriority'
This option sets the default priority for all logical and temporal operators.
`--equivalencepriority'
This option sets the priority for logical equivalence (the `<->' operator).
`--falsepriority'
This option sets the priority for the Boolean constant `false'.
`--finallypriority'
This option sets the priority for the temporal “finally” operator (`<>').
`--formulachangeinterval=NUMBER-OF-ROUNDS'
This option determines how often (in number of test rounds) lbtt should generate a new random LTL formula. A value of 0 forces lbtt to use a fixed LTL formula for all tests.
`--formulageneratemode=normal | nnf'
This option can be used to choose how lbtt should generate random LTL formulas. With the option `--formulageneratemode=nnf', all generated formulas will be in (a weakened) negation normal form in which all negations in the formula (if any) precede atomic propositions. (Note that the formulas may still contain some of the “abbreviated” operators if their priorities are not explicitly set to zero.)
`--formulaoutputmode=normal | nnf'
This option can be used to force or prevent lbtt from converting each LTL formula into (strict) negation normal form (i.e., rewriting it with the operators `!', `/\', `\/', `U' and `V') before passing it to the LTL-to-Büchi translators.
`--formulapropositions'
This option sets the maximum number of different atomic propositions that lbtt may use for generating random LTL formulas.
`--formularandomseed=INTEGER'
This option gives a seed value for generating random numbers used by the random LTL formula generation algorithm.
`--formulasize=INTEGER'
`--formulasize=MINIMUM-SIZE-MAXIMUM-SIZE'
`--formulasize=MINIMUM-SIZE...MAXIMUM-SIZE'
This option sets the size of the random LTL formulas generated for the tests. The size can be given either as a fixed integer or as an interval, in which case the size of each generated formula will be chosen randomly in the interval using a uniform random distribution.
`--generatennf'
`--nogeneratennf'
These options can be used instead of the `--formulageneratemode' option to select the random formula generation mode.
`--globallypriority'
This option sets the priority for the temporal “globally” operator (`[]').
`--implicationpriority'
This option sets the priority for logical implication (the `->' operator).
`--nextpriority'
This option sets the priority for the temporal “next time” operator (`X').
`--notpriority'
This option sets the priority for logical negation (the `!' operator).
`--orpriority'
This option sets the priority for logical disjunction (the `\/' operator).
`--outputnnf'
`--nooutputnnf'
These options can be used instead of the `--formulaoutputmode' option to choose the format in which lbtt passes LTL formulas to LTL-to-Büchi translators.
`--propositionpriority'
This option sets the priority for atomic propositions.
`--releasepriority'
This option sets the priority for the temporal “(weak) release” operator (`V').
`--strongreleasepriority'
This option sets the priority for the temporal “strong release” operator (`M').
`--truepriority'
This option sets the priority for the Boolean constant `true'.
`--untilpriority'
This option sets the priority for the temporal “(strong) until” operator (`U').
`--weakuntilpriority'
This option sets the priority for the temporal “weak until” operator (`W').
`--xorpriority'
This option sets the priority for the logical “exclusive or” operator.

Note also the `--formulafile=FILE-NAME' option (see `--formulafile' option), which can be used to instruct lbtt to read LTL formulas from a file (or standard input) instead of generating them randomly.