From b3f38e3c2c06b75f0aa70e6cd479c87ca76950fa Mon Sep 17 00:00:00 2001 From: Amanda Stjerna Date: Tue, 27 Feb 2024 15:00:06 +0100 Subject: [PATCH] Add failing instance to basket --- basket/prob.par | 298 ++++++++++++++++++++++++++++++++++++++++ basket/prob.reduced.par | 38 +++++ 2 files changed, 336 insertions(+) create mode 100644 basket/prob.par create mode 100644 basket/prob.reduced.par diff --git a/basket/prob.par b/basket/prob.par new file mode 100644 index 000000000..e6b677d83 --- /dev/null +++ b/basket/prob.par @@ -0,0 +1,298 @@ +counter int a0, a1, a2, a3, a4; +synchronised { +automaton aut_X0 { + init s7; + s0 -> s44 [116, 116] {a0 += 1}; + s1 -> s37 [97, 97] {a1 += 1}; + s2 -> s18 [101, 101] {a2 += 1}; + s3 -> s55 [97, 97] {a3 += 1}; + s4 -> s35 [110, 110] {a4 += 1}; + s5 -> s25 [116, 116] {}; + s6 -> s34 [102, 102] {}; + s7 -> s42 [102, 102] {}; + s8 -> s52 [83, 83] {}; + s9 -> s16 [97, 97] {}; + s10 -> s20 [107, 107] {}; + s11 -> s36 [111, 111] {}; + s12 -> s33 [111, 111] {}; + s13 -> s8 [9, 10] {}; + s13 -> s8 [12, 13] {}; + s13 -> s8 [32, 32] {}; + s14 -> s17 [117, 117] {}; + s15 -> s49 [119, 119] {}; + s16 -> s0 [114, 114] {}; + s17 -> s29 [113, 113] {}; + s18 -> s39 [114, 114] {}; + s19 -> s11 [72, 72] {}; + s19 -> s19 [12, 13] {}; + s19 -> s19 [9, 10] {}; + s19 -> s19 [32, 32] {}; + s20 -> s27 [115, 115] {}; + s21 -> s22 [102, 102] {}; + s22 -> s4 [105, 105] {}; + s23 -> s3 [47, 47] {}; + s25 -> s30 [58, 58] {}; + s26 -> s12 [99, 99] {}; + s27 -> s48 [106, 106] {}; + s28 -> s51 [51, 51] {}; + s29 -> s31 [115, 115] {}; + s30 -> s15 [12, 13] {}; + s30 -> s15 [9, 10] {}; + s30 -> s15 [32, 32] {}; + s31 -> s43 [9, 10] {}; + s31 -> s43 [32, 32] {}; + s31 -> s43 [12, 13] {}; + s32 -> s21 [45, 45] {}; + s33 -> s13 [109, 109] {}; + s34 -> s23 [117, 117] {}; + s35 -> s2 [100, 100] {}; + s36 -> s5 [115, 115] {}; + s37 -> s41 [115, 115] {}; + s38 -> s47 [109, 109] {}; + s39 -> s26 [46, 46] {}; + s40 -> s46 [46, 46] {}; + s41 -> s32 [116, 116] {}; + s42 -> s53 [104, 104] {}; + s43 -> s11 [72, 72] {}; + s43 -> s19 [12, 13] {}; + s43 -> s19 [32, 32] {}; + s43 -> s19 [9, 10] {}; + s44 -> s50 [101, 101] {}; + s45 -> s6 [115, 115] {}; + s46 -> s1 [102, 102] {}; + s47 -> s14 [46, 46] {}; + s48 -> s45 [122, 122] {}; + s49 -> s54 [119, 119] {}; + s50 -> s56 [100, 100] {}; + s51 -> s24 [10, 10] {}; + s52 -> s9 [116, 116] {}; + s53 -> s10 [102, 102] {}; + s54 -> s40 [119, 119] {}; + s55 -> s38 [104, 104] {}; + s56 -> s28 [33, 33] {}; + accepting s24; +}; +automaton aut_X1 { + init s0; + s0 -> s1 [58, 65535] {}; + s0 -> s4 [48, 57] {}; + s0 -> s1 [0, 47] {}; + s1 -> s1 [0, 65535] {}; + s2 -> s2 [48, 57] {}; + s2 -> s1 [58, 65535] {}; + s2 -> s1 [11, 47] {}; + s2 -> s1 [0, 9] {}; + s2 -> s7 [10, 10] {}; + s3 -> s1 [0, 9] {}; + s3 -> s3 [48, 57] {}; + s3 -> s1 [47, 47] {}; + s3 -> s1 [58, 65535] {}; + s3 -> s6 [46, 46] {}; + s3 -> s7 [10, 10] {}; + s3 -> s1 [11, 45] {}; + s4 -> s1 [58, 65535] {}; + s4 -> s3 [48, 57] {}; + s4 -> s1 [0, 9] {}; + s4 -> s1 [47, 47] {}; + s4 -> s6 [46, 46] {}; + s4 -> s7 [10, 10] {}; + s4 -> s1 [11, 45] {}; + s5 -> s1 [0, 9] {}; + s5 -> s7 [10, 10] {}; + s5 -> s1 [11, 47] {}; + s5 -> s1 [58, 65535] {}; + s5 -> s2 [48, 57] {}; + s6 -> s1 [58, 65535] {}; + s6 -> s1 [0, 47] {}; + s6 -> s5 [48, 57] {}; + s7 -> s1 [0, 65535] {}; + accepting s3, s4, s5, s2, s6, s1, s0; +}; +automaton aut_X2 { + init s4; + s0 -> s19 [111, 65535] {}; + s0 -> s19 [0, 109] {}; + s0 -> s18 [110, 110] {}; + s1 -> s19 [0, 121] {}; + s1 -> s19 [123, 65535] {}; + s1 -> s17 [122, 122] {}; + s2 -> s1 [122, 122] {}; + s2 -> s19 [0, 121] {}; + s2 -> s19 [123, 65535] {}; + s3 -> s19 [120, 65535] {}; + s3 -> s23 [119, 119] {}; + s3 -> s19 [0, 118] {}; + s4 -> s7 [122, 122] {}; + s4 -> s19 [123, 65535] {}; + s4 -> s19 [0, 121] {}; + s5 -> s22 [109, 109] {}; + s5 -> s19 [110, 65535] {}; + s5 -> s19 [0, 108] {}; + s6 -> s19 [0, 108] {}; + s6 -> s19 [110, 65535] {}; + s6 -> s26 [109, 109] {}; + s7 -> s19 [110, 65535] {}; + s7 -> s19 [0, 108] {}; + s7 -> s0 [109, 109] {}; + s8 -> s19 [0, 96] {}; + s8 -> s25 [97, 97] {}; + s8 -> s19 [98, 65535] {}; + s9 -> s19 [0, 65535] {}; + s10 -> s19 [48, 65535] {}; + s10 -> s19 [0, 46] {}; + s10 -> s2 [47, 47] {}; + s11 -> s19 [83, 65535] {}; + s11 -> s19 [58, 81] {}; + s11 -> s29 [82, 82] {}; + s11 -> s19 [0, 47] {}; + s11 -> s15 [48, 57] {}; + s12 -> s19 [0, 120] {}; + s12 -> s19 [122, 65535] {}; + s12 -> s24 [121, 121] {}; + s13 -> s19 [0, 102] {}; + s13 -> s19 [104, 65535] {}; + s13 -> s27 [103, 103] {}; + s14 -> s11 [48, 57] {}; + s14 -> s19 [0, 47] {}; + s14 -> s19 [58, 65535] {}; + s15 -> s19 [58, 81] {}; + s15 -> s19 [0, 47] {}; + s15 -> s29 [82, 82] {}; + s15 -> s19 [83, 65535] {}; + s15 -> s15 [48, 57] {}; + s16 -> s19 [99, 65535] {}; + s16 -> s19 [0, 97] {}; + s16 -> s28 [98, 98] {}; + s17 -> s19 [0, 108] {}; + s17 -> s3 [109, 109] {}; + s17 -> s19 [110, 65535] {}; + s18 -> s19 [0, 105] {}; + s18 -> s19 [107, 65535] {}; + s18 -> s30 [106, 106] {}; + s19 -> s19 [0, 65535] {}; + s20 -> s14 [116, 116] {}; + s20 -> s19 [117, 65535] {}; + s20 -> s19 [0, 115] {}; + s21 -> s19 [0, 121] {}; + s21 -> s10 [122, 122] {}; + s21 -> s19 [123, 65535] {}; + s22 -> s19 [0, 102] {}; + s22 -> s16 [103, 103] {}; + s22 -> s19 [104, 65535] {}; + s23 -> s13 [46, 46] {}; + s23 -> s19 [0, 45] {}; + s23 -> s19 [47, 65535] {}; + s24 -> s19 [11, 65535] {}; + s24 -> s19 [0, 9] {}; + s24 -> s9 [10, 10] {}; + s25 -> s19 [101, 65535] {}; + s25 -> s12 [100, 100] {}; + s25 -> s19 [0, 99] {}; + s26 -> s19 [112, 65535] {}; + s26 -> s5 [111, 111] {}; + s26 -> s19 [0, 110] {}; + s27 -> s19 [123, 65535] {}; + s27 -> s20 [122, 122] {}; + s27 -> s19 [0, 121] {}; + s28 -> s19 [0, 99] {}; + s28 -> s21 [100, 100] {}; + s28 -> s19 [101, 65535] {}; + s29 -> s19 [102, 65535] {}; + s29 -> s19 [0, 100] {}; + s29 -> s8 [101, 101] {}; + s30 -> s19 [104, 65535] {}; + s30 -> s6 [103, 103] {}; + s30 -> s19 [0, 102] {}; + accepting s12, s8, s24, s13, s2, s26, s1, s29, s20, s7, s0, s18, s15, s10, s17, s3, s16, s30, s4, s19, s5, s23, s28, s27, s14, s22, s21, s6, s11, s25; +}; +automaton aut_X3 { + init s0; + s0 -> s1 [65, 65] {}; + s0 -> s4 [83, 83] {}; + s0 -> s3 [71, 77] {}; + s0 -> s3 [88, 65535] {}; + s0 -> s3 [69, 69] {}; + s0 -> s3 [79, 82] {}; + s0 -> s9 [87, 87] {}; + s0 -> s2 [70, 70] {}; + s0 -> s7 [66, 68] {}; + s0 -> s4 [78, 78] {}; + s0 -> s3 [0, 64] {}; + s0 -> s3 [84, 86] {}; + s1 -> s3 [0, 44] {}; + s1 -> s3 [46, 65535] {}; + s1 -> s8 [45, 45] {}; + s2 -> s3 [0, 65535] {}; + s3 -> s3 [0, 65535] {}; + s4 -> s3 [0, 69] {}; + s4 -> s2 [70, 70] {}; + s4 -> s3 [71, 65535] {}; + s5 -> s3 [0, 65535] {}; + s6 -> s3 [0, 65535] {}; + s7 -> s5 [43, 43] {}; + s7 -> s3 [46, 65535] {}; + s7 -> s5 [45, 45] {}; + s7 -> s3 [0, 42] {}; + s7 -> s3 [44, 44] {}; + s8 -> s3 [0, 65535] {}; + s9 -> s6 [10, 10] {}; + s9 -> s3 [11, 65535] {}; + s9 -> s3 [0, 9] {}; + accepting s0, s3, s4, s9; +}; +automaton aut_X4 { + init s8; + s0 -> s0 [0, 65535] {}; + s1 -> s0 [0, 64] {}; + s1 -> s0 [91, 65535] {}; + s1 -> s9 [65, 90] {}; + s2 -> s0 [58, 64] {}; + s2 -> s0 [0, 47] {}; + s2 -> s5 [48, 57] {}; + s2 -> s0 [91, 65535] {}; + s2 -> s6 [65, 90] {}; + s3 -> s12 [45, 45] {}; + s3 -> s0 [46, 65535] {}; + s3 -> s12 [32, 32] {}; + s3 -> s0 [33, 44] {}; + s3 -> s0 [0, 31] {}; + s4 -> s0 [0, 65535] {}; + s5 -> s0 [33, 44] {}; + s5 -> s0 [58, 64] {}; + s5 -> s0 [91, 65535] {}; + s5 -> s3 [65, 90] {}; + s5 -> s0 [0, 31] {}; + s5 -> s12 [32, 32] {}; + s5 -> s12 [45, 45] {}; + s5 -> s0 [46, 47] {}; + s5 -> s10 [48, 57] {}; + s6 -> s0 [46, 65535] {}; + s6 -> s12 [45, 45] {}; + s6 -> s12 [32, 32] {}; + s6 -> s0 [33, 44] {}; + s6 -> s0 [0, 31] {}; + s7 -> s0 [0, 64] {}; + s7 -> s0 [91, 65535] {}; + s7 -> s1 [65, 90] {}; + s8 -> s0 [91, 65535] {}; + s8 -> s11 [65, 90] {}; + s8 -> s0 [0, 64] {}; + s9 -> s0 [11, 65535] {}; + s9 -> s4 [10, 10] {}; + s9 -> s0 [0, 9] {}; + s10 -> s12 [45, 45] {}; + s10 -> s0 [0, 31] {}; + s10 -> s12 [32, 32] {}; + s10 -> s0 [33, 44] {}; + s10 -> s0 [46, 65535] {}; + s11 -> s5 [48, 57] {}; + s11 -> s0 [58, 64] {}; + s11 -> s0 [91, 65535] {}; + s11 -> s2 [65, 90] {}; + s11 -> s0 [0, 47] {}; + s12 -> s0 [0, 47] {}; + s12 -> s7 [48, 57] {}; + s12 -> s0 [58, 65535] {}; + accepting s3, s12, s8, s5, s2, s9, s6, s1, s7, s0, s10, s11; +}; +}; diff --git a/basket/prob.reduced.par b/basket/prob.reduced.par new file mode 100644 index 000000000..83c5397a6 --- /dev/null +++ b/basket/prob.reduced.par @@ -0,0 +1,38 @@ +// Needs --nr-unknown-to-start-materialise 2 to trigger lazier materialisation in order for the bug to appear + +synchronised { +automaton aut_X0 { + init s7; + + s7 -> soak [any] {}; // Needed for SAT + + soak -> s13 [any] {}; // Load-bearing -- not in solution + + s8 -> soak [any] {}; // Load-bearing -- not in solution + soak -> s24 [any] {}; // Needed for SAT + + s13 -> s8 [12, 13] {}; // Load-bearing -- not in solution + + accepting s24; +}; +automaton aut_X2 { + init s4; + s4 -> s19 [0, 121] {}; + s19 -> s19 [0, 65535] {}; + accepting s4, s19; // Load-bearing s4 +}; +automaton aut_X3 { + init s0; + s0 -> s3 [88, 65535] {}; //-- not in solution + s0 -> s4 [78, 78] {}; // Load-bearing! + s4 -> s3 [71, 65535] {}; // Load-bearing + accepting s0, s3; // Load-bearing: s0 +}; +automaton aut_X4 { + init s8; + s8 -> s11 [65, 90] {}; // Needed for SAT + s11 -> s2 [65, 90] {}; // Needed for SAT + s11 -> s0 [0, 47] {}; // Load-bearing -- not in solution + accepting s8, s2, s0; // Load-bearing (all of them) +}; +};