(******************************************************************************* * IMITATOR MODEL * * Title : gear-1000 * Description : Parametric timed pattern matching benchmark : gear * Correctness : N/A * Scalable : yes * Generated : yes * Categories : Automotive ; Industrial ; Monitoring * Source : Benchmarks for Temporal Logic Requirements for Automotive Systems (ARCH@CPSWeek 2014) + Masaki Waga / Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018) * bibkey : HAF14 ; AHW18 * Author : The same * Modeling : Étienne André * Input by : Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : 2018/03/30 * Last modified : 2020/08/18 * Model version : * * IMITATOR version : 3 ******************************************************************************) var (* Clocks *) x, xabs : clock; (* Parameters *) p1, t, tprime : parameter; (* MEANING OF THE EVENTS * A: the gear changed to 1 * B: the gear changed to 2 * C: the gear changed to 3 * D: the gear changed to 4 *) (************************************************************) automaton pta (************************************************************) synclabs: A, B, C, D, 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} goto pre_s0_prime; when True sync B do {x := 0} goto pre_s0_prime; when True sync C do {x := 0} goto pre_s0_prime; when True sync D do {x := 0} goto pre_s0_prime; loc pre_s0_prime: invariant True (* Skip some more letter and wait *) when True sync A do {x := 0} goto pre_s0_prime; when True sync B do {x := 0} goto pre_s0_prime; when True sync C do {x := 0} goto pre_s0_prime; when True sync D do {x := 0} goto pre_s0_prime; (* Or decide to start the pattern *) when t = xabs & x > 0 do {x := 0} sync start goto s0; loc s0: invariant True when True sync A do {x := 0} goto s1; loc s1: invariant True (*** NOTE: equality is more interesting than inequality here :-) ***) when x = p1 sync B goto s2; loc s2: invariant True when tprime = xabs sync dollar do {x := 0} goto s_soon_end; loc s_soon_end: invariant True when x > 0 goto s_end; (* urgent to avoid time elapsing *) urgent loc s_end: invariant True end (* pta *) (************************************************************) automaton word (************************************************************) synclabs: A, B, C, D; loc w1: invariant xabs <= 2.32 when xabs = 2.32 sync A goto w2; loc w2: invariant xabs <= 4.52 when xabs = 4.52 sync B goto w3; loc w3: invariant xabs <= 9.72 when xabs = 9.72 sync C goto w4; loc w4: invariant xabs <= 18.28 when xabs = 18.28 sync D goto w5; loc w5: invariant xabs <= 18.4 when xabs = 18.4 sync C goto w6; loc w6: invariant xabs <= 18.52 when xabs = 18.52 sync B goto w7; loc w7: invariant xabs <= 21.6 when xabs = 21.6 sync A goto w8; loc w8: invariant xabs <= 23.12 when xabs = 23.12 sync B goto w9; loc w9: invariant xabs <= 27.08 when xabs = 27.08 sync C goto w10; loc w10: invariant xabs <= 38.32 when xabs = 38.32 sync D goto w11; loc w11: invariant xabs <= 38.44 when xabs = 38.44 sync C goto w12; loc w12: invariant xabs <= 38.56 when xabs = 38.56 sync B goto w13; loc w13: invariant xabs <= 41.12 when xabs = 41.12 sync A goto w14; loc w14: invariant xabs <= 42.48 when xabs = 42.48 sync B goto w15; loc w15: invariant xabs <= 45.32 when xabs = 45.32 sync C goto w16; loc w16: invariant xabs <= 58.32 when xabs = 58.32 sync D goto w17; loc w17: invariant xabs <= 58.44 when xabs = 58.44 sync C goto w18; loc w18: invariant xabs <= 58.56 when xabs = 58.56 sync B goto w19; loc w19: invariant xabs <= 61.32 when xabs = 61.32 sync A goto w20; loc w20: invariant xabs <= 63.24 when xabs = 63.24 sync B goto w21; loc w21: invariant xabs <= 66.08 when xabs = 66.08 sync C goto w22; loc w22: invariant xabs <= 78.28 when xabs = 78.28 sync D goto w23; loc w23: invariant xabs <= 78.4 when xabs = 78.4 sync C goto w24; loc w24: invariant xabs <= 78.52 when xabs = 78.52 sync B goto w25; loc w25: invariant xabs <= 82 when xabs = 82 sync A goto w26; loc w26: invariant xabs <= 83 when xabs = 83 sync B goto w27; loc w27: invariant xabs <= 83.48 when xabs = 83.48 sync C goto w28; loc w28: invariant xabs <= 83.6 when xabs = 83.6 sync D goto w29; loc w29: invariant xabs <= 85.44 when xabs = 85.44 sync C goto w30; loc w30: invariant xabs <= 85.56 when xabs = 85.56 sync D goto w31; loc w31: invariant xabs <= 85.92 when xabs = 85.92 sync C goto w32; loc w32: invariant xabs <= 86.08 when xabs = 86.08 sync D goto w33; loc w33: invariant xabs <= 86.4 when xabs = 86.4 sync C goto w34; loc w34: invariant xabs <= 98.2 when xabs = 98.2 sync D goto w35; loc w35: invariant xabs <= 98.32 when xabs = 98.32 sync C goto w36; loc w36: invariant xabs <= 98.44 when xabs = 98.44 sync B goto w37; loc w37: invariant xabs <= 101.84 when xabs = 101.84 sync A goto w38; loc w38: invariant xabs <= 104.68 when xabs = 104.68 sync B goto w39; loc w39: invariant xabs <= 104.8 when xabs = 104.8 sync C goto w40; loc w40: invariant xabs <= 105.96 when xabs = 105.96 sync D goto w41; loc w41: invariant xabs <= 107.68 when xabs = 107.68 sync C goto w42; loc w42: invariant xabs <= 109.4 when xabs = 109.4 sync D goto w43; loc w43: invariant xabs <= 110.56 when xabs = 110.56 sync C goto w44; loc w44: invariant xabs <= 112.88 when xabs = 112.88 sync D goto w45; loc w45: invariant xabs <= 113.48 when xabs = 113.48 sync C goto w46; loc w46: invariant xabs <= 118.16 when xabs = 118.16 sync D goto w47; loc w47: invariant xabs <= 118.28 when xabs = 118.28 sync C goto w48; loc w48: invariant xabs <= 118.44 when xabs = 118.44 sync B goto w49; loc w49: invariant xabs <= 122.6 when xabs = 122.6 sync A goto w50; loc w50: invariant xabs <= 122.84 when xabs = 122.84 sync B goto w51; loc w51: invariant xabs <= 123.08 when xabs = 123.08 sync A goto w52; loc w52: invariant xabs <= 123.36 when xabs = 123.36 sync B goto w53; loc w53: invariant xabs <= 123.52 when xabs = 123.52 sync A goto w54; loc w54: invariant xabs <= 123.88 when xabs = 123.88 sync B goto w55; loc w55: invariant xabs <= 124 when xabs = 124 sync A goto w56; loc w56: invariant xabs <= 124.36 when xabs = 124.36 sync B goto w57; loc w57: invariant xabs <= 124.52 when xabs = 124.52 sync A goto w58; loc w58: invariant xabs <= 124.84 when xabs = 124.84 sync B goto w59; loc w59: invariant xabs <= 125 when xabs = 125 sync A goto w60; loc w60: invariant xabs <= 125.32 when xabs = 125.32 sync B goto w61; loc w61: invariant xabs <= 125.52 when xabs = 125.52 sync A goto w62; loc w62: invariant xabs <= 125.8 when xabs = 125.8 sync B goto w63; loc w63: invariant xabs <= 126 when xabs = 126 sync A goto w64; loc w64: invariant xabs <= 126.32 when xabs = 126.32 sync B goto w65; loc w65: invariant xabs <= 126.48 when xabs = 126.48 sync A goto w66; loc w66: invariant xabs <= 126.8 when xabs = 126.8 sync B goto w67; loc w67: invariant xabs <= 126.96 when xabs = 126.96 sync A goto w68; loc w68: invariant xabs <= 127.32 when xabs = 127.32 sync B goto w69; loc w69: invariant xabs <= 127.44 when xabs = 127.44 sync A goto w70; loc w70: invariant xabs <= 127.8 when xabs = 127.8 sync B goto w71; loc w71: invariant xabs <= 127.96 when xabs = 127.96 sync A goto w72; loc w72: invariant xabs <= 128.24 when xabs = 128.24 sync B goto w73; loc w73: invariant xabs <= 128.44 when xabs = 128.44 sync A goto w74; loc w74: invariant xabs <= 128.72 when xabs = 128.72 sync B goto w75; loc w75: invariant xabs <= 128.92 when xabs = 128.92 sync A goto w76; loc w76: invariant xabs <= 129.24 when xabs = 129.24 sync B goto w77; loc w77: invariant xabs <= 129.4 when xabs = 129.4 sync A goto w78; loc w78: invariant xabs <= 129.76 when xabs = 129.76 sync B goto w79; loc w79: invariant xabs <= 129.88 when xabs = 129.88 sync A goto w80; loc w80: invariant xabs <= 130.24 when xabs = 130.24 sync B goto w81; loc w81: invariant xabs <= 130.36 when xabs = 130.36 sync A goto w82; loc w82: invariant xabs <= 130.72 when xabs = 130.72 sync B goto w83; loc w83: invariant xabs <= 130.88 when xabs = 130.88 sync A goto w84; loc w84: invariant xabs <= 131.2 when xabs = 131.2 sync B goto w85; loc w85: invariant xabs <= 131.36 when xabs = 131.36 sync A goto w86; loc w86: invariant xabs <= 131.68 when xabs = 131.68 sync B goto w87; loc w87: invariant xabs <= 131.88 when xabs = 131.88 sync A goto w88; loc w88: invariant xabs <= 132.16 when xabs = 132.16 sync B goto w89; loc w89: invariant xabs <= 132.36 when xabs = 132.36 sync A goto w90; loc w90: invariant xabs <= 132.68 when xabs = 132.68 sync B goto w91; loc w91: invariant xabs <= 132.84 when xabs = 132.84 sync A goto w92; loc w92: invariant xabs <= 133.68 when xabs = 133.68 sync B goto w93; loc w93: invariant xabs <= 134.32 when xabs = 134.32 sync A goto w94; loc w94: invariant xabs <= 134.64 when xabs = 134.64 sync B goto w95; loc w95: invariant xabs <= 134.8 when xabs = 134.8 sync A goto w96; loc w96: invariant xabs <= 135.12 when xabs = 135.12 sync B goto w97; loc w97: invariant xabs <= 135.32 when xabs = 135.32 sync A goto w98; loc w98: invariant xabs <= 135.6 when xabs = 135.6 sync B goto w99; loc w99: invariant xabs <= 135.8 when xabs = 135.8 sync A goto w100; loc w100: invariant xabs <= 136.12 when xabs = 136.12 sync B goto w101; loc w101: invariant xabs <= 136.28 when xabs = 136.28 sync A goto w102; loc w102: invariant xabs <= 137.56 when xabs = 137.56 sync B goto w103; loc w103: invariant xabs <= 141.68 when xabs = 141.68 sync A goto w104; loc w104: invariant xabs <= 142 when xabs = 142 sync B goto w105; loc w105: invariant xabs <= 142.12 when xabs = 142.12 sync A goto w106; loc w106: invariant xabs <= 142.48 when xabs = 142.48 sync B goto w107; loc w107: invariant xabs <= 142.6 when xabs = 142.6 sync A goto w108; loc w108: invariant xabs <= 143.44 when xabs = 143.44 sync B goto w109; loc w109: invariant xabs <= 144.16 when xabs = 144.16 sync A goto w110; loc w110: invariant xabs <= 144.4 when xabs = 144.4 sync B goto w111; loc w111: invariant xabs <= 148.04 when xabs = 148.04 sync A goto w112; loc w112: invariant xabs <= 148.36 when xabs = 148.36 sync B goto w113; loc w113: invariant xabs <= 148.52 when xabs = 148.52 sync A goto w114; loc w114: invariant xabs <= 148.84 when xabs = 148.84 sync B goto w115; loc w115: invariant xabs <= 149 when xabs = 149 sync A goto w116; loc w116: invariant xabs <= 149.36 when xabs = 149.36 sync B goto w117; loc w117: invariant xabs <= 149.48 when xabs = 149.48 sync A goto w118; loc w118: invariant xabs <= 149.84 when xabs = 149.84 sync B goto w119; loc w119: invariant xabs <= 149.96 when xabs = 149.96 sync A goto w120; loc w120: invariant xabs <= 150.32 when xabs = 150.32 sync B goto w121; loc w121: invariant xabs <= 150.48 when xabs = 150.48 sync A goto w122; loc w122: invariant xabs <= 150.8 when xabs = 150.8 sync B goto w123; loc w123: invariant xabs <= 150.96 when xabs = 150.96 sync A goto w124; loc w124: invariant xabs <= 151.28 when xabs = 151.28 sync B goto w125; loc w125: invariant xabs <= 151.44 when xabs = 151.44 sync A goto w126; loc w126: invariant xabs <= 151.8 when xabs = 151.8 sync B goto w127; loc w127: invariant xabs <= 153.92 when xabs = 153.92 sync A goto w128; loc w128: invariant xabs <= 154.2 when xabs = 154.2 sync B goto w129; loc w129: invariant xabs <= 154.4 when xabs = 154.4 sync A goto w130; loc w130: invariant xabs <= 154.72 when xabs = 154.72 sync B goto w131; loc w131: invariant xabs <= 154.88 when xabs = 154.88 sync A goto w132; loc w132: invariant xabs <= 155.2 when xabs = 155.2 sync B goto w133; loc w133: invariant xabs <= 155.36 when xabs = 155.36 sync A goto w134; loc w134: invariant xabs <= 155.72 when xabs = 155.72 sync B goto w135; loc w135: invariant xabs <= 155.84 when xabs = 155.84 sync A goto w136; loc w136: invariant xabs <= 156.2 when xabs = 156.2 sync B goto w137; loc w137: invariant xabs <= 156.36 when xabs = 156.36 sync A goto w138; loc w138: invariant xabs <= 156.64 when xabs = 156.64 sync B goto w139; loc w139: invariant xabs <= 156.84 when xabs = 156.84 sync A goto w140; loc w140: invariant xabs <= 157.12 when xabs = 157.12 sync B goto w141; loc w141: invariant xabs <= 157.36 when xabs = 157.36 sync A goto w142; loc w142: invariant xabs <= 157.64 when xabs = 157.64 sync B goto w143; loc w143: invariant xabs <= 157.84 when xabs = 157.84 sync A goto w144; loc w144: invariant xabs <= 158.24 when xabs = 158.24 sync B goto w145; loc w145: invariant xabs <= 161.24 when xabs = 161.24 sync A goto w146; loc w146: invariant xabs <= 161.56 when xabs = 161.56 sync B goto w147; loc w147: invariant xabs <= 161.72 when xabs = 161.72 sync A goto w148; loc w148: invariant xabs <= 162.04 when xabs = 162.04 sync B goto w149; loc w149: invariant xabs <= 162.2 when xabs = 162.2 sync A goto w150; loc w150: invariant xabs <= 162.52 when xabs = 162.52 sync B goto w151; loc w151: invariant xabs <= 162.72 when xabs = 162.72 sync A goto w152; loc w152: invariant xabs <= 163 when xabs = 163 sync B goto w153; loc w153: invariant xabs <= 163.24 when xabs = 163.24 sync A goto w154; loc w154: invariant xabs <= 163.48 when xabs = 163.48 sync B goto w155; loc w155: invariant xabs <= 163.72 when xabs = 163.72 sync A goto w156; loc w156: invariant xabs <= 164 when xabs = 164 sync B goto w157; loc w157: invariant xabs <= 164.2 when xabs = 164.2 sync A goto w158; loc w158: invariant xabs <= 164.48 when xabs = 164.48 sync B goto w159; loc w159: invariant xabs <= 164.68 when xabs = 164.68 sync A goto w160; loc w160: invariant xabs <= 165 when xabs = 165 sync B goto w161; loc w161: invariant xabs <= 165.16 when xabs = 165.16 sync A goto w162; loc w162: invariant xabs <= 165.48 when xabs = 165.48 sync B goto w163; loc w163: invariant xabs <= 165.68 when xabs = 165.68 sync A goto w164; loc w164: invariant xabs <= 165.96 when xabs = 165.96 sync B goto w165; loc w165: invariant xabs <= 166.16 when xabs = 166.16 sync A goto w166; loc w166: invariant xabs <= 166.44 when xabs = 166.44 sync B goto w167; loc w167: invariant xabs <= 166.68 when xabs = 166.68 sync A goto w168; loc w168: invariant xabs <= 166.92 when xabs = 166.92 sync B goto w169; loc w169: invariant xabs <= 167.16 when xabs = 167.16 sync A goto w170; loc w170: invariant xabs <= 167.44 when xabs = 167.44 sync B goto w171; loc w171: invariant xabs <= 167.6 when xabs = 167.6 sync A goto w172; loc w172: invariant xabs <= 167.92 when xabs = 167.92 sync B goto w173; loc w173: invariant xabs <= 168.12 when xabs = 168.12 sync A goto w174; loc w174: invariant xabs <= 168.4 when xabs = 168.4 sync B goto w175; loc w175: invariant xabs <= 168.6 when xabs = 168.6 sync A goto w176; loc w176: invariant xabs <= 168.88 when xabs = 168.88 sync B goto w177; loc w177: invariant xabs <= 169.12 when xabs = 169.12 sync A goto w178; loc w178: invariant xabs <= 169.36 when xabs = 169.36 sync B goto w179; loc w179: invariant xabs <= 169.6 when xabs = 169.6 sync A goto w180; loc w180: invariant xabs <= 169.84 when xabs = 169.84 sync B goto w181; loc w181: invariant xabs <= 170.08 when xabs = 170.08 sync A goto w182; loc w182: invariant xabs <= 170.36 when xabs = 170.36 sync B goto w183; loc w183: invariant xabs <= 170.56 when xabs = 170.56 sync A goto w184; loc w184: invariant xabs <= 170.84 when xabs = 170.84 sync B goto w185; loc w185: invariant xabs <= 171.04 when xabs = 171.04 sync A goto w186; loc w186: invariant xabs <= 171.36 when xabs = 171.36 sync B goto w187; loc w187: invariant xabs <= 171.52 when xabs = 171.52 sync A goto w188; loc w188: invariant xabs <= 171.84 when xabs = 171.84 sync B goto w189; loc w189: invariant xabs <= 172.04 when xabs = 172.04 sync A goto w190; loc w190: invariant xabs <= 172.32 when xabs = 172.32 sync B goto w191; loc w191: invariant xabs <= 172.56 when xabs = 172.56 sync A goto w192; loc w192: invariant xabs <= 173.04 when xabs = 173.04 sync B goto w193; loc w193: invariant xabs <= 173.28 when xabs = 173.28 sync C goto w194; loc w194: invariant xabs <= 173.52 when xabs = 173.52 sync B goto w195; loc w195: invariant xabs <= 173.76 when xabs = 173.76 sync C goto w196; loc w196: invariant xabs <= 174 when xabs = 174 sync B goto w197; loc w197: invariant xabs <= 174.28 when xabs = 174.28 sync C goto w198; loc w198: invariant xabs <= 174.48 when xabs = 174.48 sync B goto w199; loc w199: invariant xabs <= 174.76 when xabs = 174.76 sync C goto w200; loc w200: invariant xabs <= 175 when xabs = 175 sync B goto w201; loc w201: invariant xabs <= 175.24 when xabs = 175.24 sync C goto w202; loc w202: invariant xabs <= 175.48 when xabs = 175.48 sync B goto w203; loc w203: invariant xabs <= 175.72 when xabs = 175.72 sync C goto w204; loc w204: invariant xabs <= 176 when xabs = 176 sync B goto w205; loc w205: invariant xabs <= 176.2 when xabs = 176.2 sync C goto w206; loc w206: invariant xabs <= 176.48 when xabs = 176.48 sync B goto w207; loc w207: invariant xabs <= 176.68 when xabs = 176.68 sync C goto w208; loc w208: invariant xabs <= 176.96 when xabs = 176.96 sync B goto w209; loc w209: invariant xabs <= 177.2 when xabs = 177.2 sync C goto w210; loc w210: invariant xabs <= 177.44 when xabs = 177.44 sync B goto w211; loc w211: invariant xabs <= 177.68 when xabs = 177.68 sync C goto w212; loc w212: invariant xabs <= 177.92 when xabs = 177.92 sync B goto w213; loc w213: invariant xabs <= 178.12 when xabs = 178.12 sync C goto w214; loc w214: invariant xabs <= 178.24 when xabs = 178.24 sync B goto w215; loc w215: invariant xabs <= 181.36 when xabs = 181.36 sync A goto w216; loc w216: invariant xabs <= 181.6 when xabs = 181.6 sync B goto w217; loc w217: invariant xabs <= 181.88 when xabs = 181.88 sync A goto w218; loc w218: invariant xabs <= 182.08 when xabs = 182.08 sync B goto w219; loc w219: invariant xabs <= 182.36 when xabs = 182.36 sync A goto w220; loc w220: invariant xabs <= 182.56 when xabs = 182.56 sync B goto w221; loc w221: invariant xabs <= 182.84 when xabs = 182.84 sync A goto w222; loc w222: invariant xabs <= 183.04 when xabs = 183.04 sync B goto w223; loc w223: invariant xabs <= 183.32 when xabs = 183.32 sync A goto w224; loc w224: invariant xabs <= 183.56 when xabs = 183.56 sync B goto w225; loc w225: invariant xabs <= 183.8 when xabs = 183.8 sync A goto w226; loc w226: invariant xabs <= 184.04 when xabs = 184.04 sync B goto w227; loc w227: invariant xabs <= 184.32 when xabs = 184.32 sync A goto w228; loc w228: invariant xabs <= 184.52 when xabs = 184.52 sync B goto w229; loc w229: invariant xabs <= 184.8 when xabs = 184.8 sync A goto w230; loc w230: invariant xabs <= 185 when xabs = 185 sync B goto w231; loc w231: invariant xabs <= 185.32 when xabs = 185.32 sync A goto w232; loc w232: invariant xabs <= 185.8 when xabs = 185.8 sync B goto w233; loc w233: invariant xabs <= 185.96 when xabs = 185.96 sync C goto w234; loc w234: invariant xabs <= 186.28 when xabs = 186.28 sync B goto w235; loc w235: invariant xabs <= 186.48 when xabs = 186.48 sync C goto w236; loc w236: invariant xabs <= 186.76 when xabs = 186.76 sync B goto w237; loc w237: invariant xabs <= 186.96 when xabs = 186.96 sync C goto w238; loc w238: invariant xabs <= 187.24 when xabs = 187.24 sync B goto w239; loc w239: invariant xabs <= 187.44 when xabs = 187.44 sync C goto w240; loc w240: invariant xabs <= 187.76 when xabs = 187.76 sync B goto w241; loc w241: invariant xabs <= 187.92 when xabs = 187.92 sync C goto w242; loc w242: invariant xabs <= 188.24 when xabs = 188.24 sync B goto w243; loc w243: invariant xabs <= 188.4 when xabs = 188.4 sync C goto w244; loc w244: invariant xabs <= 188.76 when xabs = 188.76 sync B goto w245; loc w245: invariant xabs <= 188.88 when xabs = 188.88 sync C goto w246; loc w246: invariant xabs <= 189.24 when xabs = 189.24 sync B goto w247; loc w247: invariant xabs <= 189.44 when xabs = 189.44 sync C goto w248; loc w248: invariant xabs <= 189.72 when xabs = 189.72 sync B goto w249; loc w249: invariant xabs <= 190.2 when xabs = 190.2 sync C goto w250; loc w250: invariant xabs <= 190.4 when xabs = 190.4 sync D goto w251; loc w251: invariant xabs <= 190.72 when xabs = 190.72 sync C goto w252; loc w252: invariant xabs <= 190.88 when xabs = 190.88 sync D goto w253; loc w253: invariant xabs <= 191.2 when xabs = 191.2 sync C goto w254; loc w254: invariant xabs <= 191.32 when xabs = 191.32 sync D goto w255; loc w255: invariant xabs <= 192.2 when xabs = 192.2 sync C goto w256; loc w256: invariant xabs <= 192.32 when xabs = 192.32 sync D goto w257; loc w257: invariant xabs <= 192.64 when xabs = 192.64 sync C goto w258; loc w258: invariant xabs <= 192.84 when xabs = 192.84 sync D goto w259; loc w259: invariant xabs <= 193.12 when xabs = 193.12 sync C goto w260; loc w260: invariant xabs <= 193.32 when xabs = 193.32 sync D goto w261; loc w261: invariant xabs <= 193.64 when xabs = 193.64 sync C goto w262; loc w262: invariant xabs <= 193.8 when xabs = 193.8 sync D goto w263; loc w263: invariant xabs <= 194.12 when xabs = 194.12 sync C goto w264; loc w264: invariant xabs <= 194.28 when xabs = 194.28 sync D goto w265; loc w265: invariant xabs <= 195.12 when xabs = 195.12 sync C goto w266; loc w266: invariant xabs <= 195.24 when xabs = 195.24 sync D goto w267; loc w267: invariant xabs <= 195.6 when xabs = 195.6 sync C goto w268; loc w268: invariant xabs <= 195.76 when xabs = 195.76 sync D goto w269; loc w269: invariant xabs <= 196.08 when xabs = 196.08 sync C goto w270; loc w270: invariant xabs <= 196.24 when xabs = 196.24 sync D goto w271; loc w271: invariant xabs <= 196.56 when xabs = 196.56 sync C goto w272; loc w272: invariant xabs <= 196.72 when xabs = 196.72 sync D goto w273; loc w273: invariant xabs <= 197.08 when xabs = 197.08 sync C goto w274; loc w274: invariant xabs <= 197.2 when xabs = 197.2 sync D goto w275; loc w275: invariant xabs <= 198.24 when xabs = 198.24 sync C goto w276; loc w276: invariant xabs <= 198.36 when xabs = 198.36 sync B goto w277; loc w277: invariant xabs <= 201.68 when xabs = 201.68 sync A goto w278; loc w278: invariant xabs <= 203.96 when xabs = 203.96 sync B goto w279; loc w279: invariant xabs <= 207.68 when xabs = 207.68 sync C goto w280; loc w280: invariant xabs <= 218.32 when xabs = 218.32 sync D goto w281; loc w281: invariant xabs <= 218.44 when xabs = 218.44 sync C goto w282; loc w282: invariant xabs <= 218.56 when xabs = 218.56 sync B goto w283; loc w283: invariant xabs <= 221.36 when xabs = 221.36 sync A goto w284; loc w284: invariant xabs <= 222.88 when xabs = 222.88 sync B goto w285; loc w285: invariant xabs <= 225.36 when xabs = 225.36 sync C goto w286; loc w286: invariant xabs <= 238.32 when xabs = 238.32 sync D goto w287; loc w287: invariant xabs <= 238.44 when xabs = 238.44 sync C goto w288; loc w288: invariant xabs <= 238.56 when xabs = 238.56 sync B goto w289; loc w289: invariant xabs <= 241.2 when xabs = 241.2 sync A goto w290; loc w290: invariant xabs <= 242.4 when xabs = 242.4 sync B goto w291; loc w291: invariant xabs <= 245.32 when xabs = 245.32 sync C goto w292; loc w292: invariant xabs <= 258.32 when xabs = 258.32 sync D goto w293; loc w293: invariant xabs <= 258.44 when xabs = 258.44 sync C goto w294; loc w294: invariant xabs <= 258.56 when xabs = 258.56 sync B goto w295; loc w295: invariant xabs <= 261.2 when xabs = 261.2 sync A goto w296; loc w296: invariant xabs <= 263.44 when xabs = 263.44 sync B goto w297; loc w297: invariant xabs <= 265.16 when xabs = 265.16 sync C goto w298; loc w298: invariant xabs <= 278.24 when xabs = 278.24 sync D goto w299; loc w299: invariant xabs <= 278.36 when xabs = 278.36 sync C goto w300; loc w300: invariant xabs <= 278.48 when xabs = 278.48 sync B goto w301; loc w301: invariant xabs <= 281.28 when xabs = 281.28 sync A goto w302; loc w302: invariant xabs <= 281.48 when xabs = 281.48 sync B goto w303; loc w303: invariant xabs <= 281.76 when xabs = 281.76 sync A goto w304; loc w304: invariant xabs <= 281.96 when xabs = 281.96 sync B goto w305; loc w305: invariant xabs <= 282.28 when xabs = 282.28 sync A goto w306; loc w306: invariant xabs <= 282.4 when xabs = 282.4 sync B goto w307; loc w307: invariant xabs <= 282.76 when xabs = 282.76 sync A goto w308; loc w308: invariant xabs <= 282.92 when xabs = 282.92 sync B goto w309; loc w309: invariant xabs <= 283.24 when xabs = 283.24 sync A goto w310; loc w310: invariant xabs <= 283.4 when xabs = 283.4 sync B goto w311; loc w311: invariant xabs <= 283.72 when xabs = 283.72 sync A goto w312; loc w312: invariant xabs <= 283.92 when xabs = 283.92 sync B goto w313; loc w313: invariant xabs <= 284.2 when xabs = 284.2 sync A goto w314; loc w314: invariant xabs <= 284.68 when xabs = 284.68 sync B goto w315; loc w315: invariant xabs <= 284.88 when xabs = 284.88 sync C goto w316; loc w316: invariant xabs <= 285.2 when xabs = 285.2 sync B goto w317; loc w317: invariant xabs <= 285.36 when xabs = 285.36 sync C goto w318; loc w318: invariant xabs <= 285.72 when xabs = 285.72 sync B goto w319; loc w319: invariant xabs <= 285.88 when xabs = 285.88 sync C goto w320; loc w320: invariant xabs <= 286.2 when xabs = 286.2 sync B goto w321; loc w321: invariant xabs <= 286.36 when xabs = 286.36 sync C goto w322; loc w322: invariant xabs <= 286.64 when xabs = 286.64 sync B goto w323; loc w323: invariant xabs <= 286.88 when xabs = 286.88 sync C goto w324; loc w324: invariant xabs <= 287.12 when xabs = 287.12 sync B goto w325; loc w325: invariant xabs <= 287.36 when xabs = 287.36 sync C goto w326; loc w326: invariant xabs <= 287.6 when xabs = 287.6 sync B goto w327; loc w327: invariant xabs <= 287.84 when xabs = 287.84 sync C goto w328; loc w328: invariant xabs <= 288.12 when xabs = 288.12 sync B goto w329; loc w329: invariant xabs <= 288.64 when xabs = 288.64 sync C goto w330; loc w330: invariant xabs <= 288.8 when xabs = 288.8 sync D goto w331; loc w331: invariant xabs <= 288.92 when xabs = 288.92 sync C goto w332; loc w332: invariant xabs <= 289.12 when xabs = 289.12 sync B goto w333; loc w333: invariant xabs <= 289.28 when xabs = 289.28 sync C goto w334; loc w334: invariant xabs <= 289.6 when xabs = 289.6 sync B goto w335; loc w335: invariant xabs <= 290.08 when xabs = 290.08 sync C goto w336; loc w336: invariant xabs <= 290.32 when xabs = 290.32 sync D goto w337; loc w337: invariant xabs <= 290.56 when xabs = 290.56 sync C goto w338; loc w338: invariant xabs <= 290.8 when xabs = 290.8 sync D goto w339; loc w339: invariant xabs <= 291.04 when xabs = 291.04 sync C goto w340; loc w340: invariant xabs <= 291.28 when xabs = 291.28 sync D goto w341; loc w341: invariant xabs <= 291.56 when xabs = 291.56 sync C goto w342; loc w342: invariant xabs <= 291.76 when xabs = 291.76 sync D goto w343; loc w343: invariant xabs <= 292.04 when xabs = 292.04 sync C goto w344; loc w344: invariant xabs <= 292.24 when xabs = 292.24 sync D goto w345; loc w345: invariant xabs <= 292.52 when xabs = 292.52 sync C goto w346; loc w346: invariant xabs <= 292.72 when xabs = 292.72 sync D goto w347; loc w347: invariant xabs <= 293 when xabs = 293 sync C goto w348; loc w348: invariant xabs <= 293.24 when xabs = 293.24 sync D goto w349; loc w349: invariant xabs <= 293.48 when xabs = 293.48 sync C goto w350; loc w350: invariant xabs <= 293.72 when xabs = 293.72 sync D goto w351; loc w351: invariant xabs <= 293.96 when xabs = 293.96 sync C goto w352; loc w352: invariant xabs <= 294.24 when xabs = 294.24 sync D goto w353; loc w353: invariant xabs <= 294.48 when xabs = 294.48 sync C goto w354; loc w354: invariant xabs <= 294.72 when xabs = 294.72 sync D goto w355; loc w355: invariant xabs <= 294.96 when xabs = 294.96 sync C goto w356; loc w356: invariant xabs <= 295.2 when xabs = 295.2 sync D goto w357; loc w357: invariant xabs <= 295.48 when xabs = 295.48 sync C goto w358; loc w358: invariant xabs <= 295.68 when xabs = 295.68 sync D goto w359; loc w359: invariant xabs <= 295.96 when xabs = 295.96 sync C goto w360; loc w360: invariant xabs <= 296.2 when xabs = 296.2 sync D goto w361; loc w361: invariant xabs <= 296.4 when xabs = 296.4 sync C goto w362; loc w362: invariant xabs <= 296.68 when xabs = 296.68 sync D goto w363; loc w363: invariant xabs <= 296.88 when xabs = 296.88 sync C goto w364; loc w364: invariant xabs <= 297.16 when xabs = 297.16 sync D goto w365; loc w365: invariant xabs <= 297.4 when xabs = 297.4 sync C goto w366; loc w366: invariant xabs <= 297.64 when xabs = 297.64 sync D goto w367; loc w367: invariant xabs <= 297.88 when xabs = 297.88 sync C goto w368; loc w368: invariant xabs <= 298.16 when xabs = 298.16 sync D goto w369; loc w369: invariant xabs <= 298.28 when xabs = 298.28 sync C goto w370; loc w370: invariant xabs <= 298.4 when xabs = 298.4 sync B goto w371; loc w371: invariant xabs <= 302.08 when xabs = 302.08 sync A goto w372; loc w372: invariant xabs <= 313.52 when xabs = 313.52 sync B goto w373; loc w373: invariant xabs <= 323.84 when xabs = 323.84 sync A goto w374; loc w374: invariant xabs <= 324.12 when xabs = 324.12 sync B goto w375; loc w375: invariant xabs <= 324.28 when xabs = 324.28 sync A goto w376; loc w376: invariant xabs <= 324.64 when xabs = 324.64 sync B goto w377; loc w377: invariant xabs <= 324.76 when xabs = 324.76 sync A goto w378; loc w378: invariant xabs <= 325.12 when xabs = 325.12 sync B goto w379; loc w379: invariant xabs <= 325.28 when xabs = 325.28 sync A goto w380; loc w380: invariant xabs <= 325.64 when xabs = 325.64 sync B goto w381; loc w381: invariant xabs <= 330.2 when xabs = 330.2 sync A goto w382; loc w382: invariant xabs <= 330.52 when xabs = 330.52 sync B goto w383; loc w383: invariant xabs <= 330.68 when xabs = 330.68 sync A goto w384; loc w384: invariant xabs <= 331 when xabs = 331 sync B goto w385; loc w385: invariant xabs <= 331.12 when xabs = 331.12 sync A goto w386; loc w386: invariant xabs <= 332 when xabs = 332 sync B goto w387; loc w387: invariant xabs <= 336.6 when xabs = 336.6 sync A goto w388; loc w388: invariant xabs <= 336.84 when xabs = 336.84 sync B goto w389; loc w389: invariant xabs <= 337 when xabs = 337 sync A goto w390; loc w390: invariant xabs <= 337.36 when xabs = 337.36 sync B goto w391; loc w391: invariant xabs <= 337.48 when xabs = 337.48 sync A goto w392; loc w392: invariant xabs <= 337.84 when xabs = 337.84 sync B goto w393; loc w393: invariant xabs <= 342.48 when xabs = 342.48 sync A goto w394; loc w394: invariant xabs <= 342.72 when xabs = 342.72 sync B goto w395; loc w395: invariant xabs <= 342.92 when xabs = 342.92 sync A goto w396; loc w396: invariant xabs <= 343.24 when xabs = 343.24 sync B goto w397; loc w397: invariant xabs <= 343.4 when xabs = 343.4 sync A goto w398; loc w398: invariant xabs <= 343.72 when xabs = 343.72 sync B goto w399; loc w399: invariant xabs <= 343.88 when xabs = 343.88 sync A goto w400; loc w400: invariant xabs <= 344.24 when xabs = 344.24 sync B goto w401; loc w401: invariant xabs <= 344.36 when xabs = 344.36 sync A goto w402; loc w402: invariant xabs <= 344.72 when xabs = 344.72 sync B goto w403; loc w403: invariant xabs <= 344.88 when xabs = 344.88 sync A goto w404; loc w404: invariant xabs <= 345.16 when xabs = 345.16 sync B goto w405; loc w405: invariant xabs <= 345.36 when xabs = 345.36 sync A goto w406; loc w406: invariant xabs <= 345.64 when xabs = 345.64 sync B goto w407; loc w407: invariant xabs <= 345.88 when xabs = 345.88 sync A goto w408; loc w408: invariant xabs <= 346.16 when xabs = 346.16 sync B goto w409; loc w409: invariant xabs <= 346.32 when xabs = 346.32 sync A goto w410; loc w410: invariant xabs <= 346.64 when xabs = 346.64 sync B goto w411; loc w411: invariant xabs <= 346.8 when xabs = 346.8 sync A goto w412; loc w412: invariant xabs <= 347.16 when xabs = 347.16 sync B goto w413; loc w413: invariant xabs <= 347.28 when xabs = 347.28 sync A goto w414; loc w414: invariant xabs <= 347.64 when xabs = 347.64 sync B goto w415; loc w415: invariant xabs <= 347.8 when xabs = 347.8 sync A goto w416; loc w416: invariant xabs <= 348.12 when xabs = 348.12 sync B goto w417; loc w417: invariant xabs <= 348.32 when xabs = 348.32 sync A goto w418; loc w418: invariant xabs <= 348.6 when xabs = 348.6 sync B goto w419; loc w419: invariant xabs <= 348.8 when xabs = 348.8 sync A goto w420; loc w420: invariant xabs <= 349.08 when xabs = 349.08 sync B goto w421; loc w421: invariant xabs <= 349.28 when xabs = 349.28 sync A goto w422; loc w422: invariant xabs <= 349.6 when xabs = 349.6 sync B goto w423; loc w423: invariant xabs <= 349.76 when xabs = 349.76 sync A goto w424; loc w424: invariant xabs <= 350.08 when xabs = 350.08 sync B goto w425; loc w425: invariant xabs <= 350.24 when xabs = 350.24 sync A goto w426; loc w426: invariant xabs <= 350.6 when xabs = 350.6 sync B goto w427; loc w427: invariant xabs <= 350.72 when xabs = 350.72 sync A goto w428; loc w428: invariant xabs <= 351.04 when xabs = 351.04 sync B goto w429; loc w429: invariant xabs <= 351.24 when xabs = 351.24 sync A goto w430; loc w430: invariant xabs <= 351.52 when xabs = 351.52 sync B goto w431; loc w431: invariant xabs <= 351.76 when xabs = 351.76 sync A goto w432; loc w432: invariant xabs <= 352 when xabs = 352 sync B goto w433; loc w433: invariant xabs <= 352.24 when xabs = 352.24 sync A goto w434; loc w434: invariant xabs <= 352.52 when xabs = 352.52 sync B goto w435; loc w435: invariant xabs <= 352.72 when xabs = 352.72 sync A goto w436; loc w436: invariant xabs <= 353 when xabs = 353 sync B goto w437; loc w437: invariant xabs <= 353.2 when xabs = 353.2 sync A goto w438; loc w438: invariant xabs <= 353.52 when xabs = 353.52 sync B goto w439; loc w439: invariant xabs <= 353.68 when xabs = 353.68 sync A goto w440; loc w440: invariant xabs <= 354 when xabs = 354 sync B goto w441; loc w441: invariant xabs <= 354.2 when xabs = 354.2 sync A goto w442; loc w442: invariant xabs <= 354.48 when xabs = 354.48 sync B goto w443; loc w443: invariant xabs <= 354.68 when xabs = 354.68 sync A goto w444; loc w444: invariant xabs <= 354.96 when xabs = 354.96 sync B goto w445; loc w445: invariant xabs <= 355.2 when xabs = 355.2 sync A goto w446; loc w446: invariant xabs <= 355.44 when xabs = 355.44 sync B goto w447; loc w447: invariant xabs <= 355.68 when xabs = 355.68 sync A goto w448; loc w448: invariant xabs <= 355.92 when xabs = 355.92 sync B goto w449; loc w449: invariant xabs <= 356.12 when xabs = 356.12 sync A goto w450; loc w450: invariant xabs <= 356.44 when xabs = 356.44 sync B goto w451; loc w451: invariant xabs <= 356.6 when xabs = 356.6 sync A goto w452; loc w452: invariant xabs <= 356.92 when xabs = 356.92 sync B goto w453; loc w453: invariant xabs <= 357.12 when xabs = 357.12 sync A goto w454; loc w454: invariant xabs <= 357.4 when xabs = 357.4 sync B goto w455; loc w455: invariant xabs <= 357.64 when xabs = 357.64 sync A goto w456; loc w456: invariant xabs <= 357.88 when xabs = 357.88 sync B goto w457; loc w457: invariant xabs <= 361.08 when xabs = 361.08 sync A goto w458; loc w458: invariant xabs <= 361.28 when xabs = 361.28 sync B goto w459; loc w459: invariant xabs <= 361.56 when xabs = 361.56 sync A goto w460; loc w460: invariant xabs <= 361.8 when xabs = 361.8 sync B goto w461; loc w461: invariant xabs <= 362.04 when xabs = 362.04 sync A goto w462; loc w462: invariant xabs <= 362.28 when xabs = 362.28 sync B goto w463; loc w463: invariant xabs <= 362.52 when xabs = 362.52 sync A goto w464; loc w464: invariant xabs <= 362.8 when xabs = 362.8 sync B goto w465; loc w465: invariant xabs <= 363 when xabs = 363 sync A goto w466; loc w466: invariant xabs <= 363.28 when xabs = 363.28 sync B goto w467; loc w467: invariant xabs <= 363.52 when xabs = 363.52 sync A goto w468; loc w468: invariant xabs <= 363.76 when xabs = 363.76 sync B goto w469; loc w469: invariant xabs <= 364 when xabs = 364 sync A goto w470; loc w470: invariant xabs <= 364.24 when xabs = 364.24 sync B goto w471; loc w471: invariant xabs <= 364.52 when xabs = 364.52 sync A goto w472; loc w472: invariant xabs <= 364.72 when xabs = 364.72 sync B goto w473; loc w473: invariant xabs <= 365 when xabs = 365 sync A goto w474; loc w474: invariant xabs <= 365.2 when xabs = 365.2 sync B goto w475; loc w475: invariant xabs <= 365.48 when xabs = 365.48 sync A goto w476; loc w476: invariant xabs <= 365.72 when xabs = 365.72 sync B goto w477; loc w477: invariant xabs <= 365.96 when xabs = 365.96 sync A goto w478; loc w478: invariant xabs <= 366.2 when xabs = 366.2 sync B goto w479; loc w479: invariant xabs <= 366.44 when xabs = 366.44 sync A goto w480; loc w480: invariant xabs <= 366.56 when xabs = 366.56 sync B goto w481; loc w481: invariant xabs <= 366.68 when xabs = 366.68 sync C goto w482; loc w482: invariant xabs <= 366.96 when xabs = 366.96 sync B goto w483; loc w483: invariant xabs <= 367.16 when xabs = 367.16 sync C goto w484; loc w484: invariant xabs <= 367.44 when xabs = 367.44 sync B goto w485; loc w485: invariant xabs <= 367.64 when xabs = 367.64 sync C goto w486; loc w486: invariant xabs <= 367.92 when xabs = 367.92 sync B goto w487; loc w487: invariant xabs <= 368.12 when xabs = 368.12 sync C goto w488; loc w488: invariant xabs <= 368.4 when xabs = 368.4 sync B goto w489; loc w489: invariant xabs <= 368.64 when xabs = 368.64 sync C goto w490; loc w490: invariant xabs <= 368.88 when xabs = 368.88 sync B goto w491; loc w491: invariant xabs <= 369.16 when xabs = 369.16 sync C goto w492; loc w492: invariant xabs <= 369.4 when xabs = 369.4 sync B goto w493; loc w493: invariant xabs <= 369.64 when xabs = 369.64 sync C goto w494; loc w494: invariant xabs <= 369.88 when xabs = 369.88 sync B goto w495; loc w495: invariant xabs <= 370.12 when xabs = 370.12 sync C goto w496; loc w496: invariant xabs <= 370.4 when xabs = 370.4 sync B goto w497; loc w497: invariant xabs <= 370.56 when xabs = 370.56 sync C goto w498; loc w498: invariant xabs <= 370.88 when xabs = 370.88 sync B goto w499; loc w499: invariant xabs <= 371.08 when xabs = 371.08 sync C goto w500; loc w500: invariant xabs <= 371.36 when xabs = 371.36 sync B goto w501; loc w501: invariant xabs <= 371.56 when xabs = 371.56 sync C goto w502; loc w502: invariant xabs <= 371.84 when xabs = 371.84 sync B goto w503; loc w503: invariant xabs <= 372.08 when xabs = 372.08 sync C goto w504; loc w504: invariant xabs <= 372.32 when xabs = 372.32 sync B goto w505; loc w505: invariant xabs <= 372.56 when xabs = 372.56 sync C goto w506; loc w506: invariant xabs <= 372.84 when xabs = 372.84 sync B goto w507; loc w507: invariant xabs <= 373.04 when xabs = 373.04 sync C goto w508; loc w508: invariant xabs <= 373.32 when xabs = 373.32 sync B goto w509; loc w509: invariant xabs <= 373.52 when xabs = 373.52 sync C goto w510; loc w510: invariant xabs <= 373.84 when xabs = 373.84 sync B goto w511; loc w511: invariant xabs <= 374.32 when xabs = 374.32 sync C goto w512; loc w512: invariant xabs <= 374.48 when xabs = 374.48 sync D goto w513; loc w513: invariant xabs <= 374.8 when xabs = 374.8 sync C goto w514; loc w514: invariant xabs <= 375 when xabs = 375 sync D goto w515; loc w515: invariant xabs <= 375.28 when xabs = 375.28 sync C goto w516; loc w516: invariant xabs <= 375.48 when xabs = 375.48 sync D goto w517; loc w517: invariant xabs <= 375.76 when xabs = 375.76 sync C goto w518; loc w518: invariant xabs <= 375.96 when xabs = 375.96 sync D goto w519; loc w519: invariant xabs <= 376.28 when xabs = 376.28 sync C goto w520; loc w520: invariant xabs <= 376.44 when xabs = 376.44 sync D goto w521; loc w521: invariant xabs <= 376.8 when xabs = 376.8 sync C goto w522; loc w522: invariant xabs <= 376.92 when xabs = 376.92 sync D goto w523; loc w523: invariant xabs <= 377.28 when xabs = 377.28 sync C goto w524; loc w524: invariant xabs <= 377.4 when xabs = 377.4 sync D goto w525; loc w525: invariant xabs <= 377.76 when xabs = 377.76 sync C goto w526; loc w526: invariant xabs <= 377.92 when xabs = 377.92 sync D goto w527; loc w527: invariant xabs <= 378.16 when xabs = 378.16 sync C goto w528; loc w528: invariant xabs <= 378.4 when xabs = 378.4 sync B goto w529; loc w529: invariant xabs <= 380.72 when xabs = 380.72 sync A goto w530; loc w530: invariant xabs <= 380.84 when xabs = 380.84 sync B goto w531; loc w531: invariant xabs <= 381.2 when xabs = 381.2 sync A goto w532; loc w532: invariant xabs <= 381.36 when xabs = 381.36 sync B goto w533; loc w533: invariant xabs <= 381.64 when xabs = 381.64 sync A goto w534; loc w534: invariant xabs <= 381.84 when xabs = 381.84 sync B goto w535; loc w535: invariant xabs <= 382.16 when xabs = 382.16 sync A goto w536; loc w536: invariant xabs <= 382.32 when xabs = 382.32 sync B goto w537; loc w537: invariant xabs <= 382.64 when xabs = 382.64 sync A goto w538; loc w538: invariant xabs <= 382.8 when xabs = 382.8 sync B goto w539; loc w539: invariant xabs <= 383.16 when xabs = 383.16 sync A goto w540; loc w540: invariant xabs <= 383.64 when xabs = 383.64 sync B goto w541; loc w541: invariant xabs <= 383.76 when xabs = 383.76 sync C goto w542; loc w542: invariant xabs <= 384.12 when xabs = 384.12 sync B goto w543; loc w543: invariant xabs <= 384.28 when xabs = 384.28 sync C goto w544; loc w544: invariant xabs <= 384.6 when xabs = 384.6 sync B goto w545; loc w545: invariant xabs <= 384.8 when xabs = 384.8 sync C goto w546; loc w546: invariant xabs <= 385.08 when xabs = 385.08 sync B goto w547; loc w547: invariant xabs <= 385.6 when xabs = 385.6 sync C goto w548; loc w548: invariant xabs <= 385.72 when xabs = 385.72 sync D goto w549; loc w549: invariant xabs <= 387.08 when xabs = 387.08 sync C goto w550; loc w550: invariant xabs <= 387.2 when xabs = 387.2 sync D goto w551; loc w551: invariant xabs <= 387.56 when xabs = 387.56 sync C goto w552; loc w552: invariant xabs <= 387.68 when xabs = 387.68 sync D goto w553; loc w553: invariant xabs <= 388.04 when xabs = 388.04 sync C goto w554; loc w554: invariant xabs <= 388.2 when xabs = 388.2 sync D goto w555; loc w555: invariant xabs <= 388.52 when xabs = 388.52 sync C goto w556; loc w556: invariant xabs <= 388.68 when xabs = 388.68 sync D goto w557; loc w557: invariant xabs <= 391 when xabs = 391 sync C goto w558; loc w558: invariant xabs <= 398.24 when xabs = 398.24 sync D goto w559; loc w559: invariant xabs <= 398.36 when xabs = 398.36 sync C goto w560; loc w560: invariant xabs <= 398.48 when xabs = 398.48 sync B goto w561; loc w561: invariant xabs <= 401.52 when xabs = 401.52 sync A goto w562; loc w562: invariant xabs <= 403.28 when xabs = 403.28 sync B goto w563; loc w563: invariant xabs <= 405.68 when xabs = 405.68 sync C goto w564; loc w564: invariant xabs <= 418.32 when xabs = 418.32 sync D goto w565; loc w565: invariant xabs <= 418.44 when xabs = 418.44 sync C goto w566; loc w566: invariant xabs <= 418.56 when xabs = 418.56 sync B goto w567; loc w567: invariant xabs <= 421.24 when xabs = 421.24 sync A goto w568; loc w568: invariant xabs <= 422.76 when xabs = 422.76 sync B goto w569; loc w569: invariant xabs <= 424.76 when xabs = 424.76 sync C goto w570; loc w570: invariant xabs <= 438.32 when xabs = 438.32 sync D goto w571; loc w571: invariant xabs <= 438.44 when xabs = 438.44 sync C goto w572; loc w572: invariant xabs <= 438.56 when xabs = 438.56 sync B goto w573; loc w573: invariant xabs <= 441.4 when xabs = 441.4 sync A goto w574; loc w574: invariant xabs <= 442.96 when xabs = 442.96 sync B goto w575; loc w575: invariant xabs <= 446.28 when xabs = 446.28 sync C goto w576; loc w576: invariant xabs <= 458.28 when xabs = 458.28 sync D goto w577; loc w577: invariant xabs <= 458.4 when xabs = 458.4 sync C goto w578; loc w578: invariant xabs <= 458.52 when xabs = 458.52 sync B goto w579; loc w579: invariant xabs <= 462.04 when xabs = 462.04 sync A goto w580; loc w580: invariant xabs <= 462.48 when xabs = 462.48 sync B goto w581; loc w581: invariant xabs <= 462.96 when xabs = 462.96 sync C goto w582; loc w582: invariant xabs <= 463.12 when xabs = 463.12 sync D goto w583; loc w583: invariant xabs <= 463.44 when xabs = 463.44 sync C goto w584; loc w584: invariant xabs <= 463.6 when xabs = 463.6 sync D goto w585; loc w585: invariant xabs <= 463.92 when xabs = 463.92 sync C goto w586; loc w586: invariant xabs <= 464.08 when xabs = 464.08 sync D goto w587; loc w587: invariant xabs <= 464.44 when xabs = 464.44 sync C goto w588; loc w588: invariant xabs <= 464.56 when xabs = 464.56 sync D goto w589; loc w589: invariant xabs <= 465.88 when xabs = 465.88 sync C goto w590; loc w590: invariant xabs <= 466.04 when xabs = 466.04 sync D goto w591; loc w591: invariant xabs <= 466.36 when xabs = 466.36 sync C goto w592; loc w592: invariant xabs <= 466.56 when xabs = 466.56 sync D goto w593; loc w593: invariant xabs <= 466.84 when xabs = 466.84 sync C goto w594; loc w594: invariant xabs <= 467.04 when xabs = 467.04 sync D goto w595; loc w595: invariant xabs <= 467.36 when xabs = 467.36 sync C goto w596; loc w596: invariant xabs <= 467.52 when xabs = 467.52 sync D goto w597; loc w597: invariant xabs <= 467.84 when xabs = 467.84 sync C goto w598; loc w598: invariant xabs <= 468 when xabs = 468 sync D goto w599; loc w599: invariant xabs <= 468.36 when xabs = 468.36 sync C goto w600; loc w600: invariant xabs <= 468.48 when xabs = 468.48 sync D goto w601; loc w601: invariant xabs <= 468.84 when xabs = 468.84 sync C goto w602; loc w602: invariant xabs <= 469 when xabs = 469 sync D goto w603; loc w603: invariant xabs <= 469.32 when xabs = 469.32 sync C goto w604; loc w604: invariant xabs <= 470.48 when xabs = 470.48 sync D goto w605; loc w605: invariant xabs <= 470.8 when xabs = 470.8 sync C goto w606; loc w606: invariant xabs <= 470.92 when xabs = 470.92 sync D goto w607; loc w607: invariant xabs <= 471.28 when xabs = 471.28 sync C goto w608; loc w608: invariant xabs <= 471.44 when xabs = 471.44 sync D goto w609; loc w609: invariant xabs <= 471.76 when xabs = 471.76 sync C goto w610; loc w610: invariant xabs <= 471.92 when xabs = 471.92 sync D goto w611; loc w611: invariant xabs <= 472.24 when xabs = 472.24 sync C goto w612; loc w612: invariant xabs <= 472.92 when xabs = 472.92 sync D goto w613; loc w613: invariant xabs <= 473.2 when xabs = 473.2 sync C goto w614; loc w614: invariant xabs <= 473.4 when xabs = 473.4 sync D goto w615; loc w615: invariant xabs <= 473.72 when xabs = 473.72 sync C goto w616; loc w616: invariant xabs <= 478.2 when xabs = 478.2 sync D goto w617; loc w617: invariant xabs <= 478.32 when xabs = 478.32 sync C goto w618; loc w618: invariant xabs <= 478.44 when xabs = 478.44 sync B goto w619; loc w619: invariant xabs <= 481.04 when xabs = 481.04 sync A goto w620; loc w620: invariant xabs <= 481.24 when xabs = 481.24 sync B goto w621; loc w621: invariant xabs <= 481.52 when xabs = 481.52 sync A goto w622; loc w622: invariant xabs <= 481.76 when xabs = 481.76 sync B goto w623; loc w623: invariant xabs <= 482 when xabs = 482 sync A goto w624; loc w624: invariant xabs <= 482.24 when xabs = 482.24 sync B goto w625; loc w625: invariant xabs <= 482.48 when xabs = 482.48 sync A goto w626; loc w626: invariant xabs <= 482.76 when xabs = 482.76 sync B goto w627; loc w627: invariant xabs <= 483 when xabs = 483 sync A goto w628; loc w628: invariant xabs <= 483.24 when xabs = 483.24 sync B goto w629; loc w629: invariant xabs <= 483.48 when xabs = 483.48 sync A goto w630; loc w630: invariant xabs <= 483.72 when xabs = 483.72 sync B goto w631; loc w631: invariant xabs <= 484 when xabs = 484 sync A goto w632; loc w632: invariant xabs <= 484.2 when xabs = 484.2 sync B goto w633; loc w633: invariant xabs <= 484.44 when xabs = 484.44 sync A goto w634; loc w634: invariant xabs <= 484.72 when xabs = 484.72 sync B goto w635; loc w635: invariant xabs <= 484.92 when xabs = 484.92 sync A goto w636; loc w636: invariant xabs <= 485.2 when xabs = 485.2 sync B goto w637; loc w637: invariant xabs <= 485.4 when xabs = 485.4 sync A goto w638; loc w638: invariant xabs <= 485.72 when xabs = 485.72 sync B goto w639; loc w639: invariant xabs <= 485.92 when xabs = 485.92 sync A goto w640; loc w640: invariant xabs <= 486.16 when xabs = 486.16 sync B goto w641; loc w641: invariant xabs <= 486.4 when xabs = 486.4 sync A goto w642; loc w642: invariant xabs <= 486.52 when xabs = 486.52 sync B goto w643; loc w643: invariant xabs <= 486.64 when xabs = 486.64 sync C goto w644; loc w644: invariant xabs <= 486.92 when xabs = 486.92 sync B goto w645; loc w645: invariant xabs <= 487.12 when xabs = 487.12 sync C goto w646; loc w646: invariant xabs <= 487.4 when xabs = 487.4 sync B goto w647; loc w647: invariant xabs <= 487.64 when xabs = 487.64 sync C goto w648; loc w648: invariant xabs <= 487.88 when xabs = 487.88 sync B goto w649; loc w649: invariant xabs <= 488.16 when xabs = 488.16 sync C goto w650; loc w650: invariant xabs <= 488.36 when xabs = 488.36 sync B goto w651; loc w651: invariant xabs <= 488.64 when xabs = 488.64 sync C goto w652; loc w652: invariant xabs <= 488.84 when xabs = 488.84 sync B goto w653; loc w653: invariant xabs <= 489.12 when xabs = 489.12 sync C goto w654; loc w654: invariant xabs <= 489.32 when xabs = 489.32 sync B goto w655; loc w655: invariant xabs <= 489.6 when xabs = 489.6 sync C goto w656; loc w656: invariant xabs <= 489.84 when xabs = 489.84 sync B goto w657; loc w657: invariant xabs <= 490.08 when xabs = 490.08 sync C goto w658; loc w658: invariant xabs <= 490.32 when xabs = 490.32 sync B goto w659; loc w659: invariant xabs <= 490.56 when xabs = 490.56 sync C goto w660; loc w660: invariant xabs <= 490.8 when xabs = 490.8 sync B goto w661; loc w661: invariant xabs <= 491.08 when xabs = 491.08 sync C goto w662; loc w662: invariant xabs <= 491.28 when xabs = 491.28 sync B goto w663; loc w663: invariant xabs <= 491.6 when xabs = 491.6 sync C goto w664; loc w664: invariant xabs <= 491.76 when xabs = 491.76 sync B goto w665; loc w665: invariant xabs <= 492.08 when xabs = 492.08 sync C goto w666; loc w666: invariant xabs <= 492.28 when xabs = 492.28 sync B goto w667; loc w667: invariant xabs <= 492.56 when xabs = 492.56 sync C goto w668; loc w668: invariant xabs <= 492.76 when xabs = 492.76 sync B goto w669; loc w669: invariant xabs <= 493.04 when xabs = 493.04 sync C goto w670; loc w670: invariant xabs <= 493.28 when xabs = 493.28 sync B goto w671; loc w671: invariant xabs <= 493.52 when xabs = 493.52 sync C goto w672; loc w672: invariant xabs <= 493.76 when xabs = 493.76 sync B goto w673; loc w673: invariant xabs <= 494.04 when xabs = 494.04 sync C goto w674; loc w674: invariant xabs <= 494.2 when xabs = 494.2 sync B goto w675; loc w675: invariant xabs <= 494.52 when xabs = 494.52 sync C goto w676; loc w676: invariant xabs <= 494.68 when xabs = 494.68 sync B goto w677; loc w677: invariant xabs <= 495.04 when xabs = 495.04 sync C goto w678; loc w678: invariant xabs <= 495.2 when xabs = 495.2 sync B goto w679; loc w679: invariant xabs <= 495.52 when xabs = 495.52 sync C goto w680; loc w680: invariant xabs <= 495.68 when xabs = 495.68 sync B goto w681; loc w681: invariant xabs <= 495.96 when xabs = 495.96 sync C goto w682; loc w682: invariant xabs <= 496.2 when xabs = 496.2 sync B goto w683; loc w683: invariant xabs <= 496.44 when xabs = 496.44 sync C goto w684; loc w684: invariant xabs <= 496.68 when xabs = 496.68 sync B goto w685; loc w685: invariant xabs <= 496.96 when xabs = 496.96 sync C goto w686; loc w686: invariant xabs <= 497.16 when xabs = 497.16 sync B goto w687; loc w687: invariant xabs <= 497.44 when xabs = 497.44 sync C goto w688; loc w688: invariant xabs <= 497.64 when xabs = 497.64 sync B goto w689; loc w689: invariant xabs <= 497.96 when xabs = 497.96 sync C goto w690; loc w690: invariant xabs <= 498.4 when xabs = 498.4 sync B goto w691; loc w691: invariant xabs <= 525.08 when xabs = 525.08 sync A goto w692; loc w692: invariant xabs <= 525.4 when xabs = 525.4 sync B goto w693; loc w693: invariant xabs <= 525.52 when xabs = 525.52 sync A goto w694; loc w694: invariant xabs <= 525.88 when xabs = 525.88 sync B goto w695; loc w695: invariant xabs <= 526 when xabs = 526 sync A goto w696; loc w696: invariant xabs <= 526.84 when xabs = 526.84 sync B goto w697; loc w697: invariant xabs <= 530.96 when xabs = 530.96 sync A goto w698; loc w698: invariant xabs <= 531.24 when xabs = 531.24 sync B goto w699; loc w699: invariant xabs <= 531.44 when xabs = 531.44 sync A goto w700; loc w700: invariant xabs <= 531.72 when xabs = 531.72 sync B goto w701; loc w701: invariant xabs <= 531.92 when xabs = 531.92 sync A goto w702; loc w702: invariant xabs <= 532.24 when xabs = 532.24 sync B goto w703; loc w703: invariant xabs <= 532.4 when xabs = 532.4 sync A goto w704; loc w704: invariant xabs <= 532.72 when xabs = 532.72 sync B goto w705; loc w705: invariant xabs <= 532.88 when xabs = 532.88 sync A goto w706; loc w706: invariant xabs <= 533.2 when xabs = 533.2 sync B goto w707; loc w707: invariant xabs <= 533.4 when xabs = 533.4 sync A goto w708; loc w708: invariant xabs <= 533.68 when xabs = 533.68 sync B goto w709; loc w709: invariant xabs <= 533.88 when xabs = 533.88 sync A goto w710; loc w710: invariant xabs <= 534.16 when xabs = 534.16 sync B goto w711; loc w711: invariant xabs <= 534.4 when xabs = 534.4 sync A goto w712; loc w712: invariant xabs <= 534.68 when xabs = 534.68 sync B goto w713; loc w713: invariant xabs <= 534.88 when xabs = 534.88 sync A goto w714; loc w714: invariant xabs <= 535.16 when xabs = 535.16 sync B goto w715; loc w715: invariant xabs <= 535.32 when xabs = 535.32 sync A goto w716; loc w716: invariant xabs <= 535.68 when xabs = 535.68 sync B goto w717; loc w717: invariant xabs <= 535.8 when xabs = 535.8 sync A goto w718; loc w718: invariant xabs <= 536.16 when xabs = 536.16 sync B goto w719; loc w719: invariant xabs <= 536.32 when xabs = 536.32 sync A goto w720; loc w720: invariant xabs <= 536.64 when xabs = 536.64 sync B goto w721; loc w721: invariant xabs <= 536.84 when xabs = 536.84 sync A goto w722; loc w722: invariant xabs <= 537.12 when xabs = 537.12 sync B goto w723; loc w723: invariant xabs <= 537.32 when xabs = 537.32 sync A goto w724; loc w724: invariant xabs <= 537.6 when xabs = 537.6 sync B goto w725; loc w725: invariant xabs <= 537.8 when xabs = 537.8 sync A goto w726; loc w726: invariant xabs <= 538.12 when xabs = 538.12 sync B goto w727; loc w727: invariant xabs <= 542.72 when xabs = 542.72 sync A goto w728; loc w728: invariant xabs <= 543 when xabs = 543 sync B goto w729; loc w729: invariant xabs <= 543.2 when xabs = 543.2 sync A goto w730; loc w730: invariant xabs <= 543.44 when xabs = 543.44 sync B goto w731; loc w731: invariant xabs <= 543.72 when xabs = 543.72 sync A goto w732; loc w732: invariant xabs <= 543.96 when xabs = 543.96 sync B goto w733; loc w733: invariant xabs <= 544.2 when xabs = 544.2 sync A goto w734; loc w734: invariant xabs <= 544.44 when xabs = 544.44 sync B goto w735; loc w735: invariant xabs <= 544.64 when xabs = 544.64 sync A goto w736; loc w736: invariant xabs <= 544.96 when xabs = 544.96 sync B goto w737; loc w737: invariant xabs <= 545.12 when xabs = 545.12 sync A goto w738; loc w738: invariant xabs <= 545.44 when xabs = 545.44 sync B goto w739; loc w739: invariant xabs <= 545.64 when xabs = 545.64 sync A goto w740; loc w740: invariant xabs <= 545.92 when xabs = 545.92 sync B goto w741; loc w741: invariant xabs <= 546.12 when xabs = 546.12 sync A goto w742; loc w742: invariant xabs <= 546.4 when xabs = 546.4 sync B goto w743; loc w743: invariant xabs <= 546.64 when xabs = 546.64 sync A goto w744; loc w744: invariant xabs <= 546.88 when xabs = 546.88 sync B goto w745; loc w745: invariant xabs <= 547.12 when xabs = 547.12 sync A goto w746; loc w746: invariant xabs <= 547.4 when xabs = 547.4 sync B goto w747; loc w747: invariant xabs <= 547.6 when xabs = 547.6 sync A goto w748; loc w748: invariant xabs <= 547.88 when xabs = 547.88 sync B goto w749; loc w749: invariant xabs <= 548.08 when xabs = 548.08 sync A goto w750; loc w750: invariant xabs <= 548.4 when xabs = 548.4 sync B goto w751; loc w751: invariant xabs <= 548.56 when xabs = 548.56 sync A goto w752; loc w752: invariant xabs <= 548.84 when xabs = 548.84 sync B goto w753; loc w753: invariant xabs <= 549.08 when xabs = 549.08 sync A goto w754; loc w754: invariant xabs <= 549.32 when xabs = 549.32 sync B goto w755; loc w755: invariant xabs <= 549.6 when xabs = 549.6 sync A goto w756; loc w756: invariant xabs <= 549.8 when xabs = 549.8 sync B goto w757; loc w757: invariant xabs <= 550.08 when xabs = 550.08 sync A goto w758; loc w758: invariant xabs <= 550.2 when xabs = 550.2 sync B goto w759; loc w759: invariant xabs <= 550.32 when xabs = 550.32 sync C goto w760; loc w760: invariant xabs <= 550.56 when xabs = 550.56 sync B goto w761; loc w761: invariant xabs <= 550.8 when xabs = 550.8 sync C goto w762; loc w762: invariant xabs <= 551.04 when xabs = 551.04 sync B goto w763; loc w763: invariant xabs <= 551.32 when xabs = 551.32 sync C goto w764; loc w764: invariant xabs <= 551.52 when xabs = 551.52 sync B goto w765; loc w765: invariant xabs <= 551.8 when xabs = 551.8 sync C goto w766; loc w766: invariant xabs <= 552 when xabs = 552 sync B goto w767; loc w767: invariant xabs <= 552.28 when xabs = 552.28 sync C goto w768; loc w768: invariant xabs <= 552.52 when xabs = 552.52 sync B goto w769; loc w769: invariant xabs <= 552.76 when xabs = 552.76 sync C goto w770; loc w770: invariant xabs <= 553.04 when xabs = 553.04 sync B goto w771; loc w771: invariant xabs <= 553.24 when xabs = 553.24 sync C goto w772; loc w772: invariant xabs <= 553.52 when xabs = 553.52 sync B goto w773; loc w773: invariant xabs <= 553.72 when xabs = 553.72 sync C goto w774; loc w774: invariant xabs <= 554 when xabs = 554 sync B goto w775; loc w775: invariant xabs <= 554.24 when xabs = 554.24 sync C goto w776; loc w776: invariant xabs <= 554.48 when xabs = 554.48 sync B goto w777; loc w777: invariant xabs <= 554.72 when xabs = 554.72 sync C goto w778; loc w778: invariant xabs <= 554.96 when xabs = 554.96 sync B goto w779; loc w779: invariant xabs <= 555.2 when xabs = 555.2 sync C goto w780; loc w780: invariant xabs <= 555.48 when xabs = 555.48 sync B goto w781; loc w781: invariant xabs <= 555.68 when xabs = 555.68 sync C goto w782; loc w782: invariant xabs <= 555.96 when xabs = 555.96 sync B goto w783; loc w783: invariant xabs <= 556.16 when xabs = 556.16 sync C goto w784; loc w784: invariant xabs <= 556.44 when xabs = 556.44 sync B goto w785; loc w785: invariant xabs <= 556.68 when xabs = 556.68 sync C goto w786; loc w786: invariant xabs <= 556.92 when xabs = 556.92 sync B goto w787; loc w787: invariant xabs <= 557.16 when xabs = 557.16 sync C goto w788; loc w788: invariant xabs <= 557.4 when xabs = 557.4 sync B goto w789; loc w789: invariant xabs <= 557.68 when xabs = 557.68 sync C goto w790; loc w790: invariant xabs <= 557.92 when xabs = 557.92 sync B goto w791; loc w791: invariant xabs <= 558.16 when xabs = 558.16 sync C goto w792; loc w792: invariant xabs <= 558.28 when xabs = 558.28 sync B goto w793; loc w793: invariant xabs <= 561.36 when xabs = 561.36 sync A goto w794; loc w794: invariant xabs <= 561.56 when xabs = 561.56 sync B goto w795; loc w795: invariant xabs <= 561.84 when xabs = 561.84 sync A goto w796; loc w796: invariant xabs <= 562.04 when xabs = 562.04 sync B goto w797; loc w797: invariant xabs <= 562.36 when xabs = 562.36 sync A goto w798; loc w798: invariant xabs <= 562.52 when xabs = 562.52 sync B goto w799; loc w799: invariant xabs <= 562.84 when xabs = 562.84 sync A goto w800; loc w800: invariant xabs <= 563 when xabs = 563 sync B goto w801; loc w801: invariant xabs <= 563.32 when xabs = 563.32 sync A goto w802; loc w802: invariant xabs <= 563.8 when xabs = 563.8 sync B goto w803; loc w803: invariant xabs <= 564 when xabs = 564 sync C goto w804; loc w804: invariant xabs <= 564.28 when xabs = 564.28 sync B goto w805; loc w805: invariant xabs <= 564.48 when xabs = 564.48 sync C goto w806; loc w806: invariant xabs <= 564.8 when xabs = 564.8 sync B goto w807; loc w807: invariant xabs <= 564.96 when xabs = 564.96 sync C goto w808; loc w808: invariant xabs <= 565.32 when xabs = 565.32 sync B goto w809; loc w809: invariant xabs <= 565.44 when xabs = 565.44 sync C goto w810; loc w810: invariant xabs <= 565.8 when xabs = 565.8 sync B goto w811; loc w811: invariant xabs <= 565.92 when xabs = 565.92 sync C goto w812; loc w812: invariant xabs <= 566.28 when xabs = 566.28 sync B goto w813; loc w813: invariant xabs <= 566.44 when xabs = 566.44 sync C goto w814; loc w814: invariant xabs <= 566.72 when xabs = 566.72 sync B goto w815; loc w815: invariant xabs <= 566.92 when xabs = 566.92 sync C goto w816; loc w816: invariant xabs <= 567.24 when xabs = 567.24 sync B goto w817; loc w817: invariant xabs <= 567.44 when xabs = 567.44 sync C goto w818; loc w818: invariant xabs <= 567.72 when xabs = 567.72 sync B goto w819; loc w819: invariant xabs <= 567.88 when xabs = 567.88 sync C goto w820; loc w820: invariant xabs <= 568.24 when xabs = 568.24 sync B goto w821; loc w821: invariant xabs <= 568.36 when xabs = 568.36 sync C goto w822; loc w822: invariant xabs <= 568.72 when xabs = 568.72 sync B goto w823; loc w823: invariant xabs <= 569.24 when xabs = 569.24 sync C goto w824; loc w824: invariant xabs <= 569.36 when xabs = 569.36 sync D goto w825; loc w825: invariant xabs <= 569.68 when xabs = 569.68 sync C goto w826; loc w826: invariant xabs <= 569.88 when xabs = 569.88 sync D goto w827; loc w827: invariant xabs <= 570.16 when xabs = 570.16 sync C goto w828; loc w828: invariant xabs <= 570.36 when xabs = 570.36 sync D goto w829; loc w829: invariant xabs <= 570.68 when xabs = 570.68 sync C goto w830; loc w830: invariant xabs <= 570.84 when xabs = 570.84 sync D goto w831; loc w831: invariant xabs <= 572.16 when xabs = 572.16 sync C goto w832; loc w832: invariant xabs <= 572.28 when xabs = 572.28 sync D goto w833; loc w833: invariant xabs <= 572.64 when xabs = 572.64 sync C goto w834; loc w834: invariant xabs <= 572.8 when xabs = 572.8 sync D goto w835; loc w835: invariant xabs <= 573.12 when xabs = 573.12 sync C goto w836; loc w836: invariant xabs <= 573.28 when xabs = 573.28 sync D goto w837; loc w837: invariant xabs <= 573.6 when xabs = 573.6 sync C goto w838; loc w838: invariant xabs <= 573.76 when xabs = 573.76 sync D goto w839; loc w839: invariant xabs <= 574.12 when xabs = 574.12 sync C goto w840; loc w840: invariant xabs <= 574.24 when xabs = 574.24 sync D goto w841; loc w841: invariant xabs <= 576.08 when xabs = 576.08 sync C goto w842; loc w842: invariant xabs <= 578.2 when xabs = 578.2 sync D goto w843; loc w843: invariant xabs <= 578.32 when xabs = 578.32 sync C goto w844; loc w844: invariant xabs <= 578.44 when xabs = 578.44 sync B goto w845; loc w845: invariant xabs <= 581.48 when xabs = 581.48 sync A goto w846; loc w846: invariant xabs <= 582.44 when xabs = 582.44 sync B goto w847; loc w847: invariant xabs <= 585.88 when xabs = 585.88 sync C goto w848; loc w848: invariant xabs <= 598.28 when xabs = 598.28 sync D goto w849; loc w849: invariant xabs <= 598.4 when xabs = 598.4 sync C goto w850; loc w850: invariant xabs <= 598.52 when xabs = 598.52 sync B goto w851; loc w851: invariant xabs <= 601.16 when xabs = 601.16 sync A goto w852; loc w852: invariant xabs <= 602.68 when xabs = 602.68 sync B goto w853; loc w853: invariant xabs <= 605.28 when xabs = 605.28 sync C goto w854; loc w854: invariant xabs <= 618.32 when xabs = 618.32 sync D goto w855; loc w855: invariant xabs <= 618.44 when xabs = 618.44 sync C goto w856; loc w856: invariant xabs <= 618.56 when xabs = 618.56 sync B goto w857; loc w857: invariant xabs <= 621.36 when xabs = 621.36 sync A goto w858; loc w858: invariant xabs <= 623 when xabs = 623 sync B goto w859; loc w859: invariant xabs <= 625.36 when xabs = 625.36 sync C goto w860; loc w860: invariant xabs <= 638.32 when xabs = 638.32 sync D goto w861; loc w861: invariant xabs <= 638.44 when xabs = 638.44 sync C goto w862; loc w862: invariant xabs <= 638.56 when xabs = 638.56 sync B goto w863; loc w863: invariant xabs <= 641.48 when xabs = 641.48 sync A goto w864; loc w864: invariant xabs <= 642.68 when xabs = 642.68 sync B goto w865; loc w865: invariant xabs <= 645.12 when xabs = 645.12 sync C goto w866; loc w866: invariant xabs <= 658.24 when xabs = 658.24 sync D goto w867; loc w867: invariant xabs <= 658.36 when xabs = 658.36 sync C goto w868; loc w868: invariant xabs <= 658.48 when xabs = 658.48 sync B goto w869; loc w869: invariant xabs <= 661.72 when xabs = 661.72 sync A goto w870; loc w870: invariant xabs <= 661.92 when xabs = 661.92 sync B goto w871; loc w871: invariant xabs <= 662.24 when xabs = 662.24 sync A goto w872; loc w872: invariant xabs <= 662.4 when xabs = 662.4 sync B goto w873; loc w873: invariant xabs <= 662.72 when xabs = 662.72 sync A goto w874; loc w874: invariant xabs <= 662.88 when xabs = 662.88 sync B goto w875; loc w875: invariant xabs <= 663.2 when xabs = 663.2 sync A goto w876; loc w876: invariant xabs <= 663.4 when xabs = 663.4 sync B goto w877; loc w877: invariant xabs <= 663.68 when xabs = 663.68 sync A goto w878; loc w878: invariant xabs <= 664.16 when xabs = 664.16 sync B goto w879; loc w879: invariant xabs <= 664.4 when xabs = 664.4 sync C goto w880; loc w880: invariant xabs <= 664.64 when xabs = 664.64 sync B goto w881; loc w881: invariant xabs <= 664.88 when xabs = 664.88 sync C goto w882; loc w882: invariant xabs <= 665.16 when xabs = 665.16 sync B goto w883; loc w883: invariant xabs <= 665.36 when xabs = 665.36 sync C goto w884; loc w884: invariant xabs <= 665.64 when xabs = 665.64 sync B goto w885; loc w885: invariant xabs <= 665.84 when xabs = 665.84 sync C goto w886; loc w886: invariant xabs <= 666.16 when xabs = 666.16 sync B goto w887; loc w887: invariant xabs <= 666.32 when xabs = 666.32 sync C goto w888; loc w888: invariant xabs <= 666.64 when xabs = 666.64 sync B goto w889; loc w889: invariant xabs <= 666.84 when xabs = 666.84 sync C goto w890; loc w890: invariant xabs <= 667.12 when xabs = 667.12 sync B goto w891; loc w891: invariant xabs <= 667.32 when xabs = 667.32 sync C goto w892; loc w892: invariant xabs <= 667.6 when xabs = 667.6 sync B goto w893; loc w893: invariant xabs <= 667.84 when xabs = 667.84 sync C goto w894; loc w894: invariant xabs <= 668.08 when xabs = 668.08 sync B goto w895; loc w895: invariant xabs <= 668.32 when xabs = 668.32 sync C goto w896; loc w896: invariant xabs <= 668.6 when xabs = 668.6 sync B goto w897; loc w897: invariant xabs <= 668.8 when xabs = 668.8 sync C goto w898; loc w898: invariant xabs <= 669.08 when xabs = 669.08 sync B goto w899; loc w899: invariant xabs <= 669.28 when xabs = 669.28 sync C goto w900; loc w900: invariant xabs <= 669.56 when xabs = 669.56 sync B goto w901; loc w901: invariant xabs <= 669.76 when xabs = 669.76 sync C goto w902; loc w902: invariant xabs <= 670.04 when xabs = 670.04 sync B goto w903; loc w903: invariant xabs <= 670.16 when xabs = 670.16 sync C goto w904; loc w904: invariant xabs <= 670.28 when xabs = 670.28 sync D goto w905; loc w905: invariant xabs <= 670.52 when xabs = 670.52 sync C goto w906; loc w906: invariant xabs <= 670.76 when xabs = 670.76 sync D goto w907; loc w907: invariant xabs <= 671 when xabs = 671 sync C goto w908; loc w908: invariant xabs <= 671.24 when xabs = 671.24 sync D goto w909; loc w909: invariant xabs <= 671.52 when xabs = 671.52 sync C goto w910; loc w910: invariant xabs <= 671.72 when xabs = 671.72 sync D goto w911; loc w911: invariant xabs <= 672 when xabs = 672 sync C goto w912; loc w912: invariant xabs <= 672.2 when xabs = 672.2 sync D goto w913; loc w913: invariant xabs <= 672.52 when xabs = 672.52 sync C goto w914; loc w914: invariant xabs <= 672.72 when xabs = 672.72 sync D goto w915; loc w915: invariant xabs <= 672.84 when xabs = 672.84 sync C goto w916; loc w916: invariant xabs <= 672.96 when xabs = 672.96 sync B goto w917; loc w917: invariant xabs <= 673.08 when xabs = 673.08 sync C goto w918; loc w918: invariant xabs <= 673.2 when xabs = 673.2 sync D goto w919; loc w919: invariant xabs <= 673.44 when xabs = 673.44 sync C goto w920; loc w920: invariant xabs <= 673.72 when xabs = 673.72 sync D goto w921; loc w921: invariant xabs <= 673.92 when xabs = 673.92 sync C goto w922; loc w922: invariant xabs <= 674.2 when xabs = 674.2 sync D goto w923; loc w923: invariant xabs <= 674.44 when xabs = 674.44 sync C goto w924; loc w924: invariant xabs <= 674.68 when xabs = 674.68 sync D goto w925; loc w925: invariant xabs <= 674.92 when xabs = 674.92 sync C goto w926; loc w926: invariant xabs <= 675.16 when xabs = 675.16 sync D goto w927; loc w927: invariant xabs <= 675.44 when xabs = 675.44 sync C goto w928; loc w928: invariant xabs <= 675.64 when xabs = 675.64 sync D goto w929; loc w929: invariant xabs <= 675.92 when xabs = 675.92 sync C goto w930; loc w930: invariant xabs <= 676.16 when xabs = 676.16 sync D goto w931; loc w931: invariant xabs <= 676.4 when xabs = 676.4 sync C goto w932; loc w932: invariant xabs <= 676.64 when xabs = 676.64 sync D goto w933; loc w933: invariant xabs <= 676.88 when xabs = 676.88 sync C goto w934; loc w934: invariant xabs <= 677.16 when xabs = 677.16 sync D goto w935; loc w935: invariant xabs <= 677.36 when xabs = 677.36 sync C goto w936; loc w936: invariant xabs <= 677.64 when xabs = 677.64 sync D goto w937; loc w937: invariant xabs <= 677.84 when xabs = 677.84 sync C goto w938; loc w938: invariant xabs <= 678.16 when xabs = 678.16 sync D goto w939; loc w939: invariant xabs <= 678.28 when xabs = 678.28 sync C goto w940; loc w940: invariant xabs <= 678.4 when xabs = 678.4 sync B goto w941; loc w941: invariant xabs <= 681.28 when xabs = 681.28 sync A goto w942; loc w942: invariant xabs <= 681.56 when xabs = 681.56 sync B goto w943; loc w943: invariant xabs <= 681.8 when xabs = 681.8 sync A goto w944; loc w944: invariant xabs <= 682.04 when xabs = 682.04 sync B goto w945; loc w945: invariant xabs <= 682.28 when xabs = 682.28 sync A goto w946; loc w946: invariant xabs <= 682.52 when xabs = 682.52 sync B goto w947; loc w947: invariant xabs <= 682.72 when xabs = 682.72 sync A goto w948; loc w948: invariant xabs <= 683.04 when xabs = 683.04 sync B goto w949; loc w949: invariant xabs <= 683.2 when xabs = 683.2 sync A goto w950; loc w950: invariant xabs <= 683.52 when xabs = 683.52 sync B goto w951; loc w951: invariant xabs <= 683.72 when xabs = 683.72 sync A goto w952; loc w952: invariant xabs <= 684 when xabs = 684 sync B goto w953; loc w953: invariant xabs <= 684.2 when xabs = 684.2 sync A goto w954; loc w954: invariant xabs <= 684.48 when xabs = 684.48 sync B goto w955; loc w955: invariant xabs <= 684.72 when xabs = 684.72 sync A goto w956; loc w956: invariant xabs <= 685 when xabs = 685 sync B goto w957; loc w957: invariant xabs <= 685.2 when xabs = 685.2 sync A goto w958; loc w958: invariant xabs <= 685.48 when xabs = 685.48 sync B goto w959; loc w959: invariant xabs <= 685.68 when xabs = 685.68 sync A goto w960; loc w960: invariant xabs <= 686 when xabs = 686 sync B goto w961; loc w961: invariant xabs <= 686.16 when xabs = 686.16 sync A goto w962; loc w962: invariant xabs <= 686.48 when xabs = 686.48 sync B goto w963; loc w963: invariant xabs <= 686.64 when xabs = 686.64 sync A goto w964; loc w964: invariant xabs <= 686.96 when xabs = 686.96 sync B goto w965; loc w965: invariant xabs <= 687.12 when xabs = 687.12 sync A goto w966; loc w966: invariant xabs <= 687.44 when xabs = 687.44 sync B goto w967; loc w967: invariant xabs <= 687.64 when xabs = 687.64 sync A goto w968; loc w968: invariant xabs <= 687.92 when xabs = 687.92 sync B goto w969; loc w969: invariant xabs <= 688.12 when xabs = 688.12 sync A goto w970; loc w970: invariant xabs <= 688.4 when xabs = 688.4 sync B goto w971; loc w971: invariant xabs <= 688.6 when xabs = 688.6 sync A goto w972; loc w972: invariant xabs <= 688.92 when xabs = 688.92 sync B goto w973; loc w973: invariant xabs <= 689.08 when xabs = 689.08 sync A goto w974; loc w974: invariant xabs <= 689.44 when xabs = 689.44 sync B goto w975; loc w975: invariant xabs <= 689.56 when xabs = 689.56 sync A goto w976; loc w976: invariant xabs <= 689.92 when xabs = 689.92 sync B goto w977; loc w977: invariant xabs <= 690.08 when xabs = 690.08 sync A goto w978; loc w978: invariant xabs <= 690.4 when xabs = 690.4 sync B goto w979; loc w979: invariant xabs <= 690.56 when xabs = 690.56 sync A goto w980; loc w980: invariant xabs <= 690.88 when xabs = 690.88 sync B goto w981; loc w981: invariant xabs <= 691.08 when xabs = 691.08 sync A goto w982; loc w982: invariant xabs <= 691.36 when xabs = 691.36 sync B goto w983; loc w983: invariant xabs <= 691.56 when xabs = 691.56 sync A goto w984; loc w984: invariant xabs <= 691.84 when xabs = 691.84 sync B goto w985; loc w985: invariant xabs <= 692.04 when xabs = 692.04 sync A goto w986; loc w986: invariant xabs <= 692.36 when xabs = 692.36 sync B goto w987; loc w987: invariant xabs <= 692.52 when xabs = 692.52 sync A goto w988; loc w988: invariant xabs <= 692.84 when xabs = 692.84 sync B goto w989; loc w989: invariant xabs <= 693 when xabs = 693 sync A goto w990; loc w990: invariant xabs <= 693.32 when xabs = 693.32 sync B goto w991; loc w991: invariant xabs <= 693.48 when xabs = 693.48 sync A goto w992; loc w992: invariant xabs <= 693.8 when xabs = 693.8 sync B goto w993; loc w993: invariant xabs <= 694 when xabs = 694 sync A goto w994; loc w994: invariant xabs <= 694.28 when xabs = 694.28 sync B goto w995; loc w995: invariant xabs <= 694.48 when xabs = 694.48 sync A goto w996; loc w996: invariant xabs <= 694.8 when xabs = 694.8 sync B goto w997; loc w997: invariant xabs <= 694.96 when xabs = 694.96 sync A goto w998; loc w998: invariant xabs <= 695.32 when xabs = 695.32 sync B goto w999; loc w999: invariant xabs <= 695.44 when xabs = 695.44 sync A goto w1000; loc w1000: invariant xabs <= 695.8 when xabs = 695.8 sync B goto w1001; loc w1001: invariant xabs <= 695.92 when xabs = 695.92 sync A goto w1002; loc w1002: invariant xabs <= 696.28 when xabs = 696.28 sync B goto w1003; loc w1003: invariant xabs <= 696.4 when xabs = 696.4 sync A goto w1004; loc w1004: invariant xabs <= 696.76 when xabs = 696.76 sync B goto w1005; loc w1005: invariant xabs <= 696.92 when xabs = 696.92 sync A goto w1006; loc w1006: invariant xabs <= 697.24 when xabs = 697.24 sync B goto w1007; loc w1007: invariant xabs <= 697.44 when xabs = 697.44 sync A goto w1008; loc w1008: invariant xabs <= 697.72 when xabs = 697.72 sync B goto w1009; loc w1009: invariant xabs <= 697.92 when xabs = 697.92 sync A goto w1010; loc w1010: invariant xabs <= 698.12 when xabs = 698.12 sync B goto w1011; loc w1011: invariant xabs <= 725.36 when xabs = 725.36 sync A goto w1012; loc w1012: invariant xabs <= 725.64 when xabs = 725.64 sync B goto w1013; loc w1013: invariant xabs <= 725.84 when xabs = 725.84 sync A goto w1014; loc w1014: invariant xabs <= 726.12 when xabs = 726.12 sync B goto w1015; loc w1015: invariant xabs <= 726.32 when xabs = 726.32 sync A goto w1016; loc w1016: invariant xabs <= 726.64 when xabs = 726.64 sync B goto w1017; loc w1017: invariant xabs <= 726.8 when xabs = 726.8 sync A goto w1018; loc w1018: invariant xabs <= 727.12 when xabs = 727.12 sync B goto w1019; loc w1019: invariant xabs <= 727.28 when xabs = 727.28 sync A goto w1020; loc w1020: invariant xabs <= 727.6 when xabs = 727.6 sync B goto w1021; loc w1021: invariant xabs <= 727.76 when xabs = 727.76 sync A goto w1022; loc w1022: invariant xabs <= 728.08 when xabs = 728.08 sync B goto w1023; loc w1023: invariant xabs <= 728.28 when xabs = 728.28 sync A goto w1024; loc w1024: invariant xabs <= 728.56 when xabs = 728.56 sync B goto w1025; loc w1025: invariant xabs <= 728.8 when xabs = 728.8 sync A goto w1026; loc w1026: invariant xabs <= 729.04 when xabs = 729.04 sync B goto w1027; loc w1027: invariant xabs <= 729.28 when xabs = 729.28 sync A goto w1028; loc w1028: invariant xabs <= 729.56 when xabs = 729.56 sync B goto w1029; loc w1029: invariant xabs <= 729.76 when xabs = 729.76 sync A goto w1030; loc w1030: invariant xabs <= 730.04 when xabs = 730.04 sync B goto w1031; loc w1031: invariant xabs <= 730.24 when xabs = 730.24 sync A goto w1032; loc w1032: invariant xabs <= 730.56 when xabs = 730.56 sync B goto w1033; loc w1033: invariant xabs <= 730.72 when xabs = 730.72 sync A goto w1034; loc w1034: invariant xabs <= 731.04 when xabs = 731.04 sync B goto w1035; loc w1035: invariant xabs <= 731.2 when xabs = 731.2 sync A goto w1036; loc w1036: invariant xabs <= 731.52 when xabs = 731.52 sync B goto w1037; loc w1037: invariant xabs <= 731.72 when xabs = 731.72 sync A goto w1038; loc w1038: invariant xabs <= 732 when xabs = 732 sync B goto w1039; loc w1039: invariant xabs <= 732.2 when xabs = 732.2 sync A goto w1040; loc w1040: invariant xabs <= 732.48 when xabs = 732.48 sync B goto w1041; loc w1041: invariant xabs <= 732.68 when xabs = 732.68 sync A goto w1042; loc w1042: invariant xabs <= 733 when xabs = 733 sync B goto w1043; loc w1043: invariant xabs <= 733.16 when xabs = 733.16 sync A goto w1044; loc w1044: invariant xabs <= 733.48 when xabs = 733.48 sync B goto w1045; loc w1045: invariant xabs <= 733.64 when xabs = 733.64 sync A goto w1046; loc w1046: invariant xabs <= 733.96 when xabs = 733.96 sync B goto w1047; loc w1047: invariant xabs <= 734.16 when xabs = 734.16 sync A goto w1048; loc w1048: invariant xabs <= 734.44 when xabs = 734.44 sync B goto w1049; loc w1049: invariant xabs <= 734.68 when xabs = 734.68 sync A goto w1050; loc w1050: invariant xabs <= 734.92 when xabs = 734.92 sync B goto w1051; loc w1051: invariant xabs <= 735.16 when xabs = 735.16 sync A goto w1052; loc w1052: invariant xabs <= 735.4 when xabs = 735.4 sync B goto w1053; loc w1053: invariant xabs <= 735.64 when xabs = 735.64 sync A goto w1054; loc w1054: invariant xabs <= 735.92 when xabs = 735.92 sync B goto w1055; loc w1055: invariant xabs <= 736.12 when xabs = 736.12 sync A goto w1056; loc w1056: invariant xabs <= 736.4 when xabs = 736.4 sync B goto w1057; loc w1057: invariant xabs <= 736.6 when xabs = 736.6 sync A goto w1058; loc w1058: invariant xabs <= 736.92 when xabs = 736.92 sync B goto w1059; loc w1059: invariant xabs <= 737.08 when xabs = 737.08 sync A goto w1060; loc w1060: invariant xabs <= 737.36 when xabs = 737.36 sync B goto w1061; loc w1061: invariant xabs <= 737.6 when xabs = 737.6 sync A goto w1062; loc w1062: invariant xabs <= 737.84 when xabs = 737.84 sync B goto w1063; loc w1063: invariant xabs <= 738.08 when xabs = 738.08 sync A goto w1064; loc w1064: invariant xabs <= 738.32 when xabs = 738.32 sync B goto w1065; loc w1065: invariant xabs <= 741.6 when xabs = 741.6 sync A goto w1066; loc w1066: invariant xabs <= 741.76 when xabs = 741.76 sync B goto w1067; loc w1067: invariant xabs <= 742.04 when xabs = 742.04 sync A goto w1068; loc w1068: invariant xabs <= 742.24 when xabs = 742.24 sync B goto w1069; loc w1069: invariant xabs <= 742.52 when xabs = 742.52 sync A goto w1070; loc w1070: invariant xabs <= 742.76 when xabs = 742.76 sync B goto w1071; loc w1071: invariant xabs <= 743 when xabs = 743 sync A goto w1072; loc w1072: invariant xabs <= 743.24 when xabs = 743.24 sync B goto w1073; loc w1073: invariant xabs <= 743.48 when xabs = 743.48 sync A goto w1074; loc w1074: invariant xabs <= 743.72 when xabs = 743.72 sync B goto w1075; loc w1075: invariant xabs <= 744 when xabs = 744 sync A goto w1076; loc w1076: invariant xabs <= 744.2 when xabs = 744.2 sync B goto w1077; loc w1077: invariant xabs <= 744.48 when xabs = 744.48 sync A goto w1078; loc w1078: invariant xabs <= 744.96 when xabs = 744.96 sync B goto w1079; loc w1079: invariant xabs <= 745.16 when xabs = 745.16 sync C goto w1080; loc w1080: invariant xabs <= 745.44 when xabs = 745.44 sync B goto w1081; loc w1081: invariant xabs <= 745.68 when xabs = 745.68 sync C goto w1082; loc w1082: invariant xabs <= 745.92 when xabs = 745.92 sync B goto w1083; loc w1083: invariant xabs <= 746.16 when xabs = 746.16 sync C goto w1084; loc w1084: invariant xabs <= 746.4 when xabs = 746.4 sync B goto w1085; loc w1085: invariant xabs <= 746.64 when xabs = 746.64 sync C goto w1086; loc w1086: invariant xabs <= 746.92 when xabs = 746.92 sync B goto w1087; loc w1087: invariant xabs <= 747.12 when xabs = 747.12 sync C goto w1088; loc w1088: invariant xabs <= 747.44 when xabs = 747.44 sync B goto w1089; loc w1089: invariant xabs <= 747.6 when xabs = 747.6 sync C goto w1090; loc w1090: invariant xabs <= 747.92 when xabs = 747.92 sync B goto w1091; loc w1091: invariant xabs <= 748.12 when xabs = 748.12 sync C goto w1092; loc w1092: invariant xabs <= 748.4 when xabs = 748.4 sync B goto w1093; loc w1093: invariant xabs <= 748.6 when xabs = 748.6 sync C goto w1094; loc w1094: invariant xabs <= 748.88 when xabs = 748.88 sync B goto w1095; loc w1095: invariant xabs <= 749.12 when xabs = 749.12 sync C goto w1096; loc w1096: invariant xabs <= 749.36 when xabs = 749.36 sync B goto w1097; loc w1097: invariant xabs <= 749.6 when xabs = 749.6 sync C goto w1098; loc w1098: invariant xabs <= 749.84 when xabs = 749.84 sync B goto w1099; loc w1099: invariant xabs <= 750.08 when xabs = 750.08 sync C goto w1100; loc w1100: invariant xabs <= 750.36 when xabs = 750.36 sync B goto w1101; loc w1101: invariant xabs <= 750.56 when xabs = 750.56 sync C goto w1102; loc w1102: invariant xabs <= 750.88 when xabs = 750.88 sync B goto w1103; loc w1103: invariant xabs <= 751.36 when xabs = 751.36 sync C goto w1104; loc w1104: invariant xabs <= 751.52 when xabs = 751.52 sync D goto w1105; loc w1105: invariant xabs <= 751.84 when xabs = 751.84 sync C goto w1106; loc w1106: invariant xabs <= 752.04 when xabs = 752.04 sync D goto w1107; loc w1107: invariant xabs <= 752.32 when xabs = 752.32 sync C goto w1108; loc w1108: invariant xabs <= 752.52 when xabs = 752.52 sync D goto w1109; loc w1109: invariant xabs <= 752.8 when xabs = 752.8 sync C goto w1110; loc w1110: invariant xabs <= 753 when xabs = 753 sync D goto w1111; loc w1111: invariant xabs <= 753.32 when xabs = 753.32 sync C goto w1112; loc w1112: invariant xabs <= 753.48 when xabs = 753.48 sync D goto w1113; loc w1113: invariant xabs <= 753.84 when xabs = 753.84 sync C goto w1114; loc w1114: invariant xabs <= 753.96 when xabs = 753.96 sync D goto w1115; loc w1115: invariant xabs <= 754.32 when xabs = 754.32 sync C goto w1116; loc w1116: invariant xabs <= 754.44 when xabs = 754.44 sync D goto w1117; loc w1117: invariant xabs <= 754.8 when xabs = 754.8 sync C goto w1118; loc w1118: invariant xabs <= 754.96 when xabs = 754.96 sync D goto w1119; loc w1119: invariant xabs <= 755.24 when xabs = 755.24 sync C goto w1120; loc w1120: invariant xabs <= 755.44 when xabs = 755.44 sync D goto w1121; loc w1121: invariant xabs <= 755.76 when xabs = 755.76 sync C goto w1122; loc w1122: invariant xabs <= 755.92 when xabs = 755.92 sync D goto w1123; loc w1123: invariant xabs <= 756.24 when xabs = 756.24 sync C goto w1124; loc w1124: invariant xabs <= 756.4 when xabs = 756.4 sync D goto w1125; loc w1125: invariant xabs <= 756.76 when xabs = 756.76 sync C goto w1126; loc w1126: invariant xabs <= 756.88 when xabs = 756.88 sync D goto w1127; loc w1127: invariant xabs <= 757.24 when xabs = 757.24 sync C goto w1128; loc w1128: invariant xabs <= 757.36 when xabs = 757.36 sync D goto w1129; loc w1129: invariant xabs <= 757.72 when xabs = 757.72 sync C goto w1130; loc w1130: invariant xabs <= 757.88 when xabs = 757.88 sync D goto w1131; loc w1131: invariant xabs <= 758.2 when xabs = 758.2 sync C goto w1132; loc w1132: invariant xabs <= 758.32 when xabs = 758.32 sync B goto w1133; loc w1133: invariant xabs <= 761.16 when xabs = 761.16 sync A goto w1134; loc w1134: invariant xabs <= 761.28 when xabs = 761.28 sync B goto w1135; loc w1135: invariant xabs <= 761.64 when xabs = 761.64 sync A goto w1136; loc w1136: invariant xabs <= 761.8 when xabs = 761.8 sync B goto w1137; loc w1137: invariant xabs <= 762.12 when xabs = 762.12 sync A goto w1138; loc w1138: invariant xabs <= 762.28 when xabs = 762.28 sync B goto w1139; loc w1139: invariant xabs <= 762.64 when xabs = 762.64 sync A goto w1140; loc w1140: invariant xabs <= 762.76 when xabs = 762.76 sync B goto w1141; loc w1141: invariant xabs <= 763.32 when xabs = 763.32 sync A goto w1142; loc w1142: invariant xabs <= 764.6 when xabs = 764.6 sync B goto w1143; loc w1143: invariant xabs <= 765.08 when xabs = 765.08 sync C goto w1144; loc w1144: invariant xabs <= 765.2 when xabs = 765.2 sync D goto w1145; loc w1145: invariant xabs <= 767.56 when xabs = 767.56 sync C goto w1146; loc w1146: invariant xabs <= 767.68 when xabs = 767.68 sync D goto w1147; loc w1147: invariant xabs <= 768.04 when xabs = 768.04 sync C goto w1148; loc w1148: invariant xabs <= 778.28 when xabs = 778.28 sync D goto w1149; loc w1149: invariant xabs <= 778.4 when xabs = 778.4 sync C goto w1150; loc w1150: invariant xabs <= 778.52 when xabs = 778.52 sync B goto w1151; loc w1151: invariant xabs <= 781.48 when xabs = 781.48 sync A goto w1152; loc w1152: invariant xabs <= 782.88 when xabs = 782.88 sync B goto w1153; loc w1153: invariant xabs <= 786.28 when xabs = 786.28 sync C goto w1154; loc w1154: invariant xabs <= 798.32 when xabs = 798.32 sync D goto w1155; loc w1155: invariant xabs <= 798.44 when xabs = 798.44 sync C goto w1156; loc w1156: invariant xabs <= 798.64 when xabs = 798.64 sync B goto w1157; loc w1157: invariant xabs <= 801.08 when xabs = 801.08 sync A goto w1158; loc w1158: invariant xabs <= 802.24 when xabs = 802.24 sync B goto w1159; loc w1159: invariant xabs <= 804.84 when xabs = 804.84 sync C goto w1160; loc w1160: invariant xabs <= 818.32 when xabs = 818.32 sync D goto w1161; loc w1161: invariant xabs <= 818.44 when xabs = 818.44 sync C goto w1162; loc w1162: invariant xabs <= 818.56 when xabs = 818.56 sync B goto w1163; loc w1163: invariant xabs <= 821.32 when xabs = 821.32 sync A goto w1164; loc w1164: invariant xabs <= 823.36 when xabs = 823.36 sync B goto w1165; loc w1165: invariant xabs <= 826.56 when xabs = 826.56 sync C goto w1166; loc w1166: invariant xabs <= 838.28 when xabs = 838.28 sync D goto w1167; loc w1167: invariant xabs <= 838.4 when xabs = 838.4 sync C goto w1168; loc w1168: invariant xabs <= 838.56 when xabs = 838.56 sync B goto w1169; loc w1169: invariant xabs <= 840.96 when xabs = 840.96 sync A goto w1170; loc w1170: invariant xabs <= 841.12 when xabs = 841.12 sync B goto w1171; loc w1171: invariant xabs <= 842.44 when xabs = 842.44 sync A goto w1172; loc w1172: invariant xabs <= 842.92 when xabs = 842.92 sync B goto w1173; loc w1173: invariant xabs <= 843.08 when xabs = 843.08 sync C goto w1174; loc w1174: invariant xabs <= 843.4 when xabs = 843.4 sync B goto w1175; loc w1175: invariant xabs <= 843.6 when xabs = 843.6 sync C goto w1176; loc w1176: invariant xabs <= 843.88 when xabs = 843.88 sync B goto w1177; loc w1177: invariant xabs <= 844.08 when xabs = 844.08 sync C goto w1178; loc w1178: invariant xabs <= 844.4 when xabs = 844.4 sync B goto w1179; loc w1179: invariant xabs <= 844.56 when xabs = 844.56 sync C goto w1180; loc w1180: invariant xabs <= 845.4 when xabs = 845.4 sync B goto w1181; loc w1181: invariant xabs <= 845.84 when xabs = 845.84 sync C goto w1182; loc w1182: invariant xabs <= 846 when xabs = 846 sync D goto w1183; loc w1183: invariant xabs <= 846.32 when xabs = 846.32 sync C goto w1184; loc w1184: invariant xabs <= 846.52 when xabs = 846.52 sync D goto w1185; loc w1185: invariant xabs <= 846.84 when xabs = 846.84 sync C goto w1186; loc w1186: invariant xabs <= 847 when xabs = 847 sync D goto w1187; loc w1187: invariant xabs <= 847.32 when xabs = 847.32 sync C goto w1188; loc w1188: invariant xabs <= 847.48 when xabs = 847.48 sync D goto w1189; loc w1189: invariant xabs <= 847.84 when xabs = 847.84 sync C goto w1190; loc w1190: invariant xabs <= 847.96 when xabs = 847.96 sync D goto w1191; loc w1191: invariant xabs <= 848.32 when xabs = 848.32 sync C goto w1192; loc w1192: invariant xabs <= 848.48 when xabs = 848.48 sync D goto w1193; loc w1193: invariant xabs <= 848.8 when xabs = 848.8 sync C goto w1194; loc w1194: invariant xabs <= 848.96 when xabs = 848.96 sync D goto w1195; loc w1195: invariant xabs <= 849.28 when xabs = 849.28 sync C goto w1196; loc w1196: invariant xabs <= 849.48 when xabs = 849.48 sync D goto w1197; loc w1197: invariant xabs <= 849.76 when xabs = 849.76 sync C goto w1198; loc w1198: invariant xabs <= 849.96 when xabs = 849.96 sync D goto w1199; loc w1199: invariant xabs <= 850.24 when xabs = 850.24 sync C goto w1200; loc w1200: invariant xabs <= 850.44 when xabs = 850.44 sync D goto w1201; loc w1201: invariant xabs <= 850.76 when xabs = 850.76 sync C goto w1202; loc w1202: invariant xabs <= 850.92 when xabs = 850.92 sync D goto w1203; loc w1203: invariant xabs <= 851.24 when xabs = 851.24 sync C goto w1204; loc w1204: invariant xabs <= 851.4 when xabs = 851.4 sync D goto w1205; loc w1205: invariant xabs <= 851.72 when xabs = 851.72 sync C goto w1206; loc w1206: invariant xabs <= 851.92 when xabs = 851.92 sync D goto w1207; loc w1207: invariant xabs <= 852.2 when xabs = 852.2 sync C goto w1208; loc w1208: invariant xabs <= 852.4 when xabs = 852.4 sync D goto w1209; loc w1209: invariant xabs <= 852.68 when xabs = 852.68 sync C goto w1210; loc w1210: invariant xabs <= 852.92 when xabs = 852.92 sync D goto w1211; loc w1211: invariant xabs <= 853.16 when xabs = 853.16 sync C goto w1212; loc w1212: invariant xabs <= 853.4 when xabs = 853.4 sync D goto w1213; loc w1213: invariant xabs <= 853.68 when xabs = 853.68 sync C goto w1214; loc w1214: invariant xabs <= 853.88 when xabs = 853.88 sync D goto w1215; loc w1215: invariant xabs <= 854.16 when xabs = 854.16 sync C goto w1216; loc w1216: invariant xabs <= 854.36 when xabs = 854.36 sync D goto w1217; loc w1217: invariant xabs <= 854.68 when xabs = 854.68 sync C goto w1218; loc w1218: invariant xabs <= 854.84 when xabs = 854.84 sync D goto w1219; loc w1219: invariant xabs <= 855.16 when xabs = 855.16 sync C goto w1220; loc w1220: invariant xabs <= 855.36 when xabs = 855.36 sync D goto w1221; loc w1221: invariant xabs <= 855.6 when xabs = 855.6 sync C goto w1222; loc w1222: invariant xabs <= 855.84 when xabs = 855.84 sync D goto w1223; loc w1223: invariant xabs <= 856.08 when xabs = 856.08 sync C goto w1224; loc w1224: invariant xabs <= 856.36 when xabs = 856.36 sync D goto w1225; loc w1225: invariant xabs <= 856.6 when xabs = 856.6 sync C goto w1226; loc w1226: invariant xabs <= 856.84 when xabs = 856.84 sync D goto w1227; loc w1227: invariant xabs <= 857.08 when xabs = 857.08 sync C goto w1228; loc w1228: invariant xabs <= 857.32 when xabs = 857.32 sync D goto w1229; loc w1229: invariant xabs <= 857.6 when xabs = 857.6 sync C goto w1230; loc w1230: invariant xabs <= 857.8 when xabs = 857.8 sync D goto w1231; loc w1231: invariant xabs <= 858.2 when xabs = 858.2 sync C goto w1232; loc w1232: invariant xabs <= 858.32 when xabs = 858.32 sync B goto w1233; loc w1233: invariant xabs <= 861.48 when xabs = 861.48 sync A goto w1234; loc w1234: invariant xabs <= 861.72 when xabs = 861.72 sync B goto w1235; loc w1235: invariant xabs <= 861.96 when xabs = 861.96 sync A goto w1236; loc w1236: invariant xabs <= 862.24 when xabs = 862.24 sync B goto w1237; loc w1237: invariant xabs <= 862.44 when xabs = 862.44 sync A goto w1238; loc w1238: invariant xabs <= 862.72 when xabs = 862.72 sync B goto w1239; loc w1239: invariant xabs <= 862.96 when xabs = 862.96 sync A goto w1240; loc w1240: invariant xabs <= 863.2 when xabs = 863.2 sync B goto w1241; loc w1241: invariant xabs <= 863.44 when xabs = 863.44 sync A goto w1242; loc w1242: invariant xabs <= 863.68 when xabs = 863.68 sync B goto w1243; loc w1243: invariant xabs <= 863.96 when xabs = 863.96 sync A goto w1244; loc w1244: invariant xabs <= 864.16 when xabs = 864.16 sync B goto w1245; loc w1245: invariant xabs <= 864.44 when xabs = 864.44 sync A goto w1246; loc w1246: invariant xabs <= 864.68 when xabs = 864.68 sync B goto w1247; loc w1247: invariant xabs <= 864.92 when xabs = 864.92 sync A goto w1248; loc w1248: invariant xabs <= 865.2 when xabs = 865.2 sync B goto w1249; loc w1249: invariant xabs <= 865.4 when xabs = 865.4 sync A goto w1250; loc w1250: invariant xabs <= 865.68 when xabs = 865.68 sync B goto w1251; loc w1251: invariant xabs <= 865.88 when xabs = 865.88 sync A goto w1252; loc w1252: invariant xabs <= 866.16 when xabs = 866.16 sync B goto w1253; loc w1253: invariant xabs <= 866.36 when xabs = 866.36 sync A goto w1254; loc w1254: invariant xabs <= 866.64 when xabs = 866.64 sync B goto w1255; loc w1255: invariant xabs <= 866.88 when xabs = 866.88 sync A goto w1256; loc w1256: invariant xabs <= 867.12 when xabs = 867.12 sync B goto w1257; loc w1257: invariant xabs <= 867.36 when xabs = 867.36 sync A goto w1258; loc w1258: invariant xabs <= 867.6 when xabs = 867.6 sync B goto w1259; loc w1259: invariant xabs <= 867.84 when xabs = 867.84 sync A goto w1260; loc w1260: invariant xabs <= 868.12 when xabs = 868.12 sync B goto w1261; loc w1261: invariant xabs <= 868.32 when xabs = 868.32 sync A goto w1262; loc w1262: invariant xabs <= 868.64 when xabs = 868.64 sync B goto w1263; loc w1263: invariant xabs <= 868.8 when xabs = 868.8 sync A goto w1264; loc w1264: invariant xabs <= 869.12 when xabs = 869.12 sync B goto w1265; loc w1265: invariant xabs <= 869.28 when xabs = 869.28 sync A goto w1266; loc w1266: invariant xabs <= 869.6 when xabs = 869.6 sync B goto w1267; loc w1267: invariant xabs <= 869.8 when xabs = 869.8 sync A goto w1268; loc w1268: invariant xabs <= 870.08 when xabs = 870.08 sync B goto w1269; loc w1269: invariant xabs <= 870.28 when xabs = 870.28 sync A goto w1270; loc w1270: invariant xabs <= 870.56 when xabs = 870.56 sync B goto w1271; loc w1271: invariant xabs <= 870.76 when xabs = 870.76 sync A goto w1272; loc w1272: invariant xabs <= 871.04 when xabs = 871.04 sync B goto w1273; loc w1273: invariant xabs <= 871.24 when xabs = 871.24 sync A goto w1274; loc w1274: invariant xabs <= 871.36 when xabs = 871.36 sync B goto w1275; loc w1275: invariant xabs <= 871.56 when xabs = 871.56 sync C goto w1276; loc w1276: invariant xabs <= 871.72 when xabs = 871.72 sync B goto w1277; loc w1277: invariant xabs <= 872.04 when xabs = 872.04 sync C goto w1278; loc w1278: invariant xabs <= 872.52 when xabs = 872.52 sync B goto w1279; loc w1279: invariant xabs <= 872.72 when xabs = 872.72 sync A goto w1280; loc w1280: invariant xabs <= 873 when xabs = 873 sync B goto w1281; loc w1281: invariant xabs <= 873.24 when xabs = 873.24 sync A goto w1282; loc w1282: invariant xabs <= 873.48 when xabs = 873.48 sync B goto w1283; loc w1283: invariant xabs <= 873.72 when xabs = 873.72 sync A goto w1284; loc w1284: invariant xabs <= 874 when xabs = 874 sync B goto w1285; loc w1285: invariant xabs <= 874.2 when xabs = 874.2 sync A goto w1286; loc w1286: invariant xabs <= 874.52 when xabs = 874.52 sync B goto w1287; loc w1287: invariant xabs <= 874.68 when xabs = 874.68 sync A goto w1288; loc w1288: invariant xabs <= 875 when xabs = 875 sync B goto w1289; loc w1289: invariant xabs <= 875.16 when xabs = 875.16 sync A goto w1290; loc w1290: invariant xabs <= 875.48 when xabs = 875.48 sync B goto w1291; loc w1291: invariant xabs <= 875.64 when xabs = 875.64 sync A goto w1292; loc w1292: invariant xabs <= 875.96 when xabs = 875.96 sync B goto w1293; loc w1293: invariant xabs <= 876.16 when xabs = 876.16 sync A goto w1294; loc w1294: invariant xabs <= 876.44 when xabs = 876.44 sync B goto w1295; loc w1295: invariant xabs <= 876.64 when xabs = 876.64 sync A goto w1296; loc w1296: invariant xabs <= 876.92 when xabs = 876.92 sync B goto w1297; loc w1297: invariant xabs <= 877.12 when xabs = 877.12 sync A goto w1298; loc w1298: invariant xabs <= 877.44 when xabs = 877.44 sync B goto w1299; loc w1299: invariant xabs <= 877.6 when xabs = 877.6 sync A goto w1300; loc w1300: invariant xabs <= 877.96 when xabs = 877.96 sync B goto w1301; loc w1301: invariant xabs <= 878.08 when xabs = 878.08 sync A goto w1302; loc w1302: invariant xabs <= 878.28 when xabs = 878.28 sync B goto w1303; loc w1303: invariant xabs <= 883 when xabs = 883 sync A goto w1304; loc w1304: invariant xabs <= 883.32 when xabs = 883.32 sync B goto w1305; loc w1305: invariant xabs <= 883.48 when xabs = 883.48 sync A goto w1306; loc w1306: invariant xabs <= 883.8 when xabs = 883.8 sync B goto w1307; loc w1307: invariant xabs <= 883.96 when xabs = 883.96 sync A goto w1308; loc w1308: invariant xabs <= 884.32 when xabs = 884.32 sync B goto w1309; loc w1309: invariant xabs <= 884.44 when xabs = 884.44 sync A goto w1310; loc w1310: invariant xabs <= 884.8 when xabs = 884.8 sync B goto w1311; loc w1311: invariant xabs <= 884.96 when xabs = 884.96 sync A goto w1312; loc w1312: invariant xabs <= 885.28 when xabs = 885.28 sync B goto w1313; loc w1313: invariant xabs <= 886 when xabs = 886 sync A goto w1314; loc w1314: invariant xabs <= 886.24 when xabs = 886.24 sync B goto w1315; loc w1315: invariant xabs <= 886.44 when xabs = 886.44 sync A goto w1316; loc w1316: invariant xabs <= 886.76 when xabs = 886.76 sync B goto w1317; loc w1317: invariant xabs <= 886.92 when xabs = 886.92 sync A goto w1318; loc w1318: invariant xabs <= 887.24 when xabs = 887.24 sync B goto w1319; loc w1319: invariant xabs <= 887.4 when xabs = 887.4 sync A goto w1320; loc w1320: invariant xabs <= 887.76 when xabs = 887.76 sync B goto w1321; loc w1321: invariant xabs <= 887.88 when xabs = 887.88 sync A goto w1322; loc w1322: invariant xabs <= 888.24 when xabs = 888.24 sync B goto w1323; loc w1323: invariant xabs <= 888.4 when xabs = 888.4 sync A goto w1324; loc w1324: invariant xabs <= 888.72 when xabs = 888.72 sync B goto w1325; loc w1325: invariant xabs <= 888.88 when xabs = 888.88 sync A goto w1326; loc w1326: invariant xabs <= 889.2 when xabs = 889.2 sync B goto w1327; loc w1327: invariant xabs <= 889.36 when xabs = 889.36 sync A goto w1328; loc w1328: invariant xabs <= 889.68 when xabs = 889.68 sync B goto w1329; loc w1329: invariant xabs <= 889.84 when xabs = 889.84 sync A goto w1330; loc w1330: invariant xabs <= 890.2 when xabs = 890.2 sync B goto w1331; loc w1331: invariant xabs <= 890.32 when xabs = 890.32 sync A goto w1332; loc w1332: invariant xabs <= 891.16 when xabs = 891.16 sync B goto w1333; loc w1333: invariant xabs <= 891.32 when xabs = 891.32 sync A goto w1334; loc w1334: invariant xabs <= 891.64 when xabs = 891.64 sync B goto w1335; loc w1335: invariant xabs <= 892.36 when xabs = 892.36 sync A goto w1336; loc w1336: invariant xabs <= 892.6 when xabs = 892.6 sync B goto w1337; loc w1337: invariant xabs <= 895.72 when xabs = 895.72 sync A goto w1338; loc w1338: invariant xabs <= 896.04 when xabs = 896.04 sync B goto w1339; loc w1339: invariant xabs <= 896.2 when xabs = 896.2 sync A goto w1340; loc w1340: invariant xabs <= 896.56 when xabs = 896.56 sync B goto w1341; loc w1341: invariant xabs <= 896.68 when xabs = 896.68 sync A goto w1342; loc w1342: invariant xabs <= 897.04 when xabs = 897.04 sync B goto w1343; loc w1343: invariant xabs <= 921.2 when xabs = 921.2 sync A goto w1344; loc w1344: invariant xabs <= 921.48 when xabs = 921.48 sync B goto w1345; loc w1345: invariant xabs <= 921.68 when xabs = 921.68 sync A goto w1346; loc w1346: invariant xabs <= 922 when xabs = 922 sync B goto w1347; loc w1347: invariant xabs <= 922.16 when xabs = 922.16 sync A goto w1348; loc w1348: invariant xabs <= 922.48 when xabs = 922.48 sync B goto w1349; loc w1349: invariant xabs <= 922.68 when xabs = 922.68 sync A goto w1350; loc w1350: invariant xabs <= 922.96 when xabs = 922.96 sync B goto w1351; loc w1351: invariant xabs <= 923.2 when xabs = 923.2 sync A goto w1352; loc w1352: invariant xabs <= 923.44 when xabs = 923.44 sync B goto w1353; loc w1353: invariant xabs <= 923.68 when xabs = 923.68 sync A goto w1354; loc w1354: invariant xabs <= 923.92 when xabs = 923.92 sync B goto w1355; loc w1355: invariant xabs <= 924.16 when xabs = 924.16 sync A goto w1356; loc w1356: invariant xabs <= 924.4 when xabs = 924.4 sync B goto w1357; loc w1357: invariant xabs <= 924.64 when xabs = 924.64 sync A goto w1358; loc w1358: invariant xabs <= 924.92 when xabs = 924.92 sync B goto w1359; loc w1359: invariant xabs <= 925.12 when xabs = 925.12 sync A goto w1360; loc w1360: invariant xabs <= 925.4 when xabs = 925.4 sync B goto w1361; loc w1361: invariant xabs <= 925.6 when xabs = 925.6 sync A goto w1362; loc w1362: invariant xabs <= 925.88 when xabs = 925.88 sync B goto w1363; loc w1363: invariant xabs <= 926.12 when xabs = 926.12 sync A goto w1364; loc w1364: invariant xabs <= 926.36 when xabs = 926.36 sync B goto w1365; loc w1365: invariant xabs <= 926.6 when xabs = 926.6 sync A goto w1366; loc w1366: invariant xabs <= 926.84 when xabs = 926.84 sync B goto w1367; loc w1367: invariant xabs <= 927.12 when xabs = 927.12 sync A goto w1368; loc w1368: invariant xabs <= 927.36 when xabs = 927.36 sync B goto w1369; loc w1369: invariant xabs <= 927.6 when xabs = 927.6 sync A goto w1370; loc w1370: invariant xabs <= 927.72 when xabs = 927.72 sync B goto w1371; loc w1371: invariant xabs <= 927.84 when xabs = 927.84 sync C goto w1372; loc w1372: invariant xabs <= 928.08 when xabs = 928.08 sync B goto w1373; loc w1373: invariant xabs <= 928.32 when xabs = 928.32 sync C goto w1374; loc w1374: invariant xabs <= 928.56 when xabs = 928.56 sync B goto w1375; loc w1375: invariant xabs <= 928.84 when xabs = 928.84 sync C goto w1376; loc w1376: invariant xabs <= 929.04 when xabs = 929.04 sync B goto w1377; loc w1377: invariant xabs <= 929.32 when xabs = 929.32 sync C goto w1378; loc w1378: invariant xabs <= 929.56 when xabs = 929.56 sync B goto w1379; loc w1379: invariant xabs <= 929.76 when xabs = 929.76 sync C goto w1380; loc w1380: invariant xabs <= 930.04 when xabs = 930.04 sync B goto w1381; loc w1381: invariant xabs <= 930.28 when xabs = 930.28 sync C goto w1382; loc w1382: invariant xabs <= 930.52 when xabs = 930.52 sync B goto w1383; loc w1383: invariant xabs <= 930.76 when xabs = 930.76 sync C goto w1384; loc w1384: invariant xabs <= 931 when xabs = 931 sync B goto w1385; loc w1385: invariant xabs <= 931.28 when xabs = 931.28 sync C goto w1386; loc w1386: invariant xabs <= 931.52 when xabs = 931.52 sync B goto w1387; loc w1387: invariant xabs <= 931.76 when xabs = 931.76 sync C goto w1388; loc w1388: invariant xabs <= 932 when xabs = 932 sync B goto w1389; loc w1389: invariant xabs <= 932.24 when xabs = 932.24 sync C goto w1390; loc w1390: invariant xabs <= 932.52 when xabs = 932.52 sync B goto w1391; loc w1391: invariant xabs <= 932.72 when xabs = 932.72 sync C goto w1392; loc w1392: invariant xabs <= 933 when xabs = 933 sync B goto w1393; loc w1393: invariant xabs <= 933.2 when xabs = 933.2 sync C goto w1394; loc w1394: invariant xabs <= 933.48 when xabs = 933.48 sync B goto w1395; loc w1395: invariant xabs <= 933.68 when xabs = 933.68 sync C goto w1396; loc w1396: invariant xabs <= 933.96 when xabs = 933.96 sync B goto w1397; loc w1397: invariant xabs <= 934.2 when xabs = 934.2 sync C goto w1398; loc w1398: invariant xabs <= 934.44 when xabs = 934.44 sync B goto w1399; loc w1399: invariant xabs <= 934.68 when xabs = 934.68 sync C goto w1400; loc w1400: invariant xabs <= 934.92 when xabs = 934.92 sync B goto w1401; loc w1401: invariant xabs <= 935.2 when xabs = 935.2 sync C goto w1402; loc w1402: invariant xabs <= 935.44 when xabs = 935.44 sync B goto w1403; loc w1403: invariant xabs <= 935.64 when xabs = 935.64 sync C goto w1404; loc w1404: invariant xabs <= 935.96 when xabs = 935.96 sync B goto w1405; loc w1405: invariant xabs <= 936.12 when xabs = 936.12 sync C goto w1406; loc w1406: invariant xabs <= 936.44 when xabs = 936.44 sync B goto w1407; loc w1407: invariant xabs <= 936.6 when xabs = 936.6 sync C goto w1408; loc w1408: invariant xabs <= 936.92 when xabs = 936.92 sync B goto w1409; loc w1409: invariant xabs <= 937.12 when xabs = 937.12 sync C goto w1410; loc w1410: invariant xabs <= 937.4 when xabs = 937.4 sync B goto w1411; loc w1411: invariant xabs <= 937.64 when xabs = 937.64 sync C goto w1412; loc w1412: invariant xabs <= 937.88 when xabs = 937.88 sync B goto w1413; loc w1413: invariant xabs <= 938.16 when xabs = 938.16 sync C goto w1414; loc w1414: invariant xabs <= 938.28 when xabs = 938.28 sync B goto w1415; loc w1415: invariant xabs <= 940.88 when xabs = 940.88 sync A goto w1416; loc w1416: invariant xabs <= 941.04 when xabs = 941.04 sync B goto w1417; loc w1417: invariant xabs <= 941.32 when xabs = 941.32 sync A goto w1418; loc w1418: invariant xabs <= 941.52 when xabs = 941.52 sync B goto w1419; loc w1419: invariant xabs <= 941.84 when xabs = 941.84 sync A goto w1420; loc w1420: invariant xabs <= 942 when xabs = 942 sync B goto w1421; loc w1421: invariant xabs <= 942.32 when xabs = 942.32 sync A goto w1422; loc w1422: invariant xabs <= 942.48 when xabs = 942.48 sync B goto w1423; loc w1423: invariant xabs <= 942.84 when xabs = 942.84 sync A goto w1424; loc w1424: invariant xabs <= 942.96 when xabs = 942.96 sync B goto w1425; loc w1425: invariant xabs <= 943.32 when xabs = 943.32 sync A goto w1426; loc w1426: invariant xabs <= 943.48 when xabs = 943.48 sync B goto w1427; loc w1427: invariant xabs <= 943.76 when xabs = 943.76 sync A goto w1428; loc w1428: invariant xabs <= 943.96 when xabs = 943.96 sync B goto w1429; loc w1429: invariant xabs <= 944.24 when xabs = 944.24 sync A goto w1430; loc w1430: invariant xabs <= 944.76 when xabs = 944.76 sync B goto w1431; loc w1431: invariant xabs <= 944.92 when xabs = 944.92 sync C goto w1432; loc w1432: invariant xabs <= 945.28 when xabs = 945.28 sync B goto w1433; loc w1433: invariant xabs <= 945.4 when xabs = 945.4 sync C goto w1434; loc w1434: invariant xabs <= 945.76 when xabs = 945.76 sync B goto w1435; loc w1435: invariant xabs <= 945.88 when xabs = 945.88 sync C goto w1436; loc w1436: invariant xabs <= 946.24 when xabs = 946.24 sync B goto w1437; loc w1437: invariant xabs <= 946.72 when xabs = 946.72 sync C goto w1438; loc w1438: invariant xabs <= 946.88 when xabs = 946.88 sync D goto w1439; loc w1439: invariant xabs <= 947.2 when xabs = 947.2 sync C goto w1440; loc w1440: invariant xabs <= 947.4 when xabs = 947.4 sync D goto w1441; loc w1441: invariant xabs <= 947.72 when xabs = 947.72 sync C goto w1442; loc w1442: invariant xabs <= 947.88 when xabs = 947.88 sync D goto w1443; loc w1443: invariant xabs <= 949.68 when xabs = 949.68 sync C goto w1444; loc w1444: invariant xabs <= 949.8 when xabs = 949.8 sync D goto w1445; loc w1445: invariant xabs <= 950.16 when xabs = 950.16 sync C goto w1446; loc w1446: invariant xabs <= 950.32 when xabs = 950.32 sync D goto w1447; loc w1447: invariant xabs <= 950.64 when xabs = 950.64 sync C goto w1448; loc w1448: invariant xabs <= 950.8 when xabs = 950.8 sync D goto w1449; loc w1449: invariant xabs <= 951.16 when xabs = 951.16 sync C goto w1450; loc w1450: invariant xabs <= 951.28 when xabs = 951.28 sync D goto w1451; loc w1451: invariant xabs <= 953.12 when xabs = 953.12 sync C goto w1452; loc w1452: invariant xabs <= 958.24 when xabs = 958.24 sync D goto w1453; loc w1453: invariant xabs <= 958.36 when xabs = 958.36 sync C goto w1454; loc w1454: invariant xabs <= 958.52 when xabs = 958.52 sync B goto w1455; loc w1455: invariant xabs <= 961.56 when xabs = 961.56 sync A goto w1456; loc w1456: invariant xabs <= 963.72 when xabs = 963.72 sync B goto w1457; loc w1457: invariant xabs <= 966.76 when xabs = 966.76 sync C goto w1458; loc w1458: invariant xabs <= 978.32 when xabs = 978.32 sync D goto w1459; loc w1459: invariant xabs <= 978.44 when xabs = 978.44 sync C goto w1460; loc w1460: invariant xabs <= 978.56 when xabs = 978.56 sync B goto w1461; loc w1461: invariant xabs <= 981.32 when xabs = 981.32 sync A goto w1462; loc w1462: invariant xabs <= 982.8 when xabs = 982.8 sync B goto w1463; loc w1463: invariant xabs <= 984.88 when xabs = 984.88 sync C goto w1464; loc w1464: invariant xabs <= 998.32 when xabs = 998.32 sync D goto w1465; loc w1465: invariant xabs <= 998.44 when xabs = 998.44 sync C goto w1466; loc w1466: invariant xabs <= 998.56 when xabs = 998.56 sync B goto w1467; loc w1467: invariant xabs <= 1000 when xabs = 1000 sync A goto w1468; loc w1468: invariant True end (* word *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = pre_s0 & loc[word] = w1 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & xabs = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & p1 >= 0 & t >= 0 & tprime >= 0 ; (************************************************************) (* The end *) (************************************************************) end