MODULE main
VAR
  x : boolean;
  e : boolean;
  r : boolean;
ASSIGN
  init (x) := FALSE;
  next (x) := case r : FALSE; TRUE : case e : !x; TRUE : x; esac; esac;
SPEC
  AG !x