MODULE main

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

INVAR
	!_fail

VAR
	_trans : 1..6;
	_terminate : boolean;
	_fail : boolean;
	ready_to_consume : boolean;
	ready_to_remove : boolean;
	b_buffer_cell_filled : boolean;
	b_buffer_cell_empty : boolean;
	a_buffer_cell_filled : boolean;
	a_buffer_cell_empty : boolean;
	ready_to_deliver : boolean;
	ready_to_produce : boolean;

ASSIGN
	_terminate := case
			!(((ready_to_produce&(!ready_to_deliver)))|(((((ready_to_deliver&a_buffer_cell_empty)&(!ready_to_produce))&(!a_buffer_cell_filled)))|(((((ready_to_deliver&b_buffer_cell_empty)&(!ready_to_produce))&(!b_buffer_cell_filled)))|(((((a_buffer_cell_filled&ready_to_remove)&(!ready_to_consume))&(!a_buffer_cell_empty)))|(((((b_buffer_cell_filled&ready_to_remove)&(!ready_to_consume))&(!b_buffer_cell_empty)))|((ready_to_consume&(!ready_to_remove)))))))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			(((((((_trans=6)&!((ready_to_consume&(!ready_to_remove))))|((_trans=5)&!((((b_buffer_cell_filled&ready_to_remove)&(!ready_to_consume))&(!b_buffer_cell_empty)))))|((_trans=4)&!((((a_buffer_cell_filled&ready_to_remove)&(!ready_to_consume))&(!a_buffer_cell_empty)))))|((_trans=3)&!((((ready_to_deliver&b_buffer_cell_empty)&(!ready_to_produce))&(!b_buffer_cell_filled)))))|((_trans=2)&!((((ready_to_deliver&a_buffer_cell_empty)&(!ready_to_produce))&(!a_buffer_cell_filled)))))|((_trans=1)&!((ready_to_produce&(!ready_to_deliver))))) : 1;
			1 : 0;
		esac;

	init(ready_to_consume) := 0;

	next(ready_to_consume) := case
			(next(_trans)=6) : 0;
			(next(_trans)=5) : 1;
			(next(_trans)=4) : 1;
			1 : ready_to_consume;
		esac;

	init(ready_to_remove) := 1;

	next(ready_to_remove) := case
			(next(_trans)=6) : 1;
			(next(_trans)=5) : 0;
			(next(_trans)=4) : 0;
			1 : ready_to_remove;
		esac;

	init(b_buffer_cell_filled) := 0;

	next(b_buffer_cell_filled) := case
			(next(_trans)=5) : 0;
			(next(_trans)=3) : 1;
			1 : b_buffer_cell_filled;
		esac;

	init(b_buffer_cell_empty) := 1;

	next(b_buffer_cell_empty) := case
			(next(_trans)=5) : 1;
			(next(_trans)=3) : 0;
			1 : b_buffer_cell_empty;
		esac;

	init(a_buffer_cell_filled) := 0;

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

	init(a_buffer_cell_empty) := 1;

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

	init(ready_to_deliver) := 0;

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

	init(ready_to_produce) := 1;

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