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

Running the SMV program above, we obtain
nunk% smv test4.smv
-- specification AG EF b is true

so the specification holds for all initial states under the
fairness constraint !a. Note that
the CTL formula AG EF b states that at any state t reachable from the
initial state, the formula EF b is true. In the given model,
all states are reachable from the only initial state.
The path w = !ab -> a!b -> !ab -> a!b -> ... is a fair path, so !ab
staisfies EF b under the fairness constraint
a.
Similarly, the paths

 ab -> w
 !ab -> w and
 !a!b -> !ab -> w

are all fair paths, so all states satisfy EF b under the fairness constraint
a. Therefore, AG EF b is true at the
initial state with the given fairness assumption.


Back to Question.

Next Question.