These scripts generate formulas from the eight classes of scalable formulas defined by  to evaluate the performance of model checking algorithms on temporally-complex formulas.
Run them like this:
formula.pl [-v] n
where is the number of variables (ie the size) of the formula you desire. The flag -v is for ``verbose.''