MODULE main

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

INVAR
	!_fail

VAR
	_trans : 1..4;
	_terminate : boolean;
	_fail : boolean;
	can_change_shared_B : boolean;
	can_change_shared : boolean;
	shared : -100..100;
	x : -100..100;
	y : -100..100;
	z : boolean;

ASSIGN
	_terminate := case
			!(z|((!can_change_shared&can_change_shared_B)|
			(can_change_shared&!can_change_shared_B))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			(((((_trans=4)&!(can_change_shared&
			!can_change_shared_B))|((_trans=3)&
			!(!can_change_shared&can_change_shared_B)))|
			((_trans=2)&!z))|((_trans=1)&!z)) : 1;
			1 : 0;
		esac;

	init(can_change_shared_B) := 0;

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

	init(can_change_shared) := 1;

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

	init(shared) := 6;

	next(shared) := case
			((next(_trans)=4)&(shared<100)) : (shared+1);
			((next(_trans)=3)&(shared>-100)) : (shared - 1);
			1 : shared;
		esac;

	init(x) := 0;

	next(x) := case
			(next(_trans)=2) : 10;
			1 : x;
		esac;

	init(y) := 0;

	next(y) := case
			(next(_trans)=1) : 11;
			1 : y;
		esac;

	init(z) := 1;

	next(z) := z;