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