```// non-repudiation protocol (with honest recipient) - turned-based game model
// 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)

tptg

// originator
player o
originator, [message]
endplayer

// recipient
player r
recipient, [req], [ack]
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; // max time to send a message

module originator

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

x : clock; // local clock

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

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

endmodule

module recipient

r : [0..2];
// 0 - requesting
// 1 - waiting for message
// 2 - sending ack

y : clock;

invariant
(r=0 => y<=0) &
(r=1 => true) &
(r=2 => y<=AD) // means has to send ack (honest)
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;

rewards "time"
true : 1;
endrewards
```