ctmc
const double failureRate;
module walker
stator1 : [0..1] init 1;
stator2 : [0..1] init 1;
stator3 : [0..1] init 1;
stator4 : [0..1] init 1;
stator5 : [0..1] init 1;
stator6 : [0..1] init 0;
stator7 : [0..1] init 0;
stator8 : [0..1] init 0;
stator9 : [0..1] init 0;
stator10 : [0..1] init 0;
stator11 : [0..1] init 0;
stator12 : [0..1] init 0;
stator13 : [0..1] init 0;
stator14 : [0..1] init 1;
stator15 : [0..1] init 1;
stator16 : [0..1] init 0;
stator17 : [0..1] init 0;
stator18 : [0..1] init 0;
stator19 : [0..1] init 0;
stator20 : [0..1] init 0;
stator21 : [0..1] init 0;
w1 : [0..21] init 1;
blockade2: [0..1] init 0;
blockade3 : [0..1] init 0;
blockade4 : [0..1] init 0;
blockade5 : [0..1] init 0;
blockade14 : [0..1] init 0;
blockade15 : [0..1] init 0;
[block2] blockade2=0 -> 1000000.0 * failureRate : (blockade2'=1) & (stator2'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade2'=1);
[block3] blockade3=0 -> 1000000.0 * failureRate : (blockade3'=1) & (stator3'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade3'=1);
[block4] blockade4=0 -> 1000000.0 * failureRate : (blockade4'=1) & (stator4'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade4'=1);
[block5] blockade5=0 -> 1000000.0 * failureRate : (blockade5'=1) & (stator5'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade5'=1);
[block14] blockade14=0 -> 1000000.0 * failureRate : (blockade14'=1) & (stator14'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade14'=1);
[block15] blockade15=0 -> 1000000.0 * failureRate : (blockade15'=1) & (stator15'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade15'=1);
[step] w1=1 & stator2=0 -> 0.0029999999999999996 : (w1'=2) & (stator2'=1);
[step] w1=1 & stator3=0 -> 5.9999999999999995E-5 : (w1'=3) & (stator3'=1);
[step] w1=1 & stator4=0 -> 2.9999999999999997E-5 : (w1'=4) & (stator4'=1);
[step] w1=1 & stator5=0 -> 5.9999999999999995E-5 : (w1'=5) & (stator5'=1);
[step] w1=1 & stator6=0 -> 2.9999999999999997E-5 : (w1'=6) & (stator6'=1);
[step] w1=1 & stator7=0 -> 5.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=1 & stator8=0 -> 2.9999999999999997E-5 : (w1'=8) & (stator8'=1);
[step] w1=1 & stator9=0 -> 2.9999999999999997E-5 : (w1'=9) & (stator9'=1);
[step] w1=1 & stator10=0 -> 2.9999999999999997E-5 : (w1'=10) & (stator10'=1);
[step] w1=1 & stator11=0 -> 2.9999999999999997E-5 : (w1'=11) & (stator11'=1);
[step] w1=1 & stator12=0 -> 5.9999999999999995E-5 : (w1'=12) & (stator12'=1);
[step] w1=1 & stator13=0 -> 0.0029999999999999996 : (w1'=13) & (stator13'=1);
[step] w1=1 & stator14=0 -> 2.9999999999999997E-5 : (w1'=14) & (stator14'=1);
[step] w1=1 & stator15=0 -> 5.9999999999999995E-5 : (w1'=15) & (stator15'=1);
[step] w1=1 & stator16=0 -> 2.9999999999999997E-5 : (w1'=16) & (stator16'=1);
[step] w1=1 & stator17=0 -> 5.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=1 & stator18=0 -> 2.9999999999999997E-5 : (w1'=18) & (stator18'=1);
[step] w1=1 & stator19=0 -> 2.9999999999999997E-5 : (w1'=19) & (stator19'=1);
[step] w1=1 & stator20=0 -> 2.9999999999999997E-5 : (w1'=20) & (stator20'=1);
[step] w1=1 & stator21=0 -> 2.9999999999999997E-5 : (w1'=21) & (stator21'=1);
[step] w1=2 & stator1=0 -> 0.009 : (w1'=1) & (stator1'=1);
[step] w1=2 & stator3=0 -> 0.009 : (w1'=3) & (stator3'=1);
[step] w1=2 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1);
[step] w1=2 & stator5=0 -> 1.7999999999999998E-4 : (w1'=5) & (stator5'=1);
[step] w1=2 & stator6=0 -> 1.7999999999999998E-4 : (w1'=6) & (stator6'=1);
[step] w1=2 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=2 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1);
[step] w1=2 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1);
[step] w1=2 & stator10=0 -> 8.999999999999999E-5 : (w1'=10) & (stator10'=1);
[step] w1=2 & stator11=0 -> 8.999999999999999E-5 : (w1'=11) & (stator11'=1);
[step] w1=2 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1);
[step] w1=2 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=2 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1);
[step] w1=2 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1);
[step] w1=2 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1);
[step] w1=2 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=2 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1);
[step] w1=2 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1);
[step] w1=2 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1);
[step] w1=2 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1);
[step] w1=3 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1);
[step] w1=3 & stator2=0 -> 0.009 : (w1'=2) & (stator2'=1);
[step] w1=3 & stator4=0 -> 0.009 : (w1'=4) & (stator4'=1);
[step] w1=3 & stator5=0 -> 1.7999999999999998E-4 : (w1'=5) & (stator5'=1);
[step] w1=3 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1);
[step] w1=3 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=3 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1);
[step] w1=3 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=3 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=3 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1);
[step] w1=3 & stator19=0 -> 1.7999999999999998E-4 : (w1'=19) & (stator19'=1);
[step] w1=3 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1);
[step] w1=3 & stator21=0 -> 0.009 : (w1'=21) & (stator21'=1);
[step] w1=4 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=4 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=4 & stator3=0 -> 0.009 : (w1'=3) & (stator3'=1);
[step] w1=4 & stator5=0 -> 0.009 : (w1'=5) & (stator5'=1);
[step] w1=4 & stator6=0 -> 1.7999999999999998E-4 : (w1'=6) & (stator6'=1);
[step] w1=4 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=4 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1);
[step] w1=4 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=4 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1);
[step] w1=4 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1);
[step] w1=4 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1);
[step] w1=4 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1);
[step] w1=5 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1);
[step] w1=5 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=5 & stator3=0 -> 1.7999999999999998E-4 : (w1'=3) & (stator3'=1);
[step] w1=5 & stator4=0 -> 0.009 : (w1'=4) & (stator4'=1);
[step] w1=5 & stator6=0 -> 0.009 : (w1'=6) & (stator6'=1);
[step] w1=5 & stator7=0 -> 1.7999999999999997E-5 : (w1'=7) & (stator7'=1);
[step] w1=5 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1);
[step] w1=5 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1);
[step] w1=5 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=5 & stator20=0 -> 8.999999999999999E-5 : (w1'=20) & (stator20'=1);
[step] w1=5 & stator21=0 -> 8.999999999999999E-5 : (w1'=21) & (stator21'=1);
[step] w1=6 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=6 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=6 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1);
[step] w1=6 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1);
[step] w1=6 & stator5=0 -> 0.009 : (w1'=5) & (stator5'=1);
[step] w1=6 & stator7=0 -> 9.0E-4 : (w1'=7) & (stator7'=1);
[step] w1=6 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1);
[step] w1=6 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1);
[step] w1=6 & stator10=0 -> 8.999999999999999E-5 : (w1'=10) & (stator10'=1);
[step] w1=6 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=6 & stator21=0 -> 8.999999999999999E-5 : (w1'=21) & (stator21'=1);
[step] w1=8 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=8 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=8 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1);
[step] w1=8 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1);
[step] w1=8 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1);
[step] w1=8 & stator6=0 -> 1.7999999999999998E-4 : (w1'=6) & (stator6'=1);
[step] w1=8 & stator7=0 -> 9.0E-4 : (w1'=7) & (stator7'=1);
[step] w1=8 & stator9=0 -> 0.009 : (w1'=9) & (stator9'=1);
[step] w1=8 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1);
[step] w1=8 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1);
[step] w1=8 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1);
[step] w1=8 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=8 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1);
[step] w1=9 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=9 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=9 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1);
[step] w1=9 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1);
[step] w1=9 & stator7=0 -> 1.7999999999999997E-5 : (w1'=7) & (stator7'=1);
[step] w1=9 & stator8=0 -> 0.009 : (w1'=8) & (stator8'=1);
[step] w1=9 & stator10=0 -> 0.009 : (w1'=10) & (stator10'=1);
[step] w1=9 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1);
[step] w1=9 & stator12=0 -> 1.7999999999999998E-4 : (w1'=12) & (stator12'=1);
[step] w1=9 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=9 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1);
[step] w1=10 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=10 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=10 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1);
[step] w1=10 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=10 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1);
[step] w1=10 & stator9=0 -> 0.009 : (w1'=9) & (stator9'=1);
[step] w1=10 & stator11=0 -> 0.009 : (w1'=11) & (stator11'=1);
[step] w1=10 & stator12=0 -> 1.7999999999999998E-4 : (w1'=12) & (stator12'=1);
[step] w1=10 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=10 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1);
[step] w1=10 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1);
[step] w1=11 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=11 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=11 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=11 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1);
[step] w1=11 & stator9=0 -> 1.7999999999999998E-4 : (w1'=9) & (stator9'=1);
[step] w1=11 & stator10=0 -> 0.009 : (w1'=10) & (stator10'=1);
[step] w1=11 & stator12=0 -> 0.009 : (w1'=12) & (stator12'=1);
[step] w1=11 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=11 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1);
[step] w1=11 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1);
[step] w1=11 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1);
[step] w1=12 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1);
[step] w1=12 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=12 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=12 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1);
[step] w1=12 & stator9=0 -> 1.7999999999999998E-4 : (w1'=9) & (stator9'=1);
[step] w1=12 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1);
[step] w1=12 & stator11=0 -> 0.009 : (w1'=11) & (stator11'=1);
[step] w1=12 & stator13=0 -> 0.009 : (w1'=13) & (stator13'=1);
[step] w1=12 & stator14=0 -> 0.009 : (w1'=14) & (stator14'=1);
[step] w1=12 & stator15=0 -> 1.7999999999999998E-4 : (w1'=15) & (stator15'=1);
[step] w1=12 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1);
[step] w1=12 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=12 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1);
[step] w1=13 & stator1=0 -> 0.009 : (w1'=1) & (stator1'=1);
[step] w1=13 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=13 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1);
[step] w1=13 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1);
[step] w1=13 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1);
[step] w1=13 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1);
[step] w1=13 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1);
[step] w1=13 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1);
[step] w1=13 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1);
[step] w1=13 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1);
[step] w1=13 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1);
[step] w1=13 & stator12=0 -> 0.009 : (w1'=12) & (stator12'=1);
[step] w1=13 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1);
[step] w1=13 & stator15=0 -> 1.7999999999999998E-4 : (w1'=15) & (stator15'=1);
[step] w1=13 & stator16=0 -> 1.7999999999999998E-4 : (w1'=16) & (stator16'=1);
[step] w1=13 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=13 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1);
[step] w1=13 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1);
[step] w1=13 & stator20=0 -> 8.999999999999999E-5 : (w1'=20) & (stator20'=1);
[step] w1=13 & stator21=0 -> 8.999999999999999E-5 : (w1'=21) & (stator21'=1);
[step] w1=14 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=14 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=14 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1);
[step] w1=14 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1);
[step] w1=14 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1);
[step] w1=14 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1);
[step] w1=14 & stator12=0 -> 0.009 : (w1'=12) & (stator12'=1);
[step] w1=14 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=14 & stator15=0 -> 0.009 : (w1'=15) & (stator15'=1);
[step] w1=14 & stator16=0 -> 1.7999999999999998E-4 : (w1'=16) & (stator16'=1);
[step] w1=14 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=14 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1);
[step] w1=15 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1);
[step] w1=15 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=15 & stator10=0 -> 8.999999999999999E-5 : (w1'=10) & (stator10'=1);
[step] w1=15 & stator11=0 -> 8.999999999999999E-5 : (w1'=11) & (stator11'=1);
[step] w1=15 & stator12=0 -> 1.7999999999999998E-4 : (w1'=12) & (stator12'=1);
[step] w1=15 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=15 & stator14=0 -> 0.009 : (w1'=14) & (stator14'=1);
[step] w1=15 & stator16=0 -> 0.009 : (w1'=16) & (stator16'=1);
[step] w1=15 & stator17=0 -> 1.7999999999999997E-5 : (w1'=17) & (stator17'=1);
[step] w1=15 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1);
[step] w1=15 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1);
[step] w1=16 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=16 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=16 & stator11=0 -> 8.999999999999999E-5 : (w1'=11) & (stator11'=1);
[step] w1=16 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1);
[step] w1=16 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1);
[step] w1=16 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1);
[step] w1=16 & stator15=0 -> 0.009 : (w1'=15) & (stator15'=1);
[step] w1=16 & stator17=0 -> 9.0E-4 : (w1'=17) & (stator17'=1);
[step] w1=16 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1);
[step] w1=16 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1);
[step] w1=16 & stator20=0 -> 8.999999999999999E-5 : (w1'=20) & (stator20'=1);
[step] w1=18 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=18 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=18 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1);
[step] w1=18 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1);
[step] w1=18 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1);
[step] w1=18 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=18 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1);
[step] w1=18 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1);
[step] w1=18 & stator16=0 -> 1.7999999999999998E-4 : (w1'=16) & (stator16'=1);
[step] w1=18 & stator17=0 -> 9.0E-4 : (w1'=17) & (stator17'=1);
[step] w1=18 & stator19=0 -> 0.009 : (w1'=19) & (stator19'=1);
[step] w1=18 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1);
[step] w1=18 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1);
[step] w1=19 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=19 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1);
[step] w1=19 & stator3=0 -> 1.7999999999999998E-4 : (w1'=3) & (stator3'=1);
[step] w1=19 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1);
[step] w1=19 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=19 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1);
[step] w1=19 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1);
[step] w1=19 & stator17=0 -> 1.7999999999999997E-5 : (w1'=17) & (stator17'=1);
[step] w1=19 & stator18=0 -> 0.009 : (w1'=18) & (stator18'=1);
[step] w1=19 & stator20=0 -> 0.009 : (w1'=20) & (stator20'=1);
[step] w1=19 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1);
[step] w1=20 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=20 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=20 & stator3=0 -> 1.7999999999999998E-4 : (w1'=3) & (stator3'=1);
[step] w1=20 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1);
[step] w1=20 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1);
[step] w1=20 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=20 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1);
[step] w1=20 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=20 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1);
[step] w1=20 & stator19=0 -> 0.009 : (w1'=19) & (stator19'=1);
[step] w1=20 & stator21=0 -> 0.009 : (w1'=21) & (stator21'=1);
[step] w1=21 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1);
[step] w1=21 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1);
[step] w1=21 & stator3=0 -> 0.009 : (w1'=3) & (stator3'=1);
[step] w1=21 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1);
[step] w1=21 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1);
[step] w1=21 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1);
[step] w1=21 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1);
[step] w1=21 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1);
[step] w1=21 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1);
[step] w1=21 & stator19=0 -> 1.7999999999999998E-4 : (w1'=19) & (stator19'=1);
[step] w1=21 & stator20=0 -> 0.009 : (w1'=20) & (stator20'=1);
[] w1=1 -> 0.000000001 : (w1'=1);
[] w1=2 -> 0.000000001 : (w1'=2);
[] w1=3 -> 0.000000001 : (w1'=3);
[] w1=4 -> 0.000000001 : (w1'=4);
[] w1=5 -> 0.000000001 : (w1'=5);
[] w1=6 -> 0.000000001 : (w1'=6);
[] w1=7 -> 0.000000001 : (w1'=7);
[] w1=8 -> 0.000000001 : (w1'=8);
[] w1=9 -> 0.000000001 : (w1'=9);
[] w1=10 -> 0.000000001 : (w1'=10);
[] w1=11 -> 0.000000001 : (w1'=11);
[] w1=12 -> 0.000000001 : (w1'=12);
[] w1=13 -> 0.000000001 : (w1'=13);
[] w1=14 -> 0.000000001 : (w1'=14);
[] w1=15 -> 0.000000001 : (w1'=15);
[] w1=16 -> 0.000000001 : (w1'=16);
[] w1=17 -> 0.000000001 : (w1'=17);
[] w1=18 -> 0.000000001 : (w1'=18);
[] w1=19 -> 0.000000001 : (w1'=19);
[] w1=20 -> 0.000000001 : (w1'=20);
[] w1=21 -> 0.000000001 : (w1'=21);
endmodule
rewards "steps"
[step] true : 1;
endrewards
rewards "time"
true : 1;
endrewards
rewards "blocked"
w1 =2 | w1 =3 | w1 =4 | w1 =5 | w1 =14 | w1 =15: 1;
endrewards