next up previous contents
Next: The single assignment rule Up: The SMV language Previous: State machines   Contents

Rules for assignments

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:



Subsections

2002-10-28