An SMV program amounts simply to a system of simultaneous equations, with a set of unknowns 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. These rules 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: