const int DECODE1=8; // time to decode correctly
const int DECODE2=4; // time to decode probabilistically

module malicious_recipient

	r : [0..6];
	// 0 - request
	// 1 - wait
	// 2 - ack
	// 3 - try to decode correctly
	// 4 - try to decode quickly (probabilistically)
	// 5 - decode correctly
	// 6 - failed to decode or decoded and not last

	y : clock;

	invariant
		(r=0 => y<=0) &
		(r=1 => true) &
		(r=2 => true) &
		(r=3 => y<=DECODE1) &
		(r=4 => y<=DECODE2) &
		(r=5 => true) &
		(r=6 => 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 correctly
	[] r=2 -> (r'=4) & (y'=0); // try and decode fast
	[] r=3 & y>=DECODE1 -> p : (r'=5) & (y'=0) // decode and last
	                 + (1-p) : (r'=6) & (y'=0); // decode and not last
	[] r=4 & y>=DECODE2 -> p*0.25 : (r'=5) & (y'=0) // decode and last
	                 + (1-p)*0.25 : (r'=6) & (y'=0) // decode and not last 
	                       + 0.75 : (r'=6) & (y'=0); // fail to decode

	// decoded and not last (continue by sending ack)
	// could combine with location 2, but would have the opportunity of decoding again 
	// which is obviously a stupid thing to do so keep separate
	[ack] r=6 -> (r'=1) & (y'=0);

endmodule

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