The NuSMV tool offers only one traversal method that may be used with any valid conjunctive decomposition of the TR. NuSMV implements three main methods to perform this conjunctive decomposition and order the application of the resulting clusters. The methods are named as: Monolithic, Threshold and IWLS95.
Beside these three main methods, NuSMV offers several parameters that may affect to a great extent the partitioning. For instance, one may enforce NuSMV to group TRs according to their affinity as defined in [4]: the proportion of the number of variables two transitions share over the total number of their variables. By default NuSMV uses affinity in methods Threshold and IWLS95.
Monolithic
This method simply tries to build a monolithic TR from the bit relations. Although this method guarantees the minimum number of BDD operations during traversal (if iterative squaring is not used), to build a monolithic TR starts to be an unfeasible task for intermediate-sized designs.
Threshold
The bit TRs are conjoined in clusters, until the size (in BDD nodes) of the cluster exceeds a certain threshold. If affinity is used, then TRs are first ordered, thus TRs with highest affinity are clustered first. The user may specify this threshold, that has a default value of 1000 nodes. Resulting clusters are not ordered after this process.
IWLS95
It is an implementation of the method described in [9]. First of all, the transition relations are ordered using a heuristic, and then conjoined in clusters until a threshold is reached. By default this first ordering is deactivated in NuSMV so, in fact, by using default settings, the clustering produced by this method is the same as the Threshold. However, afterward the clusters are ordered using the same heuristic. The heuristic used in both orderings is a combination of weighted factors, and the weights are also user-modifiable parameters.
The factors considered by the heuristic are the following (refer to [9] for an exact definition): the number of variables that can be existentially quantified when the cluster is applied, the number of present state and primary input variables in its support, the number of present state and primary input variables not yet quantified, the number of next state variables introduced by its application, the number of next state variables not yet introduced, the maximum BDD index of the variable to quantify in its support and the maximum BDD index of the variables that remain to quantify out.