MODULE main
VAR
state : {STATE_I,STATE_A,STATE_B,STATE_C,STATE_D};
ASSIGN
    init(state) := STATE_I;
    next(state) :=
        case
            state = STATE_I : {STATE_A,STATE_B};
            state = STATE_A : {STATE_C,STATE_D};
            state = STATE_B : {STATE_C};
            state = STATE_C : {STATE_A};
            state = STATE_D : {STATE_B};
        esac;
DEFINE
    a := state = STATE_A | state = STATE_B;
    b := state = STATE_C;

LTLSPEC
    X a;
LTLSPEC
    F b;
LTLSPEC
    G( b -> F(a))