Add failing instance to basket

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;
+};
+};

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)
+};
+};