// 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

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 message 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..5];
	// 0 - requesting
	// 1 - waiting for message
	// 2 - sending ack
	// 3 - decoding
	// 4 - sending ack after decoding
	// 5 - decoded and has complete message

	y : 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); // decode
	
	// decoding (last and not last)
	[] r=3 & y>=8 -> p : (r'=5) & (y'=0) + (1-p) : (r'=4) & (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=4 -> (r'=1) & (y'=0);

endmodule

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

rewards "time"	
	true : 1;
endrewards