diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index c2bdd5650..2fd2eb070 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -372,13 +372,12 @@ namespace spot throw std::runtime_error( "twa_graph::merge_states() does not work on alternating automata"); + const unsigned nthreads = get_nthreads(); + typedef graph_t::edge_storage_t tr_t; - g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) + g_.sort_edges_srcfirst_([](const tr_t& lhs, const tr_t& rhs) { - if (lhs.src < rhs.src) - return true; - if (lhs.src > rhs.src) - return false; + assert(lhs.src == rhs.src); if (lhs.acc < rhs.acc) return true; if (lhs.acc > rhs.acc) @@ -449,7 +448,7 @@ namespace spot // Represents which states share a hash // Head is in the unordered_map, // hash_linked_list is like a linked list structure - // of false pointers + // of fake pointers auto hash_linked_list = std::vector(n_states, -1u); auto s_to_hash = std::vector(n_states, 0); @@ -530,8 +529,8 @@ namespace spot }; - static auto checked1 = std::vector(); - static auto checked2 = std::vector(); + thread_local auto checked1 = std::vector(); + thread_local auto checked2 = std::vector(); auto [i1, nsl1, sl1, e1] = e_idx[s1]; auto [i2, nsl2, sl2, e2] = e_idx[s2]; @@ -585,12 +584,10 @@ namespace spot // More efficient version? // Skip checked edges // Last element serves as break - for (; checked1[idx1 - i1]; ++idx1) - { - } - for (; checked2[idx2 - i2]; ++idx2) - { - } + while (checked1[idx1 - i1]) + ++idx1; + while (checked2[idx2 - i2]) + ++idx2; // If one is out of bounds, so is the other if (idx1 == e1) { @@ -614,47 +611,107 @@ namespace spot const unsigned nb_states = num_states(); std::vector remap(nb_states, -1U); - for (unsigned i = 0; i != nb_states; ++i) + // Check each hash + auto check_ix = [&](unsigned ix) { - auto j = spe && (*sp)[i] ? player_map.at(s_to_hash[i]).first - : env_map.at(s_to_hash[i]).first; - for (; j(); + v.clear(); + for (auto i = ix; i != -1U; i = hash_linked_list[i]) + v.push_back(i); + const unsigned N = v.size(); - // Because of the special self-loop tests we use above, - // it's possible that i can be mapped to remap[j] even - // if j was last compatible states found. Consider the - // following cases, taken from an actual test case: - // 18 is equal to 5, 35 is equal to 18, but 35 is not - // equal to 5. - // - // State: 5 - // [0&1&2] 8 {3} - // [!0&1&2] 10 {1} - // [!0&!1&!2] 18 {1} - // [!0&!1&2] 19 {1} - // [!0&1&!2] 20 {1} - // - // State: 18 - // [0&1&2] 8 {3} - // [!0&1&2] 10 {1} - // [!0&!1&!2] 18 {1} // self-loop - // [!0&!1&2] 19 {1} - // [!0&1&!2] 20 {1} - // - // State: 35 - // [0&1&2] 8 {3} - // [!0&1&2] 10 {1} - // [!0&!1&!2] 35 {1} // self-loop - // [!0&!1&2] 19 {1} - // [!0&1&!2] 20 {1} - break; + for (unsigned idx = 0; idx < N; ++idx) + { + auto i = v[idx]; + for (unsigned jdx = 0; jdx < idx; ++jdx) + { + auto j = v[jdx]; + if (state_equal(j, i)) + { + remap[i] = (remap[j] != -1U) ? remap[j] : j; + + // Because of the special self-loop tests we use above, + // it's possible that i can be mapped to remap[j] even + // if j was last compatible states found. Consider the + // following cases, taken from an actual test case: + // 18 is equal to 5, 35 is equal to 18, but 35 is not + // equal to 5. + // + // State: 5 + // [0&1&2] 8 {3} + // [!0&1&2] 10 {1} + // [!0&!1&!2] 18 {1} + // [!0&!1&2] 19 {1} + // [!0&1&!2] 20 {1} + // + // State: 18 + // [0&1&2] 8 {3} + // [!0&1&2] 10 {1} + // [!0&!1&!2] 18 {1} // self-loop + // [!0&!1&2] 19 {1} + // [!0&1&!2] 20 {1} + // + // State: 35 + // [0&1&2] 8 {3} + // [!0&1&2] 10 {1} + // [!0&!1&!2] 35 {1} // self-loop + // [!0&!1&2] 19 {1} + // [!0&1&!2] 20 {1} + break; + } } } - } + }; + + auto upd = [](auto& b, const auto&e, unsigned it) + { + while ((it > 0) & (b != e)) + { + --it; + ++b; + } + }; + + auto worker = [&upd, check_ix, nthreads](unsigned pid, auto begp, auto endp, + auto bege, auto ende) + { + upd(begp, endp, pid); + upd(bege, ende, pid); + for (; begp != endp; upd(begp, endp, nthreads)) + check_ix(begp->second.first); + for (; bege != ende; upd(bege, ende, nthreads)) + check_ix(bege->second.first); + }; + + { + auto begp = player_map.begin(); + auto endp = player_map.end(); + auto bege = env_map.begin(); + auto ende = env_map.end(); + + + if ((nthreads == 1) & (num_states() > 1000)) // Bound? + { + worker(0, begp, endp, bege, ende); + } + else + { + static auto tv = std::vector(); + assert(tv.empty()); + tv.resize(nthreads); + for (unsigned pid = 0; pid < nthreads; ++pid) + tv[pid] = std::thread( + [worker, pid, begp, endp, bege, ende]() + { + worker(pid, begp, endp, bege, ende); + return; + }); + for (auto& t : tv) + t.join(); + tv.clear(); + } + } for (auto& e: edges()) if (remap[e.dst] != -1U) @@ -765,7 +822,7 @@ namespace spot comp_classes_.clear(); // get all compatible classes // Candidate classes share a hash - // A state is compatible to a class if it is compatble + // A state is compatible to a class if it is compatible // to any of its states auto& cand_classes = equiv_class_[hi]; unsigned n_c_classes = cand_classes.size(); diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py index 4e97abe23..2be4d4984 100644 --- a/tests/python/mergedge.py +++ b/tests/python/mergedge.py @@ -23,148 +23,151 @@ import spot from unittest import TestCase tc = TestCase() -aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a" -Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""") -tc.assertEqual(aut.num_edges(), 2) -aut.merge_edges() -tc.assertEqual(aut.num_edges(), 1) +for nthread in range(1, 16, 2): + spot.set_nthreads(nthread) + tc.assertEqual(spot.get_nthreads(), nthread) + aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a" + Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""") + tc.assertEqual(aut.num_edges(), 2) + aut.merge_edges() + tc.assertEqual(aut.num_edges(), 1) -aut = spot.automaton(""" -HOA: v1 -States: 2 -Start: 0 -AP: 2 "p0" "p1" -acc-name: Buchi -Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels trans-acc complete ---BODY-- -State: 0 -[!0] 0 {0} -[0] 1 {0} -State: 1 -[!0&!1] 0 {0} -[0 | 1] 1 -[0&!1] 1 {0} ---END--""") -tc.assertEqual(aut.num_edges(), 5) -aut.merge_edges() -tc.assertEqual(aut.num_edges(), 5) -tc.assertFalse(spot.is_deterministic(aut)) -aut = spot.split_edges(aut) -tc.assertEqual(aut.num_edges(), 9) -aut.merge_edges() -tc.assertEqual(aut.num_edges(), 5) -tc.assertTrue(spot.is_deterministic(aut)) + aut = spot.automaton(""" + HOA: v1 + States: 2 + Start: 0 + AP: 2 "p0" "p1" + acc-name: Buchi + Acceptance: 1 Inf(0) + properties: trans-labels explicit-labels trans-acc complete + --BODY-- + State: 0 + [!0] 0 {0} + [0] 1 {0} + State: 1 + [!0&!1] 0 {0} + [0 | 1] 1 + [0&!1] 1 {0} + --END--""") + tc.assertEqual(aut.num_edges(), 5) + aut.merge_edges() + tc.assertEqual(aut.num_edges(), 5) + tc.assertFalse(spot.is_deterministic(aut)) + aut = spot.split_edges(aut) + tc.assertEqual(aut.num_edges(), 9) + aut.merge_edges() + tc.assertEqual(aut.num_edges(), 5) + tc.assertTrue(spot.is_deterministic(aut)) -aut = spot.automaton(""" -HOA: v1 -States: 3 -Start: 0 -AP: 1 "a" -acc-name: Buchi -Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels trans-acc complete ---BODY-- -State: 0 -[!0] 1 {0} -[0] 2 {0} -State: 1 -[!0] 1 {0} -[0] 1 -State: 2 -[!0] 2 {0} -[0] 1 ---END--""") -aut.merge_states() -tc.assertEqual(aut.num_edges(), 4) -tc.assertEqual(aut.num_states(), 2) -tc.assertTrue(spot.is_deterministic(aut)) -tc.assertTrue(aut.prop_complete()) -aut.merge_states() -tc.assertEqual(aut.num_edges(), 4) -tc.assertEqual(aut.num_states(), 2) -tc.assertTrue(spot.is_deterministic(aut)) -tc.assertTrue(aut.prop_complete()) + aut = spot.automaton(""" + HOA: v1 + States: 3 + Start: 0 + AP: 1 "a" + acc-name: Buchi + Acceptance: 1 Inf(0) + properties: trans-labels explicit-labels trans-acc complete + --BODY-- + State: 0 + [!0] 1 {0} + [0] 2 {0} + State: 1 + [!0] 1 {0} + [0] 1 + State: 2 + [!0] 2 {0} + [0] 1 + --END--""") + aut.merge_states() + tc.assertEqual(aut.num_edges(), 4) + tc.assertEqual(aut.num_states(), 2) + tc.assertTrue(spot.is_deterministic(aut)) + tc.assertTrue(aut.prop_complete()) + aut.merge_states() + tc.assertEqual(aut.num_edges(), 4) + tc.assertEqual(aut.num_states(), 2) + tc.assertTrue(spot.is_deterministic(aut)) + tc.assertTrue(aut.prop_complete()) -aa = spot.automaton(""" -HOA: v1 States: 41 Start: 0 AP: 3 "allfinished" "finished_0" -"finished_1" acc-name: parity max odd 4 Acceptance: 4 Inf(3) | (Fin(2) -& (Inf(1) | Fin(0))) properties: trans-labels explicit-labels -trans-acc colored properties: deterministic --BODY-- State: 0 -[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [!0&1&!2] 3 {1} [!0&1&2] 4 {1} -[0&!1&!2] 5 {1} [0&!1&2] 6 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} State: 1 -[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} -[!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} [0&!1&2] 12 {1} -State: 2 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} -[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1} -State: 3 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} -[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1} -State: 4 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} -[0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 {1} -State: 5 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 -{1} [!0&1&!2] 20 {1} State: 6 [0&1&2] 8 {1} [!0&1&2] 10 {1} [!0&!1&2] -19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 21 {1} State: 7 [0&1&2] 8 {3} -[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 22 {1} -State: 8 [!0&!1&!2] 5 {1} [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 -{1} [!0&1&!2] 20 {1} State: 9 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] 8 -{1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 {1} -[!0&!1&2] 24 {1} State: 10 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 -{3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {1} -[!0&!1&!2] 25 {1} State: 11 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 -{1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 12 [0&1&2] 8 {3} -[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 27 {1} [!0&!1&!2] 28 {1} -State: 13 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} -[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1} -State: 14 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} -[0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} -State: 15 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} -[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1} -State: 16 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 -{1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 -{1} State: 17 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] -11 {1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 -{1} State: 18 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} -[!0&!1&2] 19 {1} [!0&1&!2] 20 {1} State: 19 [0&1&!2] 7 {3} [0&1&2] 8 -{3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} [!0&1&2] 32 -{1} State: 20 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 {1} [!0&1&2] -32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 21 [0&1&2] 8 {1} -[!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} -State: 22 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 -{1} [!0&!1&!2] 35 {1} State: 23 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] -8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 -{1} [!0&!1&2] 24 {1} State: 24 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] -8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24 -{1} [!0&!1&!2] 25 {1} State: 25 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] -8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24 -{1} [!0&!1&!2] 25 {1} State: 26 [0&1&2] 8 {3} [!0&1&2] 10 {1} -[!0&!1&2] 19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 27 [0&1&2] -8 {3} [0&!1&2] 12 {3} [!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 -{1} [!0&!1&2] 37 {1} State: 28 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] -19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 29 [0&!1&!2] 5 {3} -[0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] -14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} State: 30 [0&1&!2] 7 {3} -[0&1&2] 8 {3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} -[!0&1&2] 32 {1} State: 31 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} -[0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} -[!0&!1&!2] 38 {1} State: 32 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 -{3} [0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} -[!0&!1&!2] 39 {1} State: 33 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 -{1} [!0&1&2] 32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 34 -[0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 {1} -[!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 {1} -State: 35 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 -{1} [!0&!1&!2] 35 {1} State: 36 [0&1&2] 8 {3} [0&!1&2] 12 {3} -[!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 {1} [!0&!1&2] 37 {1} -State: 37 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3} -[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1} -State: 38 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3} -[!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} [!0&!1&!2] 38 {1} -State: 39 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3} -[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1} -State: 40 [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 -{1} [!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 -{1} --END--""") -aa.merge_states() -# This used to cause a segfault reported by Philipp. -print(aa.to_str()) + aa = spot.automaton(""" + HOA: v1 States: 41 Start: 0 AP: 3 "allfinished" "finished_0" + "finished_1" acc-name: parity max odd 4 Acceptance: 4 Inf(3) | (Fin(2) + & (Inf(1) | Fin(0))) properties: trans-labels explicit-labels + trans-acc colored properties: deterministic --BODY-- State: 0 + [!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [!0&1&!2] 3 {1} [!0&1&2] 4 {1} + [0&!1&!2] 5 {1} [0&!1&2] 6 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} State: 1 + [!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} + [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} [0&!1&2] 12 {1} + State: 2 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} + [0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1} + State: 3 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} + [0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1} + State: 4 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} + [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 {1} + State: 5 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 + {1} [!0&1&!2] 20 {1} State: 6 [0&1&2] 8 {1} [!0&1&2] 10 {1} [!0&!1&2] + 19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 21 {1} State: 7 [0&1&2] 8 {3} + [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 22 {1} + State: 8 [!0&!1&!2] 5 {1} [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 + {1} [!0&1&!2] 20 {1} State: 9 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] 8 + {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 {1} + [!0&!1&2] 24 {1} State: 10 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 + {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {1} + [!0&!1&!2] 25 {1} State: 11 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 + {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 12 [0&1&2] 8 {3} + [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 27 {1} [!0&!1&!2] 28 {1} + State: 13 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} + [0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1} + State: 14 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} + [0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} + State: 15 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} + [0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1} + State: 16 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 + {1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 + {1} State: 17 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] + 11 {1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 + {1} State: 18 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} + [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} State: 19 [0&1&!2] 7 {3} [0&1&2] 8 + {3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} [!0&1&2] 32 + {1} State: 20 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 {1} [!0&1&2] + 32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 21 [0&1&2] 8 {1} + [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} + State: 22 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 + {1} [!0&!1&!2] 35 {1} State: 23 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] + 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 + {1} [!0&!1&2] 24 {1} State: 24 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] + 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24 + {1} [!0&!1&!2] 25 {1} State: 25 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] + 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24 + {1} [!0&!1&!2] 25 {1} State: 26 [0&1&2] 8 {3} [!0&1&2] 10 {1} + [!0&!1&2] 19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 27 [0&1&2] + 8 {3} [0&!1&2] 12 {3} [!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 + {1} [!0&!1&2] 37 {1} State: 28 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] + 19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 29 [0&!1&!2] 5 {3} + [0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] + 14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} State: 30 [0&1&!2] 7 {3} + [0&1&2] 8 {3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} + [!0&1&2] 32 {1} State: 31 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} + [0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} + [!0&!1&!2] 38 {1} State: 32 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 + {3} [0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} + [!0&!1&!2] 39 {1} State: 33 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 + {1} [!0&1&2] 32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 34 + [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 {1} + [!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 {1} + State: 35 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 + {1} [!0&!1&!2] 35 {1} State: 36 [0&1&2] 8 {3} [0&!1&2] 12 {3} + [!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 {1} [!0&!1&2] 37 {1} + State: 37 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3} + [!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1} + State: 38 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3} + [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} [!0&!1&!2] 38 {1} + State: 39 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3} + [!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1} + State: 40 [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 + {1} [!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 + {1} --END--""") + aa.merge_states() + # This used to cause a segfault reported by Philipp. + print(aa.to_str())