mtype = { idle, entering, critical, exiting };
#define state mtype

bool Fail = false;
bool semaphore = false;





proctype USER_0() {
state user_state = idle;
do
  ::atomic{
    user_state==idle ->
    if
      ::user_state = idle;
      ::user_state = entering;
    fi;

    };
  ::atomic{
    ((user_state==entering)&&(!semaphore)) ->
    user_state = critical;
    semaphore = true;
    };
  ::atomic{
    ((user_state==entering)&&(semaphore)) ->
    user_state = entering;
    };
  ::atomic{
    user_state==critical ->
    if
      ::user_state = critical;
      ::user_state = exiting;
    fi;

    };
  ::atomic{
    user_state==exiting ->
    user_state = idle;
    semaphore = false;
    };
od;
}

proctype USER_1() {
state user_state = idle;
do
  ::atomic{
    user_state==idle ->
    if
      ::user_state = idle;
      ::user_state = entering;
    fi;

    };
  ::atomic{
    ((user_state==entering)&&(!semaphore)) ->
    user_state = critical;
    semaphore = true;
    };
  ::atomic{
    ((user_state==entering)&&(semaphore)) ->
    user_state = entering;
    };
  ::atomic{
    user_state==critical ->
    if
      ::user_state = critical;
      ::user_state = exiting;
    fi;

    };
  ::atomic{
    user_state==exiting ->
    user_state = idle;
    semaphore = false;
    };
od;
}

init {
 atomic{
 run USER_0();
 run USER_1();
 };
}