In order to cover as much of the problem space as possible, I wrote a
script to generate sets of 500 randomly-generated formulas varying the
formula length and number of variables as in [1]. It randomly generates sets of 500 formulas varying the number of variables, , from 1 to 5, and the length of the formula, , from 5 up to 200. It sets the probability of choosing a temporal operator
to create formulas with both a nontrivial temporal structure and a
nontrivial Boolean structure. For temporal tests, formulas are also
generated with
, , and . Other choices are decided uniformly. When generating a set of length , every formula created is exactly of length and not *up to* , however, these randomly-generated formulas are frequently reducible.

Here is the script used to generate random formulas in the style of [1]:

With no arguments: generate a wide range of formula files

With 3 arguments: generate files for specified L, N, P (order matters)

In our paper, [4], all of the random formulas we used were generated prior to testing, so each tool was run on the *same* formulas. If you wish to re-create our tests exactly, the set of formulas generated for our experiments are here: