module main {
    var request : boolean;
    type status_t = enum { ready, busy };
    var status : status_t;

    init {
        // Initial state
        status = ready;
    }

    next {
        // Transition rules
        if (request) {
            status' = busy;
        } else {
            // status remains the same if request is false
            status' = status;
        }
    }

    // Property to check if, when request is true, status eventually becomes busy
    invariant request_true_implies_status_busy {
        request ==> (status == busy || next(status) == busy);
    }
}
