module main {
  // 1. Data Types Definition
  type status_t = enum { ready, busy };

  // 2. Variable Declarations
  var request : boolean;
  var status : status_t;
  var wasRequested : boolean; // Auxiliary variable to track if request was ever true

  // 3. Initialization
  init {
    status = ready;
    wasRequested = false;
  }

  // 4. State Transition
  next {
    status' = if (request) then busy else status;
    wasRequested' = wasRequested || request;
  }

  // 5. Property Specification
  property request_implies_busy_eventually: always (request -> eventually(status == busy));

  // 6. Control and Verification
  control {
    check;
    print_results;
  }
}
