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: