(************************************************************ * IMITATOR MODEL * * Parametric timed pattern matching benchmark: blowup (designed on purpose to test the limits of our algorithm) * * Description : Template of a timed word alternating between a and c * Correctness : N/A * Source : Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018) * Author : Étienne André and Masaki Waga * Modeling : Étienne André and Masaki Waga * Input by : Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : 2018/03/07 * Last modified : 2020/08/18 * * IMITATOR version: 3 ************************************************************) var (* Clocks *) x, y, xabs : clock; (* Parameters *) p1, p2, p3, t, tprime : parameter; (************************************************************) automaton pta (************************************************************) synclabs: a, b, dollar, start; loc pre_s0: invariant True (* First try immediately the pattern in 0-time *) when xabs = 0 & xabs = t sync start goto s0; (* Otherwise: first skip some letter and wait *) when True sync a do {x := 0, y := 0} goto pre_s0_prime; when True sync b do {x := 0, y := 0} goto pre_s0_prime; loc pre_s0_prime: invariant True (* Skip some more letter and wait *) when True sync a do {x := 0, y := 0} goto pre_s0_prime; when True sync b do {x := 0, y := 0} goto pre_s0_prime; (* Or decide to start the pattern *) when t = xabs & x > 0 do {x := 0, y := 0} sync start goto s0; loc s0: invariant True when True sync a do {y := 0} goto s1; loc s1: invariant True when x < p1 sync b goto s2; loc s2: invariant True when x = p1 & xabs = tprime do {x := 0} sync dollar goto soon_end; when p3 <= y & y < p2 do {y := 0} sync a goto s1; loc soon_end: invariant True when x > 0 goto s3; urgent loc s3: invariant True end (* pta *) (************************************************************) automaton word (************************************************************) synclabs: a, b; (* BEGIN AUTOMATICALLY GENERATED *) loc w0: invariant xabs <= 5/100 when xabs = 5/100 sync a goto w1; loc w1: invariant xabs <= 9/100 when xabs = 9/100 sync b goto w2; loc w2: invariant xabs <= 12/100 when xabs = 12/100 sync a goto w3; loc w3: invariant xabs <= 16/100 when xabs = 16/100 sync b goto w4; loc w4: invariant xabs <= 19/100 when xabs = 19/100 sync a goto w5; loc w5: invariant xabs <= 28/100 when xabs = 28/100 sync b goto w6; loc w6: invariant xabs <= 34/100 when xabs = 34/100 sync a goto w7; loc w7: invariant xabs <= 38/100 when xabs = 38/100 sync b goto w8; loc w8: invariant xabs <= 41/100 when xabs = 41/100 sync a goto w9; loc w9: invariant xabs <= 46/100 when xabs = 46/100 sync b goto w10; loc w10: invariant xabs <= 54/100 when xabs = 54/100 sync a goto w11; loc w11: invariant xabs <= 58/100 when xabs = 58/100 sync b goto w12; loc w12: invariant xabs <= 67/100 when xabs = 67/100 sync a goto w13; loc w13: invariant xabs <= 76/100 when xabs = 76/100 sync b goto w14; loc w14: invariant xabs <= 84/100 when xabs = 84/100 sync a goto w15; loc w15: invariant xabs <= 86/100 when xabs = 86/100 sync b goto w16; loc w16: invariant xabs <= 88/100 when xabs = 88/100 sync a goto w17; loc w17: invariant xabs <= 94/100 when xabs = 94/100 sync b goto w18; loc w18: invariant xabs <= 96/100 when xabs = 96/100 sync a goto w19; loc w19: invariant xabs <= 103/100 when xabs = 103/100 sync b goto w20; loc w20: invariant xabs <= 106/100 when xabs = 106/100 sync a goto w21; loc w21: invariant xabs <= 112/100 when xabs = 112/100 sync b goto w22; loc w22: invariant xabs <= 119/100 when xabs = 119/100 sync a goto w23; loc w23: invariant xabs <= 127/100 when xabs = 127/100 sync b goto w24; loc w24: invariant xabs <= 129/100 when xabs = 129/100 sync a goto w25; loc w25: invariant xabs <= 135/100 when xabs = 135/100 sync b goto w26; loc w26: invariant xabs <= 140/100 when xabs = 140/100 sync a goto w27; loc w27: invariant xabs <= 146/100 when xabs = 146/100 sync b goto w28; loc w28: invariant xabs <= 149/100 when xabs = 149/100 sync a goto w29; loc w29: invariant xabs <= 152/100 when xabs = 152/100 sync b goto w30; loc w30: invariant xabs <= 154/100 when xabs = 154/100 sync a goto w31; loc w31: invariant xabs <= 158/100 when xabs = 158/100 sync b goto w32; loc w32: invariant xabs <= 167/100 when xabs = 167/100 sync a goto w33; loc w33: invariant xabs <= 175/100 when xabs = 175/100 sync b goto w34; loc w34: invariant xabs <= 180/100 when xabs = 180/100 sync a goto w35; loc w35: invariant xabs <= 186/100 when xabs = 186/100 sync b goto w36; loc w36: invariant xabs <= 189/100 when xabs = 189/100 sync a goto w37; loc w37: invariant xabs <= 190/100 when xabs = 190/100 sync b goto w38; loc w38: invariant xabs <= 199/100 when xabs = 199/100 sync a goto w39; loc w39: invariant xabs <= 207/100 when xabs = 207/100 sync b goto w40; loc w40: invariant xabs <= 210/100 when xabs = 210/100 sync a goto w41; loc w41: invariant xabs <= 211/100 when xabs = 211/100 sync b goto w42; loc w42: invariant xabs <= 217/100 when xabs = 217/100 sync a goto w43; loc w43: invariant xabs <= 218/100 when xabs = 218/100 sync b goto w44; loc w44: invariant xabs <= 220/100 when xabs = 220/100 sync a goto w45; loc w45: invariant xabs <= 221/100 when xabs = 221/100 sync b goto w46; loc w46: invariant xabs <= 224/100 when xabs = 224/100 sync a goto w47; loc w47: invariant xabs <= 225/100 when xabs = 225/100 sync b goto w48; loc w48: invariant xabs <= 233/100 when xabs = 233/100 sync a goto w49; loc w49: invariant xabs <= 237/100 when xabs = 237/100 sync b goto w50; loc w50: invariant xabs <= 243/100 when xabs = 243/100 sync a goto w51; loc w51: invariant xabs <= 245/100 when xabs = 245/100 sync b goto w52; loc w52: invariant xabs <= 254/100 when xabs = 254/100 sync a goto w53; loc w53: invariant xabs <= 257/100 when xabs = 257/100 sync b goto w54; loc w54: invariant xabs <= 265/100 when xabs = 265/100 sync a goto w55; loc w55: invariant xabs <= 273/100 when xabs = 273/100 sync b goto w56; loc w56: invariant xabs <= 282/100 when xabs = 282/100 sync a goto w57; loc w57: invariant xabs <= 288/100 when xabs = 288/100 sync b goto w58; loc w58: invariant xabs <= 291/100 when xabs = 291/100 sync a goto w59; loc w59: invariant xabs <= 292/100 when xabs = 292/100 sync b goto w60; loc w60: invariant xabs <= 297/100 when xabs = 297/100 sync a goto w61; loc w61: invariant xabs <= 302/100 when xabs = 302/100 sync b goto w62; loc w62: invariant xabs <= 308/100 when xabs = 308/100 sync a goto w63; loc w63: invariant xabs <= 317/100 when xabs = 317/100 sync b goto w64; loc w64: invariant xabs <= 320/100 when xabs = 320/100 sync a goto w65; loc w65: invariant xabs <= 329/100 when xabs = 329/100 sync b goto w66; loc w66: invariant xabs <= 333/100 when xabs = 333/100 sync a goto w67; loc w67: invariant xabs <= 342/100 when xabs = 342/100 sync b goto w68; loc w68: invariant xabs <= 351/100 when xabs = 351/100 sync a goto w69; loc w69: invariant xabs <= 358/100 when xabs = 358/100 sync b goto w70; loc w70: invariant xabs <= 367/100 when xabs = 367/100 sync a goto w71; loc w71: invariant xabs <= 374/100 when xabs = 374/100 sync b goto w72; loc w72: invariant xabs <= 377/100 when xabs = 377/100 sync a goto w73; loc w73: invariant xabs <= 383/100 when xabs = 383/100 sync b goto w74; loc w74: invariant xabs <= 392/100 when xabs = 392/100 sync a goto w75; loc w75: invariant xabs <= 395/100 when xabs = 395/100 sync b goto w76; loc w76: invariant xabs <= 403/100 when xabs = 403/100 sync a goto w77; loc w77: invariant xabs <= 408/100 when xabs = 408/100 sync b goto w78; loc w78: invariant xabs <= 409/100 when xabs = 409/100 sync a goto w79; loc w79: invariant xabs <= 414/100 when xabs = 414/100 sync b goto w80; loc w80: invariant xabs <= 415/100 when xabs = 415/100 sync a goto w81; loc w81: invariant xabs <= 420/100 when xabs = 420/100 sync b goto w82; loc w82: invariant xabs <= 421/100 when xabs = 421/100 sync a goto w83; loc w83: invariant xabs <= 423/100 when xabs = 423/100 sync b goto w84; loc w84: invariant xabs <= 428/100 when xabs = 428/100 sync a goto w85; loc w85: invariant xabs <= 431/100 when xabs = 431/100 sync b goto w86; loc w86: invariant xabs <= 434/100 when xabs = 434/100 sync a goto w87; loc w87: invariant xabs <= 443/100 when xabs = 443/100 sync b goto w88; loc w88: invariant xabs <= 449/100 when xabs = 449/100 sync a goto w89; loc w89: invariant xabs <= 455/100 when xabs = 455/100 sync b goto w90; loc w90: invariant xabs <= 457/100 when xabs = 457/100 sync a goto w91; loc w91: invariant xabs <= 465/100 when xabs = 465/100 sync b goto w92; loc w92: invariant xabs <= 466/100 when xabs = 466/100 sync a goto w93; loc w93: invariant xabs <= 467/100 when xabs = 467/100 sync b goto w94; loc w94: invariant xabs <= 471/100 when xabs = 471/100 sync a goto w95; loc w95: invariant xabs <= 480/100 when xabs = 480/100 sync b goto w96; loc w96: invariant xabs <= 485/100 when xabs = 485/100 sync a goto w97; loc w97: invariant xabs <= 490/100 when xabs = 490/100 sync b goto w98; loc w98: invariant xabs <= 499/100 when xabs = 499/100 sync a goto w99; loc w99: invariant xabs <= 502/100 when xabs = 502/100 sync b goto w100; loc w100: invariant xabs <= 504/100 when xabs = 504/100 sync a goto w101; loc w101: invariant xabs <= 509/100 when xabs = 509/100 sync b goto w102; loc w102: invariant xabs <= 515/100 when xabs = 515/100 sync a goto w103; loc w103: invariant xabs <= 522/100 when xabs = 522/100 sync b goto w104; loc w104: invariant xabs <= 527/100 when xabs = 527/100 sync a goto w105; loc w105: invariant xabs <= 534/100 when xabs = 534/100 sync b goto w106; loc w106: invariant xabs <= 540/100 when xabs = 540/100 sync a goto w107; loc w107: invariant xabs <= 549/100 when xabs = 549/100 sync b goto w108; loc w108: invariant xabs <= 552/100 when xabs = 552/100 sync a goto w109; loc w109: invariant xabs <= 553/100 when xabs = 553/100 sync b goto w110; loc w110: invariant xabs <= 557/100 when xabs = 557/100 sync a goto w111; loc w111: invariant xabs <= 561/100 when xabs = 561/100 sync b goto w112; loc w112: invariant xabs <= 570/100 when xabs = 570/100 sync a goto w113; loc w113: invariant xabs <= 576/100 when xabs = 576/100 sync b goto w114; loc w114: invariant xabs <= 577/100 when xabs = 577/100 sync a goto w115; loc w115: invariant xabs <= 578/100 when xabs = 578/100 sync b goto w116; loc w116: invariant xabs <= 586/100 when xabs = 586/100 sync a goto w117; loc w117: invariant xabs <= 594/100 when xabs = 594/100 sync b goto w118; loc w118: invariant xabs <= 595/100 when xabs = 595/100 sync a goto w119; loc w119: invariant xabs <= 596/100 when xabs = 596/100 sync b goto w120; loc w120: invariant xabs <= 600/100 when xabs = 600/100 sync a goto w121; loc w121: invariant xabs <= 602/100 when xabs = 602/100 sync b goto w122; loc w122: invariant xabs <= 606/100 when xabs = 606/100 sync a goto w123; loc w123: invariant xabs <= 613/100 when xabs = 613/100 sync b goto w124; loc w124: invariant xabs <= 615/100 when xabs = 615/100 sync a goto w125; loc w125: invariant xabs <= 617/100 when xabs = 617/100 sync b goto w126; loc w126: invariant xabs <= 618/100 when xabs = 618/100 sync a goto w127; loc w127: invariant xabs <= 619/100 when xabs = 619/100 sync b goto w128; loc w128: invariant xabs <= 627/100 when xabs = 627/100 sync a goto w129; loc w129: invariant xabs <= 628/100 when xabs = 628/100 sync b goto w130; loc w130: invariant xabs <= 633/100 when xabs = 633/100 sync a goto w131; loc w131: invariant xabs <= 641/100 when xabs = 641/100 sync b goto w132; loc w132: invariant xabs <= 646/100 when xabs = 646/100 sync a goto w133; loc w133: invariant xabs <= 654/100 when xabs = 654/100 sync b goto w134; loc w134: invariant xabs <= 661/100 when xabs = 661/100 sync a goto w135; loc w135: invariant xabs <= 667/100 when xabs = 667/100 sync b goto w136; loc w136: invariant xabs <= 671/100 when xabs = 671/100 sync a goto w137; loc w137: invariant xabs <= 678/100 when xabs = 678/100 sync b goto w138; loc w138: invariant xabs <= 684/100 when xabs = 684/100 sync a goto w139; loc w139: invariant xabs <= 689/100 when xabs = 689/100 sync b goto w140; loc w140: invariant xabs <= 698/100 when xabs = 698/100 sync a goto w141; loc w141: invariant xabs <= 702/100 when xabs = 702/100 sync b goto w142; loc w142: invariant xabs <= 710/100 when xabs = 710/100 sync a goto w143; loc w143: invariant xabs <= 719/100 when xabs = 719/100 sync b goto w144; loc w144: invariant xabs <= 728/100 when xabs = 728/100 sync a goto w145; loc w145: invariant xabs <= 734/100 when xabs = 734/100 sync b goto w146; loc w146: invariant xabs <= 741/100 when xabs = 741/100 sync a goto w147; loc w147: invariant xabs <= 745/100 when xabs = 745/100 sync b goto w148; loc w148: invariant xabs <= 751/100 when xabs = 751/100 sync a goto w149; loc w149: invariant xabs <= 759/100 when xabs = 759/100 sync b goto w150; loc w150: invariant xabs <= 767/100 when xabs = 767/100 sync a goto w151; loc w151: invariant xabs <= 770/100 when xabs = 770/100 sync b goto w152; loc w152: invariant xabs <= 771/100 when xabs = 771/100 sync a goto w153; loc w153: invariant xabs <= 777/100 when xabs = 777/100 sync b goto w154; loc w154: invariant xabs <= 779/100 when xabs = 779/100 sync a goto w155; loc w155: invariant xabs <= 785/100 when xabs = 785/100 sync b goto w156; loc w156: invariant xabs <= 788/100 when xabs = 788/100 sync a goto w157; loc w157: invariant xabs <= 789/100 when xabs = 789/100 sync b goto w158; loc w158: invariant xabs <= 792/100 when xabs = 792/100 sync a goto w159; loc w159: invariant xabs <= 798/100 when xabs = 798/100 sync b goto w160; loc w160: invariant xabs <= 801/100 when xabs = 801/100 sync a goto w161; loc w161: invariant xabs <= 808/100 when xabs = 808/100 sync b goto w162; loc w162: invariant xabs <= 816/100 when xabs = 816/100 sync a goto w163; loc w163: invariant xabs <= 820/100 when xabs = 820/100 sync b goto w164; loc w164: invariant xabs <= 822/100 when xabs = 822/100 sync a goto w165; loc w165: invariant xabs <= 831/100 when xabs = 831/100 sync b goto w166; loc w166: invariant xabs <= 837/100 when xabs = 837/100 sync a goto w167; loc w167: invariant xabs <= 841/100 when xabs = 841/100 sync b goto w168; loc w168: invariant xabs <= 842/100 when xabs = 842/100 sync a goto w169; loc w169: invariant xabs <= 850/100 when xabs = 850/100 sync b goto w170; loc w170: invariant xabs <= 859/100 when xabs = 859/100 sync a goto w171; loc w171: invariant xabs <= 868/100 when xabs = 868/100 sync b goto w172; loc w172: invariant xabs <= 877/100 when xabs = 877/100 sync a goto w173; loc w173: invariant xabs <= 879/100 when xabs = 879/100 sync b goto w174; loc w174: invariant xabs <= 886/100 when xabs = 886/100 sync a goto w175; loc w175: invariant xabs <= 893/100 when xabs = 893/100 sync b goto w176; loc w176: invariant xabs <= 895/100 when xabs = 895/100 sync a goto w177; loc w177: invariant xabs <= 904/100 when xabs = 904/100 sync b goto w178; loc w178: invariant xabs <= 907/100 when xabs = 907/100 sync a goto w179; loc w179: invariant xabs <= 909/100 when xabs = 909/100 sync b goto w180; loc w180: invariant xabs <= 913/100 when xabs = 913/100 sync a goto w181; loc w181: invariant xabs <= 920/100 when xabs = 920/100 sync b goto w182; loc w182: invariant xabs <= 925/100 when xabs = 925/100 sync a goto w183; loc w183: invariant xabs <= 928/100 when xabs = 928/100 sync b goto w184; loc w184: invariant xabs <= 935/100 when xabs = 935/100 sync a goto w185; loc w185: invariant xabs <= 941/100 when xabs = 941/100 sync b goto w186; loc w186: invariant xabs <= 942/100 when xabs = 942/100 sync a goto w187; loc w187: invariant xabs <= 949/100 when xabs = 949/100 sync b goto w188; loc w188: invariant xabs <= 953/100 when xabs = 953/100 sync a goto w189; loc w189: invariant xabs <= 960/100 when xabs = 960/100 sync b goto w190; loc w190: invariant xabs <= 964/100 when xabs = 964/100 sync a goto w191; loc w191: invariant xabs <= 968/100 when xabs = 968/100 sync b goto w192; loc w192: invariant xabs <= 969/100 when xabs = 969/100 sync a goto w193; loc w193: invariant xabs <= 973/100 when xabs = 973/100 sync b goto w194; loc w194: invariant xabs <= 980/100 when xabs = 980/100 sync a goto w195; loc w195: invariant xabs <= 988/100 when xabs = 988/100 sync b goto w196; loc w196: invariant xabs <= 989/100 when xabs = 989/100 sync a goto w197; loc w197: invariant xabs <= 992/100 when xabs = 992/100 sync b goto w198; loc w198: invariant xabs <= 999/100 when xabs = 999/100 sync a goto w199; loc w199: invariant xabs <= 1007/100 when xabs = 1007/100 sync b goto w200; (* END AUTOMATICALLY GENERATED *) loc w200: invariant True end (* word *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = pre_s0 & loc[word] = w0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & y = 0 & xabs = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & p1 >= 0 & p2 >= 0 & p3 >= 0 & t >= 0 & tprime >= 0 ; (************************************************************) (* The end *) (************************************************************) end