MODULE main
VAR
  a : boolean;
  b : boolean;
INVAR
  b -> a
ASSIGN
  init (a) := FALSE;
  next (a) := b;
SPEC
  AG a = b