MODULE main
VAR
  state : {a, b};
ASSIGN
  init(state) := a;
  next(state) := {a, b}; 
    SPEC AG state=a
    SPEC EG state=a
    SPEC AF state=a
    SPEC EF state=a
    SPEC A [ state=a U state=b ]
    SPEC E [ state=a U state=b ]