mtype = { ready, busy };
#define T#SYSTEM#state mtype

bool Fail = false;





proctype v#SYSTEM#state(T#SYSTEM#state state; bool request) {
bool __init = true;
do
  ::atomic{
    __init ->
    __init = false;
    state = ready;
    };
  ::atomic{
    !__init&&(state==ready&&request) ->
    state = busy;
    };
  ::atomic{
    !__init&&!(state==ready&&request) ->
    state = ready;
    };
od;
}

init {
bool request;
    if
      ::request = true;
      ::request = false;
    fi;


T#SYSTEM#state state;
    if
      ::state = ready;
      ::state = busy;
    fi;


 atomic{
 run v#SYSTEM#state(state,request);
 };
}