3.1.3 The `FormulaOptions' section

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'.)