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