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 ith 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 definiton, 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 that this ``recurrence'' places a restriction on the order in which we can compute the values of x: we cannot comput the (i+1)st value until we have computed the ith value. Since the values of x must be computed in sequence, we have defined a sequential machine.
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 set 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;