MODULE main
VAR
  a : boolean;
  b : boolean;
ASSIGN
  init (a) := TRUE;
  init (b) := TRUE;
  next (a) := a;
SPEC
  AG (a | b)