const
	MININT	:	-32768;
	MAXINT	:	32767;
var
	next_occupied_element	:	MININT..MAXINT;
	next_free_element	:	MININT..MAXINT;
	buffer_size	:	MININT..MAXINT;

Rule "PRODUCE"
(((next_free_element + 1) % buffer_size)!=next_occupied_element)
==>
begin
  next_free_element:=(next_free_element + 1) % buffer_size;
end;

Rule "PRODUCER_WAIT"
(((next_free_element + 1) % buffer_size)=next_occupied_element)
==>
begin
  next_free_element:=next_free_element;
  next_occupied_element:=next_occupied_element;
end;

Rule "CONSUMER_WAIT"
(next_free_element=next_occupied_element)
==>
begin
  next_free_element:=next_free_element;
  next_occupied_element:=next_occupied_element;
end;

Rule "CONSUME"
(next_free_element!=next_occupied_element)
==>
begin
  next_occupied_element:=(next_occupied_element + 1) % buffer_size;
end;

startstate
begin
  buffer_size:=5;
  next_free_element:=0;
  next_occupied_element:=0;
end;