//
// This file has been generated with Kappa
//
// -- state encoding: explicit
// -- compaction : none
// -- further compaction: no

nondeterministic

module abs10000 

s : [0..525] init 0;
[] (s = 0) -> 0.500000:(s' = 1) + 0.500000:(s' = 2);
[] (s = 0) -> 0.500000:(s' = 3) + 0.500000:(s' = 4);
[] (s = 1) -> 0.500000:(s' = 5) + 0.500000:(s' = 6);
[] (s = 2) -> 0.500000:(s' = 7) + 0.500000:(s' = 8);
[] (s = 3) -> 0.500000:(s' = 5) + 0.500000:(s' = 7);
[] (s = 4) -> 0.500000:(s' = 6) + 0.500000:(s' = 8);
[] (s = 5) -> 1.000000:(s' = 9) ;
[] (s = 5) -> 1.000000:(s' = 10) ;
[] (s = 6) -> 1.000000:(s' = 11) ;
[] (s = 7) -> 1.000000:(s' = 11) ;
[] (s = 8) -> 1.000000:(s' = 12) ;
[] (s = 8) -> 1.000000:(s' = 11) ;
[] (s = 9) -> 0.500000:(s' = 13) + 0.500000:(s' = 14);
[] (s = 9) -> 0.500000:(s' = 15) + 0.500000:(s' = 16);
[] (s = 10) -> 1.000000:(s' = 17) ;
[] (s = 11) -> 1.000000:(s' = 17) ;
[] (s = 12) -> 0.500000:(s' = 18) + 0.500000:(s' = 19);
[] (s = 12) -> 0.500000:(s' = 20) + 0.500000:(s' = 21);
[] (s = 13) -> 0.500000:(s' = 22) + 0.500000:(s' = 23);
[] (s = 14) -> 0.500000:(s' = 24) + 0.500000:(s' = 25);
[] (s = 15) -> 0.500000:(s' = 22) + 0.500000:(s' = 24);
[] (s = 16) -> 0.500000:(s' = 23) + 0.500000:(s' = 25);
[] (s = 18) -> 0.500000:(s' = 26) + 0.500000:(s' = 27);
[] (s = 19) -> 0.500000:(s' = 28) + 0.500000:(s' = 29);
[] (s = 20) -> 0.500000:(s' = 26) + 0.500000:(s' = 28);
[] (s = 21) -> 0.500000:(s' = 27) + 0.500000:(s' = 29);
[] (s = 22) -> 1.000000:(s' = 30) ;
[] (s = 22) -> 1.000000:(s' = 31) ;
[] (s = 23) -> 1.000000:(s' = 32) ;
[] (s = 24) -> 1.000000:(s' = 32) ;
[] (s = 25) -> 1.000000:(s' = 33) ;
[] (s = 25) -> 1.000000:(s' = 32) ;
[] (s = 26) -> 1.000000:(s' = 33) ;
[] (s = 26) -> 1.000000:(s' = 32) ;
[] (s = 27) -> 1.000000:(s' = 34) ;
[] (s = 28) -> 1.000000:(s' = 34) ;
[] (s = 29) -> 1.000000:(s' = 35) ;
[] (s = 29) -> 1.000000:(s' = 34) ;
[] (s = 30) -> 0.500000:(s' = 36) + 0.500000:(s' = 37);
[] (s = 30) -> 0.500000:(s' = 38) + 0.500000:(s' = 39);
[] (s = 31) -> 1.000000:(s' = 17) ;
[] (s = 32) -> 1.000000:(s' = 17) ;
[] (s = 33) -> 0.500000:(s' = 40) + 0.500000:(s' = 41);
[] (s = 33) -> 0.500000:(s' = 42) + 0.500000:(s' = 43);
[] (s = 34) -> 1.000000:(s' = 17) ;
[] (s = 35) -> 0.500000:(s' = 44) + 0.500000:(s' = 45);
[] (s = 35) -> 0.500000:(s' = 46) + 0.500000:(s' = 47);
[] (s = 36) -> 0.500000:(s' = 48) + 0.500000:(s' = 49);
[] (s = 37) -> 0.500000:(s' = 50) + 0.500000:(s' = 51);
[] (s = 38) -> 0.500000:(s' = 48) + 0.500000:(s' = 50);
[] (s = 39) -> 0.500000:(s' = 49) + 0.500000:(s' = 51);
[] (s = 40) -> 0.500000:(s' = 52) + 0.500000:(s' = 53);
[] (s = 41) -> 0.500000:(s' = 54) + 0.500000:(s' = 55);
[] (s = 42) -> 0.500000:(s' = 52) + 0.500000:(s' = 54);
[] (s = 43) -> 0.500000:(s' = 53) + 0.500000:(s' = 55);
[] (s = 44) -> 0.500000:(s' = 56) + 0.500000:(s' = 57);
[] (s = 45) -> 0.500000:(s' = 58) + 0.500000:(s' = 59);
[] (s = 46) -> 0.500000:(s' = 56) + 0.500000:(s' = 58);
[] (s = 47) -> 0.500000:(s' = 57) + 0.500000:(s' = 59);
[] (s = 48) -> 1.000000:(s' = 60) ;
[] (s = 48) -> 1.000000:(s' = 61) ;
[] (s = 49) -> 1.000000:(s' = 62) ;
[] (s = 50) -> 1.000000:(s' = 62) ;
[] (s = 51) -> 1.000000:(s' = 63) ;
[] (s = 51) -> 1.000000:(s' = 62) ;
[] (s = 52) -> 1.000000:(s' = 63) ;
[] (s = 52) -> 1.000000:(s' = 62) ;
[] (s = 53) -> 1.000000:(s' = 64) ;
[] (s = 54) -> 1.000000:(s' = 64) ;
[] (s = 55) -> 1.000000:(s' = 65) ;
[] (s = 55) -> 1.000000:(s' = 64) ;
[] (s = 56) -> 1.000000:(s' = 65) ;
[] (s = 56) -> 1.000000:(s' = 64) ;
[] (s = 57) -> 1.000000:(s' = 66) ;
[] (s = 58) -> 1.000000:(s' = 66) ;
[] (s = 59) -> 1.000000:(s' = 67) ;
[] (s = 59) -> 1.000000:(s' = 66) ;
[] (s = 60) -> 0.500000:(s' = 68) + 0.500000:(s' = 69);
[] (s = 60) -> 0.500000:(s' = 70) + 0.500000:(s' = 71);
[] (s = 61) -> 1.000000:(s' = 17) ;
[] (s = 62) -> 1.000000:(s' = 17) ;
[] (s = 63) -> 0.500000:(s' = 72) + 0.500000:(s' = 73);
[] (s = 63) -> 0.500000:(s' = 74) + 0.500000:(s' = 75);
[] (s = 64) -> 1.000000:(s' = 17) ;
[] (s = 65) -> 0.500000:(s' = 76) + 0.500000:(s' = 77);
[] (s = 65) -> 0.500000:(s' = 78) + 0.500000:(s' = 79);
[] (s = 66) -> 1.000000:(s' = 17) ;
[] (s = 67) -> 0.500000:(s' = 80) + 0.500000:(s' = 81);
[] (s = 67) -> 0.500000:(s' = 82) + 0.500000:(s' = 83);
[] (s = 68) -> 0.500000:(s' = 84) + 0.500000:(s' = 85);
[] (s = 69) -> 0.500000:(s' = 86) + 0.500000:(s' = 87);
[] (s = 70) -> 0.500000:(s' = 84) + 0.500000:(s' = 86);
[] (s = 71) -> 0.500000:(s' = 85) + 0.500000:(s' = 87);
[] (s = 72) -> 0.500000:(s' = 88) + 0.500000:(s' = 89);
[] (s = 73) -> 0.500000:(s' = 90) + 0.500000:(s' = 91);
[] (s = 74) -> 0.500000:(s' = 88) + 0.500000:(s' = 90);
[] (s = 75) -> 0.500000:(s' = 89) + 0.500000:(s' = 91);
[] (s = 76) -> 0.500000:(s' = 92) + 0.500000:(s' = 93);
[] (s = 77) -> 0.500000:(s' = 94) + 0.500000:(s' = 95);
[] (s = 78) -> 0.500000:(s' = 92) + 0.500000:(s' = 94);
[] (s = 79) -> 0.500000:(s' = 93) + 0.500000:(s' = 95);
[] (s = 80) -> 0.500000:(s' = 96) + 0.500000:(s' = 97);
[] (s = 81) -> 0.500000:(s' = 98) + 0.500000:(s' = 99);
[] (s = 82) -> 0.500000:(s' = 96) + 0.500000:(s' = 98);
[] (s = 83) -> 0.500000:(s' = 97) + 0.500000:(s' = 99);
[] (s = 84) -> 1.000000:(s' = 100) ;
[] (s = 84) -> 1.000000:(s' = 101) ;
[] (s = 85) -> 1.000000:(s' = 102) ;
[] (s = 86) -> 1.000000:(s' = 102) ;
[] (s = 87) -> 1.000000:(s' = 103) ;
[] (s = 87) -> 1.000000:(s' = 102) ;
[] (s = 88) -> 1.000000:(s' = 103) ;
[] (s = 88) -> 1.000000:(s' = 102) ;
[] (s = 89) -> 1.000000:(s' = 104) ;
[] (s = 90) -> 1.000000:(s' = 104) ;
[] (s = 91) -> 1.000000:(s' = 105) ;
[] (s = 91) -> 1.000000:(s' = 104) ;
[] (s = 92) -> 1.000000:(s' = 105) ;
[] (s = 92) -> 1.000000:(s' = 104) ;
[] (s = 93) -> 1.000000:(s' = 106) ;
[] (s = 94) -> 1.000000:(s' = 106) ;
[] (s = 95) -> 1.000000:(s' = 107) ;
[] (s = 95) -> 1.000000:(s' = 106) ;
[] (s = 96) -> 1.000000:(s' = 107) ;
[] (s = 96) -> 1.000000:(s' = 106) ;
[] (s = 97) -> 1.000000:(s' = 108) ;
[] (s = 98) -> 1.000000:(s' = 108) ;
[] (s = 99) -> 1.000000:(s' = 109) ;
[] (s = 99) -> 1.000000:(s' = 108) ;
[] (s = 100) -> 0.500000:(s' = 110) + 0.500000:(s' = 111);
[] (s = 100) -> 0.500000:(s' = 112) + 0.500000:(s' = 113);
[] (s = 101) -> 1.000000:(s' = 17) ;
[] (s = 102) -> 1.000000:(s' = 17) ;
[] (s = 103) -> 0.500000:(s' = 114) + 0.500000:(s' = 115);
[] (s = 103) -> 0.500000:(s' = 116) + 0.500000:(s' = 117);
[] (s = 104) -> 1.000000:(s' = 17) ;
[] (s = 105) -> 0.500000:(s' = 118) + 0.500000:(s' = 119);
[] (s = 105) -> 0.500000:(s' = 120) + 0.500000:(s' = 121);
[] (s = 106) -> 1.000000:(s' = 17) ;
[] (s = 107) -> 0.500000:(s' = 122) + 0.500000:(s' = 123);
[] (s = 107) -> 0.500000:(s' = 124) + 0.500000:(s' = 125);
[] (s = 108) -> 1.000000:(s' = 17) ;
[] (s = 109) -> 0.500000:(s' = 126) + 0.500000:(s' = 127);
[] (s = 109) -> 0.500000:(s' = 128) + 0.500000:(s' = 129);
[] (s = 110) -> 0.500000:(s' = 130) + 0.500000:(s' = 131);
[] (s = 111) -> 0.500000:(s' = 132) + 0.500000:(s' = 133);
[] (s = 112) -> 0.500000:(s' = 130) + 0.500000:(s' = 132);
[] (s = 113) -> 0.500000:(s' = 131) + 0.500000:(s' = 133);
[] (s = 114) -> 0.500000:(s' = 134) + 0.500000:(s' = 135);
[] (s = 115) -> 0.500000:(s' = 136) + 0.500000:(s' = 137);
[] (s = 116) -> 0.500000:(s' = 134) + 0.500000:(s' = 136);
[] (s = 117) -> 0.500000:(s' = 135) + 0.500000:(s' = 137);
[] (s = 118) -> 0.500000:(s' = 138) + 0.500000:(s' = 139);
[] (s = 119) -> 0.500000:(s' = 140) + 0.500000:(s' = 141);
[] (s = 120) -> 0.500000:(s' = 138) + 0.500000:(s' = 140);
[] (s = 121) -> 0.500000:(s' = 139) + 0.500000:(s' = 141);
[] (s = 122) -> 0.500000:(s' = 142) + 0.500000:(s' = 143);
[] (s = 123) -> 0.500000:(s' = 144) + 0.500000:(s' = 145);
[] (s = 124) -> 0.500000:(s' = 142) + 0.500000:(s' = 144);
[] (s = 125) -> 0.500000:(s' = 143) + 0.500000:(s' = 145);
[] (s = 126) -> 0.500000:(s' = 146) + 0.500000:(s' = 147);
[] (s = 127) -> 0.500000:(s' = 148) + 0.500000:(s' = 149);
[] (s = 128) -> 0.500000:(s' = 146) + 0.500000:(s' = 148);
[] (s = 129) -> 0.500000:(s' = 147) + 0.500000:(s' = 149);
[] (s = 130) -> 1.000000:(s' = 150) ;
[] (s = 130) -> 1.000000:(s' = 151) ;
[] (s = 131) -> 1.000000:(s' = 152) ;
[] (s = 132) -> 1.000000:(s' = 152) ;
[] (s = 133) -> 1.000000:(s' = 153) ;
[] (s = 133) -> 1.000000:(s' = 152) ;
[] (s = 134) -> 1.000000:(s' = 153) ;
[] (s = 134) -> 1.000000:(s' = 152) ;
[] (s = 135) -> 1.000000:(s' = 154) ;
[] (s = 136) -> 1.000000:(s' = 154) ;
[] (s = 137) -> 1.000000:(s' = 155) ;
[] (s = 137) -> 1.000000:(s' = 154) ;
[] (s = 138) -> 1.000000:(s' = 155) ;
[] (s = 138) -> 1.000000:(s' = 154) ;
[] (s = 139) -> 1.000000:(s' = 156) ;
[] (s = 140) -> 1.000000:(s' = 156) ;
[] (s = 141) -> 1.000000:(s' = 157) ;
[] (s = 141) -> 1.000000:(s' = 156) ;
[] (s = 142) -> 1.000000:(s' = 157) ;
[] (s = 142) -> 1.000000:(s' = 156) ;
[] (s = 143) -> 1.000000:(s' = 158) ;
[] (s = 144) -> 1.000000:(s' = 158) ;
[] (s = 145) -> 1.000000:(s' = 159) ;
[] (s = 145) -> 1.000000:(s' = 158) ;
[] (s = 146) -> 1.000000:(s' = 159) ;
[] (s = 146) -> 1.000000:(s' = 158) ;
[] (s = 147) -> 1.000000:(s' = 160) ;
[] (s = 148) -> 1.000000:(s' = 160) ;
[] (s = 149) -> 1.000000:(s' = 161) ;
[] (s = 149) -> 1.000000:(s' = 160) ;
[] (s = 150) -> 0.500000:(s' = 162) + 0.500000:(s' = 163);
[] (s = 150) -> 0.500000:(s' = 164) + 0.500000:(s' = 165);
[] (s = 151) -> 1.000000:(s' = 17) ;
[] (s = 152) -> 1.000000:(s' = 17) ;
[] (s = 153) -> 0.500000:(s' = 166) + 0.500000:(s' = 167);
[] (s = 153) -> 0.500000:(s' = 168) + 0.500000:(s' = 169);
[] (s = 154) -> 1.000000:(s' = 17) ;
[] (s = 155) -> 0.500000:(s' = 170) + 0.500000:(s' = 171);
[] (s = 155) -> 0.500000:(s' = 172) + 0.500000:(s' = 173);
[] (s = 156) -> 1.000000:(s' = 17) ;
[] (s = 157) -> 0.500000:(s' = 174) + 0.500000:(s' = 175);
[] (s = 157) -> 0.500000:(s' = 176) + 0.500000:(s' = 177);
[] (s = 158) -> 1.000000:(s' = 17) ;
[] (s = 159) -> 0.500000:(s' = 178) + 0.500000:(s' = 179);
[] (s = 159) -> 0.500000:(s' = 180) + 0.500000:(s' = 181);
[] (s = 160) -> 1.000000:(s' = 17) ;
[] (s = 160) -> 1.000000:(s' = 182) ;
[] (s = 161) -> 0.500000:(s' = 183) + 0.500000:(s' = 184);
[] (s = 161) -> 0.500000:(s' = 185) + 0.500000:(s' = 186);
[] (s = 162) -> 0.500000:(s' = 187) + 0.500000:(s' = 188);
[] (s = 163) -> 0.500000:(s' = 189) + 0.500000:(s' = 190);
[] (s = 164) -> 0.500000:(s' = 187) + 0.500000:(s' = 189);
[] (s = 165) -> 0.500000:(s' = 188) + 0.500000:(s' = 190);
[] (s = 166) -> 0.500000:(s' = 191) + 0.500000:(s' = 192);
[] (s = 167) -> 0.500000:(s' = 193) + 0.500000:(s' = 194);
[] (s = 168) -> 0.500000:(s' = 191) + 0.500000:(s' = 193);
[] (s = 169) -> 0.500000:(s' = 192) + 0.500000:(s' = 194);
[] (s = 170) -> 0.500000:(s' = 195) + 0.500000:(s' = 196);
[] (s = 171) -> 0.500000:(s' = 197) + 0.500000:(s' = 198);
[] (s = 172) -> 0.500000:(s' = 195) + 0.500000:(s' = 197);
[] (s = 173) -> 0.500000:(s' = 196) + 0.500000:(s' = 198);
[] (s = 174) -> 0.500000:(s' = 199) + 0.500000:(s' = 200);
[] (s = 175) -> 0.500000:(s' = 201) + 0.500000:(s' = 202);
[] (s = 176) -> 0.500000:(s' = 199) + 0.500000:(s' = 201);
[] (s = 177) -> 0.500000:(s' = 200) + 0.500000:(s' = 202);
[] (s = 178) -> 0.500000:(s' = 203) + 0.500000:(s' = 204);
[] (s = 179) -> 0.500000:(s' = 205) + 0.500000:(s' = 206);
[] (s = 180) -> 0.500000:(s' = 203) + 0.500000:(s' = 205);
[] (s = 181) -> 0.500000:(s' = 204) + 0.500000:(s' = 206);
[] (s = 183) -> 0.500000:(s' = 207) + 0.500000:(s' = 208);
[] (s = 184) -> 0.500000:(s' = 209) + 0.500000:(s' = 210);
[] (s = 185) -> 0.500000:(s' = 207) + 0.500000:(s' = 209);
[] (s = 186) -> 0.500000:(s' = 208) + 0.500000:(s' = 210);
[] (s = 187) -> 1.000000:(s' = 211) ;
[] (s = 187) -> 1.000000:(s' = 212) ;
[] (s = 188) -> 1.000000:(s' = 213) ;
[] (s = 189) -> 1.000000:(s' = 213) ;
[] (s = 190) -> 1.000000:(s' = 214) ;
[] (s = 190) -> 1.000000:(s' = 213) ;
[] (s = 191) -> 1.000000:(s' = 214) ;
[] (s = 191) -> 1.000000:(s' = 213) ;
[] (s = 192) -> 1.000000:(s' = 215) ;
[] (s = 193) -> 1.000000:(s' = 215) ;
[] (s = 194) -> 1.000000:(s' = 216) ;
[] (s = 194) -> 1.000000:(s' = 215) ;
[] (s = 195) -> 1.000000:(s' = 216) ;
[] (s = 195) -> 1.000000:(s' = 215) ;
[] (s = 196) -> 1.000000:(s' = 217) ;
[] (s = 197) -> 1.000000:(s' = 217) ;
[] (s = 198) -> 1.000000:(s' = 218) ;
[] (s = 198) -> 1.000000:(s' = 217) ;
[] (s = 199) -> 1.000000:(s' = 218) ;
[] (s = 199) -> 1.000000:(s' = 217) ;
[] (s = 200) -> 1.000000:(s' = 219) ;
[] (s = 201) -> 1.000000:(s' = 219) ;
[] (s = 202) -> 1.000000:(s' = 220) ;
[] (s = 202) -> 1.000000:(s' = 219) ;
[] (s = 203) -> 1.000000:(s' = 220) ;
[] (s = 203) -> 1.000000:(s' = 219) ;
[] (s = 204) -> 1.000000:(s' = 221) ;
[] (s = 205) -> 1.000000:(s' = 221) ;
[] (s = 206) -> 1.000000:(s' = 222) ;
[] (s = 206) -> 1.000000:(s' = 221) ;
[] (s = 207) -> 1.000000:(s' = 222) ;
[] (s = 207) -> 1.000000:(s' = 221) ;
[] (s = 208) -> 1.000000:(s' = 223) ;
[] (s = 209) -> 1.000000:(s' = 223) ;
[] (s = 210) -> 1.000000:(s' = 224) ;
[] (s = 210) -> 1.000000:(s' = 223) ;
[] (s = 211) -> 0.500000:(s' = 225) + 0.500000:(s' = 226);
[] (s = 211) -> 0.500000:(s' = 227) + 0.500000:(s' = 228);
[] (s = 212) -> 1.000000:(s' = 17) ;
[] (s = 213) -> 1.000000:(s' = 17) ;
[] (s = 214) -> 0.500000:(s' = 229) + 0.500000:(s' = 230);
[] (s = 214) -> 0.500000:(s' = 231) + 0.500000:(s' = 232);
[] (s = 215) -> 1.000000:(s' = 17) ;
[] (s = 216) -> 0.500000:(s' = 233) + 0.500000:(s' = 234);
[] (s = 216) -> 0.500000:(s' = 235) + 0.500000:(s' = 236);
[] (s = 217) -> 1.000000:(s' = 17) ;
[] (s = 218) -> 0.500000:(s' = 237) + 0.500000:(s' = 238);
[] (s = 218) -> 0.500000:(s' = 239) + 0.500000:(s' = 240);
[] (s = 219) -> 1.000000:(s' = 17) ;
[] (s = 219) -> 1.000000:(s' = 182) ;
[] (s = 220) -> 0.500000:(s' = 241) + 0.500000:(s' = 242);
[] (s = 220) -> 0.500000:(s' = 243) + 0.500000:(s' = 244);
[] (s = 221) -> 1.000000:(s' = 17) ;
[] (s = 221) -> 1.000000:(s' = 182) ;
[] (s = 222) -> 0.500000:(s' = 245) + 0.500000:(s' = 246);
[] (s = 222) -> 0.500000:(s' = 247) + 0.500000:(s' = 248);
[] (s = 223) -> 1.000000:(s' = 17) ;
[] (s = 223) -> 1.000000:(s' = 182) ;
[] (s = 224) -> 0.500000:(s' = 249) + 0.500000:(s' = 250);
[] (s = 224) -> 0.500000:(s' = 251) + 0.500000:(s' = 252);
[] (s = 225) -> 0.500000:(s' = 253) + 0.500000:(s' = 254);
[] (s = 226) -> 0.500000:(s' = 255) + 0.500000:(s' = 256);
[] (s = 227) -> 0.500000:(s' = 253) + 0.500000:(s' = 255);
[] (s = 228) -> 0.500000:(s' = 254) + 0.500000:(s' = 256);
[] (s = 229) -> 0.500000:(s' = 257) + 0.500000:(s' = 258);
[] (s = 230) -> 0.500000:(s' = 259) + 0.500000:(s' = 260);
[] (s = 231) -> 0.500000:(s' = 257) + 0.500000:(s' = 259);
[] (s = 232) -> 0.500000:(s' = 258) + 0.500000:(s' = 260);
[] (s = 233) -> 0.500000:(s' = 261) + 0.500000:(s' = 262);
[] (s = 234) -> 0.500000:(s' = 263) + 0.500000:(s' = 264);
[] (s = 235) -> 0.500000:(s' = 261) + 0.500000:(s' = 263);
[] (s = 236) -> 0.500000:(s' = 262) + 0.500000:(s' = 264);
[] (s = 237) -> 0.500000:(s' = 265) + 0.500000:(s' = 266);
[] (s = 238) -> 0.500000:(s' = 267) + 0.500000:(s' = 268);
[] (s = 239) -> 0.500000:(s' = 265) + 0.500000:(s' = 267);
[] (s = 240) -> 0.500000:(s' = 266) + 0.500000:(s' = 268);
[] (s = 241) -> 0.500000:(s' = 269) + 0.500000:(s' = 270);
[] (s = 242) -> 0.500000:(s' = 271) + 0.500000:(s' = 272);
[] (s = 243) -> 0.500000:(s' = 269) + 0.500000:(s' = 271);
[] (s = 244) -> 0.500000:(s' = 270) + 0.500000:(s' = 272);
[] (s = 245) -> 0.500000:(s' = 273) + 0.500000:(s' = 274);
[] (s = 246) -> 0.500000:(s' = 275) + 0.500000:(s' = 276);
[] (s = 247) -> 0.500000:(s' = 273) + 0.500000:(s' = 275);
[] (s = 248) -> 0.500000:(s' = 274) + 0.500000:(s' = 276);
[] (s = 249) -> 0.500000:(s' = 277) + 0.500000:(s' = 278);
[] (s = 250) -> 0.500000:(s' = 279) + 0.500000:(s' = 280);
[] (s = 251) -> 0.500000:(s' = 277) + 0.500000:(s' = 279);
[] (s = 252) -> 0.500000:(s' = 278) + 0.500000:(s' = 280);
[] (s = 253) -> 1.000000:(s' = 281) ;
[] (s = 253) -> 1.000000:(s' = 282) ;
[] (s = 254) -> 1.000000:(s' = 283) ;
[] (s = 255) -> 1.000000:(s' = 283) ;
[] (s = 256) -> 1.000000:(s' = 284) ;
[] (s = 256) -> 1.000000:(s' = 283) ;
[] (s = 257) -> 1.000000:(s' = 284) ;
[] (s = 257) -> 1.000000:(s' = 283) ;
[] (s = 258) -> 1.000000:(s' = 285) ;
[] (s = 259) -> 1.000000:(s' = 285) ;
[] (s = 260) -> 1.000000:(s' = 286) ;
[] (s = 260) -> 1.000000:(s' = 285) ;
[] (s = 261) -> 1.000000:(s' = 286) ;
[] (s = 261) -> 1.000000:(s' = 285) ;
[] (s = 262) -> 1.000000:(s' = 287) ;
[] (s = 263) -> 1.000000:(s' = 287) ;
[] (s = 264) -> 1.000000:(s' = 288) ;
[] (s = 264) -> 1.000000:(s' = 287) ;
[] (s = 265) -> 1.000000:(s' = 288) ;
[] (s = 265) -> 1.000000:(s' = 287) ;
[] (s = 266) -> 1.000000:(s' = 289) ;
[] (s = 267) -> 1.000000:(s' = 289) ;
[] (s = 268) -> 1.000000:(s' = 290) ;
[] (s = 268) -> 1.000000:(s' = 289) ;
[] (s = 269) -> 1.000000:(s' = 290) ;
[] (s = 269) -> 1.000000:(s' = 289) ;
[] (s = 270) -> 1.000000:(s' = 291) ;
[] (s = 271) -> 1.000000:(s' = 291) ;
[] (s = 272) -> 1.000000:(s' = 292) ;
[] (s = 272) -> 1.000000:(s' = 291) ;
[] (s = 273) -> 1.000000:(s' = 292) ;
[] (s = 273) -> 1.000000:(s' = 291) ;
[] (s = 274) -> 1.000000:(s' = 293) ;
[] (s = 275) -> 1.000000:(s' = 293) ;
[] (s = 276) -> 1.000000:(s' = 294) ;
[] (s = 276) -> 1.000000:(s' = 293) ;
[] (s = 277) -> 1.000000:(s' = 294) ;
[] (s = 277) -> 1.000000:(s' = 293) ;
[] (s = 278) -> 1.000000:(s' = 295) ;
[] (s = 279) -> 1.000000:(s' = 295) ;
[] (s = 280) -> 1.000000:(s' = 294) ;
[] (s = 280) -> 1.000000:(s' = 295) ;
[] (s = 281) -> 0.500000:(s' = 296) + 0.500000:(s' = 297);
[] (s = 281) -> 0.500000:(s' = 298) + 0.500000:(s' = 299);
[] (s = 282) -> 1.000000:(s' = 17) ;
[] (s = 283) -> 1.000000:(s' = 17) ;
[] (s = 284) -> 0.500000:(s' = 300) + 0.500000:(s' = 301);
[] (s = 284) -> 0.500000:(s' = 302) + 0.500000:(s' = 303);
[] (s = 285) -> 1.000000:(s' = 17) ;
[] (s = 285) -> 1.000000:(s' = 182) ;
[] (s = 286) -> 0.500000:(s' = 304) + 0.500000:(s' = 305);
[] (s = 286) -> 0.500000:(s' = 306) + 0.500000:(s' = 307);
[] (s = 287) -> 1.000000:(s' = 17) ;
[] (s = 287) -> 1.000000:(s' = 182) ;
[] (s = 288) -> 0.500000:(s' = 308) + 0.500000:(s' = 309);
[] (s = 288) -> 0.500000:(s' = 310) + 0.500000:(s' = 311);
[] (s = 289) -> 1.000000:(s' = 17) ;
[] (s = 289) -> 1.000000:(s' = 182) ;
[] (s = 290) -> 0.500000:(s' = 312) + 0.500000:(s' = 313);
[] (s = 290) -> 0.500000:(s' = 314) + 0.500000:(s' = 315);
[] (s = 291) -> 1.000000:(s' = 17) ;
[] (s = 291) -> 1.000000:(s' = 182) ;
[] (s = 292) -> 0.500000:(s' = 316) + 0.500000:(s' = 317);
[] (s = 292) -> 0.500000:(s' = 318) + 0.500000:(s' = 319);
[] (s = 293) -> 1.000000:(s' = 17) ;
[] (s = 293) -> 1.000000:(s' = 182) ;
[] (s = 294) -> 0.500000:(s' = 320) + 0.500000:(s' = 321);
[] (s = 294) -> 0.500000:(s' = 322) + 0.500000:(s' = 323);
[] (s = 295) -> 1.000000:(s' = 182) ;
[] (s = 296) -> 0.500000:(s' = 324) + 0.500000:(s' = 325);
[] (s = 297) -> 0.500000:(s' = 326) + 0.500000:(s' = 327);
[] (s = 298) -> 0.500000:(s' = 324) + 0.500000:(s' = 326);
[] (s = 299) -> 0.500000:(s' = 325) + 0.500000:(s' = 327);
[] (s = 300) -> 0.500000:(s' = 328) + 0.500000:(s' = 329);
[] (s = 301) -> 0.500000:(s' = 330) + 0.500000:(s' = 331);
[] (s = 302) -> 0.500000:(s' = 328) + 0.500000:(s' = 330);
[] (s = 303) -> 0.500000:(s' = 329) + 0.500000:(s' = 331);
[] (s = 304) -> 0.500000:(s' = 332) + 0.500000:(s' = 333);
[] (s = 305) -> 0.500000:(s' = 334) + 0.500000:(s' = 335);
[] (s = 306) -> 0.500000:(s' = 332) + 0.500000:(s' = 334);
[] (s = 307) -> 0.500000:(s' = 333) + 0.500000:(s' = 335);
[] (s = 308) -> 0.500000:(s' = 336) + 0.500000:(s' = 337);
[] (s = 309) -> 0.500000:(s' = 338) + 0.500000:(s' = 339);
[] (s = 310) -> 0.500000:(s' = 336) + 0.500000:(s' = 338);
[] (s = 311) -> 0.500000:(s' = 337) + 0.500000:(s' = 339);
[] (s = 312) -> 0.500000:(s' = 340) + 0.500000:(s' = 341);
[] (s = 313) -> 0.500000:(s' = 342) + 0.500000:(s' = 343);
[] (s = 314) -> 0.500000:(s' = 340) + 0.500000:(s' = 342);
[] (s = 315) -> 0.500000:(s' = 341) + 0.500000:(s' = 343);
[] (s = 316) -> 0.500000:(s' = 344) + 0.500000:(s' = 345);
[] (s = 317) -> 0.500000:(s' = 346) + 0.500000:(s' = 347);
[] (s = 318) -> 0.500000:(s' = 344) + 0.500000:(s' = 346);
[] (s = 319) -> 0.500000:(s' = 345) + 0.500000:(s' = 347);
[] (s = 320) -> 0.500000:(s' = 348) + 0.500000:(s' = 349);
[] (s = 321) -> 0.500000:(s' = 350) + 0.500000:(s' = 351);
[] (s = 322) -> 0.500000:(s' = 348) + 0.500000:(s' = 350);
[] (s = 323) -> 0.500000:(s' = 349) + 0.500000:(s' = 351);
[] (s = 324) -> 1.000000:(s' = 352) ;
[] (s = 324) -> 1.000000:(s' = 353) ;
[] (s = 325) -> 1.000000:(s' = 354) ;
[] (s = 326) -> 1.000000:(s' = 354) ;
[] (s = 327) -> 1.000000:(s' = 355) ;
[] (s = 327) -> 1.000000:(s' = 354) ;
[] (s = 328) -> 1.000000:(s' = 355) ;
[] (s = 328) -> 1.000000:(s' = 354) ;
[] (s = 329) -> 1.000000:(s' = 356) ;
[] (s = 330) -> 1.000000:(s' = 356) ;
[] (s = 331) -> 1.000000:(s' = 357) ;
[] (s = 331) -> 1.000000:(s' = 356) ;
[] (s = 332) -> 1.000000:(s' = 357) ;
[] (s = 332) -> 1.000000:(s' = 356) ;
[] (s = 333) -> 1.000000:(s' = 358) ;
[] (s = 334) -> 1.000000:(s' = 358) ;
[] (s = 335) -> 1.000000:(s' = 359) ;
[] (s = 335) -> 1.000000:(s' = 358) ;
[] (s = 336) -> 1.000000:(s' = 359) ;
[] (s = 336) -> 1.000000:(s' = 358) ;
[] (s = 337) -> 1.000000:(s' = 360) ;
[] (s = 338) -> 1.000000:(s' = 360) ;
[] (s = 339) -> 1.000000:(s' = 361) ;
[] (s = 339) -> 1.000000:(s' = 360) ;
[] (s = 340) -> 1.000000:(s' = 361) ;
[] (s = 340) -> 1.000000:(s' = 360) ;
[] (s = 341) -> 1.000000:(s' = 362) ;
[] (s = 342) -> 1.000000:(s' = 362) ;
[] (s = 343) -> 1.000000:(s' = 294) ;
[] (s = 343) -> 1.000000:(s' = 362) ;
[] (s = 344) -> 1.000000:(s' = 294) ;
[] (s = 344) -> 1.000000:(s' = 362) ;
[] (s = 345) -> 1.000000:(s' = 295) ;
[] (s = 346) -> 1.000000:(s' = 295) ;
[] (s = 347) -> 1.000000:(s' = 294) ;
[] (s = 347) -> 1.000000:(s' = 295) ;
[] (s = 348) -> 1.000000:(s' = 294) ;
[] (s = 348) -> 1.000000:(s' = 295) ;
[] (s = 349) -> 1.000000:(s' = 295) ;
[] (s = 350) -> 1.000000:(s' = 295) ;
[] (s = 351) -> 1.000000:(s' = 294) ;
[] (s = 351) -> 1.000000:(s' = 295) ;
[] (s = 352) -> 0.500000:(s' = 363) + 0.500000:(s' = 364);
[] (s = 352) -> 0.500000:(s' = 365) + 0.500000:(s' = 366);
[] (s = 353) -> 1.000000:(s' = 17) ;
[] (s = 354) -> 1.000000:(s' = 17) ;
[] (s = 354) -> 1.000000:(s' = 182) ;
[] (s = 355) -> 0.500000:(s' = 367) + 0.500000:(s' = 368);
[] (s = 355) -> 0.500000:(s' = 369) + 0.500000:(s' = 370);
[] (s = 356) -> 1.000000:(s' = 17) ;
[] (s = 356) -> 1.000000:(s' = 182) ;
[] (s = 357) -> 0.500000:(s' = 371) + 0.500000:(s' = 372);
[] (s = 357) -> 0.500000:(s' = 373) + 0.500000:(s' = 374);
[] (s = 358) -> 1.000000:(s' = 17) ;
[] (s = 358) -> 1.000000:(s' = 182) ;
[] (s = 359) -> 0.500000:(s' = 375) + 0.500000:(s' = 376);
[] (s = 359) -> 0.500000:(s' = 377) + 0.500000:(s' = 378);
[] (s = 360) -> 1.000000:(s' = 17) ;
[] (s = 360) -> 1.000000:(s' = 182) ;
[] (s = 361) -> 0.500000:(s' = 379) + 0.500000:(s' = 380);
[] (s = 361) -> 0.500000:(s' = 381) + 0.500000:(s' = 382);
[] (s = 362) -> 1.000000:(s' = 17) ;
[] (s = 362) -> 1.000000:(s' = 182) ;
[] (s = 363) -> 0.500000:(s' = 383) + 0.500000:(s' = 384);
[] (s = 364) -> 0.500000:(s' = 385) + 0.500000:(s' = 386);
[] (s = 365) -> 0.500000:(s' = 383) + 0.500000:(s' = 385);
[] (s = 366) -> 0.500000:(s' = 384) + 0.500000:(s' = 386);
[] (s = 367) -> 0.500000:(s' = 387) + 0.500000:(s' = 388);
[] (s = 368) -> 0.500000:(s' = 389) + 0.500000:(s' = 390);
[] (s = 369) -> 0.500000:(s' = 387) + 0.500000:(s' = 389);
[] (s = 370) -> 0.500000:(s' = 388) + 0.500000:(s' = 390);
[] (s = 371) -> 0.500000:(s' = 391) + 0.500000:(s' = 392);
[] (s = 372) -> 0.500000:(s' = 393) + 0.500000:(s' = 394);
[] (s = 373) -> 0.500000:(s' = 391) + 0.500000:(s' = 393);
[] (s = 374) -> 0.500000:(s' = 392) + 0.500000:(s' = 394);
[] (s = 375) -> 0.500000:(s' = 395) + 0.500000:(s' = 396);
[] (s = 376) -> 0.500000:(s' = 397) + 0.500000:(s' = 398);
[] (s = 377) -> 0.500000:(s' = 395) + 0.500000:(s' = 397);
[] (s = 378) -> 0.500000:(s' = 396) + 0.500000:(s' = 398);
[] (s = 379) -> 0.500000:(s' = 399) + 0.500000:(s' = 400);
[] (s = 380) -> 0.500000:(s' = 401) + 0.500000:(s' = 402);
[] (s = 381) -> 0.500000:(s' = 399) + 0.500000:(s' = 401);
[] (s = 382) -> 0.500000:(s' = 400) + 0.500000:(s' = 402);
[] (s = 383) -> 1.000000:(s' = 403) ;
[] (s = 383) -> 1.000000:(s' = 404) ;
[] (s = 384) -> 1.000000:(s' = 405) ;
[] (s = 385) -> 1.000000:(s' = 405) ;
[] (s = 386) -> 1.000000:(s' = 406) ;
[] (s = 386) -> 1.000000:(s' = 405) ;
[] (s = 387) -> 1.000000:(s' = 406) ;
[] (s = 387) -> 1.000000:(s' = 405) ;
[] (s = 388) -> 1.000000:(s' = 407) ;
[] (s = 389) -> 1.000000:(s' = 407) ;
[] (s = 390) -> 1.000000:(s' = 408) ;
[] (s = 390) -> 1.000000:(s' = 407) ;
[] (s = 391) -> 1.000000:(s' = 408) ;
[] (s = 391) -> 1.000000:(s' = 407) ;
[] (s = 392) -> 1.000000:(s' = 409) ;
[] (s = 393) -> 1.000000:(s' = 409) ;
[] (s = 394) -> 1.000000:(s' = 410) ;
[] (s = 394) -> 1.000000:(s' = 409) ;
[] (s = 395) -> 1.000000:(s' = 410) ;
[] (s = 395) -> 1.000000:(s' = 409) ;
[] (s = 396) -> 1.000000:(s' = 411) ;
[] (s = 397) -> 1.000000:(s' = 411) ;
[] (s = 398) -> 1.000000:(s' = 294) ;
[] (s = 398) -> 1.000000:(s' = 411) ;
[] (s = 399) -> 1.000000:(s' = 294) ;
[] (s = 399) -> 1.000000:(s' = 411) ;
[] (s = 400) -> 1.000000:(s' = 295) ;
[] (s = 401) -> 1.000000:(s' = 295) ;
[] (s = 402) -> 1.000000:(s' = 294) ;
[] (s = 402) -> 1.000000:(s' = 295) ;
[] (s = 403) -> 0.500000:(s' = 412) + 0.500000:(s' = 413);
[] (s = 403) -> 0.500000:(s' = 414) + 0.500000:(s' = 415);
[] (s = 404) -> 1.000000:(s' = 17) ;
[] (s = 404) -> 1.000000:(s' = 182) ;
[] (s = 405) -> 1.000000:(s' = 17) ;
[] (s = 405) -> 1.000000:(s' = 182) ;
[] (s = 406) -> 0.500000:(s' = 416) + 0.500000:(s' = 417);
[] (s = 406) -> 0.500000:(s' = 418) + 0.500000:(s' = 419);
[] (s = 407) -> 1.000000:(s' = 17) ;
[] (s = 407) -> 1.000000:(s' = 182) ;
[] (s = 408) -> 0.500000:(s' = 420) + 0.500000:(s' = 421);
[] (s = 408) -> 0.500000:(s' = 422) + 0.500000:(s' = 423);
[] (s = 409) -> 1.000000:(s' = 17) ;
[] (s = 409) -> 1.000000:(s' = 182) ;
[] (s = 410) -> 0.500000:(s' = 424) + 0.500000:(s' = 425);
[] (s = 410) -> 0.500000:(s' = 426) + 0.500000:(s' = 427);
[] (s = 411) -> 1.000000:(s' = 17) ;
[] (s = 411) -> 1.000000:(s' = 182) ;
[] (s = 412) -> 0.500000:(s' = 428) + 0.500000:(s' = 429);
[] (s = 413) -> 0.500000:(s' = 430) + 0.500000:(s' = 431);
[] (s = 414) -> 0.500000:(s' = 428) + 0.500000:(s' = 430);
[] (s = 415) -> 0.500000:(s' = 429) + 0.500000:(s' = 431);
[] (s = 416) -> 0.500000:(s' = 432) + 0.500000:(s' = 433);
[] (s = 417) -> 0.500000:(s' = 434) + 0.500000:(s' = 435);
[] (s = 418) -> 0.500000:(s' = 432) + 0.500000:(s' = 434);
[] (s = 419) -> 0.500000:(s' = 433) + 0.500000:(s' = 435);
[] (s = 420) -> 0.500000:(s' = 436) + 0.500000:(s' = 437);
[] (s = 421) -> 0.500000:(s' = 438) + 0.500000:(s' = 439);
[] (s = 422) -> 0.500000:(s' = 436) + 0.500000:(s' = 438);
[] (s = 423) -> 0.500000:(s' = 437) + 0.500000:(s' = 439);
[] (s = 424) -> 0.500000:(s' = 440) + 0.500000:(s' = 441);
[] (s = 425) -> 0.500000:(s' = 442) + 0.500000:(s' = 443);
[] (s = 426) -> 0.500000:(s' = 440) + 0.500000:(s' = 442);
[] (s = 427) -> 0.500000:(s' = 441) + 0.500000:(s' = 443);
[] (s = 428) -> 1.000000:(s' = 444) ;
[] (s = 428) -> 1.000000:(s' = 445) ;
[] (s = 429) -> 1.000000:(s' = 446) ;
[] (s = 430) -> 1.000000:(s' = 446) ;
[] (s = 431) -> 1.000000:(s' = 447) ;
[] (s = 431) -> 1.000000:(s' = 446) ;
[] (s = 432) -> 1.000000:(s' = 447) ;
[] (s = 432) -> 1.000000:(s' = 446) ;
[] (s = 433) -> 1.000000:(s' = 448) ;
[] (s = 434) -> 1.000000:(s' = 448) ;
[] (s = 435) -> 1.000000:(s' = 449) ;
[] (s = 435) -> 1.000000:(s' = 448) ;
[] (s = 436) -> 1.000000:(s' = 449) ;
[] (s = 436) -> 1.000000:(s' = 448) ;
[] (s = 437) -> 1.000000:(s' = 450) ;
[] (s = 438) -> 1.000000:(s' = 450) ;
[] (s = 439) -> 1.000000:(s' = 294) ;
[] (s = 439) -> 1.000000:(s' = 450) ;
[] (s = 440) -> 1.000000:(s' = 294) ;
[] (s = 440) -> 1.000000:(s' = 450) ;
[] (s = 441) -> 1.000000:(s' = 295) ;
[] (s = 442) -> 1.000000:(s' = 295) ;
[] (s = 443) -> 1.000000:(s' = 294) ;
[] (s = 443) -> 1.000000:(s' = 295) ;
[] (s = 444) -> 0.500000:(s' = 451) + 0.500000:(s' = 452);
[] (s = 444) -> 0.500000:(s' = 453) + 0.500000:(s' = 454);
[] (s = 445) -> 1.000000:(s' = 17) ;
[] (s = 445) -> 1.000000:(s' = 182) ;
[] (s = 446) -> 1.000000:(s' = 17) ;
[] (s = 446) -> 1.000000:(s' = 182) ;
[] (s = 447) -> 0.500000:(s' = 455) + 0.500000:(s' = 456);
[] (s = 447) -> 0.500000:(s' = 457) + 0.500000:(s' = 458);
[] (s = 448) -> 1.000000:(s' = 17) ;
[] (s = 448) -> 1.000000:(s' = 182) ;
[] (s = 449) -> 0.500000:(s' = 459) + 0.500000:(s' = 460);
[] (s = 449) -> 0.500000:(s' = 461) + 0.500000:(s' = 462);
[] (s = 450) -> 1.000000:(s' = 17) ;
[] (s = 450) -> 1.000000:(s' = 182) ;
[] (s = 451) -> 0.500000:(s' = 463) + 0.500000:(s' = 464);
[] (s = 452) -> 0.500000:(s' = 465) + 0.500000:(s' = 466);
[] (s = 453) -> 0.500000:(s' = 463) + 0.500000:(s' = 465);
[] (s = 454) -> 0.500000:(s' = 464) + 0.500000:(s' = 466);
[] (s = 455) -> 0.500000:(s' = 467) + 0.500000:(s' = 468);
[] (s = 456) -> 0.500000:(s' = 469) + 0.500000:(s' = 470);
[] (s = 457) -> 0.500000:(s' = 467) + 0.500000:(s' = 469);
[] (s = 458) -> 0.500000:(s' = 468) + 0.500000:(s' = 470);
[] (s = 459) -> 0.500000:(s' = 471) + 0.500000:(s' = 472);
[] (s = 460) -> 0.500000:(s' = 473) + 0.500000:(s' = 474);
[] (s = 461) -> 0.500000:(s' = 471) + 0.500000:(s' = 473);
[] (s = 462) -> 0.500000:(s' = 472) + 0.500000:(s' = 474);
[] (s = 463) -> 1.000000:(s' = 475) ;
[] (s = 463) -> 1.000000:(s' = 476) ;
[] (s = 464) -> 1.000000:(s' = 477) ;
[] (s = 465) -> 1.000000:(s' = 477) ;
[] (s = 466) -> 1.000000:(s' = 478) ;
[] (s = 466) -> 1.000000:(s' = 477) ;
[] (s = 467) -> 1.000000:(s' = 478) ;
[] (s = 467) -> 1.000000:(s' = 477) ;
[] (s = 468) -> 1.000000:(s' = 479) ;
[] (s = 469) -> 1.000000:(s' = 479) ;
[] (s = 470) -> 1.000000:(s' = 294) ;
[] (s = 470) -> 1.000000:(s' = 479) ;
[] (s = 471) -> 1.000000:(s' = 294) ;
[] (s = 471) -> 1.000000:(s' = 479) ;
[] (s = 472) -> 1.000000:(s' = 295) ;
[] (s = 473) -> 1.000000:(s' = 295) ;
[] (s = 474) -> 1.000000:(s' = 294) ;
[] (s = 474) -> 1.000000:(s' = 295) ;
[] (s = 475) -> 0.500000:(s' = 480) + 0.500000:(s' = 481);
[] (s = 475) -> 0.500000:(s' = 482) + 0.500000:(s' = 483);
[] (s = 476) -> 1.000000:(s' = 17) ;
[] (s = 476) -> 1.000000:(s' = 182) ;
[] (s = 477) -> 1.000000:(s' = 17) ;
[] (s = 477) -> 1.000000:(s' = 182) ;
[] (s = 478) -> 0.500000:(s' = 484) + 0.500000:(s' = 485);
[] (s = 478) -> 0.500000:(s' = 486) + 0.500000:(s' = 487);
[] (s = 479) -> 1.000000:(s' = 17) ;
[] (s = 479) -> 1.000000:(s' = 182) ;
[] (s = 480) -> 0.500000:(s' = 488) + 0.500000:(s' = 489);
[] (s = 481) -> 0.500000:(s' = 490) + 0.500000:(s' = 491);
[] (s = 482) -> 0.500000:(s' = 488) + 0.500000:(s' = 490);
[] (s = 483) -> 0.500000:(s' = 489) + 0.500000:(s' = 491);
[] (s = 484) -> 0.500000:(s' = 492) + 0.500000:(s' = 493);
[] (s = 485) -> 0.500000:(s' = 494) + 0.500000:(s' = 495);
[] (s = 486) -> 0.500000:(s' = 492) + 0.500000:(s' = 494);
[] (s = 487) -> 0.500000:(s' = 493) + 0.500000:(s' = 495);
[] (s = 488) -> 1.000000:(s' = 496) ;
[] (s = 488) -> 1.000000:(s' = 497) ;
[] (s = 489) -> 1.000000:(s' = 498) ;
[] (s = 490) -> 1.000000:(s' = 498) ;
[] (s = 491) -> 1.000000:(s' = 499) ;
[] (s = 491) -> 1.000000:(s' = 498) ;
[] (s = 492) -> 1.000000:(s' = 499) ;
[] (s = 492) -> 1.000000:(s' = 498) ;
[] (s = 493) -> 1.000000:(s' = 295) ;
[] (s = 494) -> 1.000000:(s' = 295) ;
[] (s = 495) -> 1.000000:(s' = 294) ;
[] (s = 495) -> 1.000000:(s' = 295) ;
[] (s = 496) -> 0.500000:(s' = 500) + 0.500000:(s' = 501);
[] (s = 496) -> 0.500000:(s' = 502) + 0.500000:(s' = 503);
[] (s = 497) -> 1.000000:(s' = 17) ;
[] (s = 497) -> 1.000000:(s' = 182) ;
[] (s = 498) -> 1.000000:(s' = 17) ;
[] (s = 498) -> 1.000000:(s' = 182) ;
[] (s = 499) -> 0.500000:(s' = 504) + 0.500000:(s' = 505);
[] (s = 499) -> 0.500000:(s' = 506) + 0.500000:(s' = 507);
[] (s = 500) -> 0.500000:(s' = 508) + 0.500000:(s' = 509);
[] (s = 501) -> 0.500000:(s' = 510) + 0.500000:(s' = 511);
[] (s = 502) -> 0.500000:(s' = 508) + 0.500000:(s' = 510);
[] (s = 503) -> 0.500000:(s' = 509) + 0.500000:(s' = 511);
[] (s = 504) -> 0.500000:(s' = 512) + 0.500000:(s' = 513);
[] (s = 505) -> 0.500000:(s' = 514) + 0.500000:(s' = 515);
[] (s = 506) -> 0.500000:(s' = 512) + 0.500000:(s' = 514);
[] (s = 507) -> 0.500000:(s' = 513) + 0.500000:(s' = 515);
[] (s = 508) -> 1.000000:(s' = 516) ;
[] (s = 508) -> 1.000000:(s' = 517) ;
[] (s = 509) -> 1.000000:(s' = 295) ;
[] (s = 510) -> 1.000000:(s' = 295) ;
[] (s = 511) -> 1.000000:(s' = 294) ;
[] (s = 511) -> 1.000000:(s' = 295) ;
[] (s = 512) -> 1.000000:(s' = 294) ;
[] (s = 512) -> 1.000000:(s' = 295) ;
[] (s = 513) -> 1.000000:(s' = 295) ;
[] (s = 514) -> 1.000000:(s' = 295) ;
[] (s = 515) -> 1.000000:(s' = 294) ;
[] (s = 515) -> 1.000000:(s' = 295) ;
[] (s = 516) -> 0.500000:(s' = 518) + 0.500000:(s' = 519);
[] (s = 516) -> 0.500000:(s' = 520) + 0.500000:(s' = 521);
[] (s = 517) -> 1.000000:(s' = 17) ;
[] (s = 517) -> 1.000000:(s' = 182) ;
[] (s = 518) -> 0.500000:(s' = 522) + 0.500000:(s' = 523);
[] (s = 519) -> 0.500000:(s' = 524) + 0.500000:(s' = 525);
[] (s = 520) -> 0.500000:(s' = 522) + 0.500000:(s' = 524);
[] (s = 521) -> 0.500000:(s' = 523) + 0.500000:(s' = 525);
[] (s = 522) -> 1.000000:(s' = 294) ;
[] (s = 522) -> 1.000000:(s' = 295) ;
[] (s = 523) -> 1.000000:(s' = 295) ;
[] (s = 524) -> 1.000000:(s' = 295) ;
[] (s = 525) -> 1.000000:(s' = 294) ;
[] (s = 525) -> 1.000000:(s' = 295) ;

endmodule