(************************************************************ * IMITATOR MODEL * * Parametric timed pattern matching benchmark: blowup (designed on purpose to test the limits of our algorithm) * * Description : Template of a timed word alternating between a and c * Correctness : N/A * Source : Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018) * Author : Étienne André and Masaki Waga * Modeling : Étienne André and Masaki Waga * Input by : Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : 2018/03/07 * Last modified : 2018/09/13 * * IMITATOR version: 2.10.1 ************************************************************) var (* Clocks *) x, y, xabs : clock; (* Parameters *) p1, p2, p3, t, tprime : parameter; (************************************************************) automaton pta (************************************************************) synclabs: a, b, dollar, start; loc pre_s0: invariant True (* First try immediately the pattern in 0-time *) when xabs = 0 & xabs = t sync start goto s0; (* Otherwise: first skip some letter and wait *) when True sync a do {x := 0, y := 0} goto pre_s0_prime; when True sync b do {x := 0, y := 0} goto pre_s0_prime; loc pre_s0_prime: invariant True (* Skip some more letter and wait *) when True sync a do {x := 0, y := 0} goto pre_s0_prime; when True sync b do {x := 0, y := 0} goto pre_s0_prime; (* Or decide to start the pattern *) when t = xabs & x > 0 do {x := 0, y := 0} sync start goto s0; loc s0: invariant True when True sync a do {y := 0} goto s1; loc s1: invariant True when x < p1 sync b goto s2; loc s2: invariant True when x = p1 & xabs = tprime do {x := 0} sync dollar goto soon_end; when p3 <= y & y < p2 do {y := 0} sync a goto s1; loc soon_end: invariant True when x > 0 goto s3; urgent loc s3: invariant True end (* pta *) (************************************************************) automaton word (************************************************************) synclabs: a, b; (* BEGIN AUTOMATICALLY GENERATED *) loc w0: invariant xabs <= 5/100 when xabs = 5/100 sync a goto w1; loc w1: invariant xabs <= 9/100 when xabs = 9/100 sync b goto w2; loc w2: invariant xabs <= 12/100 when xabs = 12/100 sync a goto w3; loc w3: invariant xabs <= 16/100 when xabs = 16/100 sync b goto w4; loc w4: invariant xabs <= 19/100 when xabs = 19/100 sync a goto w5; loc w5: invariant xabs <= 28/100 when xabs = 28/100 sync b goto w6; loc w6: invariant xabs <= 34/100 when xabs = 34/100 sync a goto w7; loc w7: invariant xabs <= 38/100 when xabs = 38/100 sync b goto w8; loc w8: invariant xabs <= 41/100 when xabs = 41/100 sync a goto w9; loc w9: invariant xabs <= 46/100 when xabs = 46/100 sync b goto w10; loc w10: invariant xabs <= 54/100 when xabs = 54/100 sync a goto w11; loc w11: invariant xabs <= 58/100 when xabs = 58/100 sync b goto w12; loc w12: invariant xabs <= 67/100 when xabs = 67/100 sync a goto w13; loc w13: invariant xabs <= 76/100 when xabs = 76/100 sync b goto w14; loc w14: invariant xabs <= 84/100 when xabs = 84/100 sync a goto w15; loc w15: invariant xabs <= 86/100 when xabs = 86/100 sync b goto w16; loc w16: invariant xabs <= 88/100 when xabs = 88/100 sync a goto w17; loc w17: invariant xabs <= 94/100 when xabs = 94/100 sync b goto w18; loc w18: invariant xabs <= 96/100 when xabs = 96/100 sync a goto w19; loc w19: invariant xabs <= 103/100 when xabs = 103/100 sync b goto w20; loc w20: invariant xabs <= 106/100 when xabs = 106/100 sync a goto w21; loc w21: invariant xabs <= 112/100 when xabs = 112/100 sync b goto w22; loc w22: invariant xabs <= 119/100 when xabs = 119/100 sync a goto w23; loc w23: invariant xabs <= 127/100 when xabs = 127/100 sync b goto w24; loc w24: invariant xabs <= 129/100 when xabs = 129/100 sync a goto w25; loc w25: invariant xabs <= 135/100 when xabs = 135/100 sync b goto w26; loc w26: invariant xabs <= 140/100 when xabs = 140/100 sync a goto w27; loc w27: invariant xabs <= 146/100 when xabs = 146/100 sync b goto w28; loc w28: invariant xabs <= 149/100 when xabs = 149/100 sync a goto w29; loc w29: invariant xabs <= 152/100 when xabs = 152/100 sync b goto w30; loc w30: invariant xabs <= 154/100 when xabs = 154/100 sync a goto w31; loc w31: invariant xabs <= 158/100 when xabs = 158/100 sync b goto w32; loc w32: invariant xabs <= 167/100 when xabs = 167/100 sync a goto w33; loc w33: invariant xabs <= 175/100 when xabs = 175/100 sync b goto w34; loc w34: invariant xabs <= 180/100 when xabs = 180/100 sync a goto w35; loc w35: invariant xabs <= 186/100 when xabs = 186/100 sync b goto w36; loc w36: invariant xabs <= 189/100 when xabs = 189/100 sync a goto w37; loc w37: invariant xabs <= 190/100 when xabs = 190/100 sync b goto w38; loc w38: invariant xabs <= 199/100 when xabs = 199/100 sync a goto w39; loc w39: invariant xabs <= 207/100 when xabs = 207/100 sync b goto w40; loc w40: invariant xabs <= 210/100 when xabs = 210/100 sync a goto w41; loc w41: invariant xabs <= 211/100 when xabs = 211/100 sync b goto w42; loc w42: invariant xabs <= 217/100 when xabs = 217/100 sync a goto w43; loc w43: invariant xabs <= 218/100 when xabs = 218/100 sync b goto w44; loc w44: invariant xabs <= 220/100 when xabs = 220/100 sync a goto w45; loc w45: invariant xabs <= 221/100 when xabs = 221/100 sync b goto w46; loc w46: invariant xabs <= 224/100 when xabs = 224/100 sync a goto w47; loc w47: invariant xabs <= 225/100 when xabs = 225/100 sync b goto w48; loc w48: invariant xabs <= 233/100 when xabs = 233/100 sync a goto w49; loc w49: invariant xabs <= 237/100 when xabs = 237/100 sync b goto w50; loc w50: invariant xabs <= 243/100 when xabs = 243/100 sync a goto w51; loc w51: invariant xabs <= 245/100 when xabs = 245/100 sync b goto w52; loc w52: invariant xabs <= 254/100 when xabs = 254/100 sync a goto w53; loc w53: invariant xabs <= 257/100 when xabs = 257/100 sync b goto w54; loc w54: invariant xabs <= 265/100 when xabs = 265/100 sync a goto w55; loc w55: invariant xabs <= 273/100 when xabs = 273/100 sync b goto w56; loc w56: invariant xabs <= 282/100 when xabs = 282/100 sync a goto w57; loc w57: invariant xabs <= 288/100 when xabs = 288/100 sync b goto w58; loc w58: invariant xabs <= 291/100 when xabs = 291/100 sync a goto w59; loc w59: invariant xabs <= 292/100 when xabs = 292/100 sync b goto w60; loc w60: invariant xabs <= 297/100 when xabs = 297/100 sync a goto w61; loc w61: invariant xabs <= 302/100 when xabs = 302/100 sync b goto w62; loc w62: invariant xabs <= 308/100 when xabs = 308/100 sync a goto w63; loc w63: invariant xabs <= 317/100 when xabs = 317/100 sync b goto w64; loc w64: invariant xabs <= 320/100 when xabs = 320/100 sync a goto w65; loc w65: invariant xabs <= 329/100 when xabs = 329/100 sync b goto w66; loc w66: invariant xabs <= 333/100 when xabs = 333/100 sync a goto w67; loc w67: invariant xabs <= 342/100 when xabs = 342/100 sync b goto w68; loc w68: invariant xabs <= 351/100 when xabs = 351/100 sync a goto w69; loc w69: invariant xabs <= 358/100 when xabs = 358/100 sync b goto w70; loc w70: invariant xabs <= 367/100 when xabs = 367/100 sync a goto w71; loc w71: invariant xabs <= 374/100 when xabs = 374/100 sync b goto w72; loc w72: invariant xabs <= 377/100 when xabs = 377/100 sync a goto w73; loc w73: invariant xabs <= 383/100 when xabs = 383/100 sync b goto w74; loc w74: invariant xabs <= 392/100 when xabs = 392/100 sync a goto w75; loc w75: invariant xabs <= 395/100 when xabs = 395/100 sync b goto w76; loc w76: invariant xabs <= 403/100 when xabs = 403/100 sync a goto w77; loc w77: invariant xabs <= 408/100 when xabs = 408/100 sync b goto w78; loc w78: invariant xabs <= 409/100 when xabs = 409/100 sync a goto w79; loc w79: invariant xabs <= 414/100 when xabs = 414/100 sync b goto w80; loc w80: invariant xabs <= 415/100 when xabs = 415/100 sync a goto w81; loc w81: invariant xabs <= 420/100 when xabs = 420/100 sync b goto w82; loc w82: invariant xabs <= 421/100 when xabs = 421/100 sync a goto w83; loc w83: invariant xabs <= 423/100 when xabs = 423/100 sync b goto w84; loc w84: invariant xabs <= 428/100 when xabs = 428/100 sync a goto w85; loc w85: invariant xabs <= 431/100 when xabs = 431/100 sync b goto w86; loc w86: invariant xabs <= 434/100 when xabs = 434/100 sync a goto w87; loc w87: invariant xabs <= 443/100 when xabs = 443/100 sync b goto w88; loc w88: invariant xabs <= 449/100 when xabs = 449/100 sync a goto w89; loc w89: invariant xabs <= 455/100 when xabs = 455/100 sync b goto w90; loc w90: invariant xabs <= 457/100 when xabs = 457/100 sync a goto w91; loc w91: invariant xabs <= 465/100 when xabs = 465/100 sync b goto w92; loc w92: invariant xabs <= 466/100 when xabs = 466/100 sync a goto w93; loc w93: invariant xabs <= 467/100 when xabs = 467/100 sync b goto w94; loc w94: invariant xabs <= 471/100 when xabs = 471/100 sync a goto w95; loc w95: invariant xabs <= 480/100 when xabs = 480/100 sync b goto w96; loc w96: invariant xabs <= 485/100 when xabs = 485/100 sync a goto w97; loc w97: invariant xabs <= 490/100 when xabs = 490/100 sync b goto w98; loc w98: invariant xabs <= 499/100 when xabs = 499/100 sync a goto w99; loc w99: invariant xabs <= 502/100 when xabs = 502/100 sync b goto w100; loc w100: invariant xabs <= 504/100 when xabs = 504/100 sync a goto w101; loc w101: invariant xabs <= 509/100 when xabs = 509/100 sync b goto w102; loc w102: invariant xabs <= 515/100 when xabs = 515/100 sync a goto w103; loc w103: invariant xabs <= 522/100 when xabs = 522/100 sync b goto w104; loc w104: invariant xabs <= 527/100 when xabs = 527/100 sync a goto w105; loc w105: invariant xabs <= 534/100 when xabs = 534/100 sync b goto w106; loc w106: invariant xabs <= 540/100 when xabs = 540/100 sync a goto w107; loc w107: invariant xabs <= 549/100 when xabs = 549/100 sync b goto w108; loc w108: invariant xabs <= 552/100 when xabs = 552/100 sync a goto w109; loc w109: invariant xabs <= 553/100 when xabs = 553/100 sync b goto w110; loc w110: invariant xabs <= 557/100 when xabs = 557/100 sync a goto w111; loc w111: invariant xabs <= 561/100 when xabs = 561/100 sync b goto w112; loc w112: invariant xabs <= 570/100 when xabs = 570/100 sync a goto w113; loc w113: invariant xabs <= 576/100 when xabs = 576/100 sync b goto w114; loc w114: invariant xabs <= 577/100 when xabs = 577/100 sync a goto w115; loc w115: invariant xabs <= 578/100 when xabs = 578/100 sync b goto w116; loc w116: invariant xabs <= 586/100 when xabs = 586/100 sync a goto w117; loc w117: invariant xabs <= 594/100 when xabs = 594/100 sync b goto w118; loc w118: invariant xabs <= 595/100 when xabs = 595/100 sync a goto w119; loc w119: invariant xabs <= 596/100 when xabs = 596/100 sync b goto w120; loc w120: invariant xabs <= 600/100 when xabs = 600/100 sync a goto w121; loc w121: invariant xabs <= 602/100 when xabs = 602/100 sync b goto w122; loc w122: invariant xabs <= 606/100 when xabs = 606/100 sync a goto w123; loc w123: invariant xabs <= 613/100 when xabs = 613/100 sync b goto w124; loc w124: invariant xabs <= 615/100 when xabs = 615/100 sync a goto w125; loc w125: invariant xabs <= 617/100 when xabs = 617/100 sync b goto w126; loc w126: invariant xabs <= 618/100 when xabs = 618/100 sync a goto w127; loc w127: invariant xabs <= 619/100 when xabs = 619/100 sync b goto w128; loc w128: invariant xabs <= 627/100 when xabs = 627/100 sync a goto w129; loc w129: invariant xabs <= 628/100 when xabs = 628/100 sync b goto w130; loc w130: invariant xabs <= 633/100 when xabs = 633/100 sync a goto w131; loc w131: invariant xabs <= 641/100 when xabs = 641/100 sync b goto w132; loc w132: invariant xabs <= 646/100 when xabs = 646/100 sync a goto w133; loc w133: invariant xabs <= 654/100 when xabs = 654/100 sync b goto w134; loc w134: invariant xabs <= 661/100 when xabs = 661/100 sync a goto w135; loc w135: invariant xabs <= 667/100 when xabs = 667/100 sync b goto w136; loc w136: invariant xabs <= 671/100 when xabs = 671/100 sync a goto w137; loc w137: invariant xabs <= 678/100 when xabs = 678/100 sync b goto w138; loc w138: invariant xabs <= 684/100 when xabs = 684/100 sync a goto w139; loc w139: invariant xabs <= 689/100 when xabs = 689/100 sync b goto w140; loc w140: invariant xabs <= 698/100 when xabs = 698/100 sync a goto w141; loc w141: invariant xabs <= 702/100 when xabs = 702/100 sync b goto w142; loc w142: invariant xabs <= 710/100 when xabs = 710/100 sync a goto w143; loc w143: invariant xabs <= 719/100 when xabs = 719/100 sync b goto w144; loc w144: invariant xabs <= 728/100 when xabs = 728/100 sync a goto w145; loc w145: invariant xabs <= 734/100 when xabs = 734/100 sync b goto w146; loc w146: invariant xabs <= 741/100 when xabs = 741/100 sync a goto w147; loc w147: invariant xabs <= 745/100 when xabs = 745/100 sync b goto w148; loc w148: invariant xabs <= 751/100 when xabs = 751/100 sync a goto w149; loc w149: invariant xabs <= 759/100 when xabs = 759/100 sync b goto w150; loc w150: invariant xabs <= 767/100 when xabs = 767/100 sync a goto w151; loc w151: invariant xabs <= 770/100 when xabs = 770/100 sync b goto w152; loc w152: invariant xabs <= 771/100 when xabs = 771/100 sync a goto w153; loc w153: invariant xabs <= 777/100 when xabs = 777/100 sync b goto w154; loc w154: invariant xabs <= 779/100 when xabs = 779/100 sync a goto w155; loc w155: invariant xabs <= 785/100 when xabs = 785/100 sync b goto w156; loc w156: invariant xabs <= 788/100 when xabs = 788/100 sync a goto w157; loc w157: invariant xabs <= 789/100 when xabs = 789/100 sync b goto w158; loc w158: invariant xabs <= 792/100 when xabs = 792/100 sync a goto w159; loc w159: invariant xabs <= 798/100 when xabs = 798/100 sync b goto w160; loc w160: invariant xabs <= 801/100 when xabs = 801/100 sync a goto w161; loc w161: invariant xabs <= 808/100 when xabs = 808/100 sync b goto w162; loc w162: invariant xabs <= 816/100 when xabs = 816/100 sync a goto w163; loc w163: invariant xabs <= 820/100 when xabs = 820/100 sync b goto w164; loc w164: invariant xabs <= 822/100 when xabs = 822/100 sync a goto w165; loc w165: invariant xabs <= 831/100 when xabs = 831/100 sync b goto w166; loc w166: invariant xabs <= 837/100 when xabs = 837/100 sync a goto w167; loc w167: invariant xabs <= 841/100 when xabs = 841/100 sync b goto w168; loc w168: invariant xabs <= 842/100 when xabs = 842/100 sync a goto w169; loc w169: invariant xabs <= 850/100 when xabs = 850/100 sync b goto w170; loc w170: invariant xabs <= 859/100 when xabs = 859/100 sync a goto w171; loc w171: invariant xabs <= 868/100 when xabs = 868/100 sync b goto w172; loc w172: invariant xabs <= 877/100 when xabs = 877/100 sync a goto w173; loc w173: invariant xabs <= 879/100 when xabs = 879/100 sync b goto w174; loc w174: invariant xabs <= 886/100 when xabs = 886/100 sync a goto w175; loc w175: invariant xabs <= 893/100 when xabs = 893/100 sync b goto w176; loc w176: invariant xabs <= 895/100 when xabs = 895/100 sync a goto w177; loc w177: invariant xabs <= 904/100 when xabs = 904/100 sync b goto w178; loc w178: invariant xabs <= 907/100 when xabs = 907/100 sync a goto w179; loc w179: invariant xabs <= 909/100 when xabs = 909/100 sync b goto w180; loc w180: invariant xabs <= 913/100 when xabs = 913/100 sync a goto w181; loc w181: invariant xabs <= 920/100 when xabs = 920/100 sync b goto w182; loc w182: invariant xabs <= 925/100 when xabs = 925/100 sync a goto w183; loc w183: invariant xabs <= 928/100 when xabs = 928/100 sync b goto w184; loc w184: invariant xabs <= 935/100 when xabs = 935/100 sync a goto w185; loc w185: invariant xabs <= 941/100 when xabs = 941/100 sync b goto w186; loc w186: invariant xabs <= 942/100 when xabs = 942/100 sync a goto w187; loc w187: invariant xabs <= 949/100 when xabs = 949/100 sync b goto w188; loc w188: invariant xabs <= 953/100 when xabs = 953/100 sync a goto w189; loc w189: invariant xabs <= 960/100 when xabs = 960/100 sync b goto w190; loc w190: invariant xabs <= 964/100 when xabs = 964/100 sync a goto w191; loc w191: invariant xabs <= 968/100 when xabs = 968/100 sync b goto w192; loc w192: invariant xabs <= 969/100 when xabs = 969/100 sync a goto w193; loc w193: invariant xabs <= 973/100 when xabs = 973/100 sync b goto w194; loc w194: invariant xabs <= 980/100 when xabs = 980/100 sync a goto w195; loc w195: invariant xabs <= 988/100 when xabs = 988/100 sync b goto w196; loc w196: invariant xabs <= 989/100 when xabs = 989/100 sync a goto w197; loc w197: invariant xabs <= 992/100 when xabs = 992/100 sync b goto w198; loc w198: invariant xabs <= 999/100 when xabs = 999/100 sync a goto w199; loc w199: invariant xabs <= 1007/100 when xabs = 1007/100 sync b goto w200; loc w200: invariant xabs <= 1013/100 when xabs = 1013/100 sync a goto w201; loc w201: invariant xabs <= 1022/100 when xabs = 1022/100 sync b goto w202; loc w202: invariant xabs <= 1027/100 when xabs = 1027/100 sync a goto w203; loc w203: invariant xabs <= 1028/100 when xabs = 1028/100 sync b goto w204; loc w204: invariant xabs <= 1031/100 when xabs = 1031/100 sync a goto w205; loc w205: invariant xabs <= 1038/100 when xabs = 1038/100 sync b goto w206; loc w206: invariant xabs <= 1046/100 when xabs = 1046/100 sync a goto w207; loc w207: invariant xabs <= 1055/100 when xabs = 1055/100 sync b goto w208; loc w208: invariant xabs <= 1062/100 when xabs = 1062/100 sync a goto w209; loc w209: invariant xabs <= 1068/100 when xabs = 1068/100 sync b goto w210; loc w210: invariant xabs <= 1074/100 when xabs = 1074/100 sync a goto w211; loc w211: invariant xabs <= 1082/100 when xabs = 1082/100 sync b goto w212; loc w212: invariant xabs <= 1088/100 when xabs = 1088/100 sync a goto w213; loc w213: invariant xabs <= 1093/100 when xabs = 1093/100 sync b goto w214; loc w214: invariant xabs <= 1096/100 when xabs = 1096/100 sync a goto w215; loc w215: invariant xabs <= 1098/100 when xabs = 1098/100 sync b goto w216; loc w216: invariant xabs <= 1101/100 when xabs = 1101/100 sync a goto w217; loc w217: invariant xabs <= 1110/100 when xabs = 1110/100 sync b goto w218; loc w218: invariant xabs <= 1116/100 when xabs = 1116/100 sync a goto w219; loc w219: invariant xabs <= 1120/100 when xabs = 1120/100 sync b goto w220; loc w220: invariant xabs <= 1122/100 when xabs = 1122/100 sync a goto w221; loc w221: invariant xabs <= 1131/100 when xabs = 1131/100 sync b goto w222; loc w222: invariant xabs <= 1139/100 when xabs = 1139/100 sync a goto w223; loc w223: invariant xabs <= 1145/100 when xabs = 1145/100 sync b goto w224; loc w224: invariant xabs <= 1146/100 when xabs = 1146/100 sync a goto w225; loc w225: invariant xabs <= 1149/100 when xabs = 1149/100 sync b goto w226; loc w226: invariant xabs <= 1155/100 when xabs = 1155/100 sync a goto w227; loc w227: invariant xabs <= 1158/100 when xabs = 1158/100 sync b goto w228; loc w228: invariant xabs <= 1160/100 when xabs = 1160/100 sync a goto w229; loc w229: invariant xabs <= 1163/100 when xabs = 1163/100 sync b goto w230; loc w230: invariant xabs <= 1172/100 when xabs = 1172/100 sync a goto w231; loc w231: invariant xabs <= 1179/100 when xabs = 1179/100 sync b goto w232; loc w232: invariant xabs <= 1183/100 when xabs = 1183/100 sync a goto w233; loc w233: invariant xabs <= 1187/100 when xabs = 1187/100 sync b goto w234; loc w234: invariant xabs <= 1192/100 when xabs = 1192/100 sync a goto w235; loc w235: invariant xabs <= 1195/100 when xabs = 1195/100 sync b goto w236; loc w236: invariant xabs <= 1197/100 when xabs = 1197/100 sync a goto w237; loc w237: invariant xabs <= 1201/100 when xabs = 1201/100 sync b goto w238; loc w238: invariant xabs <= 1206/100 when xabs = 1206/100 sync a goto w239; loc w239: invariant xabs <= 1211/100 when xabs = 1211/100 sync b goto w240; loc w240: invariant xabs <= 1218/100 when xabs = 1218/100 sync a goto w241; loc w241: invariant xabs <= 1226/100 when xabs = 1226/100 sync b goto w242; loc w242: invariant xabs <= 1228/100 when xabs = 1228/100 sync a goto w243; loc w243: invariant xabs <= 1236/100 when xabs = 1236/100 sync b goto w244; loc w244: invariant xabs <= 1245/100 when xabs = 1245/100 sync a goto w245; loc w245: invariant xabs <= 1253/100 when xabs = 1253/100 sync b goto w246; loc w246: invariant xabs <= 1255/100 when xabs = 1255/100 sync a goto w247; loc w247: invariant xabs <= 1259/100 when xabs = 1259/100 sync b goto w248; loc w248: invariant xabs <= 1267/100 when xabs = 1267/100 sync a goto w249; loc w249: invariant xabs <= 1273/100 when xabs = 1273/100 sync b goto w250; loc w250: invariant xabs <= 1274/100 when xabs = 1274/100 sync a goto w251; loc w251: invariant xabs <= 1283/100 when xabs = 1283/100 sync b goto w252; loc w252: invariant xabs <= 1286/100 when xabs = 1286/100 sync a goto w253; loc w253: invariant xabs <= 1290/100 when xabs = 1290/100 sync b goto w254; loc w254: invariant xabs <= 1297/100 when xabs = 1297/100 sync a goto w255; loc w255: invariant xabs <= 1302/100 when xabs = 1302/100 sync b goto w256; loc w256: invariant xabs <= 1310/100 when xabs = 1310/100 sync a goto w257; loc w257: invariant xabs <= 1314/100 when xabs = 1314/100 sync b goto w258; loc w258: invariant xabs <= 1320/100 when xabs = 1320/100 sync a goto w259; loc w259: invariant xabs <= 1325/100 when xabs = 1325/100 sync b goto w260; loc w260: invariant xabs <= 1327/100 when xabs = 1327/100 sync a goto w261; loc w261: invariant xabs <= 1329/100 when xabs = 1329/100 sync b goto w262; loc w262: invariant xabs <= 1334/100 when xabs = 1334/100 sync a goto w263; loc w263: invariant xabs <= 1342/100 when xabs = 1342/100 sync b goto w264; loc w264: invariant xabs <= 1347/100 when xabs = 1347/100 sync a goto w265; loc w265: invariant xabs <= 1351/100 when xabs = 1351/100 sync b goto w266; loc w266: invariant xabs <= 1352/100 when xabs = 1352/100 sync a goto w267; loc w267: invariant xabs <= 1359/100 when xabs = 1359/100 sync b goto w268; loc w268: invariant xabs <= 1366/100 when xabs = 1366/100 sync a goto w269; loc w269: invariant xabs <= 1370/100 when xabs = 1370/100 sync b goto w270; loc w270: invariant xabs <= 1374/100 when xabs = 1374/100 sync a goto w271; loc w271: invariant xabs <= 1382/100 when xabs = 1382/100 sync b goto w272; loc w272: invariant xabs <= 1387/100 when xabs = 1387/100 sync a goto w273; loc w273: invariant xabs <= 1394/100 when xabs = 1394/100 sync b goto w274; loc w274: invariant xabs <= 1402/100 when xabs = 1402/100 sync a goto w275; loc w275: invariant xabs <= 1408/100 when xabs = 1408/100 sync b goto w276; loc w276: invariant xabs <= 1411/100 when xabs = 1411/100 sync a goto w277; loc w277: invariant xabs <= 1417/100 when xabs = 1417/100 sync b goto w278; loc w278: invariant xabs <= 1418/100 when xabs = 1418/100 sync a goto w279; loc w279: invariant xabs <= 1420/100 when xabs = 1420/100 sync b goto w280; loc w280: invariant xabs <= 1423/100 when xabs = 1423/100 sync a goto w281; loc w281: invariant xabs <= 1424/100 when xabs = 1424/100 sync b goto w282; loc w282: invariant xabs <= 1433/100 when xabs = 1433/100 sync a goto w283; loc w283: invariant xabs <= 1436/100 when xabs = 1436/100 sync b goto w284; loc w284: invariant xabs <= 1438/100 when xabs = 1438/100 sync a goto w285; loc w285: invariant xabs <= 1440/100 when xabs = 1440/100 sync b goto w286; loc w286: invariant xabs <= 1449/100 when xabs = 1449/100 sync a goto w287; loc w287: invariant xabs <= 1452/100 when xabs = 1452/100 sync b goto w288; loc w288: invariant xabs <= 1456/100 when xabs = 1456/100 sync a goto w289; loc w289: invariant xabs <= 1465/100 when xabs = 1465/100 sync b goto w290; loc w290: invariant xabs <= 1473/100 when xabs = 1473/100 sync a goto w291; loc w291: invariant xabs <= 1477/100 when xabs = 1477/100 sync b goto w292; loc w292: invariant xabs <= 1483/100 when xabs = 1483/100 sync a goto w293; loc w293: invariant xabs <= 1486/100 when xabs = 1486/100 sync b goto w294; loc w294: invariant xabs <= 1489/100 when xabs = 1489/100 sync a goto w295; loc w295: invariant xabs <= 1493/100 when xabs = 1493/100 sync b goto w296; loc w296: invariant xabs <= 1498/100 when xabs = 1498/100 sync a goto w297; loc w297: invariant xabs <= 1501/100 when xabs = 1501/100 sync b goto w298; loc w298: invariant xabs <= 1508/100 when xabs = 1508/100 sync a goto w299; loc w299: invariant xabs <= 1513/100 when xabs = 1513/100 sync b goto w300; loc w300: invariant xabs <= 1519/100 when xabs = 1519/100 sync a goto w301; loc w301: invariant xabs <= 1526/100 when xabs = 1526/100 sync b goto w302; loc w302: invariant xabs <= 1528/100 when xabs = 1528/100 sync a goto w303; loc w303: invariant xabs <= 1532/100 when xabs = 1532/100 sync b goto w304; loc w304: invariant xabs <= 1540/100 when xabs = 1540/100 sync a goto w305; loc w305: invariant xabs <= 1544/100 when xabs = 1544/100 sync b goto w306; loc w306: invariant xabs <= 1545/100 when xabs = 1545/100 sync a goto w307; loc w307: invariant xabs <= 1554/100 when xabs = 1554/100 sync b goto w308; loc w308: invariant xabs <= 1557/100 when xabs = 1557/100 sync a goto w309; loc w309: invariant xabs <= 1566/100 when xabs = 1566/100 sync b goto w310; loc w310: invariant xabs <= 1572/100 when xabs = 1572/100 sync a goto w311; loc w311: invariant xabs <= 1580/100 when xabs = 1580/100 sync b goto w312; loc w312: invariant xabs <= 1582/100 when xabs = 1582/100 sync a goto w313; loc w313: invariant xabs <= 1591/100 when xabs = 1591/100 sync b goto w314; loc w314: invariant xabs <= 1592/100 when xabs = 1592/100 sync a goto w315; loc w315: invariant xabs <= 1596/100 when xabs = 1596/100 sync b goto w316; loc w316: invariant xabs <= 1604/100 when xabs = 1604/100 sync a goto w317; loc w317: invariant xabs <= 1605/100 when xabs = 1605/100 sync b goto w318; loc w318: invariant xabs <= 1607/100 when xabs = 1607/100 sync a goto w319; loc w319: invariant xabs <= 1608/100 when xabs = 1608/100 sync b goto w320; loc w320: invariant xabs <= 1617/100 when xabs = 1617/100 sync a goto w321; loc w321: invariant xabs <= 1620/100 when xabs = 1620/100 sync b goto w322; loc w322: invariant xabs <= 1622/100 when xabs = 1622/100 sync a goto w323; loc w323: invariant xabs <= 1626/100 when xabs = 1626/100 sync b goto w324; loc w324: invariant xabs <= 1635/100 when xabs = 1635/100 sync a goto w325; loc w325: invariant xabs <= 1644/100 when xabs = 1644/100 sync b goto w326; loc w326: invariant xabs <= 1653/100 when xabs = 1653/100 sync a goto w327; loc w327: invariant xabs <= 1654/100 when xabs = 1654/100 sync b goto w328; loc w328: invariant xabs <= 1656/100 when xabs = 1656/100 sync a goto w329; loc w329: invariant xabs <= 1660/100 when xabs = 1660/100 sync b goto w330; loc w330: invariant xabs <= 1668/100 when xabs = 1668/100 sync a goto w331; loc w331: invariant xabs <= 1676/100 when xabs = 1676/100 sync b goto w332; loc w332: invariant xabs <= 1684/100 when xabs = 1684/100 sync a goto w333; loc w333: invariant xabs <= 1687/100 when xabs = 1687/100 sync b goto w334; loc w334: invariant xabs <= 1694/100 when xabs = 1694/100 sync a goto w335; loc w335: invariant xabs <= 1697/100 when xabs = 1697/100 sync b goto w336; loc w336: invariant xabs <= 1698/100 when xabs = 1698/100 sync a goto w337; loc w337: invariant xabs <= 1703/100 when xabs = 1703/100 sync b goto w338; loc w338: invariant xabs <= 1706/100 when xabs = 1706/100 sync a goto w339; loc w339: invariant xabs <= 1715/100 when xabs = 1715/100 sync b goto w340; loc w340: invariant xabs <= 1716/100 when xabs = 1716/100 sync a goto w341; loc w341: invariant xabs <= 1723/100 when xabs = 1723/100 sync b goto w342; loc w342: invariant xabs <= 1731/100 when xabs = 1731/100 sync a goto w343; loc w343: invariant xabs <= 1732/100 when xabs = 1732/100 sync b goto w344; loc w344: invariant xabs <= 1733/100 when xabs = 1733/100 sync a goto w345; loc w345: invariant xabs <= 1734/100 when xabs = 1734/100 sync b goto w346; loc w346: invariant xabs <= 1738/100 when xabs = 1738/100 sync a goto w347; loc w347: invariant xabs <= 1747/100 when xabs = 1747/100 sync b goto w348; loc w348: invariant xabs <= 1751/100 when xabs = 1751/100 sync a goto w349; loc w349: invariant xabs <= 1752/100 when xabs = 1752/100 sync b goto w350; loc w350: invariant xabs <= 1760/100 when xabs = 1760/100 sync a goto w351; loc w351: invariant xabs <= 1767/100 when xabs = 1767/100 sync b goto w352; loc w352: invariant xabs <= 1769/100 when xabs = 1769/100 sync a goto w353; loc w353: invariant xabs <= 1776/100 when xabs = 1776/100 sync b goto w354; loc w354: invariant xabs <= 1784/100 when xabs = 1784/100 sync a goto w355; loc w355: invariant xabs <= 1789/100 when xabs = 1789/100 sync b goto w356; loc w356: invariant xabs <= 1795/100 when xabs = 1795/100 sync a goto w357; loc w357: invariant xabs <= 1797/100 when xabs = 1797/100 sync b goto w358; loc w358: invariant xabs <= 1805/100 when xabs = 1805/100 sync a goto w359; loc w359: invariant xabs <= 1806/100 when xabs = 1806/100 sync b goto w360; loc w360: invariant xabs <= 1813/100 when xabs = 1813/100 sync a goto w361; loc w361: invariant xabs <= 1819/100 when xabs = 1819/100 sync b goto w362; loc w362: invariant xabs <= 1826/100 when xabs = 1826/100 sync a goto w363; loc w363: invariant xabs <= 1829/100 when xabs = 1829/100 sync b goto w364; loc w364: invariant xabs <= 1837/100 when xabs = 1837/100 sync a goto w365; loc w365: invariant xabs <= 1842/100 when xabs = 1842/100 sync b goto w366; loc w366: invariant xabs <= 1851/100 when xabs = 1851/100 sync a goto w367; loc w367: invariant xabs <= 1854/100 when xabs = 1854/100 sync b goto w368; loc w368: invariant xabs <= 1862/100 when xabs = 1862/100 sync a goto w369; loc w369: invariant xabs <= 1863/100 when xabs = 1863/100 sync b goto w370; loc w370: invariant xabs <= 1865/100 when xabs = 1865/100 sync a goto w371; loc w371: invariant xabs <= 1873/100 when xabs = 1873/100 sync b goto w372; loc w372: invariant xabs <= 1875/100 when xabs = 1875/100 sync a goto w373; loc w373: invariant xabs <= 1883/100 when xabs = 1883/100 sync b goto w374; loc w374: invariant xabs <= 1890/100 when xabs = 1890/100 sync a goto w375; loc w375: invariant xabs <= 1896/100 when xabs = 1896/100 sync b goto w376; loc w376: invariant xabs <= 1904/100 when xabs = 1904/100 sync a goto w377; loc w377: invariant xabs <= 1908/100 when xabs = 1908/100 sync b goto w378; loc w378: invariant xabs <= 1915/100 when xabs = 1915/100 sync a goto w379; loc w379: invariant xabs <= 1922/100 when xabs = 1922/100 sync b goto w380; loc w380: invariant xabs <= 1928/100 when xabs = 1928/100 sync a goto w381; loc w381: invariant xabs <= 1936/100 when xabs = 1936/100 sync b goto w382; loc w382: invariant xabs <= 1944/100 when xabs = 1944/100 sync a goto w383; loc w383: invariant xabs <= 1947/100 when xabs = 1947/100 sync b goto w384; loc w384: invariant xabs <= 1953/100 when xabs = 1953/100 sync a goto w385; loc w385: invariant xabs <= 1955/100 when xabs = 1955/100 sync b goto w386; loc w386: invariant xabs <= 1957/100 when xabs = 1957/100 sync a goto w387; loc w387: invariant xabs <= 1959/100 when xabs = 1959/100 sync b goto w388; loc w388: invariant xabs <= 1961/100 when xabs = 1961/100 sync a goto w389; loc w389: invariant xabs <= 1970/100 when xabs = 1970/100 sync b goto w390; loc w390: invariant xabs <= 1975/100 when xabs = 1975/100 sync a goto w391; loc w391: invariant xabs <= 1976/100 when xabs = 1976/100 sync b goto w392; loc w392: invariant xabs <= 1977/100 when xabs = 1977/100 sync a goto w393; loc w393: invariant xabs <= 1981/100 when xabs = 1981/100 sync b goto w394; loc w394: invariant xabs <= 1986/100 when xabs = 1986/100 sync a goto w395; loc w395: invariant xabs <= 1992/100 when xabs = 1992/100 sync b goto w396; loc w396: invariant xabs <= 1997/100 when xabs = 1997/100 sync a goto w397; loc w397: invariant xabs <= 1999/100 when xabs = 1999/100 sync b goto w398; loc w398: invariant xabs <= 2008/100 when xabs = 2008/100 sync a goto w399; loc w399: invariant xabs <= 2015/100 when xabs = 2015/100 sync b goto w400; loc w400: invariant xabs <= 2022/100 when xabs = 2022/100 sync a goto w401; loc w401: invariant xabs <= 2024/100 when xabs = 2024/100 sync b goto w402; loc w402: invariant xabs <= 2032/100 when xabs = 2032/100 sync a goto w403; loc w403: invariant xabs <= 2035/100 when xabs = 2035/100 sync b goto w404; loc w404: invariant xabs <= 2037/100 when xabs = 2037/100 sync a goto w405; loc w405: invariant xabs <= 2040/100 when xabs = 2040/100 sync b goto w406; loc w406: invariant xabs <= 2048/100 when xabs = 2048/100 sync a goto w407; loc w407: invariant xabs <= 2053/100 when xabs = 2053/100 sync b goto w408; loc w408: invariant xabs <= 2061/100 when xabs = 2061/100 sync a goto w409; loc w409: invariant xabs <= 2069/100 when xabs = 2069/100 sync b goto w410; loc w410: invariant xabs <= 2072/100 when xabs = 2072/100 sync a goto w411; loc w411: invariant xabs <= 2080/100 when xabs = 2080/100 sync b goto w412; loc w412: invariant xabs <= 2086/100 when xabs = 2086/100 sync a goto w413; loc w413: invariant xabs <= 2095/100 when xabs = 2095/100 sync b goto w414; loc w414: invariant xabs <= 2104/100 when xabs = 2104/100 sync a goto w415; loc w415: invariant xabs <= 2106/100 when xabs = 2106/100 sync b goto w416; loc w416: invariant xabs <= 2114/100 when xabs = 2114/100 sync a goto w417; loc w417: invariant xabs <= 2117/100 when xabs = 2117/100 sync b goto w418; loc w418: invariant xabs <= 2122/100 when xabs = 2122/100 sync a goto w419; loc w419: invariant xabs <= 2123/100 when xabs = 2123/100 sync b goto w420; loc w420: invariant xabs <= 2125/100 when xabs = 2125/100 sync a goto w421; loc w421: invariant xabs <= 2128/100 when xabs = 2128/100 sync b goto w422; loc w422: invariant xabs <= 2136/100 when xabs = 2136/100 sync a goto w423; loc w423: invariant xabs <= 2140/100 when xabs = 2140/100 sync b goto w424; loc w424: invariant xabs <= 2144/100 when xabs = 2144/100 sync a goto w425; loc w425: invariant xabs <= 2145/100 when xabs = 2145/100 sync b goto w426; loc w426: invariant xabs <= 2149/100 when xabs = 2149/100 sync a goto w427; loc w427: invariant xabs <= 2158/100 when xabs = 2158/100 sync b goto w428; loc w428: invariant xabs <= 2163/100 when xabs = 2163/100 sync a goto w429; loc w429: invariant xabs <= 2164/100 when xabs = 2164/100 sync b goto w430; loc w430: invariant xabs <= 2167/100 when xabs = 2167/100 sync a goto w431; loc w431: invariant xabs <= 2176/100 when xabs = 2176/100 sync b goto w432; loc w432: invariant xabs <= 2181/100 when xabs = 2181/100 sync a goto w433; loc w433: invariant xabs <= 2185/100 when xabs = 2185/100 sync b goto w434; loc w434: invariant xabs <= 2194/100 when xabs = 2194/100 sync a goto w435; loc w435: invariant xabs <= 2201/100 when xabs = 2201/100 sync b goto w436; loc w436: invariant xabs <= 2204/100 when xabs = 2204/100 sync a goto w437; loc w437: invariant xabs <= 2211/100 when xabs = 2211/100 sync b goto w438; loc w438: invariant xabs <= 2214/100 when xabs = 2214/100 sync a goto w439; loc w439: invariant xabs <= 2216/100 when xabs = 2216/100 sync b goto w440; loc w440: invariant xabs <= 2222/100 when xabs = 2222/100 sync a goto w441; loc w441: invariant xabs <= 2231/100 when xabs = 2231/100 sync b goto w442; loc w442: invariant xabs <= 2239/100 when xabs = 2239/100 sync a goto w443; loc w443: invariant xabs <= 2240/100 when xabs = 2240/100 sync b goto w444; loc w444: invariant xabs <= 2248/100 when xabs = 2248/100 sync a goto w445; loc w445: invariant xabs <= 2251/100 when xabs = 2251/100 sync b goto w446; loc w446: invariant xabs <= 2260/100 when xabs = 2260/100 sync a goto w447; loc w447: invariant xabs <= 2266/100 when xabs = 2266/100 sync b goto w448; loc w448: invariant xabs <= 2270/100 when xabs = 2270/100 sync a goto w449; loc w449: invariant xabs <= 2276/100 when xabs = 2276/100 sync b goto w450; loc w450: invariant xabs <= 2277/100 when xabs = 2277/100 sync a goto w451; loc w451: invariant xabs <= 2284/100 when xabs = 2284/100 sync b goto w452; loc w452: invariant xabs <= 2292/100 when xabs = 2292/100 sync a goto w453; loc w453: invariant xabs <= 2296/100 when xabs = 2296/100 sync b goto w454; loc w454: invariant xabs <= 2300/100 when xabs = 2300/100 sync a goto w455; loc w455: invariant xabs <= 2303/100 when xabs = 2303/100 sync b goto w456; loc w456: invariant xabs <= 2304/100 when xabs = 2304/100 sync a goto w457; loc w457: invariant xabs <= 2308/100 when xabs = 2308/100 sync b goto w458; loc w458: invariant xabs <= 2313/100 when xabs = 2313/100 sync a goto w459; loc w459: invariant xabs <= 2319/100 when xabs = 2319/100 sync b goto w460; loc w460: invariant xabs <= 2321/100 when xabs = 2321/100 sync a goto w461; loc w461: invariant xabs <= 2327/100 when xabs = 2327/100 sync b goto w462; loc w462: invariant xabs <= 2328/100 when xabs = 2328/100 sync a goto w463; loc w463: invariant xabs <= 2329/100 when xabs = 2329/100 sync b goto w464; loc w464: invariant xabs <= 2331/100 when xabs = 2331/100 sync a goto w465; loc w465: invariant xabs <= 2339/100 when xabs = 2339/100 sync b goto w466; loc w466: invariant xabs <= 2341/100 when xabs = 2341/100 sync a goto w467; loc w467: invariant xabs <= 2350/100 when xabs = 2350/100 sync b goto w468; loc w468: invariant xabs <= 2356/100 when xabs = 2356/100 sync a goto w469; loc w469: invariant xabs <= 2364/100 when xabs = 2364/100 sync b goto w470; loc w470: invariant xabs <= 2371/100 when xabs = 2371/100 sync a goto w471; loc w471: invariant xabs <= 2375/100 when xabs = 2375/100 sync b goto w472; loc w472: invariant xabs <= 2377/100 when xabs = 2377/100 sync a goto w473; loc w473: invariant xabs <= 2382/100 when xabs = 2382/100 sync b goto w474; loc w474: invariant xabs <= 2390/100 when xabs = 2390/100 sync a goto w475; loc w475: invariant xabs <= 2399/100 when xabs = 2399/100 sync b goto w476; loc w476: invariant xabs <= 2405/100 when xabs = 2405/100 sync a goto w477; loc w477: invariant xabs <= 2410/100 when xabs = 2410/100 sync b goto w478; loc w478: invariant xabs <= 2415/100 when xabs = 2415/100 sync a goto w479; loc w479: invariant xabs <= 2417/100 when xabs = 2417/100 sync b goto w480; loc w480: invariant xabs <= 2421/100 when xabs = 2421/100 sync a goto w481; loc w481: invariant xabs <= 2429/100 when xabs = 2429/100 sync b goto w482; loc w482: invariant xabs <= 2432/100 when xabs = 2432/100 sync a goto w483; loc w483: invariant xabs <= 2435/100 when xabs = 2435/100 sync b goto w484; loc w484: invariant xabs <= 2443/100 when xabs = 2443/100 sync a goto w485; loc w485: invariant xabs <= 2445/100 when xabs = 2445/100 sync b goto w486; loc w486: invariant xabs <= 2451/100 when xabs = 2451/100 sync a goto w487; loc w487: invariant xabs <= 2457/100 when xabs = 2457/100 sync b goto w488; loc w488: invariant xabs <= 2458/100 when xabs = 2458/100 sync a goto w489; loc w489: invariant xabs <= 2465/100 when xabs = 2465/100 sync b goto w490; loc w490: invariant xabs <= 2466/100 when xabs = 2466/100 sync a goto w491; loc w491: invariant xabs <= 2472/100 when xabs = 2472/100 sync b goto w492; loc w492: invariant xabs <= 2473/100 when xabs = 2473/100 sync a goto w493; loc w493: invariant xabs <= 2482/100 when xabs = 2482/100 sync b goto w494; loc w494: invariant xabs <= 2491/100 when xabs = 2491/100 sync a goto w495; loc w495: invariant xabs <= 2497/100 when xabs = 2497/100 sync b goto w496; loc w496: invariant xabs <= 2506/100 when xabs = 2506/100 sync a goto w497; loc w497: invariant xabs <= 2510/100 when xabs = 2510/100 sync b goto w498; loc w498: invariant xabs <= 2516/100 when xabs = 2516/100 sync a goto w499; loc w499: invariant xabs <= 2523/100 when xabs = 2523/100 sync b goto w500; loc w500: invariant xabs <= 2525/100 when xabs = 2525/100 sync a goto w501; loc w501: invariant xabs <= 2532/100 when xabs = 2532/100 sync b goto w502; loc w502: invariant xabs <= 2533/100 when xabs = 2533/100 sync a goto w503; loc w503: invariant xabs <= 2539/100 when xabs = 2539/100 sync b goto w504; loc w504: invariant xabs <= 2548/100 when xabs = 2548/100 sync a goto w505; loc w505: invariant xabs <= 2554/100 when xabs = 2554/100 sync b goto w506; loc w506: invariant xabs <= 2557/100 when xabs = 2557/100 sync a goto w507; loc w507: invariant xabs <= 2564/100 when xabs = 2564/100 sync b goto w508; loc w508: invariant xabs <= 2571/100 when xabs = 2571/100 sync a goto w509; loc w509: invariant xabs <= 2577/100 when xabs = 2577/100 sync b goto w510; loc w510: invariant xabs <= 2579/100 when xabs = 2579/100 sync a goto w511; loc w511: invariant xabs <= 2584/100 when xabs = 2584/100 sync b goto w512; loc w512: invariant xabs <= 2588/100 when xabs = 2588/100 sync a goto w513; loc w513: invariant xabs <= 2595/100 when xabs = 2595/100 sync b goto w514; loc w514: invariant xabs <= 2599/100 when xabs = 2599/100 sync a goto w515; loc w515: invariant xabs <= 2603/100 when xabs = 2603/100 sync b goto w516; loc w516: invariant xabs <= 2607/100 when xabs = 2607/100 sync a goto w517; loc w517: invariant xabs <= 2609/100 when xabs = 2609/100 sync b goto w518; loc w518: invariant xabs <= 2610/100 when xabs = 2610/100 sync a goto w519; loc w519: invariant xabs <= 2615/100 when xabs = 2615/100 sync b goto w520; loc w520: invariant xabs <= 2623/100 when xabs = 2623/100 sync a goto w521; loc w521: invariant xabs <= 2627/100 when xabs = 2627/100 sync b goto w522; loc w522: invariant xabs <= 2633/100 when xabs = 2633/100 sync a goto w523; loc w523: invariant xabs <= 2634/100 when xabs = 2634/100 sync b goto w524; loc w524: invariant xabs <= 2641/100 when xabs = 2641/100 sync a goto w525; loc w525: invariant xabs <= 2648/100 when xabs = 2648/100 sync b goto w526; loc w526: invariant xabs <= 2657/100 when xabs = 2657/100 sync a goto w527; loc w527: invariant xabs <= 2661/100 when xabs = 2661/100 sync b goto w528; loc w528: invariant xabs <= 2663/100 when xabs = 2663/100 sync a goto w529; loc w529: invariant xabs <= 2671/100 when xabs = 2671/100 sync b goto w530; loc w530: invariant xabs <= 2677/100 when xabs = 2677/100 sync a goto w531; loc w531: invariant xabs <= 2683/100 when xabs = 2683/100 sync b goto w532; loc w532: invariant xabs <= 2692/100 when xabs = 2692/100 sync a goto w533; loc w533: invariant xabs <= 2696/100 when xabs = 2696/100 sync b goto w534; loc w534: invariant xabs <= 2705/100 when xabs = 2705/100 sync a goto w535; loc w535: invariant xabs <= 2714/100 when xabs = 2714/100 sync b goto w536; loc w536: invariant xabs <= 2717/100 when xabs = 2717/100 sync a goto w537; loc w537: invariant xabs <= 2721/100 when xabs = 2721/100 sync b goto w538; loc w538: invariant xabs <= 2728/100 when xabs = 2728/100 sync a goto w539; loc w539: invariant xabs <= 2737/100 when xabs = 2737/100 sync b goto w540; loc w540: invariant xabs <= 2739/100 when xabs = 2739/100 sync a goto w541; loc w541: invariant xabs <= 2742/100 when xabs = 2742/100 sync b goto w542; loc w542: invariant xabs <= 2745/100 when xabs = 2745/100 sync a goto w543; loc w543: invariant xabs <= 2748/100 when xabs = 2748/100 sync b goto w544; loc w544: invariant xabs <= 2751/100 when xabs = 2751/100 sync a goto w545; loc w545: invariant xabs <= 2755/100 when xabs = 2755/100 sync b goto w546; loc w546: invariant xabs <= 2757/100 when xabs = 2757/100 sync a goto w547; loc w547: invariant xabs <= 2760/100 when xabs = 2760/100 sync b goto w548; loc w548: invariant xabs <= 2761/100 when xabs = 2761/100 sync a goto w549; loc w549: invariant xabs <= 2765/100 when xabs = 2765/100 sync b goto w550; loc w550: invariant xabs <= 2770/100 when xabs = 2770/100 sync a goto w551; loc w551: invariant xabs <= 2773/100 when xabs = 2773/100 sync b goto w552; loc w552: invariant xabs <= 2780/100 when xabs = 2780/100 sync a goto w553; loc w553: invariant xabs <= 2787/100 when xabs = 2787/100 sync b goto w554; loc w554: invariant xabs <= 2788/100 when xabs = 2788/100 sync a goto w555; loc w555: invariant xabs <= 2792/100 when xabs = 2792/100 sync b goto w556; loc w556: invariant xabs <= 2793/100 when xabs = 2793/100 sync a goto w557; loc w557: invariant xabs <= 2794/100 when xabs = 2794/100 sync b goto w558; loc w558: invariant xabs <= 2795/100 when xabs = 2795/100 sync a goto w559; loc w559: invariant xabs <= 2800/100 when xabs = 2800/100 sync b goto w560; loc w560: invariant xabs <= 2808/100 when xabs = 2808/100 sync a goto w561; loc w561: invariant xabs <= 2810/100 when xabs = 2810/100 sync b goto w562; loc w562: invariant xabs <= 2819/100 when xabs = 2819/100 sync a goto w563; loc w563: invariant xabs <= 2828/100 when xabs = 2828/100 sync b goto w564; loc w564: invariant xabs <= 2831/100 when xabs = 2831/100 sync a goto w565; loc w565: invariant xabs <= 2834/100 when xabs = 2834/100 sync b goto w566; loc w566: invariant xabs <= 2837/100 when xabs = 2837/100 sync a goto w567; loc w567: invariant xabs <= 2841/100 when xabs = 2841/100 sync b goto w568; loc w568: invariant xabs <= 2844/100 when xabs = 2844/100 sync a goto w569; loc w569: invariant xabs <= 2848/100 when xabs = 2848/100 sync b goto w570; loc w570: invariant xabs <= 2852/100 when xabs = 2852/100 sync a goto w571; loc w571: invariant xabs <= 2861/100 when xabs = 2861/100 sync b goto w572; loc w572: invariant xabs <= 2865/100 when xabs = 2865/100 sync a goto w573; loc w573: invariant xabs <= 2869/100 when xabs = 2869/100 sync b goto w574; loc w574: invariant xabs <= 2876/100 when xabs = 2876/100 sync a goto w575; loc w575: invariant xabs <= 2885/100 when xabs = 2885/100 sync b goto w576; loc w576: invariant xabs <= 2888/100 when xabs = 2888/100 sync a goto w577; loc w577: invariant xabs <= 2895/100 when xabs = 2895/100 sync b goto w578; loc w578: invariant xabs <= 2898/100 when xabs = 2898/100 sync a goto w579; loc w579: invariant xabs <= 2907/100 when xabs = 2907/100 sync b goto w580; loc w580: invariant xabs <= 2914/100 when xabs = 2914/100 sync a goto w581; loc w581: invariant xabs <= 2917/100 when xabs = 2917/100 sync b goto w582; loc w582: invariant xabs <= 2922/100 when xabs = 2922/100 sync a goto w583; loc w583: invariant xabs <= 2931/100 when xabs = 2931/100 sync b goto w584; loc w584: invariant xabs <= 2939/100 when xabs = 2939/100 sync a goto w585; loc w585: invariant xabs <= 2940/100 when xabs = 2940/100 sync b goto w586; loc w586: invariant xabs <= 2942/100 when xabs = 2942/100 sync a goto w587; loc w587: invariant xabs <= 2945/100 when xabs = 2945/100 sync b goto w588; loc w588: invariant xabs <= 2951/100 when xabs = 2951/100 sync a goto w589; loc w589: invariant xabs <= 2956/100 when xabs = 2956/100 sync b goto w590; loc w590: invariant xabs <= 2961/100 when xabs = 2961/100 sync a goto w591; loc w591: invariant xabs <= 2970/100 when xabs = 2970/100 sync b goto w592; loc w592: invariant xabs <= 2979/100 when xabs = 2979/100 sync a goto w593; loc w593: invariant xabs <= 2988/100 when xabs = 2988/100 sync b goto w594; loc w594: invariant xabs <= 2995/100 when xabs = 2995/100 sync a goto w595; loc w595: invariant xabs <= 2998/100 when xabs = 2998/100 sync b goto w596; loc w596: invariant xabs <= 3002/100 when xabs = 3002/100 sync a goto w597; loc w597: invariant xabs <= 3005/100 when xabs = 3005/100 sync b goto w598; loc w598: invariant xabs <= 3014/100 when xabs = 3014/100 sync a goto w599; loc w599: invariant xabs <= 3023/100 when xabs = 3023/100 sync b goto w600; loc w600: invariant xabs <= 3028/100 when xabs = 3028/100 sync a goto w601; loc w601: invariant xabs <= 3033/100 when xabs = 3033/100 sync b goto w602; loc w602: invariant xabs <= 3040/100 when xabs = 3040/100 sync a goto w603; loc w603: invariant xabs <= 3049/100 when xabs = 3049/100 sync b goto w604; loc w604: invariant xabs <= 3055/100 when xabs = 3055/100 sync a goto w605; loc w605: invariant xabs <= 3062/100 when xabs = 3062/100 sync b goto w606; loc w606: invariant xabs <= 3063/100 when xabs = 3063/100 sync a goto w607; loc w607: invariant xabs <= 3066/100 when xabs = 3066/100 sync b goto w608; loc w608: invariant xabs <= 3069/100 when xabs = 3069/100 sync a goto w609; loc w609: invariant xabs <= 3070/100 when xabs = 3070/100 sync b goto w610; loc w610: invariant xabs <= 3072/100 when xabs = 3072/100 sync a goto w611; loc w611: invariant xabs <= 3076/100 when xabs = 3076/100 sync b goto w612; loc w612: invariant xabs <= 3081/100 when xabs = 3081/100 sync a goto w613; loc w613: invariant xabs <= 3086/100 when xabs = 3086/100 sync b goto w614; loc w614: invariant xabs <= 3092/100 when xabs = 3092/100 sync a goto w615; loc w615: invariant xabs <= 3097/100 when xabs = 3097/100 sync b goto w616; loc w616: invariant xabs <= 3102/100 when xabs = 3102/100 sync a goto w617; loc w617: invariant xabs <= 3111/100 when xabs = 3111/100 sync b goto w618; loc w618: invariant xabs <= 3120/100 when xabs = 3120/100 sync a goto w619; loc w619: invariant xabs <= 3121/100 when xabs = 3121/100 sync b goto w620; loc w620: invariant xabs <= 3128/100 when xabs = 3128/100 sync a goto w621; loc w621: invariant xabs <= 3131/100 when xabs = 3131/100 sync b goto w622; loc w622: invariant xabs <= 3139/100 when xabs = 3139/100 sync a goto w623; loc w623: invariant xabs <= 3147/100 when xabs = 3147/100 sync b goto w624; loc w624: invariant xabs <= 3156/100 when xabs = 3156/100 sync a goto w625; loc w625: invariant xabs <= 3160/100 when xabs = 3160/100 sync b goto w626; loc w626: invariant xabs <= 3168/100 when xabs = 3168/100 sync a goto w627; loc w627: invariant xabs <= 3171/100 when xabs = 3171/100 sync b goto w628; loc w628: invariant xabs <= 3177/100 when xabs = 3177/100 sync a goto w629; loc w629: invariant xabs <= 3179/100 when xabs = 3179/100 sync b goto w630; loc w630: invariant xabs <= 3186/100 when xabs = 3186/100 sync a goto w631; loc w631: invariant xabs <= 3192/100 when xabs = 3192/100 sync b goto w632; loc w632: invariant xabs <= 3197/100 when xabs = 3197/100 sync a goto w633; loc w633: invariant xabs <= 3198/100 when xabs = 3198/100 sync b goto w634; loc w634: invariant xabs <= 3203/100 when xabs = 3203/100 sync a goto w635; loc w635: invariant xabs <= 3208/100 when xabs = 3208/100 sync b goto w636; loc w636: invariant xabs <= 3211/100 when xabs = 3211/100 sync a goto w637; loc w637: invariant xabs <= 3212/100 when xabs = 3212/100 sync b goto w638; loc w638: invariant xabs <= 3218/100 when xabs = 3218/100 sync a goto w639; loc w639: invariant xabs <= 3223/100 when xabs = 3223/100 sync b goto w640; loc w640: invariant xabs <= 3228/100 when xabs = 3228/100 sync a goto w641; loc w641: invariant xabs <= 3237/100 when xabs = 3237/100 sync b goto w642; loc w642: invariant xabs <= 3245/100 when xabs = 3245/100 sync a goto w643; loc w643: invariant xabs <= 3250/100 when xabs = 3250/100 sync b goto w644; loc w644: invariant xabs <= 3258/100 when xabs = 3258/100 sync a goto w645; loc w645: invariant xabs <= 3267/100 when xabs = 3267/100 sync b goto w646; loc w646: invariant xabs <= 3272/100 when xabs = 3272/100 sync a goto w647; loc w647: invariant xabs <= 3273/100 when xabs = 3273/100 sync b goto w648; loc w648: invariant xabs <= 3279/100 when xabs = 3279/100 sync a goto w649; loc w649: invariant xabs <= 3281/100 when xabs = 3281/100 sync b goto w650; loc w650: invariant xabs <= 3289/100 when xabs = 3289/100 sync a goto w651; loc w651: invariant xabs <= 3291/100 when xabs = 3291/100 sync b goto w652; loc w652: invariant xabs <= 3300/100 when xabs = 3300/100 sync a goto w653; loc w653: invariant xabs <= 3302/100 when xabs = 3302/100 sync b goto w654; loc w654: invariant xabs <= 3309/100 when xabs = 3309/100 sync a goto w655; loc w655: invariant xabs <= 3312/100 when xabs = 3312/100 sync b goto w656; loc w656: invariant xabs <= 3313/100 when xabs = 3313/100 sync a goto w657; loc w657: invariant xabs <= 3315/100 when xabs = 3315/100 sync b goto w658; loc w658: invariant xabs <= 3321/100 when xabs = 3321/100 sync a goto w659; loc w659: invariant xabs <= 3326/100 when xabs = 3326/100 sync b goto w660; loc w660: invariant xabs <= 3335/100 when xabs = 3335/100 sync a goto w661; loc w661: invariant xabs <= 3338/100 when xabs = 3338/100 sync b goto w662; loc w662: invariant xabs <= 3345/100 when xabs = 3345/100 sync a goto w663; loc w663: invariant xabs <= 3346/100 when xabs = 3346/100 sync b goto w664; loc w664: invariant xabs <= 3354/100 when xabs = 3354/100 sync a goto w665; loc w665: invariant xabs <= 3355/100 when xabs = 3355/100 sync b goto w666; loc w666: invariant xabs <= 3359/100 when xabs = 3359/100 sync a goto w667; loc w667: invariant xabs <= 3363/100 when xabs = 3363/100 sync b goto w668; loc w668: invariant xabs <= 3366/100 when xabs = 3366/100 sync a goto w669; loc w669: invariant xabs <= 3374/100 when xabs = 3374/100 sync b goto w670; loc w670: invariant xabs <= 3378/100 when xabs = 3378/100 sync a goto w671; loc w671: invariant xabs <= 3384/100 when xabs = 3384/100 sync b goto w672; loc w672: invariant xabs <= 3386/100 when xabs = 3386/100 sync a goto w673; loc w673: invariant xabs <= 3391/100 when xabs = 3391/100 sync b goto w674; loc w674: invariant xabs <= 3399/100 when xabs = 3399/100 sync a goto w675; loc w675: invariant xabs <= 3403/100 when xabs = 3403/100 sync b goto w676; loc w676: invariant xabs <= 3405/100 when xabs = 3405/100 sync a goto w677; loc w677: invariant xabs <= 3411/100 when xabs = 3411/100 sync b goto w678; loc w678: invariant xabs <= 3418/100 when xabs = 3418/100 sync a goto w679; loc w679: invariant xabs <= 3426/100 when xabs = 3426/100 sync b goto w680; loc w680: invariant xabs <= 3433/100 when xabs = 3433/100 sync a goto w681; loc w681: invariant xabs <= 3440/100 when xabs = 3440/100 sync b goto w682; loc w682: invariant xabs <= 3441/100 when xabs = 3441/100 sync a goto w683; loc w683: invariant xabs <= 3445/100 when xabs = 3445/100 sync b goto w684; loc w684: invariant xabs <= 3451/100 when xabs = 3451/100 sync a goto w685; loc w685: invariant xabs <= 3457/100 when xabs = 3457/100 sync b goto w686; loc w686: invariant xabs <= 3460/100 when xabs = 3460/100 sync a goto w687; loc w687: invariant xabs <= 3461/100 when xabs = 3461/100 sync b goto w688; loc w688: invariant xabs <= 3470/100 when xabs = 3470/100 sync a goto w689; loc w689: invariant xabs <= 3473/100 when xabs = 3473/100 sync b goto w690; loc w690: invariant xabs <= 3475/100 when xabs = 3475/100 sync a goto w691; loc w691: invariant xabs <= 3484/100 when xabs = 3484/100 sync b goto w692; loc w692: invariant xabs <= 3485/100 when xabs = 3485/100 sync a goto w693; loc w693: invariant xabs <= 3486/100 when xabs = 3486/100 sync b goto w694; loc w694: invariant xabs <= 3488/100 when xabs = 3488/100 sync a goto w695; loc w695: invariant xabs <= 3495/100 when xabs = 3495/100 sync b goto w696; loc w696: invariant xabs <= 3497/100 when xabs = 3497/100 sync a goto w697; loc w697: invariant xabs <= 3499/100 when xabs = 3499/100 sync b goto w698; loc w698: invariant xabs <= 3507/100 when xabs = 3507/100 sync a goto w699; loc w699: invariant xabs <= 3515/100 when xabs = 3515/100 sync b goto w700; loc w700: invariant xabs <= 3521/100 when xabs = 3521/100 sync a goto w701; loc w701: invariant xabs <= 3526/100 when xabs = 3526/100 sync b goto w702; loc w702: invariant xabs <= 3534/100 when xabs = 3534/100 sync a goto w703; loc w703: invariant xabs <= 3543/100 when xabs = 3543/100 sync b goto w704; loc w704: invariant xabs <= 3548/100 when xabs = 3548/100 sync a goto w705; loc w705: invariant xabs <= 3557/100 when xabs = 3557/100 sync b goto w706; loc w706: invariant xabs <= 3566/100 when xabs = 3566/100 sync a goto w707; loc w707: invariant xabs <= 3575/100 when xabs = 3575/100 sync b goto w708; loc w708: invariant xabs <= 3582/100 when xabs = 3582/100 sync a goto w709; loc w709: invariant xabs <= 3591/100 when xabs = 3591/100 sync b goto w710; loc w710: invariant xabs <= 3592/100 when xabs = 3592/100 sync a goto w711; loc w711: invariant xabs <= 3600/100 when xabs = 3600/100 sync b goto w712; loc w712: invariant xabs <= 3608/100 when xabs = 3608/100 sync a goto w713; loc w713: invariant xabs <= 3615/100 when xabs = 3615/100 sync b goto w714; loc w714: invariant xabs <= 3620/100 when xabs = 3620/100 sync a goto w715; loc w715: invariant xabs <= 3628/100 when xabs = 3628/100 sync b goto w716; loc w716: invariant xabs <= 3636/100 when xabs = 3636/100 sync a goto w717; loc w717: invariant xabs <= 3642/100 when xabs = 3642/100 sync b goto w718; loc w718: invariant xabs <= 3647/100 when xabs = 3647/100 sync a goto w719; loc w719: invariant xabs <= 3656/100 when xabs = 3656/100 sync b goto w720; loc w720: invariant xabs <= 3659/100 when xabs = 3659/100 sync a goto w721; loc w721: invariant xabs <= 3660/100 when xabs = 3660/100 sync b goto w722; loc w722: invariant xabs <= 3664/100 when xabs = 3664/100 sync a goto w723; loc w723: invariant xabs <= 3665/100 when xabs = 3665/100 sync b goto w724; loc w724: invariant xabs <= 3674/100 when xabs = 3674/100 sync a goto w725; loc w725: invariant xabs <= 3683/100 when xabs = 3683/100 sync b goto w726; loc w726: invariant xabs <= 3690/100 when xabs = 3690/100 sync a goto w727; loc w727: invariant xabs <= 3693/100 when xabs = 3693/100 sync b goto w728; loc w728: invariant xabs <= 3701/100 when xabs = 3701/100 sync a goto w729; loc w729: invariant xabs <= 3702/100 when xabs = 3702/100 sync b goto w730; loc w730: invariant xabs <= 3705/100 when xabs = 3705/100 sync a goto w731; loc w731: invariant xabs <= 3709/100 when xabs = 3709/100 sync b goto w732; loc w732: invariant xabs <= 3718/100 when xabs = 3718/100 sync a goto w733; loc w733: invariant xabs <= 3722/100 when xabs = 3722/100 sync b goto w734; loc w734: invariant xabs <= 3726/100 when xabs = 3726/100 sync a goto w735; loc w735: invariant xabs <= 3735/100 when xabs = 3735/100 sync b goto w736; loc w736: invariant xabs <= 3739/100 when xabs = 3739/100 sync a goto w737; loc w737: invariant xabs <= 3744/100 when xabs = 3744/100 sync b goto w738; loc w738: invariant xabs <= 3746/100 when xabs = 3746/100 sync a goto w739; loc w739: invariant xabs <= 3747/100 when xabs = 3747/100 sync b goto w740; loc w740: invariant xabs <= 3748/100 when xabs = 3748/100 sync a goto w741; loc w741: invariant xabs <= 3754/100 when xabs = 3754/100 sync b goto w742; loc w742: invariant xabs <= 3757/100 when xabs = 3757/100 sync a goto w743; loc w743: invariant xabs <= 3763/100 when xabs = 3763/100 sync b goto w744; loc w744: invariant xabs <= 3765/100 when xabs = 3765/100 sync a goto w745; loc w745: invariant xabs <= 3768/100 when xabs = 3768/100 sync b goto w746; loc w746: invariant xabs <= 3775/100 when xabs = 3775/100 sync a goto w747; loc w747: invariant xabs <= 3777/100 when xabs = 3777/100 sync b goto w748; loc w748: invariant xabs <= 3786/100 when xabs = 3786/100 sync a goto w749; loc w749: invariant xabs <= 3791/100 when xabs = 3791/100 sync b goto w750; loc w750: invariant xabs <= 3799/100 when xabs = 3799/100 sync a goto w751; loc w751: invariant xabs <= 3803/100 when xabs = 3803/100 sync b goto w752; loc w752: invariant xabs <= 3804/100 when xabs = 3804/100 sync a goto w753; loc w753: invariant xabs <= 3812/100 when xabs = 3812/100 sync b goto w754; loc w754: invariant xabs <= 3819/100 when xabs = 3819/100 sync a goto w755; loc w755: invariant xabs <= 3825/100 when xabs = 3825/100 sync b goto w756; loc w756: invariant xabs <= 3829/100 when xabs = 3829/100 sync a goto w757; loc w757: invariant xabs <= 3838/100 when xabs = 3838/100 sync b goto w758; loc w758: invariant xabs <= 3847/100 when xabs = 3847/100 sync a goto w759; loc w759: invariant xabs <= 3855/100 when xabs = 3855/100 sync b goto w760; loc w760: invariant xabs <= 3862/100 when xabs = 3862/100 sync a goto w761; loc w761: invariant xabs <= 3871/100 when xabs = 3871/100 sync b goto w762; loc w762: invariant xabs <= 3877/100 when xabs = 3877/100 sync a goto w763; loc w763: invariant xabs <= 3886/100 when xabs = 3886/100 sync b goto w764; loc w764: invariant xabs <= 3891/100 when xabs = 3891/100 sync a goto w765; loc w765: invariant xabs <= 3893/100 when xabs = 3893/100 sync b goto w766; loc w766: invariant xabs <= 3900/100 when xabs = 3900/100 sync a goto w767; loc w767: invariant xabs <= 3905/100 when xabs = 3905/100 sync b goto w768; loc w768: invariant xabs <= 3908/100 when xabs = 3908/100 sync a goto w769; loc w769: invariant xabs <= 3913/100 when xabs = 3913/100 sync b goto w770; loc w770: invariant xabs <= 3920/100 when xabs = 3920/100 sync a goto w771; loc w771: invariant xabs <= 3924/100 when xabs = 3924/100 sync b goto w772; loc w772: invariant xabs <= 3932/100 when xabs = 3932/100 sync a goto w773; loc w773: invariant xabs <= 3936/100 when xabs = 3936/100 sync b goto w774; loc w774: invariant xabs <= 3943/100 when xabs = 3943/100 sync a goto w775; loc w775: invariant xabs <= 3947/100 when xabs = 3947/100 sync b goto w776; loc w776: invariant xabs <= 3955/100 when xabs = 3955/100 sync a goto w777; loc w777: invariant xabs <= 3964/100 when xabs = 3964/100 sync b goto w778; loc w778: invariant xabs <= 3972/100 when xabs = 3972/100 sync a goto w779; loc w779: invariant xabs <= 3980/100 when xabs = 3980/100 sync b goto w780; loc w780: invariant xabs <= 3982/100 when xabs = 3982/100 sync a goto w781; loc w781: invariant xabs <= 3987/100 when xabs = 3987/100 sync b goto w782; loc w782: invariant xabs <= 3990/100 when xabs = 3990/100 sync a goto w783; loc w783: invariant xabs <= 3997/100 when xabs = 3997/100 sync b goto w784; loc w784: invariant xabs <= 3999/100 when xabs = 3999/100 sync a goto w785; loc w785: invariant xabs <= 4005/100 when xabs = 4005/100 sync b goto w786; loc w786: invariant xabs <= 4014/100 when xabs = 4014/100 sync a goto w787; loc w787: invariant xabs <= 4015/100 when xabs = 4015/100 sync b goto w788; loc w788: invariant xabs <= 4019/100 when xabs = 4019/100 sync a goto w789; loc w789: invariant xabs <= 4021/100 when xabs = 4021/100 sync b goto w790; loc w790: invariant xabs <= 4023/100 when xabs = 4023/100 sync a goto w791; loc w791: invariant xabs <= 4028/100 when xabs = 4028/100 sync b goto w792; loc w792: invariant xabs <= 4029/100 when xabs = 4029/100 sync a goto w793; loc w793: invariant xabs <= 4034/100 when xabs = 4034/100 sync b goto w794; loc w794: invariant xabs <= 4035/100 when xabs = 4035/100 sync a goto w795; loc w795: invariant xabs <= 4038/100 when xabs = 4038/100 sync b goto w796; loc w796: invariant xabs <= 4046/100 when xabs = 4046/100 sync a goto w797; loc w797: invariant xabs <= 4052/100 when xabs = 4052/100 sync b goto w798; loc w798: invariant xabs <= 4053/100 when xabs = 4053/100 sync a goto w799; loc w799: invariant xabs <= 4054/100 when xabs = 4054/100 sync b goto w800; loc w800: invariant xabs <= 4062/100 when xabs = 4062/100 sync a goto w801; loc w801: invariant xabs <= 4071/100 when xabs = 4071/100 sync b goto w802; loc w802: invariant xabs <= 4074/100 when xabs = 4074/100 sync a goto w803; loc w803: invariant xabs <= 4079/100 when xabs = 4079/100 sync b goto w804; loc w804: invariant xabs <= 4082/100 when xabs = 4082/100 sync a goto w805; loc w805: invariant xabs <= 4091/100 when xabs = 4091/100 sync b goto w806; loc w806: invariant xabs <= 4095/100 when xabs = 4095/100 sync a goto w807; loc w807: invariant xabs <= 4097/100 when xabs = 4097/100 sync b goto w808; loc w808: invariant xabs <= 4102/100 when xabs = 4102/100 sync a goto w809; loc w809: invariant xabs <= 4110/100 when xabs = 4110/100 sync b goto w810; loc w810: invariant xabs <= 4114/100 when xabs = 4114/100 sync a goto w811; loc w811: invariant xabs <= 4122/100 when xabs = 4122/100 sync b goto w812; loc w812: invariant xabs <= 4126/100 when xabs = 4126/100 sync a goto w813; loc w813: invariant xabs <= 4135/100 when xabs = 4135/100 sync b goto w814; loc w814: invariant xabs <= 4140/100 when xabs = 4140/100 sync a goto w815; loc w815: invariant xabs <= 4145/100 when xabs = 4145/100 sync b goto w816; loc w816: invariant xabs <= 4147/100 when xabs = 4147/100 sync a goto w817; loc w817: invariant xabs <= 4156/100 when xabs = 4156/100 sync b goto w818; loc w818: invariant xabs <= 4159/100 when xabs = 4159/100 sync a goto w819; loc w819: invariant xabs <= 4165/100 when xabs = 4165/100 sync b goto w820; loc w820: invariant xabs <= 4173/100 when xabs = 4173/100 sync a goto w821; loc w821: invariant xabs <= 4180/100 when xabs = 4180/100 sync b goto w822; loc w822: invariant xabs <= 4181/100 when xabs = 4181/100 sync a goto w823; loc w823: invariant xabs <= 4189/100 when xabs = 4189/100 sync b goto w824; loc w824: invariant xabs <= 4193/100 when xabs = 4193/100 sync a goto w825; loc w825: invariant xabs <= 4198/100 when xabs = 4198/100 sync b goto w826; loc w826: invariant xabs <= 4205/100 when xabs = 4205/100 sync a goto w827; loc w827: invariant xabs <= 4214/100 when xabs = 4214/100 sync b goto w828; loc w828: invariant xabs <= 4217/100 when xabs = 4217/100 sync a goto w829; loc w829: invariant xabs <= 4224/100 when xabs = 4224/100 sync b goto w830; loc w830: invariant xabs <= 4229/100 when xabs = 4229/100 sync a goto w831; loc w831: invariant xabs <= 4231/100 when xabs = 4231/100 sync b goto w832; loc w832: invariant xabs <= 4236/100 when xabs = 4236/100 sync a goto w833; loc w833: invariant xabs <= 4239/100 when xabs = 4239/100 sync b goto w834; loc w834: invariant xabs <= 4243/100 when xabs = 4243/100 sync a goto w835; loc w835: invariant xabs <= 4252/100 when xabs = 4252/100 sync b goto w836; loc w836: invariant xabs <= 4259/100 when xabs = 4259/100 sync a goto w837; loc w837: invariant xabs <= 4267/100 when xabs = 4267/100 sync b goto w838; loc w838: invariant xabs <= 4268/100 when xabs = 4268/100 sync a goto w839; loc w839: invariant xabs <= 4274/100 when xabs = 4274/100 sync b goto w840; loc w840: invariant xabs <= 4282/100 when xabs = 4282/100 sync a goto w841; loc w841: invariant xabs <= 4289/100 when xabs = 4289/100 sync b goto w842; loc w842: invariant xabs <= 4290/100 when xabs = 4290/100 sync a goto w843; loc w843: invariant xabs <= 4295/100 when xabs = 4295/100 sync b goto w844; loc w844: invariant xabs <= 4298/100 when xabs = 4298/100 sync a goto w845; loc w845: invariant xabs <= 4301/100 when xabs = 4301/100 sync b goto w846; loc w846: invariant xabs <= 4306/100 when xabs = 4306/100 sync a goto w847; loc w847: invariant xabs <= 4307/100 when xabs = 4307/100 sync b goto w848; loc w848: invariant xabs <= 4315/100 when xabs = 4315/100 sync a goto w849; loc w849: invariant xabs <= 4318/100 when xabs = 4318/100 sync b goto w850; loc w850: invariant xabs <= 4322/100 when xabs = 4322/100 sync a goto w851; loc w851: invariant xabs <= 4330/100 when xabs = 4330/100 sync b goto w852; loc w852: invariant xabs <= 4333/100 when xabs = 4333/100 sync a goto w853; loc w853: invariant xabs <= 4339/100 when xabs = 4339/100 sync b goto w854; loc w854: invariant xabs <= 4340/100 when xabs = 4340/100 sync a goto w855; loc w855: invariant xabs <= 4349/100 when xabs = 4349/100 sync b goto w856; loc w856: invariant xabs <= 4358/100 when xabs = 4358/100 sync a goto w857; loc w857: invariant xabs <= 4362/100 when xabs = 4362/100 sync b goto w858; loc w858: invariant xabs <= 4369/100 when xabs = 4369/100 sync a goto w859; loc w859: invariant xabs <= 4371/100 when xabs = 4371/100 sync b goto w860; loc w860: invariant xabs <= 4374/100 when xabs = 4374/100 sync a goto w861; loc w861: invariant xabs <= 4377/100 when xabs = 4377/100 sync b goto w862; loc w862: invariant xabs <= 4378/100 when xabs = 4378/100 sync a goto w863; loc w863: invariant xabs <= 4383/100 when xabs = 4383/100 sync b goto w864; loc w864: invariant xabs <= 4385/100 when xabs = 4385/100 sync a goto w865; loc w865: invariant xabs <= 4393/100 when xabs = 4393/100 sync b goto w866; loc w866: invariant xabs <= 4402/100 when xabs = 4402/100 sync a goto w867; loc w867: invariant xabs <= 4407/100 when xabs = 4407/100 sync b goto w868; loc w868: invariant xabs <= 4408/100 when xabs = 4408/100 sync a goto w869; loc w869: invariant xabs <= 4414/100 when xabs = 4414/100 sync b goto w870; loc w870: invariant xabs <= 4423/100 when xabs = 4423/100 sync a goto w871; loc w871: invariant xabs <= 4428/100 when xabs = 4428/100 sync b goto w872; loc w872: invariant xabs <= 4433/100 when xabs = 4433/100 sync a goto w873; loc w873: invariant xabs <= 4435/100 when xabs = 4435/100 sync b goto w874; loc w874: invariant xabs <= 4443/100 when xabs = 4443/100 sync a goto w875; loc w875: invariant xabs <= 4444/100 when xabs = 4444/100 sync b goto w876; loc w876: invariant xabs <= 4449/100 when xabs = 4449/100 sync a goto w877; loc w877: invariant xabs <= 4454/100 when xabs = 4454/100 sync b goto w878; loc w878: invariant xabs <= 4456/100 when xabs = 4456/100 sync a goto w879; loc w879: invariant xabs <= 4463/100 when xabs = 4463/100 sync b goto w880; loc w880: invariant xabs <= 4464/100 when xabs = 4464/100 sync a goto w881; loc w881: invariant xabs <= 4467/100 when xabs = 4467/100 sync b goto w882; loc w882: invariant xabs <= 4473/100 when xabs = 4473/100 sync a goto w883; loc w883: invariant xabs <= 4474/100 when xabs = 4474/100 sync b goto w884; loc w884: invariant xabs <= 4483/100 when xabs = 4483/100 sync a goto w885; loc w885: invariant xabs <= 4491/100 when xabs = 4491/100 sync b goto w886; loc w886: invariant xabs <= 4496/100 when xabs = 4496/100 sync a goto w887; loc w887: invariant xabs <= 4497/100 when xabs = 4497/100 sync b goto w888; loc w888: invariant xabs <= 4501/100 when xabs = 4501/100 sync a goto w889; loc w889: invariant xabs <= 4510/100 when xabs = 4510/100 sync b goto w890; loc w890: invariant xabs <= 4517/100 when xabs = 4517/100 sync a goto w891; loc w891: invariant xabs <= 4521/100 when xabs = 4521/100 sync b goto w892; loc w892: invariant xabs <= 4526/100 when xabs = 4526/100 sync a goto w893; loc w893: invariant xabs <= 4529/100 when xabs = 4529/100 sync b goto w894; loc w894: invariant xabs <= 4537/100 when xabs = 4537/100 sync a goto w895; loc w895: invariant xabs <= 4545/100 when xabs = 4545/100 sync b goto w896; loc w896: invariant xabs <= 4551/100 when xabs = 4551/100 sync a goto w897; loc w897: invariant xabs <= 4556/100 when xabs = 4556/100 sync b goto w898; loc w898: invariant xabs <= 4561/100 when xabs = 4561/100 sync a goto w899; loc w899: invariant xabs <= 4563/100 when xabs = 4563/100 sync b goto w900; loc w900: invariant xabs <= 4564/100 when xabs = 4564/100 sync a goto w901; loc w901: invariant xabs <= 4566/100 when xabs = 4566/100 sync b goto w902; loc w902: invariant xabs <= 4568/100 when xabs = 4568/100 sync a goto w903; loc w903: invariant xabs <= 4570/100 when xabs = 4570/100 sync b goto w904; loc w904: invariant xabs <= 4579/100 when xabs = 4579/100 sync a goto w905; loc w905: invariant xabs <= 4582/100 when xabs = 4582/100 sync b goto w906; loc w906: invariant xabs <= 4587/100 when xabs = 4587/100 sync a goto w907; loc w907: invariant xabs <= 4591/100 when xabs = 4591/100 sync b goto w908; loc w908: invariant xabs <= 4596/100 when xabs = 4596/100 sync a goto w909; loc w909: invariant xabs <= 4601/100 when xabs = 4601/100 sync b goto w910; loc w910: invariant xabs <= 4604/100 when xabs = 4604/100 sync a goto w911; loc w911: invariant xabs <= 4607/100 when xabs = 4607/100 sync b goto w912; loc w912: invariant xabs <= 4610/100 when xabs = 4610/100 sync a goto w913; loc w913: invariant xabs <= 4615/100 when xabs = 4615/100 sync b goto w914; loc w914: invariant xabs <= 4621/100 when xabs = 4621/100 sync a goto w915; loc w915: invariant xabs <= 4624/100 when xabs = 4624/100 sync b goto w916; loc w916: invariant xabs <= 4625/100 when xabs = 4625/100 sync a goto w917; loc w917: invariant xabs <= 4630/100 when xabs = 4630/100 sync b goto w918; loc w918: invariant xabs <= 4639/100 when xabs = 4639/100 sync a goto w919; loc w919: invariant xabs <= 4642/100 when xabs = 4642/100 sync b goto w920; loc w920: invariant xabs <= 4643/100 when xabs = 4643/100 sync a goto w921; loc w921: invariant xabs <= 4648/100 when xabs = 4648/100 sync b goto w922; loc w922: invariant xabs <= 4656/100 when xabs = 4656/100 sync a goto w923; loc w923: invariant xabs <= 4660/100 when xabs = 4660/100 sync b goto w924; loc w924: invariant xabs <= 4666/100 when xabs = 4666/100 sync a goto w925; loc w925: invariant xabs <= 4669/100 when xabs = 4669/100 sync b goto w926; loc w926: invariant xabs <= 4677/100 when xabs = 4677/100 sync a goto w927; loc w927: invariant xabs <= 4678/100 when xabs = 4678/100 sync b goto w928; loc w928: invariant xabs <= 4684/100 when xabs = 4684/100 sync a goto w929; loc w929: invariant xabs <= 4693/100 when xabs = 4693/100 sync b goto w930; loc w930: invariant xabs <= 4695/100 when xabs = 4695/100 sync a goto w931; loc w931: invariant xabs <= 4698/100 when xabs = 4698/100 sync b goto w932; loc w932: invariant xabs <= 4700/100 when xabs = 4700/100 sync a goto w933; loc w933: invariant xabs <= 4704/100 when xabs = 4704/100 sync b goto w934; loc w934: invariant xabs <= 4709/100 when xabs = 4709/100 sync a goto w935; loc w935: invariant xabs <= 4713/100 when xabs = 4713/100 sync b goto w936; loc w936: invariant xabs <= 4721/100 when xabs = 4721/100 sync a goto w937; loc w937: invariant xabs <= 4724/100 when xabs = 4724/100 sync b goto w938; loc w938: invariant xabs <= 4731/100 when xabs = 4731/100 sync a goto w939; loc w939: invariant xabs <= 4735/100 when xabs = 4735/100 sync b goto w940; loc w940: invariant xabs <= 4744/100 when xabs = 4744/100 sync a goto w941; loc w941: invariant xabs <= 4746/100 when xabs = 4746/100 sync b goto w942; loc w942: invariant xabs <= 4751/100 when xabs = 4751/100 sync a goto w943; loc w943: invariant xabs <= 4758/100 when xabs = 4758/100 sync b goto w944; loc w944: invariant xabs <= 4762/100 when xabs = 4762/100 sync a goto w945; loc w945: invariant xabs <= 4764/100 when xabs = 4764/100 sync b goto w946; loc w946: invariant xabs <= 4766/100 when xabs = 4766/100 sync a goto w947; loc w947: invariant xabs <= 4769/100 when xabs = 4769/100 sync b goto w948; loc w948: invariant xabs <= 4777/100 when xabs = 4777/100 sync a goto w949; loc w949: invariant xabs <= 4782/100 when xabs = 4782/100 sync b goto w950; loc w950: invariant xabs <= 4787/100 when xabs = 4787/100 sync a goto w951; loc w951: invariant xabs <= 4789/100 when xabs = 4789/100 sync b goto w952; loc w952: invariant xabs <= 4795/100 when xabs = 4795/100 sync a goto w953; loc w953: invariant xabs <= 4800/100 when xabs = 4800/100 sync b goto w954; loc w954: invariant xabs <= 4801/100 when xabs = 4801/100 sync a goto w955; loc w955: invariant xabs <= 4804/100 when xabs = 4804/100 sync b goto w956; loc w956: invariant xabs <= 4813/100 when xabs = 4813/100 sync a goto w957; loc w957: invariant xabs <= 4816/100 when xabs = 4816/100 sync b goto w958; loc w958: invariant xabs <= 4825/100 when xabs = 4825/100 sync a goto w959; loc w959: invariant xabs <= 4832/100 when xabs = 4832/100 sync b goto w960; loc w960: invariant xabs <= 4837/100 when xabs = 4837/100 sync a goto w961; loc w961: invariant xabs <= 4839/100 when xabs = 4839/100 sync b goto w962; loc w962: invariant xabs <= 4840/100 when xabs = 4840/100 sync a goto w963; loc w963: invariant xabs <= 4846/100 when xabs = 4846/100 sync b goto w964; loc w964: invariant xabs <= 4853/100 when xabs = 4853/100 sync a goto w965; loc w965: invariant xabs <= 4861/100 when xabs = 4861/100 sync b goto w966; loc w966: invariant xabs <= 4867/100 when xabs = 4867/100 sync a goto w967; loc w967: invariant xabs <= 4874/100 when xabs = 4874/100 sync b goto w968; loc w968: invariant xabs <= 4881/100 when xabs = 4881/100 sync a goto w969; loc w969: invariant xabs <= 4888/100 when xabs = 4888/100 sync b goto w970; loc w970: invariant xabs <= 4894/100 when xabs = 4894/100 sync a goto w971; loc w971: invariant xabs <= 4901/100 when xabs = 4901/100 sync b goto w972; loc w972: invariant xabs <= 4907/100 when xabs = 4907/100 sync a goto w973; loc w973: invariant xabs <= 4916/100 when xabs = 4916/100 sync b goto w974; loc w974: invariant xabs <= 4919/100 when xabs = 4919/100 sync a goto w975; loc w975: invariant xabs <= 4923/100 when xabs = 4923/100 sync b goto w976; loc w976: invariant xabs <= 4929/100 when xabs = 4929/100 sync a goto w977; loc w977: invariant xabs <= 4937/100 when xabs = 4937/100 sync b goto w978; loc w978: invariant xabs <= 4943/100 when xabs = 4943/100 sync a goto w979; loc w979: invariant xabs <= 4950/100 when xabs = 4950/100 sync b goto w980; loc w980: invariant xabs <= 4951/100 when xabs = 4951/100 sync a goto w981; loc w981: invariant xabs <= 4957/100 when xabs = 4957/100 sync b goto w982; loc w982: invariant xabs <= 4960/100 when xabs = 4960/100 sync a goto w983; loc w983: invariant xabs <= 4967/100 when xabs = 4967/100 sync b goto w984; loc w984: invariant xabs <= 4973/100 when xabs = 4973/100 sync a goto w985; loc w985: invariant xabs <= 4975/100 when xabs = 4975/100 sync b goto w986; loc w986: invariant xabs <= 4976/100 when xabs = 4976/100 sync a goto w987; loc w987: invariant xabs <= 4977/100 when xabs = 4977/100 sync b goto w988; loc w988: invariant xabs <= 4985/100 when xabs = 4985/100 sync a goto w989; loc w989: invariant xabs <= 4986/100 when xabs = 4986/100 sync b goto w990; loc w990: invariant xabs <= 4994/100 when xabs = 4994/100 sync a goto w991; loc w991: invariant xabs <= 4999/100 when xabs = 4999/100 sync b goto w992; loc w992: invariant xabs <= 5007/100 when xabs = 5007/100 sync a goto w993; loc w993: invariant xabs <= 5012/100 when xabs = 5012/100 sync b goto w994; loc w994: invariant xabs <= 5015/100 when xabs = 5015/100 sync a goto w995; loc w995: invariant xabs <= 5018/100 when xabs = 5018/100 sync b goto w996; loc w996: invariant xabs <= 5021/100 when xabs = 5021/100 sync a goto w997; loc w997: invariant xabs <= 5023/100 when xabs = 5023/100 sync b goto w998; loc w998: invariant xabs <= 5026/100 when xabs = 5026/100 sync a goto w999; loc w999: invariant xabs <= 5029/100 when xabs = 5029/100 sync b goto w1000; (* END AUTOMATICALLY GENERATED *) loc w1000: invariant True end (* word *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = pre_s0 & loc[word] = w0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & y = 0 & xabs = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & p1 >= 0 & p2 >= 0 & p3 >= 0 & t >= 0 & tprime >= 0 ; (************************************************************) (* Property specification *) (************************************************************) property := unreachable loc[pta] = s3; minimize(p1) (************************************************************) (* The end *) (************************************************************) end