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