Incorrect Answer.
MODULE main
VAR
a : boolean;
b : boolean;
ASSIGN
init(a) := 0;
init(b) := 0;
next(a) := case
!a : 1;
1 : {0, 1};
esac;
next(b) := case
!a : 0;
b : 1;
1 : {0, 1};
esac;
For the SMV code, if a and b are both 1, then the next value of b is 1
(executing the second clause of the next(b) statement). But
the next value of a can be either 0 or 1 (executing the default case
of the next(a) statement). Therefore, the
state ab should have a transition to each of the states !ab and ab, not
just to ab.
See Section 3.6 of the book for a description of the SMV description
and verification language.
Back to Question.
Next Question.