HOLD_PREVIOUS

MODULE SYSTEM(){
	BUFFER()
}

MODULE BUFFER(){
	VAR
	
	ready_to_produce: boolean INITVAL true;
	ready_to_deliver: boolean INITVAL false;
	a_buffer_cell_empty: boolean INITVAL true;
	a_buffer_cell_filled: boolean INITVAL false;
	b_buffer_cell_empty: boolean INITVAL true;
	b_buffer_cell_filled: boolean INITVAL false;
	ready_to_remove: boolean INITVAL true;
	ready_to_consume: boolean INITVAL false;

	TRANS PRODUCE:
		enable: (ready_to_produce /\ (!ready_to_deliver));
		assign: ready_to_produce' := false;
			ready_to_deliver' := true;

	TRANS DELIVER_TO_FIRST_BUFFER:
		enable: (ready_to_deliver /\ a_buffer_cell_empty /\ (!ready_to_produce) /\
(!a_buffer_cell_filled));
		assign: ready_to_deliver' := false;
			a_buffer_cell_empty' := false;
			ready_to_produce' := true;
			a_buffer_cell_filled' := true;

	TRANS DELIVER_TO_SECOND_BUFFER:
		enable: (ready_to_deliver /\ b_buffer_cell_empty /\(!ready_to_produce) /\ (!b_buffer_cell_filled));
		assign: ready_to_deliver' := false;
			b_buffer_cell_empty' := false;
			ready_to_produce' := true;
			b_buffer_cell_filled' := true;

	TRANS REMOVE_FROM_FIRST_BUFFER:
		enable: (a_buffer_cell_filled /\ ready_to_remove /\(!ready_to_consume) /\ (!a_buffer_cell_empty));
		assign: a_buffer_cell_filled' := false;
			ready_to_remove' := false;
			a_buffer_cell_empty' := true;
			ready_to_consume' := true;

	TRANS REMOVE_FROM_SECOND_BUFFER:
		enable: (b_buffer_cell_filled /\ ready_to_remove /\(!ready_to_consume) /\ (!b_buffer_cell_empty));
		assign: b_buffer_cell_filled' := false;
			ready_to_remove' := false;
			b_buffer_cell_empty' := true;
			ready_to_consume' := true;

	TRANS CONSUME:
		enable: (ready_to_consume /\ (!ready_to_remove));
		assign: ready_to_consume' := false;
			ready_to_remove' := true;
}