mdp
const int N=20;
const int K;
const double loss = 0.1;
const double old = N/65024;
const double new = (1-old);
const int CONSEC = 2;
const int TRANSTIME = 1;
const int LONGWAIT = 60;
const int DEFEND = 10;
const int TIME_MAX_X = 60;
const int TIME_MAX_Y = 10;
const int TIME_MAX_Z = 1;
const int MAXCOLL = 10;
const int B0 = 20;
const int B1 = 8;
module environment
b_ip7 : [0..2];
b_ip6 : [0..2];
b_ip5 : [0..2];
b_ip4 : [0..2];
b_ip3 : [0..2];
b_ip2 : [0..2];
b_ip1 : [0..2];
b_ip0 : [0..2];
n : [0..8];
n0 : [0..B0];
n1 : [0..B1];
b : [0..2];
z : [0..1];
ip_mess : [0..2];
[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1))
& (ip_mess'=0)
& (b_ip7'=0)
& (b_ip6'=0)
& (b_ip5'=0)
& (b_ip4'=0)
& (b_ip3'=0)
& (b_ip2'=0)
& (b_ip1'=0)
& (b_ip0'=0);
[time] b=0 & n=0 & n0=0 & n1=0 -> (b'=b);
[time] b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z));
[send1] n=0 -> (b_ip0'=1) & (n'=n+1);
[send1] n=1 -> (b_ip1'=1) & (n'=n+1);
[send1] n=2 -> (b_ip2'=1) & (n'=n+1);
[send1] n=3 -> (b_ip3'=1) & (n'=n+1);
[send1] n=4 -> (b_ip4'=1) & (n'=n+1);
[send1] n=5 -> (b_ip5'=1) & (n'=n+1);
[send1] n=6 -> (b_ip6'=1) & (n'=n+1);
[send1] n=7 -> (b_ip7'=1) & (n'=n+1);
[send1] n=8 -> (n'=n);
[send2] n=0 -> (b_ip0'=2) & (n'=n+1);
[send2] n=1 -> (b_ip1'=2) & (n'=n+1);
[send2] n=2 -> (b_ip2'=2) & (n'=n+1);
[send2] n=3 -> (b_ip3'=2) & (n'=n+1);
[send2] n=4 -> (b_ip4'=2) & (n'=n+1);
[send2] n=5 -> (b_ip5'=2) & (n'=n+1);
[send2] n=6 -> (b_ip6'=2) & (n'=n+1);
[send2] n=7 -> (b_ip7'=2) & (n'=n+1);
[send2] n=8 -> (n'=n);
[] b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0)
& (n'=n-1)
& (b_ip7'=0)
& (b_ip6'=b_ip7)
& (b_ip5'=b_ip6)
& (b_ip4'=b_ip5)
& (b_ip3'=b_ip4)
& (b_ip2'=b_ip3)
& (b_ip1'=b_ip2)
& (b_ip0'=b_ip1)
+ loss : (n'=n-1)
& (b_ip7'=0)
& (b_ip6'=b_ip7)
& (b_ip5'=b_ip6)
& (b_ip4'=b_ip5)
& (b_ip3'=b_ip4)
& (b_ip2'=b_ip3)
& (b_ip1'=b_ip2)
& (b_ip0'=b_ip1);
[] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1);
[] b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1);
[] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
[] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
[] b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
[rec0] b=2 & ip_mess=0 -> (b'=0) & (z'=0) & (ip_mess'=0);
[rec1] b=2 & ip_mess=1 -> (b'=0) & (z'=0) & (ip_mess'=0);
endmodule
module host0
x : [0..TIME_MAX_X];
y : [0..TIME_MAX_Y];
coll : [0..MAXCOLL];
probes : [0..K];
mess : [0..1];
defend : [0..1];
ip : [1..2];
l : [0..4] init 1;
[reset] l=0 -> (l'=1);
[rec0] (l=1) -> true;
[rec1] (l=1) -> true;
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X));
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
[time] l=2 & x<2 -> (x'=min(x+1,2));
[send1] l=2 & ip=1 & x=2 & probes<K -> (x'=0) & (probes'=probes+1);
[send2] l=2 & ip=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1);
[configured] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
[rec0] l=2 & ip!=0 -> (l'=l);
[rec1] l=2 & ip!=1 -> (l'=l);
[rec1] l=2 & ip=1 -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X));
[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND));
[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
[rec0] l=3 & mess=0 & ip!=0 -> (l'=l);
[rec1] l=3 & mess=0 & ip!=1 -> (l'=l);
[send1] l=3 & ip=1 & mess=1 -> (mess'=0);
[send2] l=3 & ip=2 & mess=1 -> (mess'=0);
[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
[] l=4 -> true;
endmodule
const int T;
module time_error
time_error : [0..1];
done : [0..1];
t : [0..T];
[time] t<T-1 & done=0 & time_error=0 -> (t'=t+1);
[time] t=T-1 & done=0 & time_error=0 -> (time_error'=1);
[configured] time_error=0 -> (done'=1);
[configured] time_error=1 | done=1 -> true;
[time] time_error=1 | done=1 -> true;
endmodule