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]:
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: