const int DECODE=8; // time to decode

module malicious_recipient

	r : [0..5];
	// 0 - request
	// 1 - wait
	// 2 - ack
	// 3 - try to decode
	// 4 - gains information (message was last)
	// 5 - does not gain information (message not last)

	y : clock; // local clock

	invariant
		(r=0 => y<=0) &
		(r=1 => true) &
		(r=2 => true) &
		(r=3 => y<=10) &
		(r=4 => true) &
		(r=5 => true)
	endinvariant

	[req] r=0 & y=0 -> (r'=1); // initiate protocol
	[message] r=1 -> (r'=2) & (y'=0); // receive message
	[ack] r=2 -> (r'=1); // send ack (no time bound now as malicious)
	[] r=2 -> (r'=3) & (y'=0); // try and decode
	[] r=3 & y>=DECODE -> p : (r'=4) & (y'=0) // decode and last
	                + (1-p) : (r'=5) & (y'=0); // decode and not last
	[ack] r=5 -> (r'=1) & (y'=0); // unsuccessful so try and continue

endmodule

// decodes last (nth) message
label "gains_information" = r=4;