var
	ready_to_produce	:	BOOLEAN;
	ready_to_deliver	:	BOOLEAN;
	a_buffer_cell_empty	:	BOOLEAN;
	a_buffer_cell_filled	:	BOOLEAN;
	b_buffer_cell_empty	:	BOOLEAN;
	b_buffer_cell_filled	:	BOOLEAN;
	ready_to_remove	:	BOOLEAN;
	ready_to_consume	:	BOOLEAN;

Rule "CONSUME"
(ready_to_consume & (!ready_to_remove))
==>
begin
  ready_to_consume:=FALSE;
  ready_to_remove:=TRUE;
end;

Rule "REMOVE_FROM_SECOND_BUFFER"
(b_buffer_cell_filled & ready_to_remove & (!ready_to_consume) & (!b_buffer_cell_empty))
==>
begin
  b_buffer_cell_filled:=FALSE;
  ready_to_remove:=FALSE;
  b_buffer_cell_empty:=TRUE;
  ready_to_consume:=TRUE;
end;

Rule "REMOVE_FROM_FIRST_BUFFER"
(a_buffer_cell_filled & ready_to_remove & (!ready_to_consume) & (!a_buffer_cell_empty))
==>
begin
  a_buffer_cell_filled:=FALSE;
  ready_to_remove:=FALSE;
  a_buffer_cell_empty:=TRUE;
  ready_to_consume:=TRUE;
end;

Rule "DELIVER_TO_SECOND_BUFFER"
(ready_to_deliver & b_buffer_cell_empty & (!ready_to_produce) & (!b_buffer_cell_filled))
==>
begin
  ready_to_deliver:=FALSE;
  b_buffer_cell_empty:=FALSE;
  ready_to_produce:=TRUE;
  b_buffer_cell_filled:=TRUE;
end;

Rule "DELIVER_TO_FIRST_BUFFER"
(ready_to_deliver & a_buffer_cell_empty & (!ready_to_produce) & (!a_buffer_cell_filled))
==>
begin
  ready_to_deliver:=FALSE;
  a_buffer_cell_empty:=FALSE;
  ready_to_produce:=TRUE;
  a_buffer_cell_filled:=TRUE;
end;

Rule "PRODUCE"
(ready_to_produce & (!ready_to_deliver))
==>
begin
  ready_to_produce:=FALSE;
  ready_to_deliver:=TRUE;
end;

startstate
begin
  ready_to_consume:=FALSE;
  ready_to_remove:=TRUE;
  b_buffer_cell_filled:=FALSE;
  b_buffer_cell_empty:=TRUE;
  a_buffer_cell_filled:=FALSE;
  a_buffer_cell_empty:=TRUE;
  ready_to_deliver:=FALSE;
  ready_to_produce:=TRUE;
end;