module main {

    var request : boolean;
    var status : enum { ready, busy };

    init {
        status = ready;
    }

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

    property eventually_busy_if_request {
        var t : boolean;
        t = false;
        t = request;
        eventually(t);
    }
}
