HOLD_PREVIOUS

VAR

buffer_filled: boolean INITVAL false;
buffer_empty: boolean INITVAL true;

MODULE PRODUCER(){

	VAR
	ready_to_produce: boolean INITVAL true;
	ready_to_deliver: boolean INITVAL false;

	TRANS PRODUCE:
		enable: ready_to_produce = true;
		assign: ready_to_produce' := false;
			ready_to_deliver' := true;

	TRANS DELIVER:
		enable: ((ready_to_deliver = true) /\ (buffer_empty = true));
		assign: ready_to_deliver' := false;
			buffer_empty' := false;
			ready_to_produce' := true;
			buffer_filled' := true;
}

MODULE CONSUMER(){

	VAR
	ready_to_remove: boolean INITVAL true;
	ready_to_consume: boolean INITVAL false;

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

MODULE SYSTEM(){

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