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;
       FAIRNESS !a
       SPEC AG(!a & EX(b))

Running the SMV program above, we obtain
nunk% smv test5.smv
-- specification AG (!a & EX b) is false
-- as demonstrated by the following execution sequence
state 1.1:
a = 0
b = 0

so the specification does not hold for some initial state under the
fairness constraint !a. Note that
the CTL formula
AG ( a  EX b) states that at every state t reachable from the
initial state, the formula  a  EX b is true. The state a!b is reachable from 
the initial sate, but a and hence a  EX b, does
not hold at state a!b. Note that this analysis
is not impacted by the presence, or
absence, of the given fairness constraint.


Back to Question.
 Next Question.