popta
observables
last, r, mess, ack, o, x, y
endobservables
const K;
const int ad = 1;
const int AD = 4;
module originator
o : [0..4];
N : [0..K];
ack : [0..K];
x : clock;
invariant
(o=0 => true) &
(o=1 => x<=0) &
(o=2 => x<=AD) &
(o=3 => true) &
(o=4 => true)
endinvariant
[req] o=0 & K=1 -> 1/K : (o'=1) & (N'=1);
[req] o=0 & K=2 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2);
[req] o=0 & K=3 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2)
+ 1/K : (o'=1) & (N'=3);
[req] o=0 & K=4 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2)
+ 1/K : (o'=1) & (N'=3)
+ 1/K : (o'=1) & (N'=4);
[req] o=0 & K=5 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2)
+ 1/K : (o'=1) & (N'=3)
+ 1/K : (o'=1) & (N'=4)
+ 1/K : (o'=1) & (N'=5);
[req] o=0 & K=6 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2)
+ 1/K : (o'=1) & (N'=3)
+ 1/K : (o'=1) & (N'=4)
+ 1/K : (o'=1) & (N'=5)
+ 1/K : (o'=1) & (N'=6);
[req] o=0 & K=7 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2)
+ 1/K : (o'=1) & (N'=3)
+ 1/K : (o'=1) & (N'=4)
+ 1/K : (o'=1) & (N'=5)
+ 1/K : (o'=1) & (N'=6)
+ 1/K : (o'=1) & (N'=7);
[req] o=0 & K=8 -> 1/K : (o'=1) & (N'=1)
+ 1/K : (o'=1) & (N'=2)
+ 1/K : (o'=1) & (N'=3)
+ 1/K : (o'=1) & (N'=4)
+ 1/K : (o'=1) & (N'=5)
+ 1/K : (o'=1) & (N'=6)
+ 1/K : (o'=1) & (N'=7)
+ 1/K : (o'=1) & (N'=8);
[message] o=1 & x<=0 -> (o'=2);
[ack] o=2 & ack<N-1 & x<=AD -> (o'=1) & (ack'=min(ack+1,K)) & (x'=0);
[ack] o=2 & ack=N-1 & x<=AD -> (o'=3) & (ack'=min(ack+1,K)) & (x'=0);
[] o=2 & x>=AD -> (o'=4) & (x'=0);
endmodule
module malicious_recipient
r : [0..6];
mess : [0..K];
last : [0..1];
y : clock;
invariant
(r=0 => y<=0) &
(r=1 => true) &
(r=2 => true) &
(r=3 => y<=4) &
(r=4 => y<=AD+1) &
(r=5 => y<=0) &
(r=6 => true)
endinvariant
[req] r=0 & y=0 -> (r'=1);
[message] r=1 -> (r'=2) & (y'=0) & (mess'=min(mess+1,K));
[ack] r=2 & y>=ad -> (r'=1);
[] r=2 -> (r'=3);
[] r=2 -> (r'=4);
[] r=3 & y>=3 -> 0.75 : (r'=2) & (y'=0) + 0.25 : (r'=5) & (y'=0);
[] r=4 & y>=AD+1 -> (r'=5) & (y'=0);
[] r=5 & mess=N & ack<N & y<=0 -> (r'=6) & (last'=1);
[] r=5 & mess=N & ack=N & y<=0 -> (r'=6);
[] r=5 & mess<N & y<=0 -> (r'=2);
endmodule
label "unfair" = last=1;