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 case 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, but the CTL model only allows a transition to
state !ab.
See Section 3.6 of the book for a description of the SMV description and
verification language.
Back to Question.
Next Question.