bool global_ready_to_consume_0;
bool global_ready_to_remove_0;
bool global_buffer_empty_0;
bool global_buffer_filled_0;
bool global_ready_to_deliver_0;
bool global_ready_to_produce_0;
bool Fail = false;

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




proctype v#SYSTEM#ready_to_produce() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_0?0;
    q_1?0;
    q_2?0;
    q_3?0;
    q_4?0;
    __init = false;
    global_ready_to_produce_0 = 1;
    q_0?1;
    q_1?1;
    q_2?1;
    q_3?1;
    q_4?1;
    };
  ::atomic{
    !__init&&(global_ready_to_produce_0&&!global_ready_to_deliver_0) ->
    q_0?0;
    q_1?0;
    q_2?0;
    q_3?0;
    q_4?0;
    global_ready_to_produce_0 = 0;
    q_0?1;
    q_1?1;
    q_2?1;
    q_3?1;
    q_4?1;
    };
  ::atomic{
    !__init&&!(global_ready_to_produce_0&&!global_ready_to_deliver_0)&&(global_ready_to_deliver_0&&global_buffer_empty_0&&!global_ready_to_produce_0&&!global_buffer_filled_0) ->
    q_0?0;
    q_1?0;
    q_2?0;
    q_3?0;
    q_4?0;
    global_ready_to_produce_0 = 1;
    q_0?1;
    q_1?1;
    q_2?1;
    q_3?1;
    q_4?1;
    };
od;
}

proctype v#SYSTEM#ready_to_deliver() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_0!0;
    __init = false;
    global_ready_to_deliver_0 = 0;
    q_0!1;
    };
  ::atomic{
    !__init&&(global_ready_to_deliver_0&&global_buffer_empty_0&&!global_ready_to_produce_0&&!global_buffer_filled_0) ->
    q_0!0;
    global_ready_to_deliver_0 = 0;
    q_0!1;
    };
  ::atomic{
    !__init&&!(global_ready_to_deliver_0&&global_buffer_empty_0&&!global_ready_to_produce_0&&!global_buffer_filled_0)&&(global_ready_to_produce_0&&!global_ready_to_deliver_0) ->
    q_0!0;
    global_ready_to_deliver_0 = 1;
    q_0!1;
    };
od;
}

proctype v#SYSTEM#buffer_filled() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_1!0;
    __init = false;
    global_buffer_filled_0 = 0;
    q_1!1;
    };
  ::atomic{
    !__init&&(global_buffer_filled_0&&global_ready_to_remove_0&&!global_buffer_empty_0&&!global_ready_to_consume_0) ->
    q_1!0;
    global_buffer_filled_0 = 0;
    q_1!1;
    };
  ::atomic{
    !__init&&!(global_buffer_filled_0&&global_ready_to_remove_0&&!global_buffer_empty_0&&!global_ready_to_consume_0)&&(global_ready_to_deliver_0&&global_buffer_empty_0&&!global_ready_to_produce_0&&!global_buffer_filled_0) ->
    q_1!0;
    global_buffer_filled_0 = 1;
    q_1!1;
    };
od;
}

proctype v#SYSTEM#buffer_empty() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_2!0;
    __init = false;
    global_buffer_empty_0 = 1;
    q_2!1;
    };
  ::atomic{
    !__init&&(global_ready_to_deliver_0&&global_buffer_empty_0&&!global_ready_to_produce_0&&!global_buffer_filled_0) ->
    q_2!0;
    global_buffer_empty_0 = 0;
    q_2!1;
    };
  ::atomic{
    !__init&&!(global_ready_to_deliver_0&&global_buffer_empty_0&&!global_ready_to_produce_0&&!global_buffer_filled_0)&&(global_buffer_filled_0&&global_ready_to_remove_0&&!global_buffer_empty_0&&!global_ready_to_consume_0) ->
    q_2!0;
    global_buffer_empty_0 = 1;
    q_2!1;
    };
od;
}

proctype v#SYSTEM#ready_to_remove() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_3!0;
    __init = false;
    global_ready_to_remove_0 = 1;
    q_3!1;
    };
  ::atomic{
    !__init&&(global_buffer_filled_0&&global_ready_to_remove_0&&!global_buffer_empty_0&&!global_ready_to_consume_0) ->
    q_3!0;
    global_ready_to_remove_0 = 0;
    q_3!1;
    };
  ::atomic{
    !__init&&!(global_buffer_filled_0&&global_ready_to_remove_0&&!global_buffer_empty_0&&!global_ready_to_consume_0)&&(global_ready_to_consume_0&&!global_ready_to_remove_0) ->
    q_3!0;
    global_ready_to_remove_0 = 1;
    q_3!1;
    };
od;
}

proctype v#SYSTEM#ready_to_consume() {
bool __init = true;
do
  ::atomic{
    __init ->
    q_4!0;
    __init = false;
    global_ready_to_consume_0 = 0;
    q_4!1;
    };
  ::atomic{
    !__init&&(global_ready_to_consume_0&&!global_ready_to_remove_0) ->
    q_4!0;
    global_ready_to_consume_0 = 0;
    q_4!1;
    };
  ::atomic{
    !__init&&!(global_ready_to_consume_0&&!global_ready_to_remove_0)&&(global_buffer_filled_0&&global_ready_to_remove_0&&!global_buffer_empty_0&&!global_ready_to_consume_0) ->
    q_4!0;
    global_ready_to_consume_0 = 1;
    q_4!1;
    };
od;
}

init {
    if
      ::global_ready_to_consume_0 = true;
      ::global_ready_to_consume_0 = false;
    fi;


    if
      ::global_ready_to_remove_0 = true;
      ::global_ready_to_remove_0 = false;
    fi;


    if
      ::global_buffer_empty_0 = true;
      ::global_buffer_empty_0 = false;
    fi;


    if
      ::global_buffer_filled_0 = true;
      ::global_buffer_filled_0 = false;
    fi;


    if
      ::global_ready_to_deliver_0 = true;
      ::global_ready_to_deliver_0 = false;
    fi;


    if
      ::global_ready_to_produce_0 = true;
      ::global_ready_to_produce_0 = false;
    fi;


 atomic{
 run v#SYSTEM#ready_to_produce();
 run v#SYSTEM#ready_to_deliver();
 run v#SYSTEM#buffer_filled();
 run v#SYSTEM#buffer_empty();
 run v#SYSTEM#ready_to_remove();
 run v#SYSTEM#ready_to_consume();
 };
}