Unit delay assignments - the ``next'' operator

A special operator is provided for describing recurrences. Recurrences are circular or recursive systems of equations, and are the way that sequential systems are described in SMV.

If x is a signal, then next(x) is, intuitively, the ``next'' value of x. More precisely, the $i$th value of next(x) is equal to the $(i+1)$st value of x. Thus, for example, if

              x = 0,1,2,3,...

then

        next(x) = 1,2,3,4,...

By assigning a value to the ``next'' value of a signal, we can define a sequential machine. For example, assuming x and y are boolean signals,

        next(x) := y ^ x;

defines a signal x which ``flips'' each time the signal y is true (the ^ operator stands for ``exclusive or''). By definition, the ``next'' value of x is equal to (y ^ x), which is equal to x if y is false and ~x if y is true. Note, however, that the above assignment does not tell us the initial value of x. Thus, we obtain a different sequence depending on whether x starts at 0 or 1. We can determine this initial value by assigning

        init(x) := 0;

In this case, if we had

        y = 0;1;0;1;...

we would get

        x = 0;0;1;1;0;0;1;1;...

On the other hand, if we assigned

        init(x) := 1;

we would obtain the sequence

        x = 1;1;0;0;1;1;0;0;...

As another example, to declare a signal x that maintains a running sum of the values of a signal y, we would say

        init(x) := 0;
        next(x) := x + y;