MODULE main
VAR
  input : boolean;
  state : boolean;
ASSIGN
  init (state) := TRUE;
  next (state) := state & input;
SPEC
  AG state