bool Fail = false;
int buffer_size = 5;
int next_free_element = 0;
int next_occupied_element = 0;





proctype PRODUCER() {
do
  ::atomic{
    (((next_free_element+1)%buffer_size)==next_occupied_element) ->
    next_free_element = next_free_element;
    next_occupied_element = next_occupied_element;
    };
  ::atomic{
    (((next_free_element+1)%buffer_size)!=next_occupied_element) ->
    next_free_element = (next_free_element+1)%buffer_size;
    };
od;
}

proctype CONSUMER() {
do
  ::atomic{
    (next_free_element==next_occupied_element) ->
    next_free_element = next_free_element;
    next_occupied_element = next_occupied_element;
    };
  ::atomic{
    (next_free_element!=next_occupied_element) ->
    next_occupied_element = (next_occupied_element+1)%buffer_size;
    };
od;
}

init {
 atomic{
 run PRODUCER();
 run CONSUMER();
 };
}