MODULE main
VAR
  x : boolean;
  y : boolean;
ASSIGN
  init (x) := FALSE;
  next (x) := !x;
  init (y) := FALSE;
  next (y) := y <-> !x;
SPEC
  AG !(x & y)