MODULE main

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

INVAR
	!_fail

VAR
	_trans : 1..3;
	_terminate : boolean;
	_fail : boolean;
	input : boolean;
	output : boolean;
	current_state : 0..7;

ASSIGN
	_terminate := case
			!((input=0)|(((((input=1))&((current_state!=7))))|((((input=1))&((current_state=7)))))) : 1;
			1 : 0;
		esac;

	_fail := case
			_terminate : 0;
			((((_trans=3)&!((((input=1))&((current_state=7)))))|((_trans=2)&!((((input=1))&((current_state!=7))))))|((_trans=1)&!(input=0))) : 1;
			1 : 0;
		esac;

	next(input) := input;

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

	init(current_state) := 0;

	next(current_state) := case
			(next(_trans)=3) : 0;
			((next(_trans)=2)&(current_state<7)) : (current_state+1);
			1 : current_state;
		esac;