MODULE main

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

INVAR
	!_fail

VAR
	_trans : 1..8;
	_terminate : boolean;
	_fail : boolean;
	num_of_messages : -100..100;
	num_of_recv_messages : -100..100;
	message_exists : boolean;
	ack_exists : boolean;
	message_bit : boolean;
	ack_bit : boolean;
	send_bit : boolean;
	recv_bit : boolean;
	send_new_message : boolean;

ASSIGN
	_terminate := 0;

	_fail := case
			_terminate : 0;
			(((((((_trans=7)&!((ack_exists&((ack_bit!=send_bit)))))
			|((_trans=6)&!((ack_exists&((ack_bit=send_bit))))))|
			((_trans=5)&!(!send_new_message)))|
		((_trans=4)&!((((num_of_messages!=0))&(send_new_message)))))|
		((_trans=3)&!((message_exists&((message_bit=recv_bit))))))|
		((_trans=2)&!((message_exists&((message_bit!=recv_bit)))))) : 1;
			1 : 0;
		esac;

	init(num_of_messages) := 3;

	next(num_of_messages) := case
			(next(_trans)=8) : num_of_messages;
			((next(_trans)=4)&(num_of_messages>-100)) : 
							(num_of_messages - 1);
			1 : num_of_messages;
		esac;

	init(num_of_recv_messages) := 0;

	next(num_of_recv_messages) := case
			((next(_trans)=3)&(num_of_recv_messages<100)): 
						(num_of_recv_messages+1);
			(next(_trans)=1) : num_of_recv_messages;
			1 : num_of_recv_messages;
		esac;

	init(message_exists) := 0;

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

	init(ack_exists) := 0;

	next(ack_exists) := case
			(next(_trans)=7) : 0;
			(next(_trans)=6) : 0;
			(next(_trans)=3) : 1;
			(next(_trans)=2) : 1;
			1 : ack_exists;
		esac;

	next(message_bit) := case
			(next(_trans)=5) : send_bit;
			(next(_trans)=4) : send_bit;
			1 : message_bit;
		esac;

	next(ack_bit) := case
			(next(_trans)=3) : message_bit;
			(next(_trans)=2) : message_bit;
			1 : ack_bit;
		esac;

	init(send_bit) := 0;

	next(send_bit) := case
			(next(_trans)=6) : !send_bit;
			1 : send_bit;
		esac;

	init(recv_bit) := 0;

	next(recv_bit) := case
			(next(_trans)=3) : !recv_bit;
			1 : recv_bit;
		esac;

	init(send_new_message) := 1;

	next(send_new_message) := case
			(next(_trans)=6) : 1;
			(next(_trans)=4) : 0;
			1 : send_new_message;
		esac;