lbtt
/
FormulaOptions
Block Generator
FormulaOptions
Block Generator for lbtt
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
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:
lbtt
's random formula
generator with given absolute priorities. See the file for usage
instructions.