MODULE main
VAR
  u : boolean;
ASSIGN
  init (u) := FALSE;
SPEC
  AG !u