--
-- Example Automaton
--
MODULE main

VAR
S: {red, blue, green};

ASSIGN
init(S) := blue;
next(S) := case S = blue: {green, red};
                S = red:  {red};
                S = green: {red, blue};
                1:         S;
           esac;

DEFINE
p := S = blue;
q := S = blue | S = green;
r := S = green | S = red;


SPEC EG(q)

SPEC AG(p -> AX(r))

SPEC AF AG(r)