// CSMA/CD protocol - two stations (PTA model using digital clocks) // gxn/mxd 31/05/05 // based on kronos (non-probabilistic) TA model and that which appears in: // M. Duflot, L. Fribourg, T. Hérault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet and C. Picaronny // Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC // In Proc. AVoCS'04, 2004 pta // PARAMETERS // parameters const int sigma=26; // time for messages to propagate along the bus const int lambda=808; // time to send a message const int delay=26; // wire delay const int slot=2*sigma; // size of back off slot const int K; // exponential backoff limit (sometimes called bmax) const int M=pow(2,K)-1; // max number of slots to wait const int COL; // max number of collisions (called K in an old version of this model) //---------------------------------------------------------------------------------------------------------------------------- // collision counter module collisions c : [0..max(1,COL)]; [csend1] true -> (c'=min(COL,c+1)); [csend2] true -> (c'=min(COL,c+1)); endmodule //---------------------------------------------------------------------------------------------------------------------------- // the bus module bus b : [0..4]; // b=0 - idle // b=1 - active // b=2 - collision // b=3 - collision1 // b=4 - collision2 y1 : clock; // clock of bus y2 : clock; // clock of bus invariant (b=0 => true) & (b=1 => true) & (b=2 => y1<=delay & y2<=delay) & (b=3 => y1<=delay) & (b=4 => y2<=delay) endinvariant // stations starts sending [send1] b=0 -> (b'=1) & (y1'=0); // no message being sent [send2] b=0 -> (b'=1) & (y2'=0); // no message being sent // collision occurs [csend1] b=1 & y2<=delay -> (b'=2) & (y1'=0); // message being sent (move to collision) [csend2] b=1 & y1<=delay -> (b'=2) & (y2'=0); // message being sent (move to collision) // message being sent [busy1] b=1 & y2>delay -> (b'=1); [busy2] b=1 & y1>delay -> (b'=1); // station finishes [end1] b=1 -> (b'=0) & (y1'=0); [end2] b=1 -> (b'=0) & (y2'=0); // collision detected [cd1] b=2 & y1>=delay -> (b'=4); // station one detects collision before station two [cd2] b=2 & y2>=delay -> (b'=3); // station two detects collision before station one [cd1] b=3 & y1>=delay -> (b'=0) & (y1'=0) & (y2'=0); // station one detects collision after station two [cd2] b=4 & y2>=delay -> (b'=0) & (y1'=0) & (y2'=0); // station two detects collision after station one endmodule //---------------------------------------------------------------------------------------------------------------------------- // STATION 1 module station1 // LOCAL STATE s1 : [0..4]; // s1=0 - initial state // s1=1 - transmit // s1=2 - collision (set backoff) // s1=3 - wait (bus busy) // s1=4 - done (since sending only one message) x1 : clock; // local clock cd1 : [0..K]; // collision counter invariant (s1=0 => x1<=delay) & (s1=1 => x1<=lambda) & (s1=2 => x1<=0) & (s1=3 => x1<=pow(2,cd1)*slot) & (s1=4 => true) endinvariant // start sending (make sure there is a collision, i.e. start before x1 equals delay) [send1] s1=0 -> (s1'=1) & (x1'=0); // start sending [csend1] s1=0 -> (s1'=1) & (x1'=0); // start sending [busy1] s1=0 -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff // transmitting [end1] s1=1 & x1=lambda -> (s1'=4) & (x1'=0); // finished [cd1] s1=1 -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected // set backoff (no time can pass in this state) // first retransmission [] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot) + 1/2 : (s1'=3) & (x1'=1*slot); // second retransmission [] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot) + 1/4 : (s1'=3) & (x1'=1*slot) + 1/4 : (s1'=3) & (x1'=2*slot) + 1/4 : (s1'=3) & (x1'=3*slot); // third retransmission [] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (x1'=0*slot) + 1/8 : (s1'=3) & (x1'=1*slot) + 1/8 : (s1'=3) & (x1'=2*slot) + 1/8 : (s1'=3) & (x1'=3*slot) + 1/8 : (s1'=3) & (x1'=4*slot) + 1/8 : (s1'=3) & (x1'=5*slot) + 1/8 : (s1'=3) & (x1'=6*slot) + 1/8 : (s1'=3) & (x1'=7*slot); // fourth retransmission [] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (x1'=0*slot) + 1/16 : (s1'=3) & (x1'=1*slot) + 1/16 : (s1'=3) & (x1'=2*slot) + 1/16 : (s1'=3) & (x1'=3*slot) + 1/16 : (s1'=3) & (x1'=4*slot) + 1/16 : (s1'=3) & (x1'=5*slot) + 1/16 : (s1'=3) & (x1'=6*slot) + 1/16 : (s1'=3) & (x1'=7*slot) + 1/16 : (s1'=3) & (x1'=8*slot) + 1/16 : (s1'=3) & (x1'=9*slot) + 1/16 : (s1'=3) & (x1'=10*slot) + 1/16 : (s1'=3) & (x1'=11*slot) + 1/16 : (s1'=3) & (x1'=12*slot) + 1/16 : (s1'=3) & (x1'=13*slot) + 1/16 : (s1'=3) & (x1'=14*slot) + 1/16 : (s1'=3) & (x1'=15*slot); // fifth retransmission [] s1=2 & cd1=5 -> 1/32 : (s1'=3) & (x1'=0*slot) + 1/32 : (s1'=3) & (x1'=1*slot) + 1/32 : (s1'=3) & (x1'=2*slot) + 1/32 : (s1'=3) & (x1'=3*slot) + 1/32 : (s1'=3) & (x1'=4*slot) + 1/32 : (s1'=3) & (x1'=5*slot) + 1/32 : (s1'=3) & (x1'=6*slot) + 1/32 : (s1'=3) & (x1'=7*slot) + 1/32 : (s1'=3) & (x1'=8*slot) + 1/32 : (s1'=3) & (x1'=9*slot) + 1/32 : (s1'=3) & (x1'=10*slot) + 1/32 : (s1'=3) & (x1'=11*slot) + 1/32 : (s1'=3) & (x1'=12*slot) + 1/32 : (s1'=3) & (x1'=13*slot) + 1/32 : (s1'=3) & (x1'=14*slot) + 1/32 : (s1'=3) & (x1'=15*slot) + 1/32 : (s1'=3) & (x1'=16*slot) + 1/32 : (s1'=3) & (x1'=17*slot) + 1/32 : (s1'=3) & (x1'=18*slot) + 1/32 : (s1'=3) & (x1'=19*slot) + 1/32 : (s1'=3) & (x1'=20*slot) + 1/32 : (s1'=3) & (x1'=21*slot) + 1/32 : (s1'=3) & (x1'=22*slot) + 1/32 : (s1'=3) & (x1'=23*slot) + 1/32 : (s1'=3) & (x1'=24*slot) + 1/32 : (s1'=3) & (x1'=25*slot) + 1/32 : (s1'=3) & (x1'=26*slot) + 1/32 : (s1'=3) & (x1'=27*slot) + 1/32 : (s1'=3) & (x1'=28*slot) + 1/32 : (s1'=3) & (x1'=29*slot) + 1/32 : (s1'=3) & (x1'=30*slot) + 1/32 : (s1'=3) & (x1'=31*slot); // sixth retransmission [] s1=2 & cd1=6 -> 1/64 : (s1'=3) & (x1'=0*slot) + 1/64 : (s1'=3) & (x1'=1*slot) + 1/64 : (s1'=3) & (x1'=2*slot) + 1/64 : (s1'=3) & (x1'=3*slot) + 1/64 : (s1'=3) & (x1'=4*slot) + 1/64 : (s1'=3) & (x1'=5*slot) + 1/64 : (s1'=3) & (x1'=6*slot) + 1/64 : (s1'=3) & (x1'=7*slot) + 1/64 : (s1'=3) & (x1'=8*slot) + 1/64 : (s1'=3) & (x1'=9*slot) + 1/64 : (s1'=3) & (x1'=10*slot) + 1/64 : (s1'=3) & (x1'=11*slot) + 1/64 : (s1'=3) & (x1'=12*slot) + 1/64 : (s1'=3) & (x1'=13*slot) + 1/64 : (s1'=3) & (x1'=14*slot) + 1/64 : (s1'=3) & (x1'=15*slot) + 1/64 : (s1'=3) & (x1'=16*slot) + 1/64 : (s1'=3) & (x1'=17*slot) + 1/64 : (s1'=3) & (x1'=18*slot) + 1/64 : (s1'=3) & (x1'=19*slot) + 1/64 : (s1'=3) & (x1'=20*slot) + 1/64 : (s1'=3) & (x1'=21*slot) + 1/64 : (s1'=3) & (x1'=22*slot) + 1/64 : (s1'=3) & (x1'=23*slot) + 1/64 : (s1'=3) & (x1'=24*slot) + 1/64 : (s1'=3) & (x1'=25*slot) + 1/64 : (s1'=3) & (x1'=26*slot) + 1/64 : (s1'=3) & (x1'=27*slot) + 1/64 : (s1'=3) & (x1'=28*slot) + 1/64 : (s1'=3) & (x1'=29*slot) + 1/64 : (s1'=3) & (x1'=30*slot) + 1/64 : (s1'=3) & (x1'=31*slot) + 1/64 : (s1'=3) & (x1'=32*slot) + 1/64 : (s1'=3) & (x1'=33*slot) + 1/64 : (s1'=3) & (x1'=34*slot) + 1/64 : (s1'=3) & (x1'=35*slot) + 1/64 : (s1'=3) & (x1'=36*slot) + 1/64 : (s1'=3) & (x1'=37*slot) + 1/64 : (s1'=3) & (x1'=38*slot) + 1/64 : (s1'=3) & (x1'=39*slot) + 1/64 : (s1'=3) & (x1'=40*slot) + 1/64 : (s1'=3) & (x1'=41*slot) + 1/64 : (s1'=3) & (x1'=42*slot) + 1/64 : (s1'=3) & (x1'=43*slot) + 1/64 : (s1'=3) & (x1'=44*slot) + 1/64 : (s1'=3) & (x1'=45*slot) + 1/64 : (s1'=3) & (x1'=46*slot) + 1/64 : (s1'=3) & (x1'=47*slot) + 1/64 : (s1'=3) & (x1'=48*slot) + 1/64 : (s1'=3) & (x1'=49*slot) + 1/64 : (s1'=3) & (x1'=50*slot) + 1/64 : (s1'=3) & (x1'=51*slot) + 1/64 : (s1'=3) & (x1'=52*slot) + 1/64 : (s1'=3) & (x1'=53*slot) + 1/64 : (s1'=3) & (x1'=54*slot) + 1/64 : (s1'=3) & (x1'=55*slot) + 1/64 : (s1'=3) & (x1'=56*slot) + 1/64 : (s1'=3) & (x1'=57*slot) + 1/64 : (s1'=3) & (x1'=58*slot) + 1/64 : (s1'=3) & (x1'=59*slot) + 1/64 : (s1'=3) & (x1'=60*slot) + 1/64 : (s1'=3) & (x1'=61*slot) + 1/64 : (s1'=3) & (x1'=62*slot) + 1/64 : (s1'=3) & (x1'=63*slot); // seventh retransmission [] s1=2 & cd1=7 -> 1/128 : (s1'=3) & (x1'=0*slot) + 1/128 : (s1'=3) & (x1'=1*slot) + 1/128 : (s1'=3) & (x1'=2*slot) + 1/128 : (s1'=3) & (x1'=3*slot) + 1/128 : (s1'=3) & (x1'=4*slot) + 1/128 : (s1'=3) & (x1'=5*slot) + 1/128 : (s1'=3) & (x1'=6*slot) + 1/128 : (s1'=3) & (x1'=7*slot) + 1/128 : (s1'=3) & (x1'=8*slot) + 1/128 : (s1'=3) & (x1'=9*slot) + 1/128 : (s1'=3) & (x1'=10*slot) + 1/128 : (s1'=3) & (x1'=11*slot) + 1/128 : (s1'=3) & (x1'=12*slot) + 1/128 : (s1'=3) & (x1'=13*slot) + 1/128 : (s1'=3) & (x1'=14*slot) + 1/128 : (s1'=3) & (x1'=15*slot) + 1/128 : (s1'=3) & (x1'=16*slot) + 1/128 : (s1'=3) & (x1'=17*slot) + 1/128 : (s1'=3) & (x1'=18*slot) + 1/128 : (s1'=3) & (x1'=19*slot) + 1/128 : (s1'=3) & (x1'=20*slot) + 1/128 : (s1'=3) & (x1'=21*slot) + 1/128 : (s1'=3) & (x1'=22*slot) + 1/128 : (s1'=3) & (x1'=23*slot) + 1/128 : (s1'=3) & (x1'=24*slot) + 1/128 : (s1'=3) & (x1'=25*slot) + 1/128 : (s1'=3) & (x1'=26*slot) + 1/128 : (s1'=3) & (x1'=27*slot) + 1/128 : (s1'=3) & (x1'=28*slot) + 1/128 : (s1'=3) & (x1'=29*slot) + 1/128 : (s1'=3) & (x1'=30*slot) + 1/128 : (s1'=3) & (x1'=31*slot) + 1/128 : (s1'=3) & (x1'=32*slot) + 1/128 : (s1'=3) & (x1'=33*slot) + 1/128 : (s1'=3) & (x1'=34*slot) + 1/128 : (s1'=3) & (x1'=35*slot) + 1/128 : (s1'=3) & (x1'=36*slot) + 1/128 : (s1'=3) & (x1'=37*slot) + 1/128 : (s1'=3) & (x1'=38*slot) + 1/128 : (s1'=3) & (x1'=39*slot) + 1/128 : (s1'=3) & (x1'=40*slot) + 1/128 : (s1'=3) & (x1'=41*slot) + 1/128 : (s1'=3) & (x1'=42*slot) + 1/128 : (s1'=3) & (x1'=43*slot) + 1/128 : (s1'=3) & (x1'=44*slot) + 1/128 : (s1'=3) & (x1'=45*slot) + 1/128 : (s1'=3) & (x1'=46*slot) + 1/128 : (s1'=3) & (x1'=47*slot) + 1/128 : (s1'=3) & (x1'=48*slot) + 1/128 : (s1'=3) & (x1'=49*slot) + 1/128 : (s1'=3) & (x1'=50*slot) + 1/128 : (s1'=3) & (x1'=51*slot) + 1/128 : (s1'=3) & (x1'=52*slot) + 1/128 : (s1'=3) & (x1'=53*slot) + 1/128 : (s1'=3) & (x1'=54*slot) + 1/128 : (s1'=3) & (x1'=55*slot) + 1/128 : (s1'=3) & (x1'=56*slot) + 1/128 : (s1'=3) & (x1'=57*slot) + 1/128 : (s1'=3) & (x1'=58*slot) + 1/128 : (s1'=3) & (x1'=59*slot) + 1/128 : (s1'=3) & (x1'=60*slot) + 1/128 : (s1'=3) & (x1'=61*slot) + 1/128 : (s1'=3) & (x1'=62*slot) + 1/128 : (s1'=3) & (x1'=63*slot) + 1/128 : (s1'=3) & (x1'=64*slot) + 1/128 : (s1'=3) & (x1'=65*slot) + 1/128 : (s1'=3) & (x1'=66*slot) + 1/128 : (s1'=3) & (x1'=67*slot) + 1/128 : (s1'=3) & (x1'=68*slot) + 1/128 : (s1'=3) & (x1'=69*slot) + 1/128 : (s1'=3) & (x1'=70*slot) + 1/128 : (s1'=3) & (x1'=71*slot) + 1/128 : (s1'=3) & (x1'=72*slot) + 1/128 : (s1'=3) & (x1'=73*slot) + 1/128 : (s1'=3) & (x1'=74*slot) + 1/128 : (s1'=3) & (x1'=75*slot) + 1/128 : (s1'=3) & (x1'=76*slot) + 1/128 : (s1'=3) & (x1'=77*slot) + 1/128 : (s1'=3) & (x1'=78*slot) + 1/128 : (s1'=3) & (x1'=79*slot) + 1/128 : (s1'=3) & (x1'=80*slot) + 1/128 : (s1'=3) & (x1'=81*slot) + 1/128 : (s1'=3) & (x1'=82*slot) + 1/128 : (s1'=3) & (x1'=83*slot) + 1/128 : (s1'=3) & (x1'=84*slot) + 1/128 : (s1'=3) & (x1'=85*slot) + 1/128 : (s1'=3) & (x1'=86*slot) + 1/128 : (s1'=3) & (x1'=87*slot) + 1/128 : (s1'=3) & (x1'=88*slot) + 1/128 : (s1'=3) & (x1'=89*slot) + 1/128 : (s1'=3) & (x1'=90*slot) + 1/128 : (s1'=3) & (x1'=91*slot) + 1/128 : (s1'=3) & (x1'=92*slot) + 1/128 : (s1'=3) & (x1'=93*slot) + 1/128 : (s1'=3) & (x1'=94*slot) + 1/128 : (s1'=3) & (x1'=95*slot) + 1/128 : (s1'=3) & (x1'=96*slot) + 1/128 : (s1'=3) & (x1'=97*slot) + 1/128 : (s1'=3) & (x1'=98*slot) + 1/128 : (s1'=3) & (x1'=99*slot) + 1/128 : (s1'=3) & (x1'=100*slot) + 1/128 : (s1'=3) & (x1'=101*slot) + 1/128 : (s1'=3) & (x1'=102*slot) + 1/128 : (s1'=3) & (x1'=103*slot) + 1/128 : (s1'=3) & (x1'=104*slot) + 1/128 : (s1'=3) & (x1'=105*slot) + 1/128 : (s1'=3) & (x1'=106*slot) + 1/128 : (s1'=3) & (x1'=107*slot) + 1/128 : (s1'=3) & (x1'=108*slot) + 1/128 : (s1'=3) & (x1'=109*slot) + 1/128 : (s1'=3) & (x1'=110*slot) + 1/128 : (s1'=3) & (x1'=111*slot) + 1/128 : (s1'=3) & (x1'=112*slot) + 1/128 : (s1'=3) & (x1'=113*slot) + 1/128 : (s1'=3) & (x1'=114*slot) + 1/128 : (s1'=3) & (x1'=115*slot) + 1/128 : (s1'=3) & (x1'=116*slot) + 1/128 : (s1'=3) & (x1'=117*slot) + 1/128 : (s1'=3) & (x1'=118*slot) + 1/128 : (s1'=3) & (x1'=119*slot) + 1/128 : (s1'=3) & (x1'=120*slot) + 1/128 : (s1'=3) & (x1'=121*slot) + 1/128 : (s1'=3) & (x1'=122*slot) + 1/128 : (s1'=3) & (x1'=123*slot) + 1/128 : (s1'=3) & (x1'=124*slot) + 1/128 : (s1'=3) & (x1'=125*slot) + 1/128 : (s1'=3) & (x1'=126*slot) + 1/128 : (s1'=3) & (x1'=127*slot); // eigth retransmission [] s1=2 & cd1=8 -> 1/256 : (s1'=3) & (x1'=0*slot) + 1/256 : (s1'=3) & (x1'=1*slot) + 1/256 : (s1'=3) & (x1'=2*slot) + 1/256 : (s1'=3) & (x1'=3*slot) + 1/256 : (s1'=3) & (x1'=4*slot) + 1/256 : (s1'=3) & (x1'=5*slot) + 1/256 : (s1'=3) & (x1'=6*slot) + 1/256 : (s1'=3) & (x1'=7*slot) + 1/256 : (s1'=3) & (x1'=8*slot) + 1/256 : (s1'=3) & (x1'=9*slot) + 1/256 : (s1'=3) & (x1'=10*slot) + 1/256 : (s1'=3) & (x1'=11*slot) + 1/256 : (s1'=3) & (x1'=12*slot) + 1/256 : (s1'=3) & (x1'=13*slot) + 1/256 : (s1'=3) & (x1'=14*slot) + 1/256 : (s1'=3) & (x1'=15*slot) + 1/256 : (s1'=3) & (x1'=16*slot) + 1/256 : (s1'=3) & (x1'=17*slot) + 1/256 : (s1'=3) & (x1'=18*slot) + 1/256 : (s1'=3) & (x1'=19*slot) + 1/256 : (s1'=3) & (x1'=20*slot) + 1/256 : (s1'=3) & (x1'=21*slot) + 1/256 : (s1'=3) & (x1'=22*slot) + 1/256 : (s1'=3) & (x1'=23*slot) + 1/256 : (s1'=3) & (x1'=24*slot) + 1/256 : (s1'=3) & (x1'=25*slot) + 1/256 : (s1'=3) & (x1'=26*slot) + 1/256 : (s1'=3) & (x1'=27*slot) + 1/256 : (s1'=3) & (x1'=28*slot) + 1/256 : (s1'=3) & (x1'=29*slot) + 1/256 : (s1'=3) & (x1'=30*slot) + 1/256 : (s1'=3) & (x1'=31*slot) + 1/256 : (s1'=3) & (x1'=32*slot) + 1/256 : (s1'=3) & (x1'=33*slot) + 1/256 : (s1'=3) & (x1'=34*slot) + 1/256 : (s1'=3) & (x1'=35*slot) + 1/256 : (s1'=3) & (x1'=36*slot) + 1/256 : (s1'=3) & (x1'=37*slot) + 1/256 : (s1'=3) & (x1'=38*slot) + 1/256 : (s1'=3) & (x1'=39*slot) + 1/256 : (s1'=3) & (x1'=40*slot) + 1/256 : (s1'=3) & (x1'=41*slot) + 1/256 : (s1'=3) & (x1'=42*slot) + 1/256 : (s1'=3) & (x1'=43*slot) + 1/256 : (s1'=3) & (x1'=44*slot) + 1/256 : (s1'=3) & (x1'=45*slot) + 1/256 : (s1'=3) & (x1'=46*slot) + 1/256 : (s1'=3) & (x1'=47*slot) + 1/256 : (s1'=3) & (x1'=48*slot) + 1/256 : (s1'=3) & (x1'=49*slot) + 1/256 : (s1'=3) & (x1'=50*slot) + 1/256 : (s1'=3) & (x1'=51*slot) + 1/256 : (s1'=3) & (x1'=52*slot) + 1/256 : (s1'=3) & (x1'=53*slot) + 1/256 : (s1'=3) & (x1'=54*slot) + 1/256 : (s1'=3) & (x1'=55*slot) + 1/256 : (s1'=3) & (x1'=56*slot) + 1/256 : (s1'=3) & (x1'=57*slot) + 1/256 : (s1'=3) & (x1'=58*slot) + 1/256 : (s1'=3) & (x1'=59*slot) + 1/256 : (s1'=3) & (x1'=60*slot) + 1/256 : (s1'=3) & (x1'=61*slot) + 1/256 : (s1'=3) & (x1'=62*slot) + 1/256 : (s1'=3) & (x1'=63*slot) + 1/256 : (s1'=3) & (x1'=64*slot) + 1/256 : (s1'=3) & (x1'=65*slot) + 1/256 : (s1'=3) & (x1'=66*slot) + 1/256 : (s1'=3) & (x1'=67*slot) + 1/256 : (s1'=3) & (x1'=68*slot) + 1/256 : (s1'=3) & (x1'=69*slot) + 1/256 : (s1'=3) & (x1'=70*slot) + 1/256 : (s1'=3) & (x1'=71*slot) + 1/256 : (s1'=3) & (x1'=72*slot) + 1/256 : (s1'=3) & (x1'=73*slot) + 1/256 : (s1'=3) & (x1'=74*slot) + 1/256 : (s1'=3) & (x1'=75*slot) + 1/256 : (s1'=3) & (x1'=76*slot) + 1/256 : (s1'=3) & (x1'=77*slot) + 1/256 : (s1'=3) & (x1'=78*slot) + 1/256 : (s1'=3) & (x1'=79*slot) + 1/256 : (s1'=3) & (x1'=80*slot) + 1/256 : (s1'=3) & (x1'=81*slot) + 1/256 : (s1'=3) & (x1'=82*slot) + 1/256 : (s1'=3) & (x1'=83*slot) + 1/256 : (s1'=3) & (x1'=84*slot) + 1/256 : (s1'=3) & (x1'=85*slot) + 1/256 : (s1'=3) & (x1'=86*slot) + 1/256 : (s1'=3) & (x1'=87*slot) + 1/256 : (s1'=3) & (x1'=88*slot) + 1/256 : (s1'=3) & (x1'=89*slot) + 1/256 : (s1'=3) & (x1'=90*slot) + 1/256 : (s1'=3) & (x1'=91*slot) + 1/256 : (s1'=3) & (x1'=92*slot) + 1/256 : (s1'=3) & (x1'=93*slot) + 1/256 : (s1'=3) & (x1'=94*slot) + 1/256 : (s1'=3) & (x1'=95*slot) + 1/256 : (s1'=3) & (x1'=96*slot) + 1/256 : (s1'=3) & (x1'=97*slot) + 1/256 : (s1'=3) & (x1'=98*slot) + 1/256 : (s1'=3) & (x1'=99*slot) + 1/256 : (s1'=3) & (x1'=100*slot) + 1/256 : (s1'=3) & (x1'=101*slot) + 1/256 : (s1'=3) & (x1'=102*slot) + 1/256 : (s1'=3) & (x1'=103*slot) + 1/256 : (s1'=3) & (x1'=104*slot) + 1/256 : (s1'=3) & (x1'=105*slot) + 1/256 : (s1'=3) & (x1'=106*slot) + 1/256 : (s1'=3) & (x1'=107*slot) + 1/256 : (s1'=3) & (x1'=108*slot) + 1/256 : (s1'=3) & (x1'=109*slot) + 1/256 : (s1'=3) & (x1'=110*slot) + 1/256 : (s1'=3) & (x1'=111*slot) + 1/256 : (s1'=3) & (x1'=112*slot) + 1/256 : (s1'=3) & (x1'=113*slot) + 1/256 : (s1'=3) & (x1'=114*slot) + 1/256 : (s1'=3) & (x1'=115*slot) + 1/256 : (s1'=3) & (x1'=116*slot) + 1/256 : (s1'=3) & (x1'=117*slot) + 1/256 : (s1'=3) & (x1'=118*slot) + 1/256 : (s1'=3) & (x1'=119*slot) + 1/256 : (s1'=3) & (x1'=120*slot) + 1/256 : (s1'=3) & (x1'=121*slot) + 1/256 : (s1'=3) & (x1'=122*slot) + 1/256 : (s1'=3) & (x1'=123*slot) + 1/256 : (s1'=3) & (x1'=124*slot) + 1/256 : (s1'=3) & (x1'=125*slot) + 1/256 : (s1'=3) & (x1'=126*slot) + 1/256 : (s1'=3) & (x1'=127*slot) + 1/256 : (s1'=3) & (x1'=128*slot) + 1/256 : (s1'=3) & (x1'=129*slot) + 1/256 : (s1'=3) & (x1'=130*slot) + 1/256 : (s1'=3) & (x1'=131*slot) + 1/256 : (s1'=3) & (x1'=132*slot) + 1/256 : (s1'=3) & (x1'=133*slot) + 1/256 : (s1'=3) & (x1'=134*slot) + 1/256 : (s1'=3) & (x1'=135*slot) + 1/256 : (s1'=3) & (x1'=136*slot) + 1/256 : (s1'=3) & (x1'=137*slot) + 1/256 : (s1'=3) & (x1'=138*slot) + 1/256 : (s1'=3) & (x1'=139*slot) + 1/256 : (s1'=3) & (x1'=140*slot) + 1/256 : (s1'=3) & (x1'=141*slot) + 1/256 : (s1'=3) & (x1'=142*slot) + 1/256 : (s1'=3) & (x1'=143*slot) + 1/256 : (s1'=3) & (x1'=144*slot) + 1/256 : (s1'=3) & (x1'=145*slot) + 1/256 : (s1'=3) & (x1'=146*slot) + 1/256 : (s1'=3) & (x1'=147*slot) + 1/256 : (s1'=3) & (x1'=148*slot) + 1/256 : (s1'=3) & (x1'=149*slot) + 1/256 : (s1'=3) & (x1'=150*slot) + 1/256 : (s1'=3) & (x1'=151*slot) + 1/256 : (s1'=3) & (x1'=152*slot) + 1/256 : (s1'=3) & (x1'=153*slot) + 1/256 : (s1'=3) & (x1'=154*slot) + 1/256 : (s1'=3) & (x1'=155*slot) + 1/256 : (s1'=3) & (x1'=156*slot) + 1/256 : (s1'=3) & (x1'=157*slot) + 1/256 : (s1'=3) & (x1'=158*slot) + 1/256 : (s1'=3) & (x1'=159*slot) + 1/256 : (s1'=3) & (x1'=160*slot) + 1/256 : (s1'=3) & (x1'=161*slot) + 1/256 : (s1'=3) & (x1'=162*slot) + 1/256 : (s1'=3) & (x1'=163*slot) + 1/256 : (s1'=3) & (x1'=164*slot) + 1/256 : (s1'=3) & (x1'=165*slot) + 1/256 : (s1'=3) & (x1'=166*slot) + 1/256 : (s1'=3) & (x1'=167*slot) + 1/256 : (s1'=3) & (x1'=168*slot) + 1/256 : (s1'=3) & (x1'=169*slot) + 1/256 : (s1'=3) & (x1'=170*slot) + 1/256 : (s1'=3) & (x1'=171*slot) + 1/256 : (s1'=3) & (x1'=172*slot) + 1/256 : (s1'=3) & (x1'=173*slot) + 1/256 : (s1'=3) & (x1'=174*slot) + 1/256 : (s1'=3) & (x1'=175*slot) + 1/256 : (s1'=3) & (x1'=176*slot) + 1/256 : (s1'=3) & (x1'=177*slot) + 1/256 : (s1'=3) & (x1'=178*slot) + 1/256 : (s1'=3) & (x1'=179*slot) + 1/256 : (s1'=3) & (x1'=180*slot) + 1/256 : (s1'=3) & (x1'=181*slot) + 1/256 : (s1'=3) & (x1'=182*slot) + 1/256 : (s1'=3) & (x1'=183*slot) + 1/256 : (s1'=3) & (x1'=184*slot) + 1/256 : (s1'=3) & (x1'=185*slot) + 1/256 : (s1'=3) & (x1'=186*slot) + 1/256 : (s1'=3) & (x1'=187*slot) + 1/256 : (s1'=3) & (x1'=188*slot) + 1/256 : (s1'=3) & (x1'=189*slot) + 1/256 : (s1'=3) & (x1'=190*slot) + 1/256 : (s1'=3) & (x1'=191*slot) + 1/256 : (s1'=3) & (x1'=192*slot) + 1/256 : (s1'=3) & (x1'=193*slot) + 1/256 : (s1'=3) & (x1'=194*slot) + 1/256 : (s1'=3) & (x1'=195*slot) + 1/256 : (s1'=3) & (x1'=196*slot) + 1/256 : (s1'=3) & (x1'=197*slot) + 1/256 : (s1'=3) & (x1'=198*slot) + 1/256 : (s1'=3) & (x1'=199*slot) + 1/256 : (s1'=3) & (x1'=200*slot) + 1/256 : (s1'=3) & (x1'=201*slot) + 1/256 : (s1'=3) & (x1'=202*slot) + 1/256 : (s1'=3) & (x1'=203*slot) + 1/256 : (s1'=3) & (x1'=204*slot) + 1/256 : (s1'=3) & (x1'=205*slot) + 1/256 : (s1'=3) & (x1'=206*slot) + 1/256 : (s1'=3) & (x1'=207*slot) + 1/256 : (s1'=3) & (x1'=208*slot) + 1/256 : (s1'=3) & (x1'=209*slot) + 1/256 : (s1'=3) & (x1'=210*slot) + 1/256 : (s1'=3) & (x1'=211*slot) + 1/256 : (s1'=3) & (x1'=212*slot) + 1/256 : (s1'=3) & (x1'=213*slot) + 1/256 : (s1'=3) & (x1'=214*slot) + 1/256 : (s1'=3) & (x1'=215*slot) + 1/256 : (s1'=3) & (x1'=216*slot) + 1/256 : (s1'=3) & (x1'=217*slot) + 1/256 : (s1'=3) & (x1'=218*slot) + 1/256 : (s1'=3) & (x1'=219*slot) + 1/256 : (s1'=3) & (x1'=220*slot) + 1/256 : (s1'=3) & (x1'=221*slot) + 1/256 : (s1'=3) & (x1'=222*slot) + 1/256 : (s1'=3) & (x1'=223*slot) + 1/256 : (s1'=3) & (x1'=224*slot) + 1/256 : (s1'=3) & (x1'=225*slot) + 1/256 : (s1'=3) & (x1'=226*slot) + 1/256 : (s1'=3) & (x1'=227*slot) + 1/256 : (s1'=3) & (x1'=228*slot) + 1/256 : (s1'=3) & (x1'=229*slot) + 1/256 : (s1'=3) & (x1'=230*slot) + 1/256 : (s1'=3) & (x1'=231*slot) + 1/256 : (s1'=3) & (x1'=232*slot) + 1/256 : (s1'=3) & (x1'=233*slot) + 1/256 : (s1'=3) & (x1'=234*slot) + 1/256 : (s1'=3) & (x1'=235*slot) + 1/256 : (s1'=3) & (x1'=236*slot) + 1/256 : (s1'=3) & (x1'=237*slot) + 1/256 : (s1'=3) & (x1'=238*slot) + 1/256 : (s1'=3) & (x1'=239*slot) + 1/256 : (s1'=3) & (x1'=240*slot) + 1/256 : (s1'=3) & (x1'=241*slot) + 1/256 : (s1'=3) & (x1'=242*slot) + 1/256 : (s1'=3) & (x1'=243*slot) + 1/256 : (s1'=3) & (x1'=244*slot) + 1/256 : (s1'=3) & (x1'=245*slot) + 1/256 : (s1'=3) & (x1'=246*slot) + 1/256 : (s1'=3) & (x1'=247*slot) + 1/256 : (s1'=3) & (x1'=248*slot) + 1/256 : (s1'=3) & (x1'=249*slot) + 1/256 : (s1'=3) & (x1'=250*slot) + 1/256 : (s1'=3) & (x1'=251*slot) + 1/256 : (s1'=3) & (x1'=252*slot) + 1/256 : (s1'=3) & (x1'=253*slot) + 1/256 : (s1'=3) & (x1'=254*slot) + 1/256 : (s1'=3) & (x1'=255*slot); // ninth retransmission [] s1=2 & cd1=9 -> 1/512 : (s1'=3) & (x1'=0*slot) + 1/512 : (s1'=3) & (x1'=1*slot) + 1/512 : (s1'=3) & (x1'=2*slot) + 1/512 : (s1'=3) & (x1'=3*slot) + 1/512 : (s1'=3) & (x1'=4*slot) + 1/512 : (s1'=3) & (x1'=5*slot) + 1/512 : (s1'=3) & (x1'=6*slot) + 1/512 : (s1'=3) & (x1'=7*slot) + 1/512 : (s1'=3) & (x1'=8*slot) + 1/512 : (s1'=3) & (x1'=9*slot) + 1/512 : (s1'=3) & (x1'=10*slot) + 1/512 : (s1'=3) & (x1'=11*slot) + 1/512 : (s1'=3) & (x1'=12*slot) + 1/512 : (s1'=3) & (x1'=13*slot) + 1/512 : (s1'=3) & (x1'=14*slot) + 1/512 : (s1'=3) & (x1'=15*slot) + 1/512 : (s1'=3) & (x1'=16*slot) + 1/512 : (s1'=3) & (x1'=17*slot) + 1/512 : (s1'=3) & (x1'=18*slot) + 1/512 : (s1'=3) & (x1'=19*slot) + 1/512 : (s1'=3) & (x1'=20*slot) + 1/512 : (s1'=3) & (x1'=21*slot) + 1/512 : (s1'=3) & (x1'=22*slot) + 1/512 : (s1'=3) & (x1'=23*slot) + 1/512 : (s1'=3) & (x1'=24*slot) + 1/512 : (s1'=3) & (x1'=25*slot) + 1/512 : (s1'=3) & (x1'=26*slot) + 1/512 : (s1'=3) & (x1'=27*slot) + 1/512 : (s1'=3) & (x1'=28*slot) + 1/512 : (s1'=3) & (x1'=29*slot) + 1/512 : (s1'=3) & (x1'=30*slot) + 1/512 : (s1'=3) & (x1'=31*slot) + 1/512 : (s1'=3) & (x1'=32*slot) + 1/512 : (s1'=3) & (x1'=33*slot) + 1/512 : (s1'=3) & (x1'=34*slot) + 1/512 : (s1'=3) & (x1'=35*slot) + 1/512 : (s1'=3) & (x1'=36*slot) + 1/512 : (s1'=3) & (x1'=37*slot) + 1/512 : (s1'=3) & (x1'=38*slot) + 1/512 : (s1'=3) & (x1'=39*slot) + 1/512 : (s1'=3) & (x1'=40*slot) + 1/512 : (s1'=3) & (x1'=41*slot) + 1/512 : (s1'=3) & (x1'=42*slot) + 1/512 : (s1'=3) & (x1'=43*slot) + 1/512 : (s1'=3) & (x1'=44*slot) + 1/512 : (s1'=3) & (x1'=45*slot) + 1/512 : (s1'=3) & (x1'=46*slot) + 1/512 : (s1'=3) & (x1'=47*slot) + 1/512 : (s1'=3) & (x1'=48*slot) + 1/512 : (s1'=3) & (x1'=49*slot) + 1/512 : (s1'=3) & (x1'=50*slot) + 1/512 : (s1'=3) & (x1'=51*slot) + 1/512 : (s1'=3) & (x1'=52*slot) + 1/512 : (s1'=3) & (x1'=53*slot) + 1/512 : (s1'=3) & (x1'=54*slot) + 1/512 : (s1'=3) & (x1'=55*slot) + 1/512 : (s1'=3) & (x1'=56*slot) + 1/512 : (s1'=3) & (x1'=57*slot) + 1/512 : (s1'=3) & (x1'=58*slot) + 1/512 : (s1'=3) & (x1'=59*slot) + 1/512 : (s1'=3) & (x1'=60*slot) + 1/512 : (s1'=3) & (x1'=61*slot) + 1/512 : (s1'=3) & (x1'=62*slot) + 1/512 : (s1'=3) & (x1'=63*slot) + 1/512 : (s1'=3) & (x1'=64*slot) + 1/512 : (s1'=3) & (x1'=65*slot) + 1/512 : (s1'=3) & (x1'=66*slot) + 1/512 : (s1'=3) & (x1'=67*slot) + 1/512 : (s1'=3) & (x1'=68*slot) + 1/512 : (s1'=3) & (x1'=69*slot) + 1/512 : (s1'=3) & (x1'=70*slot) + 1/512 : (s1'=3) & (x1'=71*slot) + 1/512 : (s1'=3) & (x1'=72*slot) + 1/512 : (s1'=3) & (x1'=73*slot) + 1/512 : (s1'=3) & (x1'=74*slot) + 1/512 : (s1'=3) & (x1'=75*slot) + 1/512 : (s1'=3) & (x1'=76*slot) + 1/512 : (s1'=3) & (x1'=77*slot) + 1/512 : (s1'=3) & (x1'=78*slot) + 1/512 : (s1'=3) & (x1'=79*slot) + 1/512 : (s1'=3) & (x1'=80*slot) + 1/512 : (s1'=3) & (x1'=81*slot) + 1/512 : (s1'=3) & (x1'=82*slot) + 1/512 : (s1'=3) & (x1'=83*slot) + 1/512 : (s1'=3) & (x1'=84*slot) + 1/512 : (s1'=3) & (x1'=85*slot) + 1/512 : (s1'=3) & (x1'=86*slot) + 1/512 : (s1'=3) & (x1'=87*slot) + 1/512 : (s1'=3) & (x1'=88*slot) + 1/512 : (s1'=3) & (x1'=89*slot) + 1/512 : (s1'=3) & (x1'=90*slot) + 1/512 : (s1'=3) & (x1'=91*slot) + 1/512 : (s1'=3) & (x1'=92*slot) + 1/512 : (s1'=3) & (x1'=93*slot) + 1/512 : (s1'=3) & (x1'=94*slot) + 1/512 : (s1'=3) & (x1'=95*slot) + 1/512 : (s1'=3) & (x1'=96*slot) + 1/512 : (s1'=3) & (x1'=97*slot) + 1/512 : (s1'=3) & (x1'=98*slot) + 1/512 : (s1'=3) & (x1'=99*slot) + 1/512 : (s1'=3) & (x1'=100*slot) + 1/512 : (s1'=3) & (x1'=101*slot) + 1/512 : (s1'=3) & (x1'=102*slot) + 1/512 : (s1'=3) & (x1'=103*slot) + 1/512 : (s1'=3) & (x1'=104*slot) + 1/512 : (s1'=3) & (x1'=105*slot) + 1/512 : (s1'=3) & (x1'=106*slot) + 1/512 : (s1'=3) & (x1'=107*slot) + 1/512 : (s1'=3) & (x1'=108*slot) + 1/512 : (s1'=3) & (x1'=109*slot) + 1/512 : (s1'=3) & (x1'=110*slot) + 1/512 : (s1'=3) & (x1'=111*slot) + 1/512 : (s1'=3) & (x1'=112*slot) + 1/512 : (s1'=3) & (x1'=113*slot) + 1/512 : (s1'=3) & (x1'=114*slot) + 1/512 : (s1'=3) & (x1'=115*slot) + 1/512 : (s1'=3) & (x1'=116*slot) + 1/512 : (s1'=3) & (x1'=117*slot) + 1/512 : (s1'=3) & (x1'=118*slot) + 1/512 : (s1'=3) & (x1'=119*slot) + 1/512 : (s1'=3) & (x1'=120*slot) + 1/512 : (s1'=3) & (x1'=121*slot) + 1/512 : (s1'=3) & (x1'=122*slot) + 1/512 : (s1'=3) & (x1'=123*slot) + 1/512 : (s1'=3) & (x1'=124*slot) + 1/512 : (s1'=3) & (x1'=125*slot) + 1/512 : (s1'=3) & (x1'=126*slot) + 1/512 : (s1'=3) & (x1'=127*slot) + 1/512 : (s1'=3) & (x1'=128*slot) + 1/512 : (s1'=3) & (x1'=129*slot) + 1/512 : (s1'=3) & (x1'=130*slot) + 1/512 : (s1'=3) & (x1'=131*slot) + 1/512 : (s1'=3) & (x1'=132*slot) + 1/512 : (s1'=3) & (x1'=133*slot) + 1/512 : (s1'=3) & (x1'=134*slot) + 1/512 : (s1'=3) & (x1'=135*slot) + 1/512 : (s1'=3) & (x1'=136*slot) + 1/512 : (s1'=3) & (x1'=137*slot) + 1/512 : (s1'=3) & (x1'=138*slot) + 1/512 : (s1'=3) & (x1'=139*slot) + 1/512 : (s1'=3) & (x1'=140*slot) + 1/512 : (s1'=3) & (x1'=141*slot) + 1/512 : (s1'=3) & (x1'=142*slot) + 1/512 : (s1'=3) & (x1'=143*slot) + 1/512 : (s1'=3) & (x1'=144*slot) + 1/512 : (s1'=3) & (x1'=145*slot) + 1/512 : (s1'=3) & (x1'=146*slot) + 1/512 : (s1'=3) & (x1'=147*slot) + 1/512 : (s1'=3) & (x1'=148*slot) + 1/512 : (s1'=3) & (x1'=149*slot) + 1/512 : (s1'=3) & (x1'=150*slot) + 1/512 : (s1'=3) & (x1'=151*slot) + 1/512 : (s1'=3) & (x1'=152*slot) + 1/512 : (s1'=3) & (x1'=153*slot) + 1/512 : (s1'=3) & (x1'=154*slot) + 1/512 : (s1'=3) & (x1'=155*slot) + 1/512 : (s1'=3) & (x1'=156*slot) + 1/512 : (s1'=3) & (x1'=157*slot) + 1/512 : (s1'=3) & (x1'=158*slot) + 1/512 : (s1'=3) & (x1'=159*slot) + 1/512 : (s1'=3) & (x1'=160*slot) + 1/512 : (s1'=3) & (x1'=161*slot) + 1/512 : (s1'=3) & (x1'=162*slot) + 1/512 : (s1'=3) & (x1'=163*slot) + 1/512 : (s1'=3) & (x1'=164*slot) + 1/512 : (s1'=3) & (x1'=165*slot) + 1/512 : (s1'=3) & (x1'=166*slot) + 1/512 : (s1'=3) & (x1'=167*slot) + 1/512 : (s1'=3) & (x1'=168*slot) + 1/512 : (s1'=3) & (x1'=169*slot) + 1/512 : (s1'=3) & (x1'=170*slot) + 1/512 : (s1'=3) & (x1'=171*slot) + 1/512 : (s1'=3) & (x1'=172*slot) + 1/512 : (s1'=3) & (x1'=173*slot) + 1/512 : (s1'=3) & (x1'=174*slot) + 1/512 : (s1'=3) & (x1'=175*slot) + 1/512 : (s1'=3) & (x1'=176*slot) + 1/512 : (s1'=3) & (x1'=177*slot) + 1/512 : (s1'=3) & (x1'=178*slot) + 1/512 : (s1'=3) & (x1'=179*slot) + 1/512 : (s1'=3) & (x1'=180*slot) + 1/512 : (s1'=3) & (x1'=181*slot) + 1/512 : (s1'=3) & (x1'=182*slot) + 1/512 : (s1'=3) & (x1'=183*slot) + 1/512 : (s1'=3) & (x1'=184*slot) + 1/512 : (s1'=3) & (x1'=185*slot) + 1/512 : (s1'=3) & (x1'=186*slot) + 1/512 : (s1'=3) & (x1'=187*slot) + 1/512 : (s1'=3) & (x1'=188*slot) + 1/512 : (s1'=3) & (x1'=189*slot) + 1/512 : (s1'=3) & (x1'=190*slot) + 1/512 : (s1'=3) & (x1'=191*slot) + 1/512 : (s1'=3) & (x1'=192*slot) + 1/512 : (s1'=3) & (x1'=193*slot) + 1/512 : (s1'=3) & (x1'=194*slot) + 1/512 : (s1'=3) & (x1'=195*slot) + 1/512 : (s1'=3) & (x1'=196*slot) + 1/512 : (s1'=3) & (x1'=197*slot) + 1/512 : (s1'=3) & (x1'=198*slot) + 1/512 : (s1'=3) & (x1'=199*slot) + 1/512 : (s1'=3) & (x1'=200*slot) + 1/512 : (s1'=3) & (x1'=201*slot) + 1/512 : (s1'=3) & (x1'=202*slot) + 1/512 : (s1'=3) & (x1'=203*slot) + 1/512 : (s1'=3) & (x1'=204*slot) + 1/512 : (s1'=3) & (x1'=205*slot) + 1/512 : (s1'=3) & (x1'=206*slot) + 1/512 : (s1'=3) & (x1'=207*slot) + 1/512 : (s1'=3) & (x1'=208*slot) + 1/512 : (s1'=3) & (x1'=209*slot) + 1/512 : (s1'=3) & (x1'=210*slot) + 1/512 : (s1'=3) & (x1'=211*slot) + 1/512 : (s1'=3) & (x1'=212*slot) + 1/512 : (s1'=3) & (x1'=213*slot) + 1/512 : (s1'=3) & (x1'=214*slot) + 1/512 : (s1'=3) & (x1'=215*slot) + 1/512 : (s1'=3) & (x1'=216*slot) + 1/512 : (s1'=3) & (x1'=217*slot) + 1/512 : (s1'=3) & (x1'=218*slot) + 1/512 : (s1'=3) & (x1'=219*slot) + 1/512 : (s1'=3) & (x1'=220*slot) + 1/512 : (s1'=3) & (x1'=221*slot) + 1/512 : (s1'=3) & (x1'=222*slot) + 1/512 : (s1'=3) & (x1'=223*slot) + 1/512 : (s1'=3) & (x1'=224*slot) + 1/512 : (s1'=3) & (x1'=225*slot) + 1/512 : (s1'=3) & (x1'=226*slot) + 1/512 : (s1'=3) & (x1'=227*slot) + 1/512 : (s1'=3) & (x1'=228*slot) + 1/512 : (s1'=3) & (x1'=229*slot) + 1/512 : (s1'=3) & (x1'=230*slot) + 1/512 : (s1'=3) & (x1'=231*slot) + 1/512 : (s1'=3) & (x1'=232*slot) + 1/512 : (s1'=3) & (x1'=233*slot) + 1/512 : (s1'=3) & (x1'=234*slot) + 1/512 : (s1'=3) & (x1'=235*slot) + 1/512 : (s1'=3) & (x1'=236*slot) + 1/512 : (s1'=3) & (x1'=237*slot) + 1/512 : (s1'=3) & (x1'=238*slot) + 1/512 : (s1'=3) & (x1'=239*slot) + 1/512 : (s1'=3) & (x1'=240*slot) + 1/512 : (s1'=3) & (x1'=241*slot) + 1/512 : (s1'=3) & (x1'=242*slot) + 1/512 : (s1'=3) & (x1'=243*slot) + 1/512 : (s1'=3) & (x1'=244*slot) + 1/512 : (s1'=3) & (x1'=245*slot) + 1/512 : (s1'=3) & (x1'=246*slot) + 1/512 : (s1'=3) & (x1'=247*slot) + 1/512 : (s1'=3) & (x1'=248*slot) + 1/512 : (s1'=3) & (x1'=249*slot) + 1/512 : (s1'=3) & (x1'=250*slot) + 1/512 : (s1'=3) & (x1'=251*slot) + 1/512 : (s1'=3) & (x1'=252*slot) + 1/512 : (s1'=3) & (x1'=253*slot) + 1/512 : (s1'=3) & (x1'=254*slot) + 1/512 : (s1'=3) & (x1'=255*slot) + 1/512 : (s1'=3) & (x1'=256*slot) + 1/512 : (s1'=3) & (x1'=257*slot) + 1/512 : (s1'=3) & (x1'=258*slot) + 1/512 : (s1'=3) & (x1'=259*slot) + 1/512 : (s1'=3) & (x1'=260*slot) + 1/512 : (s1'=3) & (x1'=261*slot) + 1/512 : (s1'=3) & (x1'=262*slot) + 1/512 : (s1'=3) & (x1'=263*slot) + 1/512 : (s1'=3) & (x1'=264*slot) + 1/512 : (s1'=3) & (x1'=265*slot) + 1/512 : (s1'=3) & (x1'=266*slot) + 1/512 : (s1'=3) & (x1'=267*slot) + 1/512 : (s1'=3) & (x1'=268*slot) + 1/512 : (s1'=3) & (x1'=269*slot) + 1/512 : (s1'=3) & (x1'=270*slot) + 1/512 : (s1'=3) & (x1'=271*slot) + 1/512 : (s1'=3) & (x1'=272*slot) + 1/512 : (s1'=3) & (x1'=273*slot) + 1/512 : (s1'=3) & (x1'=274*slot) + 1/512 : (s1'=3) & (x1'=275*slot) + 1/512 : (s1'=3) & (x1'=276*slot) + 1/512 : (s1'=3) & (x1'=277*slot) + 1/512 : (s1'=3) & (x1'=278*slot) + 1/512 : (s1'=3) & (x1'=279*slot) + 1/512 : (s1'=3) & (x1'=280*slot) + 1/512 : (s1'=3) & (x1'=281*slot) + 1/512 : (s1'=3) & (x1'=282*slot) + 1/512 : (s1'=3) & (x1'=283*slot) + 1/512 : (s1'=3) & (x1'=284*slot) + 1/512 : (s1'=3) & (x1'=285*slot) + 1/512 : (s1'=3) & (x1'=286*slot) + 1/512 : (s1'=3) & (x1'=287*slot) + 1/512 : (s1'=3) & (x1'=288*slot) + 1/512 : (s1'=3) & (x1'=289*slot) + 1/512 : (s1'=3) & (x1'=290*slot) + 1/512 : (s1'=3) & (x1'=291*slot) + 1/512 : (s1'=3) & (x1'=292*slot) + 1/512 : (s1'=3) & (x1'=293*slot) + 1/512 : (s1'=3) & (x1'=294*slot) + 1/512 : (s1'=3) & (x1'=295*slot) + 1/512 : (s1'=3) & (x1'=296*slot) + 1/512 : (s1'=3) & (x1'=297*slot) + 1/512 : (s1'=3) & (x1'=298*slot) + 1/512 : (s1'=3) & (x1'=299*slot) + 1/512 : (s1'=3) & (x1'=300*slot) + 1/512 : (s1'=3) & (x1'=301*slot) + 1/512 : (s1'=3) & (x1'=302*slot) + 1/512 : (s1'=3) & (x1'=303*slot) + 1/512 : (s1'=3) & (x1'=304*slot) + 1/512 : (s1'=3) & (x1'=305*slot) + 1/512 : (s1'=3) & (x1'=306*slot) + 1/512 : (s1'=3) & (x1'=307*slot) + 1/512 : (s1'=3) & (x1'=308*slot) + 1/512 : (s1'=3) & (x1'=309*slot) + 1/512 : (s1'=3) & (x1'=310*slot) + 1/512 : (s1'=3) & (x1'=311*slot) + 1/512 : (s1'=3) & (x1'=312*slot) + 1/512 : (s1'=3) & (x1'=313*slot) + 1/512 : (s1'=3) & (x1'=314*slot) + 1/512 : (s1'=3) & (x1'=315*slot) + 1/512 : (s1'=3) & (x1'=316*slot) + 1/512 : (s1'=3) & (x1'=317*slot) + 1/512 : (s1'=3) & (x1'=318*slot) + 1/512 : (s1'=3) & (x1'=319*slot) + 1/512 : (s1'=3) & (x1'=320*slot) + 1/512 : (s1'=3) & (x1'=321*slot) + 1/512 : (s1'=3) & (x1'=322*slot) + 1/512 : (s1'=3) & (x1'=323*slot) + 1/512 : (s1'=3) & (x1'=324*slot) + 1/512 : (s1'=3) & (x1'=325*slot) + 1/512 : (s1'=3) & (x1'=326*slot) + 1/512 : (s1'=3) & (x1'=327*slot) + 1/512 : (s1'=3) & (x1'=328*slot) + 1/512 : (s1'=3) & (x1'=329*slot) + 1/512 : (s1'=3) & (x1'=330*slot) + 1/512 : (s1'=3) & (x1'=331*slot) + 1/512 : (s1'=3) & (x1'=332*slot) + 1/512 : (s1'=3) & (x1'=333*slot) + 1/512 : (s1'=3) & (x1'=334*slot) + 1/512 : (s1'=3) & (x1'=335*slot) + 1/512 : (s1'=3) & (x1'=336*slot) + 1/512 : (s1'=3) & (x1'=337*slot) + 1/512 : (s1'=3) & (x1'=338*slot) + 1/512 : (s1'=3) & (x1'=339*slot) + 1/512 : (s1'=3) & (x1'=340*slot) + 1/512 : (s1'=3) & (x1'=341*slot) + 1/512 : (s1'=3) & (x1'=342*slot) + 1/512 : (s1'=3) & (x1'=343*slot) + 1/512 : (s1'=3) & (x1'=344*slot) + 1/512 : (s1'=3) & (x1'=345*slot) + 1/512 : (s1'=3) & (x1'=346*slot) + 1/512 : (s1'=3) & (x1'=347*slot) + 1/512 : (s1'=3) & (x1'=348*slot) + 1/512 : (s1'=3) & (x1'=349*slot) + 1/512 : (s1'=3) & (x1'=350*slot) + 1/512 : (s1'=3) & (x1'=351*slot) + 1/512 : (s1'=3) & (x1'=352*slot) + 1/512 : (s1'=3) & (x1'=353*slot) + 1/512 : (s1'=3) & (x1'=354*slot) + 1/512 : (s1'=3) & (x1'=355*slot) + 1/512 : (s1'=3) & (x1'=356*slot) + 1/512 : (s1'=3) & (x1'=357*slot) + 1/512 : (s1'=3) & (x1'=358*slot) + 1/512 : (s1'=3) & (x1'=359*slot) + 1/512 : (s1'=3) & (x1'=360*slot) + 1/512 : (s1'=3) & (x1'=361*slot) + 1/512 : (s1'=3) & (x1'=362*slot) + 1/512 : (s1'=3) & (x1'=363*slot) + 1/512 : (s1'=3) & (x1'=364*slot) + 1/512 : (s1'=3) & (x1'=365*slot) + 1/512 : (s1'=3) & (x1'=366*slot) + 1/512 : (s1'=3) & (x1'=367*slot) + 1/512 : (s1'=3) & (x1'=368*slot) + 1/512 : (s1'=3) & (x1'=369*slot) + 1/512 : (s1'=3) & (x1'=370*slot) + 1/512 : (s1'=3) & (x1'=371*slot) + 1/512 : (s1'=3) & (x1'=372*slot) + 1/512 : (s1'=3) & (x1'=373*slot) + 1/512 : (s1'=3) & (x1'=374*slot) + 1/512 : (s1'=3) & (x1'=375*slot) + 1/512 : (s1'=3) & (x1'=376*slot) + 1/512 : (s1'=3) & (x1'=377*slot) + 1/512 : (s1'=3) & (x1'=378*slot) + 1/512 : (s1'=3) & (x1'=379*slot) + 1/512 : (s1'=3) & (x1'=380*slot) + 1/512 : (s1'=3) & (x1'=381*slot) + 1/512 : (s1'=3) & (x1'=382*slot) + 1/512 : (s1'=3) & (x1'=383*slot) + 1/512 : (s1'=3) & (x1'=384*slot) + 1/512 : (s1'=3) & (x1'=385*slot) + 1/512 : (s1'=3) & (x1'=386*slot) + 1/512 : (s1'=3) & (x1'=387*slot) + 1/512 : (s1'=3) & (x1'=388*slot) + 1/512 : (s1'=3) & (x1'=389*slot) + 1/512 : (s1'=3) & (x1'=390*slot) + 1/512 : (s1'=3) & (x1'=391*slot) + 1/512 : (s1'=3) & (x1'=392*slot) + 1/512 : (s1'=3) & (x1'=393*slot) + 1/512 : (s1'=3) & (x1'=394*slot) + 1/512 : (s1'=3) & (x1'=395*slot) + 1/512 : (s1'=3) & (x1'=396*slot) + 1/512 : (s1'=3) & (x1'=397*slot) + 1/512 : (s1'=3) & (x1'=398*slot) + 1/512 : (s1'=3) & (x1'=399*slot) + 1/512 : (s1'=3) & (x1'=400*slot) + 1/512 : (s1'=3) & (x1'=401*slot) + 1/512 : (s1'=3) & (x1'=402*slot) + 1/512 : (s1'=3) & (x1'=403*slot) + 1/512 : (s1'=3) & (x1'=404*slot) + 1/512 : (s1'=3) & (x1'=405*slot) + 1/512 : (s1'=3) & (x1'=406*slot) + 1/512 : (s1'=3) & (x1'=407*slot) + 1/512 : (s1'=3) & (x1'=408*slot) + 1/512 : (s1'=3) & (x1'=409*slot) + 1/512 : (s1'=3) & (x1'=410*slot) + 1/512 : (s1'=3) & (x1'=411*slot) + 1/512 : (s1'=3) & (x1'=412*slot) + 1/512 : (s1'=3) & (x1'=413*slot) + 1/512 : (s1'=3) & (x1'=414*slot) + 1/512 : (s1'=3) & (x1'=415*slot) + 1/512 : (s1'=3) & (x1'=416*slot) + 1/512 : (s1'=3) & (x1'=417*slot) + 1/512 : (s1'=3) & (x1'=418*slot) + 1/512 : (s1'=3) & (x1'=419*slot) + 1/512 : (s1'=3) & (x1'=420*slot) + 1/512 : (s1'=3) & (x1'=421*slot) + 1/512 : (s1'=3) & (x1'=422*slot) + 1/512 : (s1'=3) & (x1'=423*slot) + 1/512 : (s1'=3) & (x1'=424*slot) + 1/512 : (s1'=3) & (x1'=425*slot) + 1/512 : (s1'=3) & (x1'=426*slot) + 1/512 : (s1'=3) & (x1'=427*slot) + 1/512 : (s1'=3) & (x1'=428*slot) + 1/512 : (s1'=3) & (x1'=429*slot) + 1/512 : (s1'=3) & (x1'=430*slot) + 1/512 : (s1'=3) & (x1'=431*slot) + 1/512 : (s1'=3) & (x1'=432*slot) + 1/512 : (s1'=3) & (x1'=433*slot) + 1/512 : (s1'=3) & (x1'=434*slot) + 1/512 : (s1'=3) & (x1'=435*slot) + 1/512 : (s1'=3) & (x1'=436*slot) + 1/512 : (s1'=3) & (x1'=437*slot) + 1/512 : (s1'=3) & (x1'=438*slot) + 1/512 : (s1'=3) & (x1'=439*slot) + 1/512 : (s1'=3) & (x1'=440*slot) + 1/512 : (s1'=3) & (x1'=441*slot) + 1/512 : (s1'=3) & (x1'=442*slot) + 1/512 : (s1'=3) & (x1'=443*slot) + 1/512 : (s1'=3) & (x1'=444*slot) + 1/512 : (s1'=3) & (x1'=445*slot) + 1/512 : (s1'=3) & (x1'=446*slot) + 1/512 : (s1'=3) & (x1'=447*slot) + 1/512 : (s1'=3) & (x1'=448*slot) + 1/512 : (s1'=3) & (x1'=449*slot) + 1/512 : (s1'=3) & (x1'=450*slot) + 1/512 : (s1'=3) & (x1'=451*slot) + 1/512 : (s1'=3) & (x1'=452*slot) + 1/512 : (s1'=3) & (x1'=453*slot) + 1/512 : (s1'=3) & (x1'=454*slot) + 1/512 : (s1'=3) & (x1'=455*slot) + 1/512 : (s1'=3) & (x1'=456*slot) + 1/512 : (s1'=3) & (x1'=457*slot) + 1/512 : (s1'=3) & (x1'=458*slot) + 1/512 : (s1'=3) & (x1'=459*slot) + 1/512 : (s1'=3) & (x1'=460*slot) + 1/512 : (s1'=3) & (x1'=461*slot) + 1/512 : (s1'=3) & (x1'=462*slot) + 1/512 : (s1'=3) & (x1'=463*slot) + 1/512 : (s1'=3) & (x1'=464*slot) + 1/512 : (s1'=3) & (x1'=465*slot) + 1/512 : (s1'=3) & (x1'=466*slot) + 1/512 : (s1'=3) & (x1'=467*slot) + 1/512 : (s1'=3) & (x1'=468*slot) + 1/512 : (s1'=3) & (x1'=469*slot) + 1/512 : (s1'=3) & (x1'=470*slot) + 1/512 : (s1'=3) & (x1'=471*slot) + 1/512 : (s1'=3) & (x1'=472*slot) + 1/512 : (s1'=3) & (x1'=473*slot) + 1/512 : (s1'=3) & (x1'=474*slot) + 1/512 : (s1'=3) & (x1'=475*slot) + 1/512 : (s1'=3) & (x1'=476*slot) + 1/512 : (s1'=3) & (x1'=477*slot) + 1/512 : (s1'=3) & (x1'=478*slot) + 1/512 : (s1'=3) & (x1'=479*slot) + 1/512 : (s1'=3) & (x1'=480*slot) + 1/512 : (s1'=3) & (x1'=481*slot) + 1/512 : (s1'=3) & (x1'=482*slot) + 1/512 : (s1'=3) & (x1'=483*slot) + 1/512 : (s1'=3) & (x1'=484*slot) + 1/512 : (s1'=3) & (x1'=485*slot) + 1/512 : (s1'=3) & (x1'=486*slot) + 1/512 : (s1'=3) & (x1'=487*slot) + 1/512 : (s1'=3) & (x1'=488*slot) + 1/512 : (s1'=3) & (x1'=489*slot) + 1/512 : (s1'=3) & (x1'=490*slot) + 1/512 : (s1'=3) & (x1'=491*slot) + 1/512 : (s1'=3) & (x1'=492*slot) + 1/512 : (s1'=3) & (x1'=493*slot) + 1/512 : (s1'=3) & (x1'=494*slot) + 1/512 : (s1'=3) & (x1'=495*slot) + 1/512 : (s1'=3) & (x1'=496*slot) + 1/512 : (s1'=3) & (x1'=497*slot) + 1/512 : (s1'=3) & (x1'=498*slot) + 1/512 : (s1'=3) & (x1'=499*slot) + 1/512 : (s1'=3) & (x1'=500*slot) + 1/512 : (s1'=3) & (x1'=501*slot) + 1/512 : (s1'=3) & (x1'=502*slot) + 1/512 : (s1'=3) & (x1'=503*slot) + 1/512 : (s1'=3) & (x1'=504*slot) + 1/512 : (s1'=3) & (x1'=505*slot) + 1/512 : (s1'=3) & (x1'=506*slot) + 1/512 : (s1'=3) & (x1'=507*slot) + 1/512 : (s1'=3) & (x1'=508*slot) + 1/512 : (s1'=3) & (x1'=509*slot) + 1/512 : (s1'=3) & (x1'=510*slot) + 1/512 : (s1'=3) & (x1'=511*slot); // tenth (or more) retransmission [] s1=2 & cd1=10 -> 1/1024 : (s1'=3) & (x1'=0*slot) + 1/1024 : (s1'=3) & (x1'=1*slot) + 1/1024 : (s1'=3) & (x1'=2*slot) + 1/1024 : (s1'=3) & (x1'=3*slot) + 1/1024 : (s1'=3) & (x1'=4*slot) + 1/1024 : (s1'=3) & (x1'=5*slot) + 1/1024 : (s1'=3) & (x1'=6*slot) + 1/1024 : (s1'=3) & (x1'=7*slot) + 1/1024 : (s1'=3) & (x1'=8*slot) + 1/1024 : (s1'=3) & (x1'=9*slot) + 1/1024 : (s1'=3) & (x1'=10*slot) + 1/1024 : (s1'=3) & (x1'=11*slot) + 1/1024 : (s1'=3) & (x1'=12*slot) + 1/1024 : (s1'=3) & (x1'=13*slot) + 1/1024 : (s1'=3) & (x1'=14*slot) + 1/1024 : (s1'=3) & (x1'=15*slot) + 1/1024 : (s1'=3) & (x1'=16*slot) + 1/1024 : (s1'=3) & (x1'=17*slot) + 1/1024 : (s1'=3) & (x1'=18*slot) + 1/1024 : (s1'=3) & (x1'=19*slot) + 1/1024 : (s1'=3) & (x1'=20*slot) + 1/1024 : (s1'=3) & (x1'=21*slot) + 1/1024 : (s1'=3) & (x1'=22*slot) + 1/1024 : (s1'=3) & (x1'=23*slot) + 1/1024 : (s1'=3) & (x1'=24*slot) + 1/1024 : (s1'=3) & (x1'=25*slot) + 1/1024 : (s1'=3) & (x1'=26*slot) + 1/1024 : (s1'=3) & (x1'=27*slot) + 1/1024 : (s1'=3) & (x1'=28*slot) + 1/1024 : (s1'=3) & (x1'=29*slot) + 1/1024 : (s1'=3) & (x1'=30*slot) + 1/1024 : (s1'=3) & (x1'=31*slot) + 1/1024 : (s1'=3) & (x1'=32*slot) + 1/1024 : (s1'=3) & (x1'=33*slot) + 1/1024 : (s1'=3) & (x1'=34*slot) + 1/1024 : (s1'=3) & (x1'=35*slot) + 1/1024 : (s1'=3) & (x1'=36*slot) + 1/1024 : (s1'=3) & (x1'=37*slot) + 1/1024 : (s1'=3) & (x1'=38*slot) + 1/1024 : (s1'=3) & (x1'=39*slot) + 1/1024 : (s1'=3) & (x1'=40*slot) + 1/1024 : (s1'=3) & (x1'=41*slot) + 1/1024 : (s1'=3) & (x1'=42*slot) + 1/1024 : (s1'=3) & (x1'=43*slot) + 1/1024 : (s1'=3) & (x1'=44*slot) + 1/1024 : (s1'=3) & (x1'=45*slot) + 1/1024 : (s1'=3) & (x1'=46*slot) + 1/1024 : (s1'=3) & (x1'=47*slot) + 1/1024 : (s1'=3) & (x1'=48*slot) + 1/1024 : (s1'=3) & (x1'=49*slot) + 1/1024 : (s1'=3) & (x1'=50*slot) + 1/1024 : (s1'=3) & (x1'=51*slot) + 1/1024 : (s1'=3) & (x1'=52*slot) + 1/1024 : (s1'=3) & (x1'=53*slot) + 1/1024 : (s1'=3) & (x1'=54*slot) + 1/1024 : (s1'=3) & (x1'=55*slot) + 1/1024 : (s1'=3) & (x1'=56*slot) + 1/1024 : (s1'=3) & (x1'=57*slot) + 1/1024 : (s1'=3) & (x1'=58*slot) + 1/1024 : (s1'=3) & (x1'=59*slot) + 1/1024 : (s1'=3) & (x1'=60*slot) + 1/1024 : (s1'=3) & (x1'=61*slot) + 1/1024 : (s1'=3) & (x1'=62*slot) + 1/1024 : (s1'=3) & (x1'=63*slot) + 1/1024 : (s1'=3) & (x1'=64*slot) + 1/1024 : (s1'=3) & (x1'=65*slot) + 1/1024 : (s1'=3) & (x1'=66*slot) + 1/1024 : (s1'=3) & (x1'=67*slot) + 1/1024 : (s1'=3) & (x1'=68*slot) + 1/1024 : (s1'=3) & (x1'=69*slot) + 1/1024 : (s1'=3) & (x1'=70*slot) + 1/1024 : (s1'=3) & (x1'=71*slot) + 1/1024 : (s1'=3) & (x1'=72*slot) + 1/1024 : (s1'=3) & (x1'=73*slot) + 1/1024 : (s1'=3) & (x1'=74*slot) + 1/1024 : (s1'=3) & (x1'=75*slot) + 1/1024 : (s1'=3) & (x1'=76*slot) + 1/1024 : (s1'=3) & (x1'=77*slot) + 1/1024 : (s1'=3) & (x1'=78*slot) + 1/1024 : (s1'=3) & (x1'=79*slot) + 1/1024 : (s1'=3) & (x1'=80*slot) + 1/1024 : (s1'=3) & (x1'=81*slot) + 1/1024 : (s1'=3) & (x1'=82*slot) + 1/1024 : (s1'=3) & (x1'=83*slot) + 1/1024 : (s1'=3) & (x1'=84*slot) + 1/1024 : (s1'=3) & (x1'=85*slot) + 1/1024 : (s1'=3) & (x1'=86*slot) + 1/1024 : (s1'=3) & (x1'=87*slot) + 1/1024 : (s1'=3) & (x1'=88*slot) + 1/1024 : (s1'=3) & (x1'=89*slot) + 1/1024 : (s1'=3) & (x1'=90*slot) + 1/1024 : (s1'=3) & (x1'=91*slot) + 1/1024 : (s1'=3) & (x1'=92*slot) + 1/1024 : (s1'=3) & (x1'=93*slot) + 1/1024 : (s1'=3) & (x1'=94*slot) + 1/1024 : (s1'=3) & (x1'=95*slot) + 1/1024 : (s1'=3) & (x1'=96*slot) + 1/1024 : (s1'=3) & (x1'=97*slot) + 1/1024 : (s1'=3) & (x1'=98*slot) + 1/1024 : (s1'=3) & (x1'=99*slot) + 1/1024 : (s1'=3) & (x1'=100*slot) + 1/1024 : (s1'=3) & (x1'=101*slot) + 1/1024 : (s1'=3) & (x1'=102*slot) + 1/1024 : (s1'=3) & (x1'=103*slot) + 1/1024 : (s1'=3) & (x1'=104*slot) + 1/1024 : (s1'=3) & (x1'=105*slot) + 1/1024 : (s1'=3) & (x1'=106*slot) + 1/1024 : (s1'=3) & (x1'=107*slot) + 1/1024 : (s1'=3) & (x1'=108*slot) + 1/1024 : (s1'=3) & (x1'=109*slot) + 1/1024 : (s1'=3) & (x1'=110*slot) + 1/1024 : (s1'=3) & (x1'=111*slot) + 1/1024 : (s1'=3) & (x1'=112*slot) + 1/1024 : (s1'=3) & (x1'=113*slot) + 1/1024 : (s1'=3) & (x1'=114*slot) + 1/1024 : (s1'=3) & (x1'=115*slot) + 1/1024 : (s1'=3) & (x1'=116*slot) + 1/1024 : (s1'=3) & (x1'=117*slot) + 1/1024 : (s1'=3) & (x1'=118*slot) + 1/1024 : (s1'=3) & (x1'=119*slot) + 1/1024 : (s1'=3) & (x1'=120*slot) + 1/1024 : (s1'=3) & (x1'=121*slot) + 1/1024 : (s1'=3) & (x1'=122*slot) + 1/1024 : (s1'=3) & (x1'=123*slot) + 1/1024 : (s1'=3) & (x1'=124*slot) + 1/1024 : (s1'=3) & (x1'=125*slot) + 1/1024 : (s1'=3) & (x1'=126*slot) + 1/1024 : (s1'=3) & (x1'=127*slot) + 1/1024 : (s1'=3) & (x1'=128*slot) + 1/1024 : (s1'=3) & (x1'=129*slot) + 1/1024 : (s1'=3) & (x1'=130*slot) + 1/1024 : (s1'=3) & (x1'=131*slot) + 1/1024 : (s1'=3) & (x1'=132*slot) + 1/1024 : (s1'=3) & (x1'=133*slot) + 1/1024 : (s1'=3) & (x1'=134*slot) + 1/1024 : (s1'=3) & (x1'=135*slot) + 1/1024 : (s1'=3) & (x1'=136*slot) + 1/1024 : (s1'=3) & (x1'=137*slot) + 1/1024 : (s1'=3) & (x1'=138*slot) + 1/1024 : (s1'=3) & (x1'=139*slot) + 1/1024 : (s1'=3) & (x1'=140*slot) + 1/1024 : (s1'=3) & (x1'=141*slot) + 1/1024 : (s1'=3) & (x1'=142*slot) + 1/1024 : (s1'=3) & (x1'=143*slot) + 1/1024 : (s1'=3) & (x1'=144*slot) + 1/1024 : (s1'=3) & (x1'=145*slot) + 1/1024 : (s1'=3) & (x1'=146*slot) + 1/1024 : (s1'=3) & (x1'=147*slot) + 1/1024 : (s1'=3) & (x1'=148*slot) + 1/1024 : (s1'=3) & (x1'=149*slot) + 1/1024 : (s1'=3) & (x1'=150*slot) + 1/1024 : (s1'=3) & (x1'=151*slot) + 1/1024 : (s1'=3) & (x1'=152*slot) + 1/1024 : (s1'=3) & (x1'=153*slot) + 1/1024 : (s1'=3) & (x1'=154*slot) + 1/1024 : (s1'=3) & (x1'=155*slot) + 1/1024 : (s1'=3) & (x1'=156*slot) + 1/1024 : (s1'=3) & (x1'=157*slot) + 1/1024 : (s1'=3) & (x1'=158*slot) + 1/1024 : (s1'=3) & (x1'=159*slot) + 1/1024 : (s1'=3) & (x1'=160*slot) + 1/1024 : (s1'=3) & (x1'=161*slot) + 1/1024 : (s1'=3) & (x1'=162*slot) + 1/1024 : (s1'=3) & (x1'=163*slot) + 1/1024 : (s1'=3) & (x1'=164*slot) + 1/1024 : (s1'=3) & (x1'=165*slot) + 1/1024 : (s1'=3) & (x1'=166*slot) + 1/1024 : (s1'=3) & (x1'=167*slot) + 1/1024 : (s1'=3) & (x1'=168*slot) + 1/1024 : (s1'=3) & (x1'=169*slot) + 1/1024 : (s1'=3) & (x1'=170*slot) + 1/1024 : (s1'=3) & (x1'=171*slot) + 1/1024 : (s1'=3) & (x1'=172*slot) + 1/1024 : (s1'=3) & (x1'=173*slot) + 1/1024 : (s1'=3) & (x1'=174*slot) + 1/1024 : (s1'=3) & (x1'=175*slot) + 1/1024 : (s1'=3) & (x1'=176*slot) + 1/1024 : (s1'=3) & (x1'=177*slot) + 1/1024 : (s1'=3) & (x1'=178*slot) + 1/1024 : (s1'=3) & (x1'=179*slot) + 1/1024 : (s1'=3) & (x1'=180*slot) + 1/1024 : (s1'=3) & (x1'=181*slot) + 1/1024 : (s1'=3) & (x1'=182*slot) + 1/1024 : (s1'=3) & (x1'=183*slot) + 1/1024 : (s1'=3) & (x1'=184*slot) + 1/1024 : (s1'=3) & (x1'=185*slot) + 1/1024 : (s1'=3) & (x1'=186*slot) + 1/1024 : (s1'=3) & (x1'=187*slot) + 1/1024 : (s1'=3) & (x1'=188*slot) + 1/1024 : (s1'=3) & (x1'=189*slot) + 1/1024 : (s1'=3) & (x1'=190*slot) + 1/1024 : (s1'=3) & (x1'=191*slot) + 1/1024 : (s1'=3) & (x1'=192*slot) + 1/1024 : (s1'=3) & (x1'=193*slot) + 1/1024 : (s1'=3) & (x1'=194*slot) + 1/1024 : (s1'=3) & (x1'=195*slot) + 1/1024 : (s1'=3) & (x1'=196*slot) + 1/1024 : (s1'=3) & (x1'=197*slot) + 1/1024 : (s1'=3) & (x1'=198*slot) + 1/1024 : (s1'=3) & (x1'=199*slot) + 1/1024 : (s1'=3) & (x1'=200*slot) + 1/1024 : (s1'=3) & (x1'=201*slot) + 1/1024 : (s1'=3) & (x1'=202*slot) + 1/1024 : (s1'=3) & (x1'=203*slot) + 1/1024 : (s1'=3) & (x1'=204*slot) + 1/1024 : (s1'=3) & (x1'=205*slot) + 1/1024 : (s1'=3) & (x1'=206*slot) + 1/1024 : (s1'=3) & (x1'=207*slot) + 1/1024 : (s1'=3) & (x1'=208*slot) + 1/1024 : (s1'=3) & (x1'=209*slot) + 1/1024 : (s1'=3) & (x1'=210*slot) + 1/1024 : (s1'=3) & (x1'=211*slot) + 1/1024 : (s1'=3) & (x1'=212*slot) + 1/1024 : (s1'=3) & (x1'=213*slot) + 1/1024 : (s1'=3) & (x1'=214*slot) + 1/1024 : (s1'=3) & (x1'=215*slot) + 1/1024 : (s1'=3) & (x1'=216*slot) + 1/1024 : (s1'=3) & (x1'=217*slot) + 1/1024 : (s1'=3) & (x1'=218*slot) + 1/1024 : (s1'=3) & (x1'=219*slot) + 1/1024 : (s1'=3) & (x1'=220*slot) + 1/1024 : (s1'=3) & (x1'=221*slot) + 1/1024 : (s1'=3) & (x1'=222*slot) + 1/1024 : (s1'=3) & (x1'=223*slot) + 1/1024 : (s1'=3) & (x1'=224*slot) + 1/1024 : (s1'=3) & (x1'=225*slot) + 1/1024 : (s1'=3) & (x1'=226*slot) + 1/1024 : (s1'=3) & (x1'=227*slot) + 1/1024 : (s1'=3) & (x1'=228*slot) + 1/1024 : (s1'=3) & (x1'=229*slot) + 1/1024 : (s1'=3) & (x1'=230*slot) + 1/1024 : (s1'=3) & (x1'=231*slot) + 1/1024 : (s1'=3) & (x1'=232*slot) + 1/1024 : (s1'=3) & (x1'=233*slot) + 1/1024 : (s1'=3) & (x1'=234*slot) + 1/1024 : (s1'=3) & (x1'=235*slot) + 1/1024 : (s1'=3) & (x1'=236*slot) + 1/1024 : (s1'=3) & (x1'=237*slot) + 1/1024 : (s1'=3) & (x1'=238*slot) + 1/1024 : (s1'=3) & (x1'=239*slot) + 1/1024 : (s1'=3) & (x1'=240*slot) + 1/1024 : (s1'=3) & (x1'=241*slot) + 1/1024 : (s1'=3) & (x1'=242*slot) + 1/1024 : (s1'=3) & (x1'=243*slot) + 1/1024 : (s1'=3) & (x1'=244*slot) + 1/1024 : (s1'=3) & (x1'=245*slot) + 1/1024 : (s1'=3) & (x1'=246*slot) + 1/1024 : (s1'=3) & (x1'=247*slot) + 1/1024 : (s1'=3) & (x1'=248*slot) + 1/1024 : (s1'=3) & (x1'=249*slot) + 1/1024 : (s1'=3) & (x1'=250*slot) + 1/1024 : (s1'=3) & (x1'=251*slot) + 1/1024 : (s1'=3) & (x1'=252*slot) + 1/1024 : (s1'=3) & (x1'=253*slot) + 1/1024 : (s1'=3) & (x1'=254*slot) + 1/1024 : (s1'=3) & (x1'=255*slot) + 1/1024 : (s1'=3) & (x1'=256*slot) + 1/1024 : (s1'=3) & (x1'=257*slot) + 1/1024 : (s1'=3) & (x1'=258*slot) + 1/1024 : (s1'=3) & (x1'=259*slot) + 1/1024 : (s1'=3) & (x1'=260*slot) + 1/1024 : (s1'=3) & (x1'=261*slot) + 1/1024 : (s1'=3) & (x1'=262*slot) + 1/1024 : (s1'=3) & (x1'=263*slot) + 1/1024 : (s1'=3) & (x1'=264*slot) + 1/1024 : (s1'=3) & (x1'=265*slot) + 1/1024 : (s1'=3) & (x1'=266*slot) + 1/1024 : (s1'=3) & (x1'=267*slot) + 1/1024 : (s1'=3) & (x1'=268*slot) + 1/1024 : (s1'=3) & (x1'=269*slot) + 1/1024 : (s1'=3) & (x1'=270*slot) + 1/1024 : (s1'=3) & (x1'=271*slot) + 1/1024 : (s1'=3) & (x1'=272*slot) + 1/1024 : (s1'=3) & (x1'=273*slot) + 1/1024 : (s1'=3) & (x1'=274*slot) + 1/1024 : (s1'=3) & (x1'=275*slot) + 1/1024 : (s1'=3) & (x1'=276*slot) + 1/1024 : (s1'=3) & (x1'=277*slot) + 1/1024 : (s1'=3) & (x1'=278*slot) + 1/1024 : (s1'=3) & (x1'=279*slot) + 1/1024 : (s1'=3) & (x1'=280*slot) + 1/1024 : (s1'=3) & (x1'=281*slot) + 1/1024 : (s1'=3) & (x1'=282*slot) + 1/1024 : (s1'=3) & (x1'=283*slot) + 1/1024 : (s1'=3) & (x1'=284*slot) + 1/1024 : (s1'=3) & (x1'=285*slot) + 1/1024 : (s1'=3) & (x1'=286*slot) + 1/1024 : (s1'=3) & (x1'=287*slot) + 1/1024 : (s1'=3) & (x1'=288*slot) + 1/1024 : (s1'=3) & (x1'=289*slot) + 1/1024 : (s1'=3) & (x1'=290*slot) + 1/1024 : (s1'=3) & (x1'=291*slot) + 1/1024 : (s1'=3) & (x1'=292*slot) + 1/1024 : (s1'=3) & (x1'=293*slot) + 1/1024 : (s1'=3) & (x1'=294*slot) + 1/1024 : (s1'=3) & (x1'=295*slot) + 1/1024 : (s1'=3) & (x1'=296*slot) + 1/1024 : (s1'=3) & (x1'=297*slot) + 1/1024 : (s1'=3) & (x1'=298*slot) + 1/1024 : (s1'=3) & (x1'=299*slot) + 1/1024 : (s1'=3) & (x1'=300*slot) + 1/1024 : (s1'=3) & (x1'=301*slot) + 1/1024 : (s1'=3) & (x1'=302*slot) + 1/1024 : (s1'=3) & (x1'=303*slot) + 1/1024 : (s1'=3) & (x1'=304*slot) + 1/1024 : (s1'=3) & (x1'=305*slot) + 1/1024 : (s1'=3) & (x1'=306*slot) + 1/1024 : (s1'=3) & (x1'=307*slot) + 1/1024 : (s1'=3) & (x1'=308*slot) + 1/1024 : (s1'=3) & (x1'=309*slot) + 1/1024 : (s1'=3) & (x1'=310*slot) + 1/1024 : (s1'=3) & (x1'=311*slot) + 1/1024 : (s1'=3) & (x1'=312*slot) + 1/1024 : (s1'=3) & (x1'=313*slot) + 1/1024 : (s1'=3) & (x1'=314*slot) + 1/1024 : (s1'=3) & (x1'=315*slot) + 1/1024 : (s1'=3) & (x1'=316*slot) + 1/1024 : (s1'=3) & (x1'=317*slot) + 1/1024 : (s1'=3) & (x1'=318*slot) + 1/1024 : (s1'=3) & (x1'=319*slot) + 1/1024 : (s1'=3) & (x1'=320*slot) + 1/1024 : (s1'=3) & (x1'=321*slot) + 1/1024 : (s1'=3) & (x1'=322*slot) + 1/1024 : (s1'=3) & (x1'=323*slot) + 1/1024 : (s1'=3) & (x1'=324*slot) + 1/1024 : (s1'=3) & (x1'=325*slot) + 1/1024 : (s1'=3) & (x1'=326*slot) + 1/1024 : (s1'=3) & (x1'=327*slot) + 1/1024 : (s1'=3) & (x1'=328*slot) + 1/1024 : (s1'=3) & (x1'=329*slot) + 1/1024 : (s1'=3) & (x1'=330*slot) + 1/1024 : (s1'=3) & (x1'=331*slot) + 1/1024 : (s1'=3) & (x1'=332*slot) + 1/1024 : (s1'=3) & (x1'=333*slot) + 1/1024 : (s1'=3) & (x1'=334*slot) + 1/1024 : (s1'=3) & (x1'=335*slot) + 1/1024 : (s1'=3) & (x1'=336*slot) + 1/1024 : (s1'=3) & (x1'=337*slot) + 1/1024 : (s1'=3) & (x1'=338*slot) + 1/1024 : (s1'=3) & (x1'=339*slot) + 1/1024 : (s1'=3) & (x1'=340*slot) + 1/1024 : (s1'=3) & (x1'=341*slot) + 1/1024 : (s1'=3) & (x1'=342*slot) + 1/1024 : (s1'=3) & (x1'=343*slot) + 1/1024 : (s1'=3) & (x1'=344*slot) + 1/1024 : (s1'=3) & (x1'=345*slot) + 1/1024 : (s1'=3) & (x1'=346*slot) + 1/1024 : (s1'=3) & (x1'=347*slot) + 1/1024 : (s1'=3) & (x1'=348*slot) + 1/1024 : (s1'=3) & (x1'=349*slot) + 1/1024 : (s1'=3) & (x1'=350*slot) + 1/1024 : (s1'=3) & (x1'=351*slot) + 1/1024 : (s1'=3) & (x1'=352*slot) + 1/1024 : (s1'=3) & (x1'=353*slot) + 1/1024 : (s1'=3) & (x1'=354*slot) + 1/1024 : (s1'=3) & (x1'=355*slot) + 1/1024 : (s1'=3) & (x1'=356*slot) + 1/1024 : (s1'=3) & (x1'=357*slot) + 1/1024 : (s1'=3) & (x1'=358*slot) + 1/1024 : (s1'=3) & (x1'=359*slot) + 1/1024 : (s1'=3) & (x1'=360*slot) + 1/1024 : (s1'=3) & (x1'=361*slot) + 1/1024 : (s1'=3) & (x1'=362*slot) + 1/1024 : (s1'=3) & (x1'=363*slot) + 1/1024 : (s1'=3) & (x1'=364*slot) + 1/1024 : (s1'=3) & (x1'=365*slot) + 1/1024 : (s1'=3) & (x1'=366*slot) + 1/1024 : (s1'=3) & (x1'=367*slot) + 1/1024 : (s1'=3) & (x1'=368*slot) + 1/1024 : (s1'=3) & (x1'=369*slot) + 1/1024 : (s1'=3) & (x1'=370*slot) + 1/1024 : (s1'=3) & (x1'=371*slot) + 1/1024 : (s1'=3) & (x1'=372*slot) + 1/1024 : (s1'=3) & (x1'=373*slot) + 1/1024 : (s1'=3) & (x1'=374*slot) + 1/1024 : (s1'=3) & (x1'=375*slot) + 1/1024 : (s1'=3) & (x1'=376*slot) + 1/1024 : (s1'=3) & (x1'=377*slot) + 1/1024 : (s1'=3) & (x1'=378*slot) + 1/1024 : (s1'=3) & (x1'=379*slot) + 1/1024 : (s1'=3) & (x1'=380*slot) + 1/1024 : (s1'=3) & (x1'=381*slot) + 1/1024 : (s1'=3) & (x1'=382*slot) + 1/1024 : (s1'=3) & (x1'=383*slot) + 1/1024 : (s1'=3) & (x1'=384*slot) + 1/1024 : (s1'=3) & (x1'=385*slot) + 1/1024 : (s1'=3) & (x1'=386*slot) + 1/1024 : (s1'=3) & (x1'=387*slot) + 1/1024 : (s1'=3) & (x1'=388*slot) + 1/1024 : (s1'=3) & (x1'=389*slot) + 1/1024 : (s1'=3) & (x1'=390*slot) + 1/1024 : (s1'=3) & (x1'=391*slot) + 1/1024 : (s1'=3) & (x1'=392*slot) + 1/1024 : (s1'=3) & (x1'=393*slot) + 1/1024 : (s1'=3) & (x1'=394*slot) + 1/1024 : (s1'=3) & (x1'=395*slot) + 1/1024 : (s1'=3) & (x1'=396*slot) + 1/1024 : (s1'=3) & (x1'=397*slot) + 1/1024 : (s1'=3) & (x1'=398*slot) + 1/1024 : (s1'=3) & (x1'=399*slot) + 1/1024 : (s1'=3) & (x1'=400*slot) + 1/1024 : (s1'=3) & (x1'=401*slot) + 1/1024 : (s1'=3) & (x1'=402*slot) + 1/1024 : (s1'=3) & (x1'=403*slot) + 1/1024 : (s1'=3) & (x1'=404*slot) + 1/1024 : (s1'=3) & (x1'=405*slot) + 1/1024 : (s1'=3) & (x1'=406*slot) + 1/1024 : (s1'=3) & (x1'=407*slot) + 1/1024 : (s1'=3) & (x1'=408*slot) + 1/1024 : (s1'=3) & (x1'=409*slot) + 1/1024 : (s1'=3) & (x1'=410*slot) + 1/1024 : (s1'=3) & (x1'=411*slot) + 1/1024 : (s1'=3) & (x1'=412*slot) + 1/1024 : (s1'=3) & (x1'=413*slot) + 1/1024 : (s1'=3) & (x1'=414*slot) + 1/1024 : (s1'=3) & (x1'=415*slot) + 1/1024 : (s1'=3) & (x1'=416*slot) + 1/1024 : (s1'=3) & (x1'=417*slot) + 1/1024 : (s1'=3) & (x1'=418*slot) + 1/1024 : (s1'=3) & (x1'=419*slot) + 1/1024 : (s1'=3) & (x1'=420*slot) + 1/1024 : (s1'=3) & (x1'=421*slot) + 1/1024 : (s1'=3) & (x1'=422*slot) + 1/1024 : (s1'=3) & (x1'=423*slot) + 1/1024 : (s1'=3) & (x1'=424*slot) + 1/1024 : (s1'=3) & (x1'=425*slot) + 1/1024 : (s1'=3) & (x1'=426*slot) + 1/1024 : (s1'=3) & (x1'=427*slot) + 1/1024 : (s1'=3) & (x1'=428*slot) + 1/1024 : (s1'=3) & (x1'=429*slot) + 1/1024 : (s1'=3) & (x1'=430*slot) + 1/1024 : (s1'=3) & (x1'=431*slot) + 1/1024 : (s1'=3) & (x1'=432*slot) + 1/1024 : (s1'=3) & (x1'=433*slot) + 1/1024 : (s1'=3) & (x1'=434*slot) + 1/1024 : (s1'=3) & (x1'=435*slot) + 1/1024 : (s1'=3) & (x1'=436*slot) + 1/1024 : (s1'=3) & (x1'=437*slot) + 1/1024 : (s1'=3) & (x1'=438*slot) + 1/1024 : (s1'=3) & (x1'=439*slot) + 1/1024 : (s1'=3) & (x1'=440*slot) + 1/1024 : (s1'=3) & (x1'=441*slot) + 1/1024 : (s1'=3) & (x1'=442*slot) + 1/1024 : (s1'=3) & (x1'=443*slot) + 1/1024 : (s1'=3) & (x1'=444*slot) + 1/1024 : (s1'=3) & (x1'=445*slot) + 1/1024 : (s1'=3) & (x1'=446*slot) + 1/1024 : (s1'=3) & (x1'=447*slot) + 1/1024 : (s1'=3) & (x1'=448*slot) + 1/1024 : (s1'=3) & (x1'=449*slot) + 1/1024 : (s1'=3) & (x1'=450*slot) + 1/1024 : (s1'=3) & (x1'=451*slot) + 1/1024 : (s1'=3) & (x1'=452*slot) + 1/1024 : (s1'=3) & (x1'=453*slot) + 1/1024 : (s1'=3) & (x1'=454*slot) + 1/1024 : (s1'=3) & (x1'=455*slot) + 1/1024 : (s1'=3) & (x1'=456*slot) + 1/1024 : (s1'=3) & (x1'=457*slot) + 1/1024 : (s1'=3) & (x1'=458*slot) + 1/1024 : (s1'=3) & (x1'=459*slot) + 1/1024 : (s1'=3) & (x1'=460*slot) + 1/1024 : (s1'=3) & (x1'=461*slot) + 1/1024 : (s1'=3) & (x1'=462*slot) + 1/1024 : (s1'=3) & (x1'=463*slot) + 1/1024 : (s1'=3) & (x1'=464*slot) + 1/1024 : (s1'=3) & (x1'=465*slot) + 1/1024 : (s1'=3) & (x1'=466*slot) + 1/1024 : (s1'=3) & (x1'=467*slot) + 1/1024 : (s1'=3) & (x1'=468*slot) + 1/1024 : (s1'=3) & (x1'=469*slot) + 1/1024 : (s1'=3) & (x1'=470*slot) + 1/1024 : (s1'=3) & (x1'=471*slot) + 1/1024 : (s1'=3) & (x1'=472*slot) + 1/1024 : (s1'=3) & (x1'=473*slot) + 1/1024 : (s1'=3) & (x1'=474*slot) + 1/1024 : (s1'=3) & (x1'=475*slot) + 1/1024 : (s1'=3) & (x1'=476*slot) + 1/1024 : (s1'=3) & (x1'=477*slot) + 1/1024 : (s1'=3) & (x1'=478*slot) + 1/1024 : (s1'=3) & (x1'=479*slot) + 1/1024 : (s1'=3) & (x1'=480*slot) + 1/1024 : (s1'=3) & (x1'=481*slot) + 1/1024 : (s1'=3) & (x1'=482*slot) + 1/1024 : (s1'=3) & (x1'=483*slot) + 1/1024 : (s1'=3) & (x1'=484*slot) + 1/1024 : (s1'=3) & (x1'=485*slot) + 1/1024 : (s1'=3) & (x1'=486*slot) + 1/1024 : (s1'=3) & (x1'=487*slot) + 1/1024 : (s1'=3) & (x1'=488*slot) + 1/1024 : (s1'=3) & (x1'=489*slot) + 1/1024 : (s1'=3) & (x1'=490*slot) + 1/1024 : (s1'=3) & (x1'=491*slot) + 1/1024 : (s1'=3) & (x1'=492*slot) + 1/1024 : (s1'=3) & (x1'=493*slot) + 1/1024 : (s1'=3) & (x1'=494*slot) + 1/1024 : (s1'=3) & (x1'=495*slot) + 1/1024 : (s1'=3) & (x1'=496*slot) + 1/1024 : (s1'=3) & (x1'=497*slot) + 1/1024 : (s1'=3) & (x1'=498*slot) + 1/1024 : (s1'=3) & (x1'=499*slot) + 1/1024 : (s1'=3) & (x1'=500*slot) + 1/1024 : (s1'=3) & (x1'=501*slot) + 1/1024 : (s1'=3) & (x1'=502*slot) + 1/1024 : (s1'=3) & (x1'=503*slot) + 1/1024 : (s1'=3) & (x1'=504*slot) + 1/1024 : (s1'=3) & (x1'=505*slot) + 1/1024 : (s1'=3) & (x1'=506*slot) + 1/1024 : (s1'=3) & (x1'=507*slot) + 1/1024 : (s1'=3) & (x1'=508*slot) + 1/1024 : (s1'=3) & (x1'=509*slot) + 1/1024 : (s1'=3) & (x1'=510*slot) + 1/1024 : (s1'=3) & (x1'=511*slot) + 1/1024 : (s1'=3) & (x1'=512*slot) + 1/1024 : (s1'=3) & (x1'=513*slot) + 1/1024 : (s1'=3) & (x1'=514*slot) + 1/1024 : (s1'=3) & (x1'=515*slot) + 1/1024 : (s1'=3) & (x1'=516*slot) + 1/1024 : (s1'=3) & (x1'=517*slot) + 1/1024 : (s1'=3) & (x1'=518*slot) + 1/1024 : (s1'=3) & (x1'=519*slot) + 1/1024 : (s1'=3) & (x1'=520*slot) + 1/1024 : (s1'=3) & (x1'=521*slot) + 1/1024 : (s1'=3) & (x1'=522*slot) + 1/1024 : (s1'=3) & (x1'=523*slot) + 1/1024 : (s1'=3) & (x1'=524*slot) + 1/1024 : (s1'=3) & (x1'=525*slot) + 1/1024 : (s1'=3) & (x1'=526*slot) + 1/1024 : (s1'=3) & (x1'=527*slot) + 1/1024 : (s1'=3) & (x1'=528*slot) + 1/1024 : (s1'=3) & (x1'=529*slot) + 1/1024 : (s1'=3) & (x1'=530*slot) + 1/1024 : (s1'=3) & (x1'=531*slot) + 1/1024 : (s1'=3) & (x1'=532*slot) + 1/1024 : (s1'=3) & (x1'=533*slot) + 1/1024 : (s1'=3) & (x1'=534*slot) + 1/1024 : (s1'=3) & (x1'=535*slot) + 1/1024 : (s1'=3) & (x1'=536*slot) + 1/1024 : (s1'=3) & (x1'=537*slot) + 1/1024 : (s1'=3) & (x1'=538*slot) + 1/1024 : (s1'=3) & (x1'=539*slot) + 1/1024 : (s1'=3) & (x1'=540*slot) + 1/1024 : (s1'=3) & (x1'=541*slot) + 1/1024 : (s1'=3) & (x1'=542*slot) + 1/1024 : (s1'=3) & (x1'=543*slot) + 1/1024 : (s1'=3) & (x1'=544*slot) + 1/1024 : (s1'=3) & (x1'=545*slot) + 1/1024 : (s1'=3) & (x1'=546*slot) + 1/1024 : (s1'=3) & (x1'=547*slot) + 1/1024 : (s1'=3) & (x1'=548*slot) + 1/1024 : (s1'=3) & (x1'=549*slot) + 1/1024 : (s1'=3) & (x1'=550*slot) + 1/1024 : (s1'=3) & (x1'=551*slot) + 1/1024 : (s1'=3) & (x1'=552*slot) + 1/1024 : (s1'=3) & (x1'=553*slot) + 1/1024 : (s1'=3) & (x1'=554*slot) + 1/1024 : (s1'=3) & (x1'=555*slot) + 1/1024 : (s1'=3) & (x1'=556*slot) + 1/1024 : (s1'=3) & (x1'=557*slot) + 1/1024 : (s1'=3) & (x1'=558*slot) + 1/1024 : (s1'=3) & (x1'=559*slot) + 1/1024 : (s1'=3) & (x1'=560*slot) + 1/1024 : (s1'=3) & (x1'=561*slot) + 1/1024 : (s1'=3) & (x1'=562*slot) + 1/1024 : (s1'=3) & (x1'=563*slot) + 1/1024 : (s1'=3) & (x1'=564*slot) + 1/1024 : (s1'=3) & (x1'=565*slot) + 1/1024 : (s1'=3) & (x1'=566*slot) + 1/1024 : (s1'=3) & (x1'=567*slot) + 1/1024 : (s1'=3) & (x1'=568*slot) + 1/1024 : (s1'=3) & (x1'=569*slot) + 1/1024 : (s1'=3) & (x1'=570*slot) + 1/1024 : (s1'=3) & (x1'=571*slot) + 1/1024 : (s1'=3) & (x1'=572*slot) + 1/1024 : (s1'=3) & (x1'=573*slot) + 1/1024 : (s1'=3) & (x1'=574*slot) + 1/1024 : (s1'=3) & (x1'=575*slot) + 1/1024 : (s1'=3) & (x1'=576*slot) + 1/1024 : (s1'=3) & (x1'=577*slot) + 1/1024 : (s1'=3) & (x1'=578*slot) + 1/1024 : (s1'=3) & (x1'=579*slot) + 1/1024 : (s1'=3) & (x1'=580*slot) + 1/1024 : (s1'=3) & (x1'=581*slot) + 1/1024 : (s1'=3) & (x1'=582*slot) + 1/1024 : (s1'=3) & (x1'=583*slot) + 1/1024 : (s1'=3) & (x1'=584*slot) + 1/1024 : (s1'=3) & (x1'=585*slot) + 1/1024 : (s1'=3) & (x1'=586*slot) + 1/1024 : (s1'=3) & (x1'=587*slot) + 1/1024 : (s1'=3) & (x1'=588*slot) + 1/1024 : (s1'=3) & (x1'=589*slot) + 1/1024 : (s1'=3) & (x1'=590*slot) + 1/1024 : (s1'=3) & (x1'=591*slot) + 1/1024 : (s1'=3) & (x1'=592*slot) + 1/1024 : (s1'=3) & (x1'=593*slot) + 1/1024 : (s1'=3) & (x1'=594*slot) + 1/1024 : (s1'=3) & (x1'=595*slot) + 1/1024 : (s1'=3) & (x1'=596*slot) + 1/1024 : (s1'=3) & (x1'=597*slot) + 1/1024 : (s1'=3) & (x1'=598*slot) + 1/1024 : (s1'=3) & (x1'=599*slot) + 1/1024 : (s1'=3) & (x1'=600*slot) + 1/1024 : (s1'=3) & (x1'=601*slot) + 1/1024 : (s1'=3) & (x1'=602*slot) + 1/1024 : (s1'=3) & (x1'=603*slot) + 1/1024 : (s1'=3) & (x1'=604*slot) + 1/1024 : (s1'=3) & (x1'=605*slot) + 1/1024 : (s1'=3) & (x1'=606*slot) + 1/1024 : (s1'=3) & (x1'=607*slot) + 1/1024 : (s1'=3) & (x1'=608*slot) + 1/1024 : (s1'=3) & (x1'=609*slot) + 1/1024 : (s1'=3) & (x1'=610*slot) + 1/1024 : (s1'=3) & (x1'=611*slot) + 1/1024 : (s1'=3) & (x1'=612*slot) + 1/1024 : (s1'=3) & (x1'=613*slot) + 1/1024 : (s1'=3) & (x1'=614*slot) + 1/1024 : (s1'=3) & (x1'=615*slot) + 1/1024 : (s1'=3) & (x1'=616*slot) + 1/1024 : (s1'=3) & (x1'=617*slot) + 1/1024 : (s1'=3) & (x1'=618*slot) + 1/1024 : (s1'=3) & (x1'=619*slot) + 1/1024 : (s1'=3) & (x1'=620*slot) + 1/1024 : (s1'=3) & (x1'=621*slot) + 1/1024 : (s1'=3) & (x1'=622*slot) + 1/1024 : (s1'=3) & (x1'=623*slot) + 1/1024 : (s1'=3) & (x1'=624*slot) + 1/1024 : (s1'=3) & (x1'=625*slot) + 1/1024 : (s1'=3) & (x1'=626*slot) + 1/1024 : (s1'=3) & (x1'=627*slot) + 1/1024 : (s1'=3) & (x1'=628*slot) + 1/1024 : (s1'=3) & (x1'=629*slot) + 1/1024 : (s1'=3) & (x1'=630*slot) + 1/1024 : (s1'=3) & (x1'=631*slot) + 1/1024 : (s1'=3) & (x1'=632*slot) + 1/1024 : (s1'=3) & (x1'=633*slot) + 1/1024 : (s1'=3) & (x1'=634*slot) + 1/1024 : (s1'=3) & (x1'=635*slot) + 1/1024 : (s1'=3) & (x1'=636*slot) + 1/1024 : (s1'=3) & (x1'=637*slot) + 1/1024 : (s1'=3) & (x1'=638*slot) + 1/1024 : (s1'=3) & (x1'=639*slot) + 1/1024 : (s1'=3) & (x1'=640*slot) + 1/1024 : (s1'=3) & (x1'=641*slot) + 1/1024 : (s1'=3) & (x1'=642*slot) + 1/1024 : (s1'=3) & (x1'=643*slot) + 1/1024 : (s1'=3) & (x1'=644*slot) + 1/1024 : (s1'=3) & (x1'=645*slot) + 1/1024 : (s1'=3) & (x1'=646*slot) + 1/1024 : (s1'=3) & (x1'=647*slot) + 1/1024 : (s1'=3) & (x1'=648*slot) + 1/1024 : (s1'=3) & (x1'=649*slot) + 1/1024 : (s1'=3) & (x1'=650*slot) + 1/1024 : (s1'=3) & (x1'=651*slot) + 1/1024 : (s1'=3) & (x1'=652*slot) + 1/1024 : (s1'=3) & (x1'=653*slot) + 1/1024 : (s1'=3) & (x1'=654*slot) + 1/1024 : (s1'=3) & (x1'=655*slot) + 1/1024 : (s1'=3) & (x1'=656*slot) + 1/1024 : (s1'=3) & (x1'=657*slot) + 1/1024 : (s1'=3) & (x1'=658*slot) + 1/1024 : (s1'=3) & (x1'=659*slot) + 1/1024 : (s1'=3) & (x1'=660*slot) + 1/1024 : (s1'=3) & (x1'=661*slot) + 1/1024 : (s1'=3) & (x1'=662*slot) + 1/1024 : (s1'=3) & (x1'=663*slot) + 1/1024 : (s1'=3) & (x1'=664*slot) + 1/1024 : (s1'=3) & (x1'=665*slot) + 1/1024 : (s1'=3) & (x1'=666*slot) + 1/1024 : (s1'=3) & (x1'=667*slot) + 1/1024 : (s1'=3) & (x1'=668*slot) + 1/1024 : (s1'=3) & (x1'=669*slot) + 1/1024 : (s1'=3) & (x1'=670*slot) + 1/1024 : (s1'=3) & (x1'=671*slot) + 1/1024 : (s1'=3) & (x1'=672*slot) + 1/1024 : (s1'=3) & (x1'=673*slot) + 1/1024 : (s1'=3) & (x1'=674*slot) + 1/1024 : (s1'=3) & (x1'=675*slot) + 1/1024 : (s1'=3) & (x1'=676*slot) + 1/1024 : (s1'=3) & (x1'=677*slot) + 1/1024 : (s1'=3) & (x1'=678*slot) + 1/1024 : (s1'=3) & (x1'=679*slot) + 1/1024 : (s1'=3) & (x1'=680*slot) + 1/1024 : (s1'=3) & (x1'=681*slot) + 1/1024 : (s1'=3) & (x1'=682*slot) + 1/1024 : (s1'=3) & (x1'=683*slot) + 1/1024 : (s1'=3) & (x1'=684*slot) + 1/1024 : (s1'=3) & (x1'=685*slot) + 1/1024 : (s1'=3) & (x1'=686*slot) + 1/1024 : (s1'=3) & (x1'=687*slot) + 1/1024 : (s1'=3) & (x1'=688*slot) + 1/1024 : (s1'=3) & (x1'=689*slot) + 1/1024 : (s1'=3) & (x1'=690*slot) + 1/1024 : (s1'=3) & (x1'=691*slot) + 1/1024 : (s1'=3) & (x1'=692*slot) + 1/1024 : (s1'=3) & (x1'=693*slot) + 1/1024 : (s1'=3) & (x1'=694*slot) + 1/1024 : (s1'=3) & (x1'=695*slot) + 1/1024 : (s1'=3) & (x1'=696*slot) + 1/1024 : (s1'=3) & (x1'=697*slot) + 1/1024 : (s1'=3) & (x1'=698*slot) + 1/1024 : (s1'=3) & (x1'=699*slot) + 1/1024 : (s1'=3) & (x1'=700*slot) + 1/1024 : (s1'=3) & (x1'=701*slot) + 1/1024 : (s1'=3) & (x1'=702*slot) + 1/1024 : (s1'=3) & (x1'=703*slot) + 1/1024 : (s1'=3) & (x1'=704*slot) + 1/1024 : (s1'=3) & (x1'=705*slot) + 1/1024 : (s1'=3) & (x1'=706*slot) + 1/1024 : (s1'=3) & (x1'=707*slot) + 1/1024 : (s1'=3) & (x1'=708*slot) + 1/1024 : (s1'=3) & (x1'=709*slot) + 1/1024 : (s1'=3) & (x1'=710*slot) + 1/1024 : (s1'=3) & (x1'=711*slot) + 1/1024 : (s1'=3) & (x1'=712*slot) + 1/1024 : (s1'=3) & (x1'=713*slot) + 1/1024 : (s1'=3) & (x1'=714*slot) + 1/1024 : (s1'=3) & (x1'=715*slot) + 1/1024 : (s1'=3) & (x1'=716*slot) + 1/1024 : (s1'=3) & (x1'=717*slot) + 1/1024 : (s1'=3) & (x1'=718*slot) + 1/1024 : (s1'=3) & (x1'=719*slot) + 1/1024 : (s1'=3) & (x1'=720*slot) + 1/1024 : (s1'=3) & (x1'=721*slot) + 1/1024 : (s1'=3) & (x1'=722*slot) + 1/1024 : (s1'=3) & (x1'=723*slot) + 1/1024 : (s1'=3) & (x1'=724*slot) + 1/1024 : (s1'=3) & (x1'=725*slot) + 1/1024 : (s1'=3) & (x1'=726*slot) + 1/1024 : (s1'=3) & (x1'=727*slot) + 1/1024 : (s1'=3) & (x1'=728*slot) + 1/1024 : (s1'=3) & (x1'=729*slot) + 1/1024 : (s1'=3) & (x1'=730*slot) + 1/1024 : (s1'=3) & (x1'=731*slot) + 1/1024 : (s1'=3) & (x1'=732*slot) + 1/1024 : (s1'=3) & (x1'=733*slot) + 1/1024 : (s1'=3) & (x1'=734*slot) + 1/1024 : (s1'=3) & (x1'=735*slot) + 1/1024 : (s1'=3) & (x1'=736*slot) + 1/1024 : (s1'=3) & (x1'=737*slot) + 1/1024 : (s1'=3) & (x1'=738*slot) + 1/1024 : (s1'=3) & (x1'=739*slot) + 1/1024 : (s1'=3) & (x1'=740*slot) + 1/1024 : (s1'=3) & (x1'=741*slot) + 1/1024 : (s1'=3) & (x1'=742*slot) + 1/1024 : (s1'=3) & (x1'=743*slot) + 1/1024 : (s1'=3) & (x1'=744*slot) + 1/1024 : (s1'=3) & (x1'=745*slot) + 1/1024 : (s1'=3) & (x1'=746*slot) + 1/1024 : (s1'=3) & (x1'=747*slot) + 1/1024 : (s1'=3) & (x1'=748*slot) + 1/1024 : (s1'=3) & (x1'=749*slot) + 1/1024 : (s1'=3) & (x1'=750*slot) + 1/1024 : (s1'=3) & (x1'=751*slot) + 1/1024 : (s1'=3) & (x1'=752*slot) + 1/1024 : (s1'=3) & (x1'=753*slot) + 1/1024 : (s1'=3) & (x1'=754*slot) + 1/1024 : (s1'=3) & (x1'=755*slot) + 1/1024 : (s1'=3) & (x1'=756*slot) + 1/1024 : (s1'=3) & (x1'=757*slot) + 1/1024 : (s1'=3) & (x1'=758*slot) + 1/1024 : (s1'=3) & (x1'=759*slot) + 1/1024 : (s1'=3) & (x1'=760*slot) + 1/1024 : (s1'=3) & (x1'=761*slot) + 1/1024 : (s1'=3) & (x1'=762*slot) + 1/1024 : (s1'=3) & (x1'=763*slot) + 1/1024 : (s1'=3) & (x1'=764*slot) + 1/1024 : (s1'=3) & (x1'=765*slot) + 1/1024 : (s1'=3) & (x1'=766*slot) + 1/1024 : (s1'=3) & (x1'=767*slot) + 1/1024 : (s1'=3) & (x1'=768*slot) + 1/1024 : (s1'=3) & (x1'=769*slot) + 1/1024 : (s1'=3) & (x1'=770*slot) + 1/1024 : (s1'=3) & (x1'=771*slot) + 1/1024 : (s1'=3) & (x1'=772*slot) + 1/1024 : (s1'=3) & (x1'=773*slot) + 1/1024 : (s1'=3) & (x1'=774*slot) + 1/1024 : (s1'=3) & (x1'=775*slot) + 1/1024 : (s1'=3) & (x1'=776*slot) + 1/1024 : (s1'=3) & (x1'=777*slot) + 1/1024 : (s1'=3) & (x1'=778*slot) + 1/1024 : (s1'=3) & (x1'=779*slot) + 1/1024 : (s1'=3) & (x1'=780*slot) + 1/1024 : (s1'=3) & (x1'=781*slot) + 1/1024 : (s1'=3) & (x1'=782*slot) + 1/1024 : (s1'=3) & (x1'=783*slot) + 1/1024 : (s1'=3) & (x1'=784*slot) + 1/1024 : (s1'=3) & (x1'=785*slot) + 1/1024 : (s1'=3) & (x1'=786*slot) + 1/1024 : (s1'=3) & (x1'=787*slot) + 1/1024 : (s1'=3) & (x1'=788*slot) + 1/1024 : (s1'=3) & (x1'=789*slot) + 1/1024 : (s1'=3) & (x1'=790*slot) + 1/1024 : (s1'=3) & (x1'=791*slot) + 1/1024 : (s1'=3) & (x1'=792*slot) + 1/1024 : (s1'=3) & (x1'=793*slot) + 1/1024 : (s1'=3) & (x1'=794*slot) + 1/1024 : (s1'=3) & (x1'=795*slot) + 1/1024 : (s1'=3) & (x1'=796*slot) + 1/1024 : (s1'=3) & (x1'=797*slot) + 1/1024 : (s1'=3) & (x1'=798*slot) + 1/1024 : (s1'=3) & (x1'=799*slot) + 1/1024 : (s1'=3) & (x1'=800*slot) + 1/1024 : (s1'=3) & (x1'=801*slot) + 1/1024 : (s1'=3) & (x1'=802*slot) + 1/1024 : (s1'=3) & (x1'=803*slot) + 1/1024 : (s1'=3) & (x1'=804*slot) + 1/1024 : (s1'=3) & (x1'=805*slot) + 1/1024 : (s1'=3) & (x1'=806*slot) + 1/1024 : (s1'=3) & (x1'=807*slot) + 1/1024 : (s1'=3) & (x1'=808*slot) + 1/1024 : (s1'=3) & (x1'=809*slot) + 1/1024 : (s1'=3) & (x1'=810*slot) + 1/1024 : (s1'=3) & (x1'=811*slot) + 1/1024 : (s1'=3) & (x1'=812*slot) + 1/1024 : (s1'=3) & (x1'=813*slot) + 1/1024 : (s1'=3) & (x1'=814*slot) + 1/1024 : (s1'=3) & (x1'=815*slot) + 1/1024 : (s1'=3) & (x1'=816*slot) + 1/1024 : (s1'=3) & (x1'=817*slot) + 1/1024 : (s1'=3) & (x1'=818*slot) + 1/1024 : (s1'=3) & (x1'=819*slot) + 1/1024 : (s1'=3) & (x1'=820*slot) + 1/1024 : (s1'=3) & (x1'=821*slot) + 1/1024 : (s1'=3) & (x1'=822*slot) + 1/1024 : (s1'=3) & (x1'=823*slot) + 1/1024 : (s1'=3) & (x1'=824*slot) + 1/1024 : (s1'=3) & (x1'=825*slot) + 1/1024 : (s1'=3) & (x1'=826*slot) + 1/1024 : (s1'=3) & (x1'=827*slot) + 1/1024 : (s1'=3) & (x1'=828*slot) + 1/1024 : (s1'=3) & (x1'=829*slot) + 1/1024 : (s1'=3) & (x1'=830*slot) + 1/1024 : (s1'=3) & (x1'=831*slot) + 1/1024 : (s1'=3) & (x1'=832*slot) + 1/1024 : (s1'=3) & (x1'=833*slot) + 1/1024 : (s1'=3) & (x1'=834*slot) + 1/1024 : (s1'=3) & (x1'=835*slot) + 1/1024 : (s1'=3) & (x1'=836*slot) + 1/1024 : (s1'=3) & (x1'=837*slot) + 1/1024 : (s1'=3) & (x1'=838*slot) + 1/1024 : (s1'=3) & (x1'=839*slot) + 1/1024 : (s1'=3) & (x1'=840*slot) + 1/1024 : (s1'=3) & (x1'=841*slot) + 1/1024 : (s1'=3) & (x1'=842*slot) + 1/1024 : (s1'=3) & (x1'=843*slot) + 1/1024 : (s1'=3) & (x1'=844*slot) + 1/1024 : (s1'=3) & (x1'=845*slot) + 1/1024 : (s1'=3) & (x1'=846*slot) + 1/1024 : (s1'=3) & (x1'=847*slot) + 1/1024 : (s1'=3) & (x1'=848*slot) + 1/1024 : (s1'=3) & (x1'=849*slot) + 1/1024 : (s1'=3) & (x1'=850*slot) + 1/1024 : (s1'=3) & (x1'=851*slot) + 1/1024 : (s1'=3) & (x1'=852*slot) + 1/1024 : (s1'=3) & (x1'=853*slot) + 1/1024 : (s1'=3) & (x1'=854*slot) + 1/1024 : (s1'=3) & (x1'=855*slot) + 1/1024 : (s1'=3) & (x1'=856*slot) + 1/1024 : (s1'=3) & (x1'=857*slot) + 1/1024 : (s1'=3) & (x1'=858*slot) + 1/1024 : (s1'=3) & (x1'=859*slot) + 1/1024 : (s1'=3) & (x1'=860*slot) + 1/1024 : (s1'=3) & (x1'=861*slot) + 1/1024 : (s1'=3) & (x1'=862*slot) + 1/1024 : (s1'=3) & (x1'=863*slot) + 1/1024 : (s1'=3) & (x1'=864*slot) + 1/1024 : (s1'=3) & (x1'=865*slot) + 1/1024 : (s1'=3) & (x1'=866*slot) + 1/1024 : (s1'=3) & (x1'=867*slot) + 1/1024 : (s1'=3) & (x1'=868*slot) + 1/1024 : (s1'=3) & (x1'=869*slot) + 1/1024 : (s1'=3) & (x1'=870*slot) + 1/1024 : (s1'=3) & (x1'=871*slot) + 1/1024 : (s1'=3) & (x1'=872*slot) + 1/1024 : (s1'=3) & (x1'=873*slot) + 1/1024 : (s1'=3) & (x1'=874*slot) + 1/1024 : (s1'=3) & (x1'=875*slot) + 1/1024 : (s1'=3) & (x1'=876*slot) + 1/1024 : (s1'=3) & (x1'=877*slot) + 1/1024 : (s1'=3) & (x1'=878*slot) + 1/1024 : (s1'=3) & (x1'=879*slot) + 1/1024 : (s1'=3) & (x1'=880*slot) + 1/1024 : (s1'=3) & (x1'=881*slot) + 1/1024 : (s1'=3) & (x1'=882*slot) + 1/1024 : (s1'=3) & (x1'=883*slot) + 1/1024 : (s1'=3) & (x1'=884*slot) + 1/1024 : (s1'=3) & (x1'=885*slot) + 1/1024 : (s1'=3) & (x1'=886*slot) + 1/1024 : (s1'=3) & (x1'=887*slot) + 1/1024 : (s1'=3) & (x1'=888*slot) + 1/1024 : (s1'=3) & (x1'=889*slot) + 1/1024 : (s1'=3) & (x1'=890*slot) + 1/1024 : (s1'=3) & (x1'=891*slot) + 1/1024 : (s1'=3) & (x1'=892*slot) + 1/1024 : (s1'=3) & (x1'=893*slot) + 1/1024 : (s1'=3) & (x1'=894*slot) + 1/1024 : (s1'=3) & (x1'=895*slot) + 1/1024 : (s1'=3) & (x1'=896*slot) + 1/1024 : (s1'=3) & (x1'=897*slot) + 1/1024 : (s1'=3) & (x1'=898*slot) + 1/1024 : (s1'=3) & (x1'=899*slot) + 1/1024 : (s1'=3) & (x1'=900*slot) + 1/1024 : (s1'=3) & (x1'=901*slot) + 1/1024 : (s1'=3) & (x1'=902*slot) + 1/1024 : (s1'=3) & (x1'=903*slot) + 1/1024 : (s1'=3) & (x1'=904*slot) + 1/1024 : (s1'=3) & (x1'=905*slot) + 1/1024 : (s1'=3) & (x1'=906*slot) + 1/1024 : (s1'=3) & (x1'=907*slot) + 1/1024 : (s1'=3) & (x1'=908*slot) + 1/1024 : (s1'=3) & (x1'=909*slot) + 1/1024 : (s1'=3) & (x1'=910*slot) + 1/1024 : (s1'=3) & (x1'=911*slot) + 1/1024 : (s1'=3) & (x1'=912*slot) + 1/1024 : (s1'=3) & (x1'=913*slot) + 1/1024 : (s1'=3) & (x1'=914*slot) + 1/1024 : (s1'=3) & (x1'=915*slot) + 1/1024 : (s1'=3) & (x1'=916*slot) + 1/1024 : (s1'=3) & (x1'=917*slot) + 1/1024 : (s1'=3) & (x1'=918*slot) + 1/1024 : (s1'=3) & (x1'=919*slot) + 1/1024 : (s1'=3) & (x1'=920*slot) + 1/1024 : (s1'=3) & (x1'=921*slot) + 1/1024 : (s1'=3) & (x1'=922*slot) + 1/1024 : (s1'=3) & (x1'=923*slot) + 1/1024 : (s1'=3) & (x1'=924*slot) + 1/1024 : (s1'=3) & (x1'=925*slot) + 1/1024 : (s1'=3) & (x1'=926*slot) + 1/1024 : (s1'=3) & (x1'=927*slot) + 1/1024 : (s1'=3) & (x1'=928*slot) + 1/1024 : (s1'=3) & (x1'=929*slot) + 1/1024 : (s1'=3) & (x1'=930*slot) + 1/1024 : (s1'=3) & (x1'=931*slot) + 1/1024 : (s1'=3) & (x1'=932*slot) + 1/1024 : (s1'=3) & (x1'=933*slot) + 1/1024 : (s1'=3) & (x1'=934*slot) + 1/1024 : (s1'=3) & (x1'=935*slot) + 1/1024 : (s1'=3) & (x1'=936*slot) + 1/1024 : (s1'=3) & (x1'=937*slot) + 1/1024 : (s1'=3) & (x1'=938*slot) + 1/1024 : (s1'=3) & (x1'=939*slot) + 1/1024 : (s1'=3) & (x1'=940*slot) + 1/1024 : (s1'=3) & (x1'=941*slot) + 1/1024 : (s1'=3) & (x1'=942*slot) + 1/1024 : (s1'=3) & (x1'=943*slot) + 1/1024 : (s1'=3) & (x1'=944*slot) + 1/1024 : (s1'=3) & (x1'=945*slot) + 1/1024 : (s1'=3) & (x1'=946*slot) + 1/1024 : (s1'=3) & (x1'=947*slot) + 1/1024 : (s1'=3) & (x1'=948*slot) + 1/1024 : (s1'=3) & (x1'=949*slot) + 1/1024 : (s1'=3) & (x1'=950*slot) + 1/1024 : (s1'=3) & (x1'=951*slot) + 1/1024 : (s1'=3) & (x1'=952*slot) + 1/1024 : (s1'=3) & (x1'=953*slot) + 1/1024 : (s1'=3) & (x1'=954*slot) + 1/1024 : (s1'=3) & (x1'=955*slot) + 1/1024 : (s1'=3) & (x1'=956*slot) + 1/1024 : (s1'=3) & (x1'=957*slot) + 1/1024 : (s1'=3) & (x1'=958*slot) + 1/1024 : (s1'=3) & (x1'=959*slot) + 1/1024 : (s1'=3) & (x1'=960*slot) + 1/1024 : (s1'=3) & (x1'=961*slot) + 1/1024 : (s1'=3) & (x1'=962*slot) + 1/1024 : (s1'=3) & (x1'=963*slot) + 1/1024 : (s1'=3) & (x1'=964*slot) + 1/1024 : (s1'=3) & (x1'=965*slot) + 1/1024 : (s1'=3) & (x1'=966*slot) + 1/1024 : (s1'=3) & (x1'=967*slot) + 1/1024 : (s1'=3) & (x1'=968*slot) + 1/1024 : (s1'=3) & (x1'=969*slot) + 1/1024 : (s1'=3) & (x1'=970*slot) + 1/1024 : (s1'=3) & (x1'=971*slot) + 1/1024 : (s1'=3) & (x1'=972*slot) + 1/1024 : (s1'=3) & (x1'=973*slot) + 1/1024 : (s1'=3) & (x1'=974*slot) + 1/1024 : (s1'=3) & (x1'=975*slot) + 1/1024 : (s1'=3) & (x1'=976*slot) + 1/1024 : (s1'=3) & (x1'=977*slot) + 1/1024 : (s1'=3) & (x1'=978*slot) + 1/1024 : (s1'=3) & (x1'=979*slot) + 1/1024 : (s1'=3) & (x1'=980*slot) + 1/1024 : (s1'=3) & (x1'=981*slot) + 1/1024 : (s1'=3) & (x1'=982*slot) + 1/1024 : (s1'=3) & (x1'=983*slot) + 1/1024 : (s1'=3) & (x1'=984*slot) + 1/1024 : (s1'=3) & (x1'=985*slot) + 1/1024 : (s1'=3) & (x1'=986*slot) + 1/1024 : (s1'=3) & (x1'=987*slot) + 1/1024 : (s1'=3) & (x1'=988*slot) + 1/1024 : (s1'=3) & (x1'=989*slot) + 1/1024 : (s1'=3) & (x1'=990*slot) + 1/1024 : (s1'=3) & (x1'=991*slot) + 1/1024 : (s1'=3) & (x1'=992*slot) + 1/1024 : (s1'=3) & (x1'=993*slot) + 1/1024 : (s1'=3) & (x1'=994*slot) + 1/1024 : (s1'=3) & (x1'=995*slot) + 1/1024 : (s1'=3) & (x1'=996*slot) + 1/1024 : (s1'=3) & (x1'=997*slot) + 1/1024 : (s1'=3) & (x1'=998*slot) + 1/1024 : (s1'=3) & (x1'=999*slot) + 1/1024 : (s1'=3) & (x1'=1000*slot) + 1/1024 : (s1'=3) & (x1'=1001*slot) + 1/1024 : (s1'=3) & (x1'=1002*slot) + 1/1024 : (s1'=3) & (x1'=1003*slot) + 1/1024 : (s1'=3) & (x1'=1004*slot) + 1/1024 : (s1'=3) & (x1'=1005*slot) + 1/1024 : (s1'=3) & (x1'=1006*slot) + 1/1024 : (s1'=3) & (x1'=1007*slot) + 1/1024 : (s1'=3) & (x1'=1008*slot) + 1/1024 : (s1'=3) & (x1'=1009*slot) + 1/1024 : (s1'=3) & (x1'=1010*slot) + 1/1024 : (s1'=3) & (x1'=1011*slot) + 1/1024 : (s1'=3) & (x1'=1012*slot) + 1/1024 : (s1'=3) & (x1'=1013*slot) + 1/1024 : (s1'=3) & (x1'=1014*slot) + 1/1024 : (s1'=3) & (x1'=1015*slot) + 1/1024 : (s1'=3) & (x1'=1016*slot) + 1/1024 : (s1'=3) & (x1'=1017*slot) + 1/1024 : (s1'=3) & (x1'=1018*slot) + 1/1024 : (s1'=3) & (x1'=1019*slot) + 1/1024 : (s1'=3) & (x1'=1020*slot) + 1/1024 : (s1'=3) & (x1'=1021*slot) + 1/1024 : (s1'=3) & (x1'=1022*slot) + 1/1024 : (s1'=3) & (x1'=1023*slot); // wait until backoff counter reaches 0 then send again [send1] s1=3 & x1=pow(2,cd1)*slot -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) [csend1] s1=3 & x1=pow(2,cd1)*slot -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) [busy1] s1=3 & x1=pow(2,cd1)*slot -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) // once finished loop (wait for other station to finish) [done] s1=4 -> (s1'=4); endmodule // construct station 2 through renaming module station2=station1[s1=s2,x1=x2,cd1=cd2,send1=send2,csend1=csend2,busy1=busy2,end1=end2] endmodule //---------------------------------------------------------------------------------------------------------------------------- // REWARD STRUCTURES // time rewards "time" true : 1; endrewards // number of collisions rewards "collisions" [csend1] true : 1; [csend2] true : 1; endrewards //---------------------------------------------------------------------------------------------------------------------------- // LABELS label "s1_done" = s1=4; label "s2_done" = s2=4; label "done" = s1=4 & s2=4; label "cmax" = c=COL;