An SMV program amounts simply to a system of equations, with a set of unkowns that are the declared signals. With an arbitrary set of equations, there is, of course, no guarantee that a solution exists, or that the solution is unique. Examples of systems that have no solutions are
x := x + 1;or
next(x) := x + 1; next(x) := x - 1;
An example of a system with many solutions is
x := y; y := x;
We avoid these difficulties by placing certain rules on the structure of assignments in a program, to guarantee that every program is executable. This means, among other things, that a schedule must exist for computing the elements of all the sequences. The rules for assignments are: