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 is 1 and b is 0, then the next value of b can
be either 0 or 1 (executing the default case
of the next(b) statement). Similarly, the next value of a can
be either 0 or 1 (executing the default case
of the next(a) statement).
Thus, there have to be transitions to all four states from state
a!b. But there are two such transitions missing in the CTL model.
See Section 3.6 of the book for a description of the SMV description and
verification language.
Back to Question.
Next Question.