This module provides the routines for constructing and manipulating FSMs at the BDD level. The FSMs can be represented in monolithic or partitioned form [9,10,11]. The heuristics used to perform the conjunctive partitioning of the transition relation and reordering of the clusters [35,53] were developed to work at the BDD level, independently of the input language. This is a precise design choice: since NUSMV is intended to be applicable to a wide range of domains, for which the current input language might not be appropriate, it is important that the heuristics do not depend on the input language. Note that for a specialized model checker this might not be a suitable choice. For instance, since VIS [6] is highly specialized for hardware, its heuristics were developed to work directly on the BLIF format [56], which is a netlist14. The interface to other modules is given by the primitives for the computation of image and pre-image of set of states. These primitives are independent from the method used to represent the transition relation (monolithic, conjunctive or disjunctive).
>