Next:
Counter Formulas Up: Input Formulas Previous: Input Formulas

Random Formulas

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, $N$, from 1 to 5, and the length of the formula, $L$, from 5 up to 200. It sets the probability of choosing a temporal operator $P = 0.5$ to create formulas with both a nontrivial temporal structure and a nontrivial Boolean structure. For temporal tests, formulas are also generated with $P = \frac{1}{3}$, $P = 0.7$, and $P = 0.95$. Other choices are decided uniformly. When generating a set of length $L$, every formula created is exactly of length $L$ and not up to $L$, however, these randomly-generated formulas are frequently reducible.


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

generateFormulas.pl
        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:


formulas/
formulas.zip



Next:
Counter Formulas Up: Input Formulas Previous: Input Formulas
Kristin Yvonne Rozier 2007-05-10