mdp
const double loss = 0.1;
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
const int K;
module host_error
count : [0..K];
t : [0..2];
host_done : [0..1];
[send1] host_done=0 & count=0 -> (count'=count+1);
[send1] host_done=0 & count<K & t=2 -> (count'=count+1) & (t'=0);
[time] host_done=0 & count>0 -> (t'=min(t+1,2));
[time] host_done=0 & count=0 -> true;
[rec1] host_done=0 -> (host_done'=1);
[send1] host_done=1 -> true;
[time] host_done=1 -> true;
[reset] host_done=1 -> true;
[rec1] host_done=1 -> true;
endmodule
const int M;
module env_error6
env : [0..1];
k : [0..6];
c1 : [0..M+1];
c2 : [0..M+1];
c3 : [0..M+1];
c4 : [0..M+1];
c5 : [0..M+1];
c6 : [0..M+1];
error : [0..1];
[send2] error=0 & env=0 -> (env'=1);
[send1] error=0 & env=0 -> (k'=min(k+1,K));
[time] error=0 & env=0 & k=0 -> true;
[time] error=0 & env=0 & k=1 & min(c1,c2,c3,c4,c5,c6)<M -> (c1'=min(c1+1,M+1));
[time] error=0 & env=0 & k=2 & min(c1,c2,c3,c4,c5,c6)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1));
[time] error=0 & env=0 & k=3 & min(c1,c2,c3,c4,c5,c6)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1));
[time] error=0 & env=0 & k=4 & min(c1,c2,c3,c4,c5,c6)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)) & (c4'=min(c4+1,M+1));
[time] error=0 & env=0 & k=5 & min(c1,c2,c3,c4,c5,c6)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)) & (c4'=min(c4+1,M+1)) & (c5'=min(c5+1,M+1));
[time] error=0 & env=0 & k=6 & min(c1,c2,c3,c4,c5,c6)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)) & (c4'=min(c4+1,M+1)) & (c5'=min(c5+1,M+1)) & (c6'=min(c6+1,M+1));
[time] error=0 & env=0 & min(c1,c2,c3,c4,c5,c6)=M -> (error'=1);
[rec1] error=0 & env=0 & k>0 & min(c1,c2,c3,c4,c5,c6)<=M -> (env'=1);
[time] error=1 | env=1 -> true;
[send1] error=1 | env=1 -> true;
[send2] error=1 | env=1 -> true;
[rec1] error=1 | env=1 -> true;
endmodule