TCS / Software / `lbtt` / `FormulaOptions` Block Generator

# `FormulaOptions` Block Generator for `lbtt`

Formula parameters
Formula size
Create a full `FormulaOptions` block
Number of atomic propositions
Priority for propositions
Priority for `true`
Priority for `false`
Formula generation interval
Random seed

Select interpretation of priorities:

Operator priorities
Unary operators Binary operators
Negation   (`!`)      Conjunction   (`/\`)
Next Time   (`X`)      Disjunction   (`\/`)
Finally   (`<>`)      Implication   (`->`)
Globally   (`[]`)      Equivalence   (`<->`)
Exclusive or   (`xor`)
Until   (`U`)
Release   (`V`)
Weak until   (`W`)
Strong release   (`M`)
Before   (`B`)

Fill in the above form with desired formula parameters and then hit the `Generate' button to generate a corresponding fragment of a `FormulaOptions` block, which can be included into an `lbtt` configuration file.

Uncheck the `Create a full `FormulaOptions` block' checkbox to generate only the settings that define the operator priorities. (In this case, the parameters listed under the checkbox can be left unspecified.)

There are two ways to interpret the specified operator priorities:

• Absolute: Copy the given priorities directly to the result.
• Relative: Try to find absolute operator priorities that balance the relative distribution of the operators in the generated formulas in the way specified. For example, by giving a relative priority of 2 for the `Next Time' operator and a relative priority of 1 for the `Until' operator (and setting all other relative priorities to zero), the resulting `FormulaOptions` block will define appropriate absolute priorities for these operators such that the expected number of Next Time operators should be (approximately) twice the number of Until operators in any LTL formula generated using the algorithm described in the `lbtt` User's Guide.

Note:

• The absolute priorities are obtained from a static database that includes the results for only selected combinations of formula size and relative priorities. Arbitrary values for these parameters are not supported.
• The absolute priorities in the database are only approximative. A program (a C++ source file) is available for testing `lbtt`'s random formula generator with given absolute priorities. See the file for usage instructions.