MODULE main

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

INVAR
	!_fail

VAR
	_trans : 1..4;
	_terminate : boolean;
	_fail : boolean;
	buffer_size : -100..100;
	next_free_element : -100..100;
	next_occupied_element : -100..100;

ASSIGN
	_terminate := case
			!(((next_free_element!=next_occupied_element))|(((next_free_element=next_occupied_element))|(((((((next_free_element+1)) mod buffer_size))=next_occupied_element))|((((((next_free_element+1)) mod buffer_size))!=next_occupied_element))))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			(((((_trans=4)&!((((((next_free_element+1)) mod buffer_size))!=next_occupied_element)))|((_trans=3)&!((((((next_free_element+1)) mod buffer_size))=next_occupied_element))))|((_trans=2)&!((next_free_element=next_occupied_element))))|((_trans=1)&!((next_free_element!=next_occupied_element)))) : 1;
			1 : 0;
		esac;

	init(buffer_size) := 5;

	next(buffer_size) := buffer_size;

	init(next_free_element) := 0;

	next(next_free_element) := case
			(next(_trans)=4) : (((next_free_element+1)) mod buffer_size);
			(next(_trans)=3) : next_free_element;
			(next(_trans)=2) : next_free_element;
			1 : next_free_element;
		esac;

	init(next_occupied_element) := 0;

	next(next_occupied_element) := case
			(next(_trans)=3) : next_occupied_element;
			(next(_trans)=2) : next_occupied_element;
			(next(_trans)=1) : (((next_occupied_element+1)) mod buffer_size);
			1 : next_occupied_element;
		esac;