MODULE main
VAR
  request : boolean;
state : {ready,busy}; ASSIGN
  init(state) := ready;
  next(state) := case
                   state = ready & request : busy;
TRUE : {ready,busy}; esac;