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.