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