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

Running the SMV program above, we obtain
nunk% smv test1.smv
-- specification AG (b -> AF (!a)) is true
resources used:
user time: 0.04 s, system time: 0.02 s
BDD nodes allocated: 27
Bytes allocated: 1245184
BDD nodes representing transition relation: 7 + 1

so the specification is true for all initial states under the
fairness constraint !a. Note that
AG(b  AF a) states that at every state t
reachable from any initial state, if b is true at state t,
then so is AF a.
Given the fairness constraint 
of a we know that on every fair path from
any state reachable from the initial state,
a eventually
holds. Therefore AF a is true at
any state reachable 
from the initial state under the fairness constraint
a.


Back to Question.

Next Question.