TranSyT image computation methods

In [14] several traversal algorithms were introduced. Here we give a short description of them. In contrast with the methods used in NuSMV and VIS which are synchronous oriented, and thus, use conjunctively partitioned transition relations, transition relations of concurrent systems are more easily represented with disjunctive partitioning. When disjunctive partitioning is used it is also important to schedule the application of the transition relations, specially when the chaining technique is used. Recall that the chaining technique is conceptually very simple: instead of firing from the same origin set (usually named as from set) each one of the transitions, all the states produced by the application of each transition is accumulated into the origin set as soon as they are produced. The methods described below are just heuristics to try to derive a good scheduling order for this technique in order to minimize the number of events needed, thus the possibility of a BDD operation that produces a blow up.

Basic chaining

This method uses chaining, but uses the same static event scheduling as plain BFS, that is, the order of event definition in the input file. This method was introduced in [12] and it is useful as a ground basis to compare the amount of reduction due to the chaining technique itself and the amount due to the particular scheduling. In some examples (notably buffers or FIFOs) it may achieve very good results as the order of event definition in the input file is already almost optimal.

Token traversal

Before starting the traversal, a causality analysis between events is performed. An event $e_j$ is said to be a causal successor of event $e_i$ if potentially there exists some state where the activation of $e_i$ enables $e_j$. This information may be derived directly from the transition relations of the events and is stored in a sparse matrix, as usually one event is a causal predecessor of very few events.

A vector of integers is used to determine which event would be fired next. Each event is assigned a place in the vector, and the places of events that are initially fireable are set to 1, the others are set to 0. The algorithm choses the event with the highest value and fires it. In case of a tie, it nondeterministically choses one of them.

After the event is fired, it adds the resulting new states to the reached set and the from set (chaining technique) and clears the position of the event. If no new states were produced no further action is done, otherwise, the vector places of the events that are causal successors of the one fired, increment their value by one.

When all the vector has zeros, the frontier set is computed and all the process starts again (we check which events are fireable, and put a one in its place, ...). This process continues until the frontier set becomes the empty set, which means that a fixpoint has been reached.

We must stress that this approach (as well as the others presented in this section) are dynamic, in the sense that the scheduling may change during the traversal process in response to the states discovered so far.

Weighed token traversal

This is a variation of the former method. It has only two minor changes: (1) instead of placing a one when the event is fireable, we put the exact number of states in which it is fireable; (2) when an event is fired, we compute the new states it produced, and increment the vector places of its causal successor events by the same amount as the number of these new states in which this particular causal event is fireable. For instance, imagine that we fire event $a$ that has two successors: events $b$ and $c$. The firing of $a$ produced four new states, three in which $b$ is fireable and two in which $c$ is fireable. Then we will increment by three the vector place of $b$ and by two the vector place of $c$.

This method selects more carefully the next firing event at the cost of performing more BDD operations.

Dynamic event-clustered traversal

This method keeps track, for each event, of how many new states have been discovered in which it can be fired. The algorithm selects always the event with more states to fire from. This states can be stored in a particular from set for the event or, if its BDD size is bigger than the reached set, we use this latter set as the from set, in order to save space. The selected event is fired, its from set is cleared and the new states produced are distributed over the from sets of the rest of the events. When all the from sets are empty, a fixpoint has been reached.