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(AF(b))

Running the SMV program above, we obtain
nunk% smv test2.smv
-- specification AG AF b is false
-- as demonstrated by the following execution sequence
-- loop starts here --
state 1.1:
a = 0
b = 0

state 1.2:
a = 1

state 1.3:
a = 0

so the specification is false for some initial state under the
fairness constraint !a. Note that
the state !a!b is obviously reachable from the
initial state !a!b. Therefore AF b must be true
at !a!b for AG AF b to also be true there. Note the 
path !a!b -> a!b -> !a!b -> a!b -> ... is a fair path,
yet b remains always false along it.
Therefore, AF b and hence AG AF b is false at !a!b.
Obeserve that this is indeed the path that SMV suggests as a
counter-witness.


Back to Question.

Next Question.