bool Fail = false;





proctype BUFFER() {
bool ready_to_produce = true;
bool ready_to_deliver = false;
bool a_buffer_cell_empty = true;
bool a_buffer_cell_filled = false;
bool b_buffer_cell_empty = true;
bool b_buffer_cell_filled = false;
bool ready_to_remove = true;
bool ready_to_consume = false;
do
  ::atomic{
    (ready_to_produce&&(!ready_to_deliver)) ->
    ready_to_produce = false;
    ready_to_deliver = true;
    };
  ::atomic{
    (ready_to_deliver&&a_buffer_cell_empty&&(!ready_to_produce)&&(!a_buffer_cell_filled)) ->
    ready_to_deliver = false;
    a_buffer_cell_empty = false;
    ready_to_produce = true;
    a_buffer_cell_filled = true;
    };
  ::atomic{
    (ready_to_deliver&&b_buffer_cell_empty&&(!ready_to_produce)&&(!b_buffer_cell_filled)) ->
    ready_to_deliver = false;
    b_buffer_cell_empty = false;
    ready_to_produce = true;
    b_buffer_cell_filled = true;
    };
  ::atomic{
    (a_buffer_cell_filled&&ready_to_remove&&(!ready_to_consume)&&(!a_buffer_cell_empty)) ->
    a_buffer_cell_filled = false;
    ready_to_remove = false;
    a_buffer_cell_empty = true;
    ready_to_consume = true;
    };
  ::atomic{
    (b_buffer_cell_filled&&ready_to_remove&&(!ready_to_consume)&&(!b_buffer_cell_empty)) ->
    b_buffer_cell_filled = false;
    ready_to_remove = false;
    b_buffer_cell_empty = true;
    ready_to_consume = true;
    };
  ::atomic{
    (ready_to_consume&&(!ready_to_remove)) ->
    ready_to_consume = false;
    ready_to_remove = true;
    };
od;
}

init {
 atomic{
 run BUFFER();
 };
}