The single assignment rule

SMV follows a ``single assignment'' rule. This means that a given signal can be assigned only once in a program. Thus, we avoid the problem of conflicting definitions. The definition of ``single assignment'' is complicated somewhat by the ``next'' and ``init'' operators. The rule is this: one may either assign a value to x, or to next(x) and init(x), but not both. Thus, the following are legal:

x := foo;	next(x) := foo;
init(x) := foo;	init(x) := foo;
	next(x) := bar;

while the following are illegal:

x := foo;	next(x) := foo;
x := bar	next(x) := bar;
x := foo;	x := foo;
init(x) := bar;	next(x) := bar;