MODULE main
VAR
  state : {a, b};
ASSIGN
  init(state) := a;
  next(state) := case 
     state = a : b ;
     state = b : a ;
    esac; 
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 ]