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;
To verify this answer, you can run the SMV program fragment above with the specification below, which characterizes the CTL model at hand (why?). If this answer is correct, SMV should reply saying that the specification holds. 
     SPEC
       !a & !b &
       AG(a & b -> AX(b)) &
       AG(!a & b -> AX(a & !b)) &
       AG(!a & !b -> AX(a & !b))
Can you explain why we omitted a conjunct for AG(a & !b -> ...)?
Back to Question.
Next Question.