
module main
{
  type status_t = enum { ready, busy };

  var request : boolean;
  var status : status_t;

  init {
    status = ready;
  }

  next {
    if (request) {
      status' = busy;
    }
    // else status remains unchanged
  }

  property eventually_status_busy {
    var found_busy : boolean;

    found_busy := false;

    while (!found_busy) {
      if (request) {
        assert status == busy;
        found_busy := true;
      }
      else {
        next;
      }
    }
  }
}
