module ProgramSpec {
  type StatusType = enum { busy, ready };

  var status: StatusType;

  input request: boolean;

  init {
    status = ready;

  }
  next {
    if (request == true) {
      status' = busy;
    }

  }
  invariant spec: (request == true);

}
