Generating random values using Binary Decision Diagrams and Convex Polyhedra

This article describes algorithms to solve Boolean and numerical constraints, and to randomly select values among the set of solutions. Those algorithms were first designed to generate inputs for testing and simulating reactive real-time programs. As a consequence, the chose a solving technology that allow a fine control in the way solutions are elected. Indeed, a fair selection is sometimes required, while favoring limit cases is often interesting for testing. Moreover, simulating a single reactive execution means generating several hundreds or even several thousands of atomic steps, and thus as many solving steps. Hence, the emphasis is put on efficiency, sometimes sacrificing precision or fairness