ctmc
const double mu=2;
formula rate1=mu*(1+min(3,b11+b21+b31+b41));
formula rate2=mu*(1+min(3,b12+b22+b32+b42));
formula rate3=mu*(1+min(3,b13+b23+b33+b43));
formula rate4=mu*(1+min(3,b14+b24+b34+b44));
formula rate5=mu*(1+min(3,b15+b25+b35+b45));
module client1
b11 : [0..1];
b12 : [0..1];
b13 : [0..1];
b14 : [0..1];
b15 : [0..1];
[] b11=0 -> rate1 : (b11'=1);
[] b12=0 -> rate2 : (b12'=1);
[] b13=0 -> rate3 : (b13'=1);
[] b14=0 -> rate4 : (b14'=1);
[] b15=0 -> rate5 : (b15'=1);
endmodule
module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15] endmodule
module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15] endmodule
module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15] endmodule
label "done1" = b11+b12+b13+b14+b15 = 5;
label "done2" = b21+b22+b23+b24+b25 = 5;
label "done3" = b31+b32+b33+b34+b35 = 5;
label "done4" = b41+b42+b43+b44+b45 = 5;
label "done" = (b11+b12+b13+b14+b15)+(b21+b22+b23+b24+b25)+(b31+b32+b33+b34+b35)+(b41+b42+b43+b44+b45) = 20;
rewards "frac_rec"
true : ((b11+b12+b13+b14+b15)/5)/4;
true : ((b21+b22+b23+b24+b25)/5)/4;
true : ((b31+b32+b33+b34+b35)/5)/4;
true : ((b41+b42+b43+b44+b45)/5)/4;
endrewards