mdp
const int N=20;
const int K;
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;
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);
[rec] (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);
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
[rec2] l=2 & ip=2 -> (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);
[rec2] l=3 & mess=0 & ip=2 -> (l'=l);
[send] l=3 & mess=1 -> (mess'=0);
[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
[send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
[] l=4 -> true;
endmodule
module host_error
count : [0..K];
t : [0..2];
host_err : [0..1];
host_done : [0..1];
[send1] host_done=0 & host_err=0 & count=0 -> (count'=count+1);
[send1] host_done=0 & host_err=0 & count<K & t=2 -> (count'=count+1) & (t'=0);
[send1] host_done=0 & host_err=0 & count=K -> (host_err'=1);
[time] host_done=0 & host_err=0 & count>0 -> (t'=min(t+1,2));
[time] host_done=0 & host_err=0 & count=0 -> true;
[rec1] host_done=0 -> (host_done'=1);
[send1] host_done=1 | host_err=1-> true;
[time] host_done=1 | host_err=1-> true;
[reset] host_done=1 | host_err=1-> true;
[rec1] host_done=1 | host_err=1-> true;
endmodule