Improving the generation of random modal formulae for testing decision procedures