// non-repudiation protocol (with malicious recipient) Markowitch & Roggeman [MR99]
// extension and modification of the PTA model from 
// R. Lanotte, A. Maggiolo-Schettini and A. Troina [LMT05]
// malicious recipient can stop early and has a probabilistic decoder

tptg

// originator
player o
  originator, [message]
endplayer

// recipient
player r
  recipient, [req], [ack], [end]
endplayer

// constants
const double p; // parameter of geometric distribution (choose number of messages)
const int ad = 1; // min time to send an ack
const int AD = 5; // deadline (if ack not arrived then end protocol)
const int md = 2; // min time to send a message
const int MD = 9; // deadline (if ack not arrived then end protocol)

module originator

	o : [0..4];
	// 0 - init
	// 1 - sending
	// 2 - waiting
	// 3 - finished
	// 4 - error

	x : clock;

	invariant
		(o=0 => true) &
		(o=1 => x<=MD) &
		(o=2 => x<=AD) &
		(o=3 => true) &
		(o=4 => true)
	endinvariant

	[req] o=0 -> (o'=1) & (x'=0); // receive a request from the recipient
	[message] o=1 & x>=md -> (o'=2) & (x'=0); // send message
	[ack] o=2 & x<=AD -> 1-p : (o'=1) & (x'=0)  // receive an ack and not last
	                      + p : (o'=3) & (x'=0); // receive an ack and last
	[end] o=2 & x>=AD -> (o'=4) & (x'=0); // ack not arrived within expected interval (stop)
	
endmodule

module recipient

	r : [0..6];
	// 0 - requesting
	// 1 - waiting for message
	// 2 - sending ack
	// 4 - decoding probabilistically but fast
	// 5 - decoding correctly
	// 6 - sending ack after decoding
	// 7 - decoded and has complete message

	y : clock;

	invariant
		(r=0 => y<=0) &
		(r=1 => true) &
		(r=2 => true) &
		(r=3 => y<=5) &
		(r=4 => y<=10) &
		(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); // decode probabilistically
	[] r=2 -> (r'=4) & (y'=0); // decode
	
	// decoding probabilistically (successfully and last, successfully and not last or unsuccessfully)
	[] r=3 & y>=4 -> p*0.25 : (r'=6) & (y'=0) + (1-p)*0.25 : (r'=5) & (y'=0) + 0.75 : (r'=2) & (y'=0);
	// decoding (last and not last)
	[] r=4 & y>=8 -> p : (r'=6) & (y'=0) + (1-p) : (r'=5) & (y'=0);

	// 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=5 -> (r'=1) & (y'=0);

endmodule

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

rewards "time"	
	true : 1;
endrewards