FormulaOptions Block Generator for lbtt

[Help]

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.