MODULE main

TRANS (_trans=1)|(_trans=2)|(_trans=3)|(_trans=4)|(_trans=5)|(_trans=6)|(_trans=7)|(_trans=8)|(_trans=9)|(_trans=10)

INVAR
	!_fail

VAR
	_trans : 1..10;
	_terminate : boolean;
	_fail : boolean;
	user_state_USER : { exiting,critical,entering,idle };
	user_state : { exiting,critical,entering,idle };
	semaphore : boolean;

ASSIGN
	_terminate := case
			!((user_state_USER=exiting)|((user_state_USER=critical)|(((((user_state_USER=entering))&((semaphore=1))))|(((((user_state_USER=entering))&((semaphore=0))))|((user_state_USER=idle)|((user_state=idle)|(((((user_state=entering))&((semaphore=0))))|(((((user_state=entering))&((semaphore=1))))|((user_state=critical)|(user_state=exiting)))))))))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			(((((((((((_trans=10)&!(user_state=exiting))|((_trans=9)&!(user_state=critical)))|((_trans=8)&!((((user_state=entering))&((semaphore=1))))))|((_trans=7)&!((((user_state=entering))&((semaphore=0))))))|((_trans=6)&!(user_state=idle)))|((_trans=5)&!(user_state_USER=idle)))|((_trans=4)&!((((user_state_USER=entering))&((semaphore=0))))))|((_trans=3)&!((((user_state_USER=entering))&((semaphore=1))))))|((_trans=2)&!(user_state_USER=critical)))|((_trans=1)&!(user_state_USER=exiting))) : 1;
			1 : 0;
		esac;

	init(user_state_USER) := idle;

	next(user_state_USER) := case
			(next(_trans)=5) : { idle,entering };
			(next(_trans)=4) : critical;
			(next(_trans)=3) : entering;
			(next(_trans)=2) : { critical,exiting };
			(next(_trans)=1) : idle;
			1 : user_state_USER;
		esac;

	init(user_state) := idle;

	next(user_state) := case
			(next(_trans)=10) : idle;
			(next(_trans)=9) : { critical,exiting };
			(next(_trans)=8) : entering;
			(next(_trans)=7) : critical;
			(next(_trans)=6) : { idle,entering };
			1 : user_state;
		esac;

	init(semaphore) := 0;

	next(semaphore) := case
			(next(_trans)=10) : 0;
			(next(_trans)=7) : 1;
			(next(_trans)=4) : 1;
			(next(_trans)=1) : 0;
			1 : semaphore;
		esac;