From dfb75632ba50f2243abb12147986fa73079a9db6 Mon Sep 17 00:00:00 2001 From: Philipp Schlehuber-Caissier Date: Thu, 24 Mar 2022 09:45:33 +0100 Subject: [PATCH] Update merge_states Current implementation of merge_states fails on certain self-loops. Updated implementation to take them into account and use a hashbased implementation to speed up calculations. Moreover, merge_states() is now aware of "state-player", just like defrag_states_ * spot/twa/twagraph.cc: Here * spot/twaalgos/game.cc: Fix odd cycle for sink * spot/twaalgos/synthesis.cc: Adapt split_det pipeline * tests/python/_synthesis.ipynb: Tests --- spot/twa/twagraph.cc | 413 ++- spot/twaalgos/game.cc | 11 +- spot/twaalgos/synthesis.cc | 7 +- tests/python/_synthesis.ipynb | 4541 ++++++++++++++++++++++++++++++++- 4 files changed, 4919 insertions(+), 53 deletions(-) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 051514550..b11ca12c5 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -21,13 +21,89 @@ #include #include #include +#include #include #include +#include #include #include using namespace std::string_literals; +namespace +{ + using namespace spot; + // If LAST is false, + // it is guaranteed that there will be another src state + template + void treat(std::vector>& e_idx, + const twa_graph::graph_t::edge_vector_t& e_vec, + std::vector& e_chain, + std::vector& use_for_hash, + unsigned& idx, + unsigned s, + unsigned n_e) + { + assert(s < e_idx.size()); + assert(idx < e_vec.size()); + assert(e_chain.size() == e_vec.size()); + + //std::cout << s << "; " << idx << std::endl; + + // Check if this state has outgoing transitions + if (s != e_vec[idx].src) + // Nothing to do + { + assert(!LAST); + return; + } + + auto& s_idx = e_idx[s]; + s_idx[0] = idx; + + // helper + unsigned sub_idx[] = {-1u, -1u}; + + // All transitions of this state + while (true) + { + assert(idx < e_vec.size() + LAST); + if constexpr (!LAST) + { + if (e_vec[idx].src != s) + break; + } + else + { + if (idx == n_e) + break; + } + + // Argh so many ifs + unsigned which = e_vec[idx].src == e_vec[idx].dst; + if (sub_idx[which] == -1u) + { + // First non-selflooping + sub_idx[which] = idx; + s_idx[1u+which] = idx; + } + else + { + // Continue the chained list + e_chain[sub_idx[which]] = idx; + sub_idx[which] = idx; + } + ++idx; + } + s_idx[3] = idx; + + // Check if self-loops appeared + // If so -> do not use for hash + if constexpr (!SPE) + use_for_hash[s] = s_idx[2] == -1u; + } +} + namespace spot { @@ -306,68 +382,287 @@ namespace spot return true; if (lhs.acc > rhs.acc) return false; + // compare with id? if (bdd_less_than_stable lt; lt(lhs.cond, rhs.cond)) return true; if (rhs.cond != lhs.cond) return false; - // The destination must be sorted last - // for our self-loop optimization to work. return lhs.dst < rhs.dst; }); g_.chain_edges_(); + const auto n_states = num_states(); + + // Edges are nicely chained and there are no erased edges + // -> We can work with the edge_vector + + // Check if it is a game <-> "state-player" is defined + // if so, the graph alternates between env and player vertices, + // so there are, by definition, no self-loops + auto sp = get_named_prop>("state-player"); + const auto spe = (bool) sp; + + // The hashing is a bit delicat: We may only use the dst + // if it has no self-loop + auto use_for_hash = spe ? std::vector() + : std::vector(n_states); + + const auto& e_vec = edge_vector(); + const auto n_edges = e_vec.size(); + + // For each state we need 4 indices of the edge vector + // [first, first_non_sfirst_selflooplfloop, first_selfloop, end] + // The init value makes sure nothing is done for dead end states + auto e_idx = + std::vector>(n_states, {-1u, -1u, + -1u, -1u}); + // Like a linked list holding the non-selfloop and selfloop transitions + auto e_chain = std::vector(e_vec.size(), -1u); + + unsigned idx = 1; + + // Edges are sorted with repected to src first + const unsigned n_high = e_vec.back().src; + if (spe) + for (auto s = 0u; s < n_high; ++s) + treat(e_idx, e_vec, e_chain, + use_for_hash, idx, s, n_edges); + else + for (auto s = 0u; s < n_high; ++s) + treat(e_idx, e_vec, e_chain, + use_for_hash, idx, s, n_edges); + // Last one + if (spe) + treat(e_idx, e_vec, e_chain, + use_for_hash, idx, n_high, n_edges); + else + treat(e_idx, e_vec, e_chain, + use_for_hash, idx, n_high, n_edges); + + assert(idx == e_vec.size() && "Something went wrong during indexing"); + + auto n_players = 0u; + if (sp) + n_players = std::accumulate(sp->begin(), sp->end(), 0u); + + // Represents which states share a hash + // Head is in the unordered_map, + // hash_linked_list is like a linked list structure + // of false pointers + + auto hash_linked_list = std::vector(n_states, -1u); + auto s_to_hash = std::vector(n_states, 0); + auto env_map = + robin_hood::unordered_flat_map>(); + auto player_map = + robin_hood::unordered_flat_map>(); + env_map.reserve(n_states - n_players); + player_map.reserve(n_players); + + // Sadly we need to loop the edges twice since we have + // to check for self-loops before hashing + + auto emplace = [&hash_linked_list](auto& m, auto h, auto s) + { + auto it = m.find(h); + if (it == m.end()) + m.emplace(h, std::make_pair(s, s)); + else + { + // "tail" + auto idx = it->second.second; + assert(idx < s && "Must be monotone"); + hash_linked_list[idx] = s; + it->second.second = s; + } + }; + + // Hash all states + constexpr auto SHIFT = sizeof(size_t)/2 * CHAR_BIT; + for (auto s = 0u; s != n_states; ++s) + { + auto h = fnv::init; + const auto e = e_idx[s][3]; + for (auto i = e_idx[s][0]; i != e; ++i) + { + // If size_t has 8byte and unsigned has 4byte + // then this works fine, otherwise there might be more collisions + size_t hh = spe || use_for_hash[e_vec[i].dst] + ? e_vec[i].dst + : fnv::init; + hh <<= SHIFT; + hh += e_vec[i].cond.id(); + h ^= hh; + h *= fnv::prime; + h ^= e_vec[i].acc.hash(); + h *= fnv::prime; + } + s_to_hash[s] = h; + if (spe && (*sp)[s]) + emplace(player_map, h, s); + else + emplace(env_map, h, s); + } + // All states that might possible be merged share the same hash + // Info hash coll + //std::cout << "Hash collission rate pre merge: " + // << ((env_map.size()+player_map.size())/((float)n_states)) + // << '\n'; + + // Check whether we can merge two states + // and takes into account the self-loops + auto state_equal = [&](unsigned s1, unsigned s2) + { + auto edge_data_comp = [](const auto& lhs, + const auto& rhs) + { + if (lhs.acc < rhs.acc) + return true; + if (lhs.acc > rhs.acc) + return false; + // todo compare with id + if (bdd_less_than_stable lt; lt(lhs.cond, rhs.cond)) + return true; + return false; + }; + + + static auto checked1 = std::vector(); + static auto checked2 = std::vector(); + + auto [i1, nsl1, sl1, e1] = e_idx[s1]; + auto [i2, nsl2, sl2, e2] = e_idx[s2]; + + if ((e2-i2) != (e1-i1)) + return false; // Different number of outgoing trans + + // checked1/2 is one element larger than necessary + // the last element is always false + // and acts like a nulltermination + checked1.resize(e1-i1+1); + std::fill(checked1.begin(), checked1.end(), false); + checked2.resize(e2-i2+1); + std::fill(checked2.begin(), checked2.end(), false); + + // Try to match self-loops + // Not entirely sure when this helps exactly + while ((sl1 < e1) & (sl2 < e2)) + { + // Like a search in ordered array + if (e_vec[sl1].data() == e_vec[sl2].data()) + { + // Matched + checked1[sl1 - i1] = true; //never touches last element + checked2[sl2 - i2] = true; + // Advance both + sl1 = e_chain[sl1]; + sl2 = e_chain[sl2]; + } + else if (edge_data_comp(e_vec[sl1].data(), + e_vec[sl2].data())) + // sl1 needs to advance + sl1 = e_chain[sl1]; + else + // sl2 needs to advance + sl2 = e_chain[sl2]; + } + + // If there are no non-self-loops, in s1 + // Check if all have been correctly treated + if ((nsl1 > e1) + && std::all_of(checked1.begin(), checked1.end(), + [](const auto& e){return e; })) + return true; + + // The remaining edges need to match exactly + auto idx1 = i1; + auto idx2 = i2; + while (((idx1 < e1) & (idx2 < e2))) + { + // More efficient version? + // Skip checked edges + // Last element serves as break + for (; checked1[idx1 - i1]; ++idx1) + { + } + for (; checked2[idx2 - i2]; ++idx2) + { + } + // If one is out of bounds, so is the other + if (idx1 == e1) + { + assert(idx2 == e2); + break; + } + + + if ((e_vec[idx1].dst != e_vec[idx2].dst) + || !(e_vec[idx1].data() == e_vec[idx2].data())) + return false; + + // Advance + ++idx1; + ++idx2; + } + // All edges have bee paired + return true; + }; + const unsigned nb_states = num_states(); std::vector remap(nb_states, -1U); + for (unsigned i = 0; i != nb_states; ++i) { - auto out1 = out(i); - for (unsigned j = 0; j != i; ++j) + auto j = spe && (*sp)[i] ? player_map.at(s_to_hash[i]).first + : env_map.at(s_to_hash[i]).first; + for (; jat(e.dst) == sp->at(remap[e.dst]))) + && "States do not have the same owner"); + e.dst = remap[e.dst]; + } + if (remap[get_init_state_number()] != -1U) set_init_state(remap[get_init_state_number()]); @@ -382,6 +677,10 @@ namespace spot unsigned merged = num_states() - st; if (merged) defrag_states(remap, st); + // Info hash coll 2 + //std::cout << "Hash collission rate post merge: " + // << ((env_map.size()+player_map.size())/((float)num_states())) + // << '\n'; return merged; } @@ -942,8 +1241,36 @@ namespace spot s = newst[s]; } } + // Reassign the state-players + if (auto sp = get_named_prop>("state-player")) + { + const auto ns = (unsigned) used_states; + const auto sps = (unsigned) sp->size(); + assert(ns <= sps); + assert(sps == newst.size()); + + for (unsigned i = 0; i < sps; ++i) + { + if (newst[i] == -1u) + continue; + (*sp)[newst[i]] = (*sp)[i]; + } + sp->resize(ns); + } init_number_ = newst[init_number_]; g_.defrag_states(newst, used_states); + // Make sure we did not mess up the structure + assert([&]() + { + if (auto sp = get_named_prop>("state-player")) + { + for (const auto& e : edges()) + if (sp->at(e.src) == sp->at(e.dst)) + return false; + return true; + } + return true; + }() && "Game not alternating!"); } void twa_graph::remove_unused_ap() diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 6bb62500d..6d319eea8 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -896,10 +896,19 @@ namespace spot arena->new_edge(sink_con, sink_env, bddtrue, um.second); arena->new_edge(sink_env, sink_con, bddtrue, um.second); } - arena->new_edge(src, sink_con, missing, um.second); + arena->new_edge(src, sink_env, missing, um.second); + assert(owner->at(src) != owner->at(sink_env)); } } + assert([&]() + { + for (const auto& e : arena->edges()) + if (owner->at(e.src) == owner->at(e.dst)) + return false; + return true; + }() && "Not alternating"); + arena->set_named_prop("state-player", owner); } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index dc79f8cce..1708923c6 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -958,6 +958,10 @@ namespace spot *vs << "determinization done\nDPA has " << dpa->num_states() << " states, " << dpa->num_sets() << " colors\n"; + // The named property "state-player" is set in split_2step + // but not propagated by ntgba2dpa + alternate_players(dpa); + // Merge states knows about players dpa->merge_states(); if (bv) bv->paritize_time += sw.stop(); @@ -966,9 +970,6 @@ namespace spot << dpa->num_states() << " states\n" << "determinization and simplification took " << bv->paritize_time << " seconds\n"; - // The named property "state-player" is set in split_2step - // but not propagated by ntgba2dpa - alternate_players(dpa); break; } case algo::ACD: diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb index 5866057a1..b9e065c18 100644 --- a/tests/python/_synthesis.ipynb +++ b/tests/python/_synthesis.ipynb @@ -737,7 +737,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7458055570> >" + " *' at 0x7fcc883a7720> >" ] }, "execution_count": 8, @@ -820,7 +820,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7458055570> >" + " *' at 0x7fcc883a7720> >" ] }, "execution_count": 9, @@ -944,7 +944,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f74580553c0> >" + " *' at 0x7fcc8833aa80> >" ] }, "execution_count": 10, @@ -1042,7 +1042,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f743a5ca6c0> >" + " *' at 0x7fcc880c2ab0> >" ] }, "execution_count": 11, @@ -1210,7 +1210,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7458059f90> >" + " *' at 0x7fcc8833ae70> >" ] }, "execution_count": 12, @@ -1419,7 +1419,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7458055870> >" + " *' at 0x7fcc880c2240> >" ] }, "execution_count": 13, @@ -1432,6 +1432,4535 @@ "print(a_s.acc())\n", "a_s" ] + }, + { + "cell_type": "markdown", + "id": "0ee90b2a", + "metadata": {}, + "source": [ + "## A problematic case for merge\n", + "\n", + "This is an example graph for which the self-loop optimisation in merge_states does not work" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "06b20a8c", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880bdc30> >" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "aut.set_buchi()\n", + "aut.new_states(5)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "b = buddy.bdd_ithvar(aut.register_ap(\"b\"))\n", + "c = buddy.bdd_ithvar(aut.register_ap(\"c\"))\n", + "x = buddy.bdd_ithvar(aut.register_ap(\"x\"))\n", + "\n", + "\n", + "aut.new_edge(0, 1, buddy.bddtrue)\n", + "aut.new_edge(0, 4, buddy.bddtrue)\n", + "\n", + "# OK, edge conditions ensure \"correct\" ordering\n", + "aut.new_edge(1, 1, a)\n", + "aut.new_edge(1, 2, b)\n", + "aut.new_edge(1, 3, c)\n", + "\n", + "aut.new_edge(4, 4, a)\n", + "aut.new_edge(4, 2, b)\n", + "aut.new_edge(4, 3, c)\n", + "\n", + "aut.new_edge(2, 2, x)\n", + "aut.new_edge(3, 3, buddy.bdd_not(x))\n", + "\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "id": "8a2f2e4d", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880bdc30> >" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.merge_states()\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "id": "b40f8ce7", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c5210> >" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "aut.set_buchi()\n", + "aut.new_states(5)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "b = buddy.bdd_ithvar(aut.register_ap(\"b\"))\n", + "c = buddy.bdd_ithvar(aut.register_ap(\"c\"))\n", + "x = buddy.bdd_ithvar(aut.register_ap(\"x\"))\n", + "\n", + "\n", + "aut.new_edge(0, 1, buddy.bddtrue)\n", + "aut.new_edge(0, 4, buddy.bddtrue)\n", + "\n", + "# Not OK, all edge equal -> sorted by destination\n", + "# Fails to merge\n", + "aut.new_edge(1, 1, a)\n", + "aut.new_edge(1, 2, a)\n", + "aut.new_edge(1, 3, a)\n", + "\n", + "aut.new_edge(4, 4, a)\n", + "aut.new_edge(4, 2, a)\n", + "aut.new_edge(4, 3, a)\n", + "\n", + "aut.new_edge(2, 2, x)\n", + "aut.new_edge(3, 3, buddy.bdd_not(x))\n", + "\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "id": "1f596284", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c5210> >" + ] + }, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.merge_states()\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "id": "761b4c96", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "11\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "13\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "cond\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "b\n", + "\n", + "c\n", + "\n", + "a\n", + "\n", + "b\n", + "\n", + "c\n", + "\n", + "x\n", + "\n", + "!x\n", + "\n", + "a\n", + "\n", + "b\n", + "\n", + "c\n", + "\n", + "acc\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "0\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "1\n", + "acceptance:\n", + "Inf(0)\n", + "ap_vars:\n", + "a b c x\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c5d50> >" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "aut.set_buchi()\n", + "aut.new_states(8)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "b = buddy.bdd_ithvar(aut.register_ap(\"b\"))\n", + "c = buddy.bdd_ithvar(aut.register_ap(\"c\"))\n", + "x = buddy.bdd_ithvar(aut.register_ap(\"x\"))\n", + "\n", + "\n", + "aut.new_edge(0, 1, buddy.bddtrue)\n", + "aut.new_edge(0, 4, buddy.bddtrue)\n", + "\n", + "aut.new_edge(1, 1, a)\n", + "aut.new_edge(1, 2, b)\n", + "aut.new_edge(1, 3, c)\n", + "\n", + "aut.new_edge(4, 4, a)\n", + "aut.new_edge(4, 2, b)\n", + "aut.new_edge(4, 3, c)\n", + "\n", + "aut.new_edge(2, 2, x)\n", + "aut.new_edge(3, 3, buddy.bdd_not(x))\n", + "\n", + "aut.new_edge(5, 1, a)\n", + "aut.new_edge(5, 2, b)\n", + "aut.new_edge(5, 3, c)\n", + "\n", + "display(aut.show_storage())\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "id": "d4e09261", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c5d50> >" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.merge_states()\n", + "aut" + ] + }, + { + "cell_type": "markdown", + "id": "4a8ace82", + "metadata": {}, + "source": [ + "## Splitting can inhibit merging\n", + "\n", + "In split automata, no self-loops exist.\n", + "Therefore states that can be merged pre-split can not be merged in a split automaton" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "id": "c9e38db9", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880cd090> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "18\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "20\n", + "\n", + "\n", + "21\n", + "\n", + "\n", + "22\n", + "\n", + "\n", + "24\n", + "\n", + "\n", + "25\n", + "\n", + "\n", + "27\n", + "\n", + "\n", + "29\n", + "\n", + "\n", + "32\n", + "\n", + "\n", + "33\n", + "\n", + "\n", + "34\n", + "\n", + "\n", + "35\n", + "\n", + "\n", + "37\n", + "\n", + "\n", + "39\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "19\n", + "\n", + "\n", + "20\n", + "\n", + "\n", + "21\n", + "\n", + "\n", + "23\n", + "\n", + "\n", + "24\n", + "\n", + "\n", + "26\n", + "\n", + "\n", + "28\n", + "\n", + "\n", + "31\n", + "\n", + "\n", + "32\n", + "\n", + "\n", + "33\n", + "\n", + "\n", + "34\n", + "\n", + "\n", + "36\n", + "\n", + "\n", + "38\n", + "\n", + "\n", + "41\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "19\n", + "\n", + "\n", + "20\n", + "\n", + "\n", + "21\n", + "\n", + "\n", + "22\n", + "\n", + "\n", + "23\n", + "\n", + "\n", + "24\n", + "\n", + "\n", + "25\n", + "\n", + "\n", + "26\n", + "\n", + "\n", + "27\n", + "\n", + "\n", + "28\n", + "\n", + "\n", + "29\n", + "\n", + "\n", + "30\n", + "\n", + "\n", + "31\n", + "\n", + "\n", + "32\n", + "\n", + "\n", + "33\n", + "\n", + "\n", + "34\n", + "\n", + "\n", + "35\n", + "\n", + "\n", + "36\n", + "\n", + "\n", + "37\n", + "\n", + "\n", + "38\n", + "\n", + "\n", + "39\n", + "\n", + "\n", + "40\n", + "\n", + "\n", + "41\n", + "\n", + "cond\n", + "\n", + "1\n", + "\n", + "!a & !b & c\n", + "\n", + "!a & b & !c\n", + "\n", + "!a & b & c\n", + "\n", + "a & !b & !c\n", + "\n", + "a & !b & c\n", + "\n", + "a & b & !c\n", + "\n", + "a & b & c\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "!a & !b & c\n", + "\n", + "!a & b & !c\n", + "\n", + "!a & b & c\n", + "\n", + "a & !b & !c\n", + "\n", + "a & !b & c\n", + "\n", + "a & b & !c\n", + "\n", + "a & b & c\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "x\n", + "\n", + "!x\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "next_succ\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "0\n", + "\n", + "\n", + "19\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "23\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "26\n", + "\n", + "0\n", + "\n", + "\n", + "28\n", + "\n", + "0\n", + "\n", + "\n", + "30\n", + "\n", + "\n", + "31\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "36\n", + "\n", + "0\n", + "\n", + "\n", + "38\n", + "\n", + "0\n", + "\n", + "\n", + "40\n", + "\n", + "\n", + "41\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "1\n", + "acceptance:\n", + "Inf(0)\n", + "ap_vars:\n", + "a b c x\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "\n", + "namedprops\n", + "named properties:\n", + "state-player\n", + "synthesis-outputs\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "1->8\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "1->10\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "1->11\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "1->12\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "10->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "10->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "11->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "12->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "12->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "12->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "2->13\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "13->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "3->14\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "14->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "4->15\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "4->16\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "4->17\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "4->18\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "15->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "16->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "16->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "17->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "17->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "18->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "18->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "18->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880bdc00> >" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "aut.set_buchi()\n", + "aut.new_states(5)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "b = buddy.bdd_ithvar(aut.register_ap(\"b\"))\n", + "c = buddy.bdd_ithvar(aut.register_ap(\"c\"))\n", + "x = buddy.bdd_ithvar(aut.register_ap(\"x\"))\n", + "\n", + "\n", + "aut.new_edge(0, 1, buddy.bddtrue)\n", + "aut.new_edge(0, 4, buddy.bddtrue)\n", + "\n", + "aut.new_edge(1, 1, a)\n", + "aut.new_edge(1, 2, b)\n", + "aut.new_edge(1, 3, c)\n", + "\n", + "aut.new_edge(4, 4, a)\n", + "aut.new_edge(4, 2, b)\n", + "aut.new_edge(4, 3, c)\n", + "\n", + "aut.new_edge(2, 2, x)\n", + "aut.new_edge(3, 3, buddy.bdd_not(x))\n", + "\n", + "display(aut)\n", + "\n", + "aut = spot.split_2step(aut, x, False)\n", + "\n", + "display(aut.show_storage())\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "id": "2009f279", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "0\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "1->8\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "1->10\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "1->11\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "1->12\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "10->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "10->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "11->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "12->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "12->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "12->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "2->13\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "13->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "3->14\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "14->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "4->15\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "4->16\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "4->17\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "4->18\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "15->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "16->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "16->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "17->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "17->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "18->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "18->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "18->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880bdc00> >" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "print(aut.merge_states())\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "id": "17c8d6bc", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880cd2a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "17\n", + "\n", + "cond\n", + "\n", + "1\n", + "\n", + "!b & c\n", + "\n", + "b & !c\n", + "\n", + "b & c\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "!b & c\n", + "\n", + "b & !c\n", + "\n", + "b & c\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "x\n", + "\n", + "!x\n", + "\n", + "acc\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "next_succ\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "0\n", + "\n", + "\n", + "11\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "15\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "1\n", + "acceptance:\n", + "Inf(0)\n", + "ap_vars:\n", + "a b c x\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "\n", + "namedprops\n", + "named properties:\n", + "state-player\n", + "synthesis-outputs\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "1->8\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "2->9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "3->10\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "10->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c55a0> >" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Merging possible even in split case\n", + "aut = spot.make_twa_graph()\n", + "aut.set_buchi()\n", + "aut.new_states(5)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "b = buddy.bdd_ithvar(aut.register_ap(\"b\"))\n", + "c = buddy.bdd_ithvar(aut.register_ap(\"c\"))\n", + "x = buddy.bdd_ithvar(aut.register_ap(\"x\"))\n", + "\n", + "\n", + "aut.new_edge(0, 1, buddy.bddtrue)\n", + "aut.new_edge(0, 4, buddy.bddtrue)\n", + "\n", + "aut.new_edge(1, 2, b)\n", + "aut.new_edge(1, 3, c)\n", + "\n", + "aut.new_edge(4, 2, b)\n", + "aut.new_edge(4, 3, c)\n", + "\n", + "aut.new_edge(2, 2, x)\n", + "aut.new_edge(3, 3, buddy.bdd_not(x))\n", + "\n", + "display(aut)\n", + "\n", + "aut = spot.split_2step(aut, x, False)\n", + "\n", + "display(aut.show_storage())\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "id": "b3e90235", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "1\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "7->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "x\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "3->9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9->3\n", + "\n", + "\n", + "!x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c55a0> >" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "print(aut.merge_states())\n", + "aut" + ] + }, + { + "cell_type": "markdown", + "id": "05785bb1", + "metadata": {}, + "source": [ + "Fail case for alternate_players" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "id": "df4aa681", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "i\n", + "/\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "1\n", + "/\n", + "\n", + "o\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c5a50> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "i\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!i\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "o\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc880c5a50> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "aut.set_buchi()\n", + "i = buddy.bdd_ithvar(aut.register_ap(\"i\"))\n", + "o = buddy.bdd_ithvar(aut.register_ap(\"o\"))\n", + "\n", + "spot.set_synthesis_outputs(aut, o)\n", + "\n", + "aut.new_states(2)\n", + "aut.new_edge(0,1,i)\n", + "aut.new_edge(1,0,o,spot.mark_t([0]))\n", + "display(aut)\n", + "spot.alternate_players(aut)\n", + "display(aut)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "f3b2d981", + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": {