MODULE main
VAR
  a : boolean;
ASSIGN
  next (a) := a;
SPEC
  AG !a