// 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]
// honest recipient

pta

/// need to generate geometric distribution on the fly i.e. the value of n (the number of messages sent)
// as otherwise the recipient would have too much information - could use the value of n and 
// win with probability 1
// really motivation for partially observable adversaries, but this fixes the problem
// an alternative would be to make the adversary to make all its choices in advance
// but this would be more complicated

// possible changes/extensions:

// add a delay for the time to send a message from the originator
// or can we suppose the originator sends its message immediately?

// increase/vary the delays - can use this to show they do not influence zone based
// and how to use scaling to approximate for digital clocks

// note to self: the correctness of boundary region graph/corner based abstraction points
// to the fact it should be feasible to extend the digital clocks approach to deal with strict bounds

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

module originator

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

	x : clock;

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

	// init
	[req] o=0 -> (o'=1) & (x'=0); // receive a request from the recipient
	
	// send
	[message] o=1 & x<=0 -> (o'=2); // send first message immediately
	
	// waiting
	[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 honest_recipient

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

	y : 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;