Next: StateSpaceOptions section, Previous: GlobalOptions section, Up: Configuration file

The ``FormulaOptions`' section defines the parameters that affect the
algorithm `lbtt` uses for generating random LTL formulas
(for more information about the algorithm, see Random LTL formulas).
This section provides the following options:

- `
`AbbreviatedOperators =`'`TRUTH-VALUE` - This option determines whether the generated formulas should be allowed to
include any of the operators `
`->`', ``<->`', ``xor`', ``W`', ``<>`', ``B`', ``V`', ``M`' or ``[]`' (all of which can be given definitions using only the operators ``!`', ``\/`', ``/\`', ``U`' and ``V`'). Setting this option to ``No`' assigns each of the abbreviated operators a zero priority, overriding any explicit priorities defined for these operators in the program configuration. The default value for the option is ``Yes`', so abbreviations are allowed by default. - `
`AndPriority =`'`INTEGER` - Priority of the logical conjunction operator (`
`/\`'). - `
`BeforePriority =`'`INTEGER` - Priority of the temporal operator “before” (`
`B`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`ChangeInterval =`'`INTEGER` - This option determines how often (in number of test rounds)
`lbtt`should generate a new random LTL formula (or read a new formula from a user-specified file). A value of 0 forces`lbtt`to use a fixed LTL formula for all tests. The default value is 1, i.e., a new formula will be generated at the beginning of each test round. - `
`DefaultOperatorPriority =`'`INTEGER` - This option sets the priority for all formula operators for which
no priority has been given explicitly in the program configuration (i.e.,
it can be used as a shorthand to initialize the priority of all operators).
The default value of this option is 0, so all operators with no explicitly
given priorities are disabled by default.
- `
`EquivalencePriority =`'`INTEGER` - Priority of the logical equivalence operator (`
`<->`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`FalsePriority =`'`INTEGER` - Priority of the Boolean constant
`
`false`' (with respect to priorities of the constant ``true`' and the atomic propositions). - `
`FinallyPriority =`'`INTEGER` - Priority of the temporal operator “finally” (`
`<>`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`GenerateMode = Normal | NNF`' - This option determines whether
`lbtt`should generate random formulas directly into (a weakened version of) negation normal form in which the negation operator may only precede atomic propositions. Note that the formulas may still contain “abbreviated” operators if they have nonzero priorities—use ``AbbreviatedOperators=No`' or ``OutputMode=NNF`' if you wish to prevent this. The default value for this option is ``Normal`'. (See the ``OutputMode`' option below for an example about the differences in the effects of the ``GenerateMode`' and ``OutputMode`' options.) - `
`GloballyPriority =`'`INTEGER` - Priority of the temporal operator “globally” (`
`[]`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`ImplicationPriority =`'`INTEGER` - Priority of the logical implication operator (`
`->`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`NextPriority =`'`INTEGER` - Priority of the temporal operator “next time” (`
`X`'). - `
`NotPriority =`'`INTEGER` - Priority of the logical negation operator (`
`!`'). - `
`OrPriority =`'`INTEGER` - Priority of the logical disjunction operator (`
`\/`'). - `
`OutputMode = Normal | NNF`' - This option determines whether
`lbtt`should transform each generated LTL formula into (strict) negation normal form before passing it to LTL-to-Büchi translators. If the value is set to ``NNF`',`lbtt`will rewrite each generated formula into a form consisting of the operators ``!`', ``\/`', ``/\`', ``U`' and ``V`' such that all negations in the formula (if any) precede atomic propositions. The default value is ``Normal`'. (See also the ``GenerateMode`' option that can be used to force formulas to be generated directly into negation normal form.)The option is probably useful only if you have a translator which does not support the “abbreviated” operators directly, but you still wish to test it with formulas which describe properties expressed using these operators. Note, however, that rewriting may change the size of the formula.

The following table illustrates the effects of the `

`GenerateMode`' and the ``OutputMode`' options.LTL formula Can

`f`be`OutputMode`'s effect on the`f`generated if formula passed to the`GenerateMode`LTL-to-Büchi translators`=NNF`?`—————————————————————————————— (p1 V ! p0)`Yes`Normal`/`NNF`:`(p1 V ! p0) [] p0 -> <> p1`Yes*`Nor`:`[] p0 -> <> p1 NNF`:`(true U ! p0) \/ (true U p1) ! <> p0`No`Nor`:`! <> p0 NNF`:`(false V ! p0)`* only if`AbbreviatedOperators=Yes` - `
`PropositionPriority =`'`INTEGER` - Priority for atomic propositions with respect to the priority of Boolean
constants. This priority is the common priority of
*all*atomic propositions. - `
`Propositions =`'`INTEGER` - This option sets the maximum number of different atomic propositions in
each generated LTL formula. No generated formula will have more than this
number of different atomic propositions. A value of 0 will generate random
formulas with only Boolean
constants (one of which must in this case have a nonzero priority). The
default value is 5. The names of the propositions are of the form
`
`p`'`n`, where`n`is a nonnegative integer less than the maximum number of propositions. - `
`RandomSeed =`'`INTEGER` - This option specifies a seed value for generating random numbers for the
random LTL formula generation algorithm. If this option is not present, the
seed defaults to 1. See the next section for information on how to change the
default seed for the random state space generation algorithm.
(The reason for having two separate random seeds is to make the sequences of random formulas and state spaces independent of each other. For example, this makes it easy to repeat tests using the same batch of random LTL formulas, but with state spaces of different size.)

- `
`ReleasePriority =`'`INTEGER` - Priority of the temporal “(weak) release” operator (`
`V`'). - `
`Size =`'`INTEGER` - `
`Size =`'`MINIMUM-SIZE`-`MAXIMUM-SIZE` - `
`Size =`'`MINIMUM-SIZE`...`MAXIMUM-SIZE` - This option defines how many nodes are allowed in the parse tree of each
randomly generated LTL formula. If the size is given as an interval (by
separating the bounds with `
`-`' or ``...`' with no white space in between),`lbtt`chooses the size of each formula randomly in the interval using a uniform random distribution. The default size is 5. - `
`StrongReleasePriority =`'`INTEGER` - Priority of the temporal “strong release” operator (`
`M`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`UntilPriority =`'`INTEGER` - Priority of the temporal “(strong) until” operator (`
`U`'). - `
`TruePriority =`'`INTEGER` - Priority of the Boolean constant
`
`true`' (with respect to the priorities of the constant ``false`' and the atomic propositions). - `
`WeakUntilPriority =`'`INTEGER` - Priority of the temporal “weak until” operator (`
`W`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.) - `
`XorPriority =`'`INTEGER` - Priority of the logical “exclusive or” operator (`
`xor`'). (Note: This option has no effect if ``AbbreviatedOperators`' is set to ``No`'.)