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
netlist^{14}.
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).

NuSMV <>