FormulaOptionsBlock Generator for
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:
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
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
described in the
lbtt User's Guide.
lbtt's random formula generator with given absolute priorities. See the file for usage instructions.