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