The VIS tool offers two different traversal methods. The first one, like NuSMV, can be used with any valid conjunctive decomposition of the transition relation. VIS implements three main methods to perform this conjunctive decomposition and order the application of the resulting clusters. The methods are named as: Monolithic, IWLS95 and MLP. The first two are equivalent to what has been said of their NuSMV counterparts, so we will just explain MLP. The second traversal method uses a hybrid approach, dynamically deciding whether to use TRs or transition functions. It must be noted that VIS implements some other techniques that are orthogonal to the method used. In particular they provide the hints mechanism [11] as well as high density traversals [10]. As hints demand user interaction we chose not to use this technique. On the other hand, we ran all the methods with and without high density traversal.
MLP [4]
Broadly speaking TRs are ordered in a way such that the dependency matrix between relations and variables tends to be triangular. This is done in order to try to achieve a minimum average lifetime for the variables. Once ordered, bit relations are clustered based on their affinity.
Hybrid [5]
This method is the only one in VIS that dynamically adapts to what is happening during the traversal process. The main idea is that, depending on the structure of the dependency matrix, one should better conjoin or split. If dependency matrix tends to be triangular, then conjunction is used, otherwise a variable is chosen and then transitions are split accordingly. This process, in general, produces problems with easier conjunctions. Based on this observation, the method switches from conjunction to split and the other way round depending on the dependency matrix and how previous decisions performed. It must be noted that in the conjunction phase one can use either IWLS95 or MLP. We chose IWLS95.
High density [10]
This technique tries to prevent the methods from having to handle too big BDDs. If during the computation of some BDD, the size of the partially computed BDD exceeds a given threshold, the computation is stopped, a dense subset of states is chosen (with a much smaller representation) and the process is resumed. When no new states are discovered, the process is started again with a larger threshold, and this is done iteratively until all states are discovered.