Next: Random state spaces, Previous: Random input generation, Up: Random input generation

The LTL formulas used by `lbtt` are built from
atomic propositions (with names of the form
``p`'`n`
for some nonnegative integer `n`), the Boolean constants
``true`' and ``false`',
and logical or temporal operators. `lbtt` supports the
following logical operators:

- logical disjunction
(`
`\/`' as shown in output messages), - logical conjunction
(`
`/\`'), - logical negation
(`
`!`'), - logical implication
(`
`->`') - logical equivalence
(`
`<->`') - logical “exclusive or”
(`
`xor`')

and the following temporal operators:

- “Next time”
(`
`X`'), - “(Strong) Until”
(`
`U`'), - “Weak Until” (also known as “Unless”)
(`
`W`'), - “Finally” (“Eventually”)
(`
`<>`') - “Before”
(`
`B`') - “(Weak) Release”, the dual of “(Strong) Until”
(`
`V`'), - “Strong Release”, the dual of “Weak Until”
(`
`M`'), - “Globally” (“Always”, “Henceforth”)
(`
`[]`').

See LTL formulas, for a reference on the exact semantics of these operators.

The behavior of `lbtt`'s random formula generation algorithm can be
adjusted with the following parameters:

- Number of nodes in the parse tree of a formula (i.e., the total number of occurrences of propositions, Boolean constants and operators in the formula).
- Number of different atomic propositions that can be used for generating a
formula. (Note that this does not restrict the total number of atomic
propositions in the formula, nor the number of occurrences of any individual
proposition. However, none of the generated formulas will have more than this
number of
*different*atomic propositions.) - Priorities for the Boolean constants and atomic propositions. The priority of a symbol determines the relative likelihood of its occurrence in a generated formula. The higher the priority of a symbol, the more likely it is that the symbol will occur (with respect to the other symbols) in a generated formula; a zero priority will exclude the symbol altogether.
- Priorities for the logical and temporal operators.

Note that the priorities for atomic symbols (Boolean constants and atomic propositions) and the priorities of the logical and temporal operators are independent, i.e., changing the priority of an atomic symbol does not affect the likelihood of the occurrence of any logical or temporal operator and vice versa.

For further details, see The formula generation algorithm for a pseudocode description of the algorithm used for generating random LTL formulas.