Proc. Foundations of Software Engineering 96
Download the PostScript.
Relational terms are replaced by matrices of boolean formulae. These formulae are then composed to give a boolean translation of the entire relational formula. Thoughout, boolean formulae are represented with BDDs; from the resulting BDD, models are easily extracted.
The performance of the BDD method is compared to our previous method based instead on explicit enumeration. The new method performs as well or better on most of our examples, but can also handle specifications that, until now, we have been unable to analyze.