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 EG(!a)

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

so the specification is false for some initial state under the
fairness constraint !a. Note that
any path from the initial state !a!b must next go 
to the state a!b, where a is false.
So EG a
is false at the sole initial state.
Observe that this is indeed what the SMV tool suggests.


Back to Question.

Next Question.