model request_status_model {
    // Define the type for status
    type status_t = enum { ready, busy };

    // Declare variables
    var request : boolean;
    var status : status_t;
    var requested : boolean; // Auxiliary variable to track if request has been true

    // Initialize the variables
    init {
        status = ready;
        requested = false;
    }

    // Transition relation
    next {
        // Track if request has been true at least once
        requested' = requested || request;

        // Update status based on request
        if (request) {
            status' = busy;
        } else {
            // Non-deterministic behaviour when request is false
            havoc status';
        }
    }

    // Property to verify: if request is true, status eventually becomes busy
    invariant property_eventually_busy : (requested -> (status == busy));

    // Control block for model checking
    control {
        v = unroll(5);  // Unroll up to 5 steps
        check;
        print_results;
    }
}
