HOLD_PREVIOUS

VAR

buffer_size: integer INITVAL 5;
next_free_element: integer INITVAL 0;   -- index of the next free element in the buffer
next_occupied_element: integer INITVAL 0; -- index of the next occupied element in the buffer


MODULE PRODUCER(){

	TRANS PRODUCER_WAIT:		-- while buffer is full , wait
		enable: (((next_free_element + 1)%buffer_size)=next_occupied_element);
		assign: next_free_element' := next_free_element;
			next_occupied_element' := next_occupied_element;

	TRANS PRODUCE:
		enable: (((next_free_element + 1)%buffer_size)!=next_occupied_element);
		assign: next_free_element' := (next_free_element + 1) % buffer_size;
}

MODULE CONSUMER(){

	TRANS CONSUMER_WAIT:		-- while buffer is empty , wait
		enable: (next_free_element = next_occupied_element);
		assign: next_free_element' := next_free_element;
			next_occupied_element' := next_occupied_element;

	TRANS CONSUME:
		enable: (next_free_element != next_occupied_element);
		assign: next_occupied_element' := (next_occupied_element + 1) % buffer_size;
}

MODULE SYSTEM(){

	(PRODUCER() ||| CONSUMER())
}