// non-repudiation protocol (with honest recipient) 
// Markowitch & Roggeman [MR99]
// extended version of the PTA model from
// R. Lanotte, A. Maggiolo-Schettini and A. Troina
// Second Workshop Quantitative Aspects of Programming Languages (QAPL 2004), 
// ENTCS, vol. 112, pp. 113–129 (2005)

pta

// constants
const double p; // parameter of geometric distribution (to generate 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)

module originator

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

	x : clock; // local clock

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

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

module recipient

	r : [0..2];
	// 0 - request
	// 1 - wait
	// 2 - ack

	y : clock; // local clock

	invariant
		(r=0 => y<=0) &
		(r=1 => true) &
		(r=2 => y<AD)
	endinvariant

	[req] r=0 & y=0 -> (r'=1); // initiate protocol
	[message] r=1 -> (r'=2) & (y'=0); // receive message
	[ack] r=2 & y>=ad -> (r'=1) & (y'=0); // send ack (which it always does)

endmodule

// received ack for final message sent
label "terminated_successfully" = o=3;