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;
	input : -100..100;
	output : boolean;
	current_state : { second_code_digit,first_code_digit,no_code_digit };

ASSIGN
	_terminate := case
			!(((((current_state=no_code_digit))&((input!=8))))|(((((input=8))&((current_state=no_code_digit))))|(((((current_state=first_code_digit))&((input!=0))))|(((((current_state=first_code_digit))&((input=0))))|(((((current_state=second_code_digit))&((input!=3))))|((((current_state=second_code_digit))&((input=3))))))))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			(((((((_trans=6)&!((((current_state=second_code_digit))&((input=3)))))|((_trans=5)&!((((current_state=second_code_digit))&((input!=3))))))|((_trans=4)&!((((current_state=first_code_digit))&((input=0))))))|((_trans=3)&!((((current_state=first_code_digit))&((input!=0))))))|((_trans=2)&!((((input=8))&((current_state=no_code_digit))))))|((_trans=1)&!((((current_state=no_code_digit))&((input!=8)))))) : 1;
			1 : 0;
		esac;

	next(input) := input;

	next(output) := case
			(next(_trans)=6) : 1;
			(next(_trans)=5) : 0;
			(next(_trans)=4) : 0;
			(next(_trans)=3) : 0;
			(next(_trans)=2) : 0;
			(next(_trans)=1) : 0;
			1 : output;
		esac;

	init(current_state) := no_code_digit;

	next(current_state) := case
			(next(_trans)=6) : no_code_digit;
			(next(_trans)=5) : no_code_digit;
			(next(_trans)=4) : second_code_digit;
			(next(_trans)=3) : no_code_digit;
			(next(_trans)=2) : first_code_digit;
			(next(_trans)=1) : no_code_digit;
			1 : current_state;
		esac;