MODULE main

TRANS (_trans=1)|(_trans=2)|(_trans=3)|(_trans=4)

INVAR
	!_fail

VAR
	_trans : 1..4;
	_terminate : boolean;
	_fail : boolean;
	ready_to_consume : boolean;
	ready_to_remove : boolean;
	ready_to_deliver : boolean;
	ready_to_produce : boolean;
	buffer_filled : boolean;
	buffer_empty : boolean;

ASSIGN
	_terminate := case
			!(((((buffer_filled=1))&((ready_to_remove=1))))|((ready_to_consume=1)|((ready_to_produce=1)|((((ready_to_deliver=1))&((buffer_empty=1))))))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			(((((_trans=4)&!((((ready_to_deliver=1))&((buffer_empty=1)))))|((_trans=3)&!(ready_to_produce=1)))|((_trans=2)&!(ready_to_consume=1)))|((_trans=1)&!((((buffer_filled=1))&((ready_to_remove=1)))))) : 1;
			1 : 0;
		esac;

	init(ready_to_consume) := 0;

	next(ready_to_consume) := case
			(next(_trans)=2) : 0;
			(next(_trans)=1) : 1;
			1 : ready_to_consume;
		esac;

	init(ready_to_remove) := 1;

	next(ready_to_remove) := case
			(next(_trans)=2) : 1;
			(next(_trans)=1) : 0;
			1 : ready_to_remove;
		esac;

	init(ready_to_deliver) := 0;

	next(ready_to_deliver) := case
			(next(_trans)=4) : 0;
			(next(_trans)=3) : 1;
			1 : ready_to_deliver;
		esac;

	init(ready_to_produce) := 1;

	next(ready_to_produce) := case
			(next(_trans)=4) : 1;
			(next(_trans)=3) : 0;
			1 : ready_to_produce;
		esac;

	init(buffer_filled) := 0;

	next(buffer_filled) := case
			(next(_trans)=4) : 1;
			(next(_trans)=1) : 0;
			1 : buffer_filled;
		esac;

	init(buffer_empty) := 1;

	next(buffer_empty) := case
			(next(_trans)=4) : 0;
			(next(_trans)=1) : 1;
			1 : buffer_empty;
		esac;