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

T#user#state global_state_1;
T#user#state global_state_0;
bool global_semaphore_0;
bool Fail = false;

chan q_1 = [0] of {bit};
chan q_2 = [0] of {bit};




proctype v#SYSTEM#semaphore() {
bool __init = true;
do
  ::atomic{
    __init ->
    __init = false;
    global_semaphore_0 = 0;
    };
  ::atomic{
    !__init ->
    global_semaphore_0 = false;
    };
od;
}

proctype v#user#state_0() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_1?0;
    __init = false;
    global_state_0 = idle;
    q_1?1;
    };
  ::atomic{
    !__init&&(global_state_0==idle) ->
    q_1?0;
    global_state_0 = idle;
    q_1?1;
    };
  ::atomic{
    !__init&&!(global_state_0==idle)&&(global_state_0==entering&&!global_semaphore_0) ->
    q_1?0;
    global_state_0 = critical;
    q_1?1;
    };
  ::atomic{
    !__init&&!(global_state_0==idle)&&!(global_state_0==entering&&!global_semaphore_0)&&(global_state_0==critical) ->
    q_1?0;
    global_state_0 = critical;
    q_1?1;
    };
  ::atomic{
    !__init&&!(global_state_0==idle)&&!(global_state_0==entering&&!global_semaphore_0)&&!(global_state_0==critical)&&(global_state_0==exiting) ->
    q_1?0;
    global_state_0 = idle;
    q_1?1;
    };
  ::atomic{
    !__init&&!(global_state_0==idle)&&!(global_state_0==entering&&!global_semaphore_0)&&!(global_state_0==critical)&&!(global_state_0==exiting) ->
    q_1?0;
    global_state_0 = global_state_0;
    q_1?1;
    };
od;
}

proctype v#user#semaphore_0() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_1!0;
    __init = false;
    global_semaphore_0 = false;
    q_1!1;
    };
  ::atomic{
    !__init&&(global_state_0==entering) ->
    q_1!0;
    global_semaphore_0 = 1;
    q_1!1;
    };
  ::atomic{
    !__init&&!(global_state_0==entering)&&(global_state_0==exiting) ->
    q_1!0;
    global_semaphore_0 = 0;
    q_1!1;
    };
  ::atomic{
    !__init&&!(global_state_0==entering)&&!(global_state_0==exiting) ->
    q_1!0;
    global_semaphore_0 = global_semaphore_0;
    q_1!1;
    };
od;
}

proctype user_0() {
 atomic{
 run v#user#state_0();
 run v#user#semaphore_0();
 };
}

proctype v#user#state_1() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_2?0;
    __init = false;
    global_state_1 = idle;
    q_2?1;
    };
  ::atomic{
    !__init&&(global_state_1==idle) ->
    q_2?0;
    global_state_1 = idle;
    q_2?1;
    };
  ::atomic{
    !__init&&!(global_state_1==idle)&&(global_state_1==entering&&!global_semaphore_0) ->
    q_2?0;
    global_state_1 = critical;
    q_2?1;
    };
  ::atomic{
    !__init&&!(global_state_1==idle)&&!(global_state_1==entering&&!global_semaphore_0)&&(global_state_1==critical) ->
    q_2?0;
    global_state_1 = critical;
    q_2?1;
    };
  ::atomic{
    !__init&&!(global_state_1==idle)&&!(global_state_1==entering&&!global_semaphore_0)&&!(global_state_1==critical)&&(global_state_1==exiting) ->
    q_2?0;
    global_state_1 = idle;
    q_2?1;
    };
  ::atomic{
    !__init&&!(global_state_1==idle)&&!(global_state_1==entering&&!global_semaphore_0)&&!(global_state_1==critical)&&!(global_state_1==exiting) ->
    q_2?0;
    global_state_1 = global_state_1;
    q_2?1;
    };
od;
}

proctype v#user#semaphore_1() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_2!0;
    __init = false;
    global_semaphore_0 = false;
    q_2!1;
    };
  ::atomic{
    !__init&&(global_state_1==entering) ->
    q_2!0;
    global_semaphore_0 = 1;
    q_2!1;
    };
  ::atomic{
    !__init&&!(global_state_1==entering)&&(global_state_1==exiting) ->
    q_2!0;
    global_semaphore_0 = 0;
    q_2!1;
    };
  ::atomic{
    !__init&&!(global_state_1==entering)&&!(global_state_1==exiting) ->
    q_2!0;
    global_semaphore_0 = global_semaphore_0;
    q_2!1;
    };
od;
}

proctype user_1() {
 atomic{
 run v#user#state_1();
 run v#user#semaphore_1();
 };
}

init {
    if
      ::global_state_1 = idle;
      ::global_state_1 = entering;
      ::global_state_1 = critical;
      ::global_state_1 = exiting;
    fi;


    if
      ::global_state_0 = idle;
      ::global_state_0 = entering;
      ::global_state_0 = critical;
      ::global_state_0 = exiting;
    fi;


    if
      ::global_semaphore_0 = true;
      ::global_semaphore_0 = false;
    fi;


 atomic{
 run v#SYSTEM#semaphore();
 run user_0();
 run user_1();
 };
}