MODULE main
VAR
    request: boolean;
    status: {ready, busy};
ASSIGN
    init(status) := ready;
    next(status) := case
                        request: busy;
                        TRUE: {ready, busy};
                    esac;

LTLSPEC
    G(request -> F status=busy)
LTLSPEC
    G(request -> F status=ready)