From 97fc3f6c0bd9732e9ec16fdb3fd34c7973155ced Mon Sep 17 00:00:00 2001 From: Philipp Schlehuber-Caissier Date: Fri, 18 Mar 2022 15:27:46 +0100 Subject: [PATCH] Introduce simplify_mealy Convenience function dispatching to minimize_mealy and reduce_mealy. Change tests accordingly * spot/twaalgos/mealy_machine.cc, spot/twaalgos/mealy_machine.hh: Here * bin/ltlsynt.cc: Use simplify * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Remove minimization, Update options * tests/core/ltlsynt.test, tests/python/synthesis.ipynb, tests/python/_synthesis.ipynb: Adapt --- bin/ltlsynt.cc | 64 +--- spot/twaalgos/mealy_machine.cc | 167 +++++++-- spot/twaalgos/mealy_machine.hh | 23 +- spot/twaalgos/synthesis.cc | 26 +- spot/twaalgos/synthesis.hh | 3 + tests/core/ltlsynt.test | 39 +- tests/python/_synthesis.ipynb | 660 +++++++++++++++++++++++---------- tests/python/synthesis.ipynb | 246 ++++++++++-- 8 files changed, 901 insertions(+), 327 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 4d118dd46..305c7a2f4 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -408,14 +408,13 @@ namespace spot::mealy_like ml; ml.success = spot::mealy_like::realizability_code::REALIZABLE_REGULAR; - if (opt_print_aiger) - // we do not care about the type, - // machine to aiger can handle it - ml.mealy_like = - spot::solved_game_to_mealy(arena, *gi); - else - ml.mealy_like = - spot::solved_game_to_separated_mealy(arena, *gi); + // By default this produces a split machine + ml.mealy_like = + spot::solved_game_to_mealy(arena, *gi); + // Keep the machine split for aiger + // else -> separated + spot::simplify_mealy_here(ml.mealy_like, *gi, + opt_print_aiger); ml.glob_cond = bddfalse; mealy_machines.push_back(ml); } @@ -429,51 +428,10 @@ namespace assert(m_like.mealy_like && "Expected success but found no mealy!"); if (!opt_real) { - spot::stopwatch sw_direct; - sw_direct.start(); - - if ((0 < gi->minimize_lvl) && (gi->minimize_lvl < 3)) - // Uses reduction or not, - // both work with mealy machines (non-separated) - reduce_mealy_here(m_like.mealy_like, gi->minimize_lvl == 2); - - auto delta = sw_direct.stop(); - - sw_direct.start(); - // todo better algo here? - m_like.mealy_like = - split_2step(m_like.mealy_like, - spot::get_synthesis_outputs(m_like.mealy_like), - false); - if (gi->bv) - gi->bv->split_time += sw_direct.stop(); - - sw_direct.start(); - if (gi->minimize_lvl >= 3) - { - sw_direct.start(); - // actual minimization, works on split mealy - m_like.mealy_like = minimize_mealy(m_like.mealy_like, - gi->minimize_lvl - 4); - delta = sw_direct.stop(); - } - - // If our goal is to have an aiger, - // we can use split or separated machines - if (!opt_print_aiger) - // Unsplit to have separated mealy - m_like.mealy_like = unsplit_mealy(m_like.mealy_like); - - if (gi->bv) - gi->bv->strat2aut_time += delta; - if (gi->verbose_stream) - *gi->verbose_stream << "final strategy has " - << m_like.mealy_like->num_states() - << " states and " - << m_like.mealy_like->num_edges() - << " edges\n" - << "minimization took " << delta - << " seconds\n"; + // Keep the machine split for aiger + // else -> separated + spot::simplify_mealy_here(m_like.mealy_like, *gi, + opt_print_aiger); } SPOT_FALLTHROUGH; } diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 36c162402..f985da506 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -135,11 +135,12 @@ namespace spot if (!is_mealy(m)) return false; - if (m->get_named_prop("state-player") == nullptr) + if (!m->get_named_prop("state-player")) { trace << "is_split_mealy(): Split mealy machine must define the named " "property \"state-player\"!\n"; } + auto sp = get_state_players(m); if (sp.size() != m->num_states()) @@ -1027,6 +1028,28 @@ namespace std::pair reorganize_mm(const_twa_graph_ptr mm, const std::vector& sp) { + // Check if the twa_graph already has the correct form + { + auto sp = get_state_players(mm); + // All player states mus be at the end + bool is_ok = true; + bool seen_player = false; + for (const auto& p : sp) + { + if (seen_player & !p) + { + is_ok = false; + break; + } + seen_player |= p; + } + if (is_ok) + return {mm, + mm->num_states() + - std::accumulate(sp.begin(), sp.end(), 0)}; + } + // We actually need to generate a new graph with the correct + // form // Purge unreachable and reorganize the graph std::vector renamed(mm->num_states(), -1u); const unsigned n_old = mm->num_states(); @@ -3607,7 +3630,7 @@ namespace spot twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm, int premin) { - assert(is_split_mealy(mm)); + assert(is_mealy(mm)); stopwatch sw; sw.start(); @@ -3615,38 +3638,33 @@ namespace spot if ((premin < -1) || (premin > 1)) throw std::runtime_error("premin has to be -1, 0 or 1"); - auto orig_spref = get_state_players(mm); - - // Check if finite traces exist - // If so, deactivate fast minimization - // todo : this is overly conservative - // If unreachable states have no outgoing edges we do not care - // but testing this as well starts to be expensive... - if (premin != -1 - && [&]() - { - for (unsigned s = 0; s < mm->num_states(); ++s) - { - auto eit = mm->out(s); - if (eit.begin() == eit.end()) - return true; - } - return false; - }()) - premin = -1; - auto do_premin = [&]()->const_twa_graph_ptr { if (premin == -1) - return mm; + { + if (!mm->get_named_prop("state-player")) + return split_2step(mm, false); + else + return mm; + } else { + bool is_split = mm->get_named_prop("state-player"); // We have a split machine -> unsplit then resplit, // as reduce mealy works on separated - auto mms = unsplit_mealy(mm); - reduce_mealy_here(mms, premin == 1); - split_separated_mealy_here(mms); - return mms; + twa_graph_ptr mms; + if (is_split) + { + auto mmi = unsplit_2step(mm); + reduce_mealy_here(mmi, premin == 1); + split_separated_mealy_here(mmi); + return mmi; + } + else + { + auto mms = reduce_mealy(mm, premin == 1); + return split_2step(mms, false); + } } }; @@ -3689,9 +3707,13 @@ namespace spot auto early_exit = [&]() { // Always keep machines split - assert(is_split_mealy_specialization(mm, mmw)); + if (mm->get_named_prop("state-player")) + assert(is_split_mealy_specialization(mm, mmw)); + else + assert(is_split_mealy_specialization(split_2step(mm, false), + mmw)); return std::const_pointer_cast(mmw); - }; + }; // If the partial solution has the same number of // states as the original automaton -> we are done @@ -3897,4 +3919,91 @@ namespace spot return p; } + + + void + simplify_mealy_here(twa_graph_ptr& m, int minimize_lvl, + bool split_out) + { + auto si = synthesis_info(); + si.minimize_lvl = minimize_lvl; + return simplify_mealy_here(m, si, split_out); + } + + void + simplify_mealy_here(twa_graph_ptr& m, synthesis_info& si, + bool split_out) + { + const auto minimize_lvl = si.minimize_lvl; + assert(is_mealy(m) + && "simplify_mealy_here(): m is not a mealy machine!"); + if (minimize_lvl < 0 || 5 < minimize_lvl) + throw std::runtime_error("simplify_mealy_here(): minimize_lvl " + "must be between 0 and 5."); + + stopwatch sw; + if (si.bv) + sw.start(); + + bool is_separated = false; + if (0 < minimize_lvl && minimize_lvl < 3) + { + // unsplit if necessary + if (m->get_named_prop("state-player")) + { + m = unsplit_mealy(m); + is_separated = true; + } + reduce_mealy_here(m, minimize_lvl == 2); + } + else if (3 <= minimize_lvl) + m = minimize_mealy(m, minimize_lvl - 4); + + // Convert to demanded output format + bool is_split = m->get_named_prop("state-player"); + if (minimize_lvl == 0) + { + if (is_split && !split_out) + m = unsplit_mealy(m); + else if (!is_split && split_out) + m = split_2step(m, false); + } + else if (0 < minimize_lvl && minimize_lvl < 3 && split_out) + { + if (is_separated) + split_separated_mealy_here(m); + else + m = split_2step(m, false); + } + else if (3 <= minimize_lvl && !split_out) + m = unsplit_mealy(m); + + if (si.bv) + { + if (si.verbose_stream) + *si.verbose_stream << "simplification took " << sw.stop() + << " seconds\n"; + si.bv->simplify_strat_time += sw.stop(); + auto n_s_env = 0u; + auto n_e_env = 0u; + if (auto sp = m->get_named_prop("state-player")) + { + n_s_env = sp->size() - std::accumulate(sp->begin(), + sp->end(), + 0u); + std::for_each(m->edges().begin(), m->edges().end(), + [&n_e_env, &sp](const auto& e) + { + n_e_env += (*sp)[e.src]; + }); + } + else + { + n_s_env = m->num_states(); + n_e_env = m->num_edges(); + } + si.bv->nb_simpl_strat_states += n_s_env; + si.bv->nb_simpl_strat_edges += n_e_env; + } + } } diff --git a/spot/twaalgos/mealy_machine.hh b/spot/twaalgos/mealy_machine.hh index 77c3968ab..7406cb61d 100644 --- a/spot/twaalgos/mealy_machine.hh +++ b/spot/twaalgos/mealy_machine.hh @@ -23,6 +23,9 @@ namespace spot { + // Forward decl + struct synthesis_info; + /// todo /// Comment je faire au mieux pour expliquer mealy dans les doc @@ -104,7 +107,7 @@ namespace spot bool output_assignment = false); /// @} - /// \brief Minimizes a split (in)completely specified mealy machine + /// \brief Minimizes an (in)completely specified mealy machine /// The approach is described in \todo TACAS /// \param premin Use reduce_mealy before applying the /// main algorithm if demanded AND @@ -138,4 +141,22 @@ namespace spot SPOT_API twa_graph_ptr mealy_product(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right); + + /// \brief Convenience function to call minimize_mealy or reduce_mealy. + /// Uses the same convention as ltlsynt for \a minimize_lvl: + /// 0: no reduction + /// 1: bisimulation based reduction + /// 2: bisimulation with output assignment + /// 3: SAT minimization + /// 4: 1 then 3 + /// 5: 2 then 3 + /// Minimizes the given machine \a m inplace, the parameter + /// \a split_out defines whether it is split or not + SPOT_API void + simplify_mealy_here(twa_graph_ptr& m, int minimize_lvl, + bool split_out); + + SPOT_API void + simplify_mealy_here(twa_graph_ptr& m, synthesis_info& si, + bool split_out); } \ No newline at end of file diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 6d4537206..7620a1098 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1051,22 +1051,25 @@ namespace spot if (!get_state_winner(arena, arena->get_init_state_number())) return nullptr; - // If we use minimizations 0,1 or 2 -> unsplit - const bool do_unsplit = gi.minimize_lvl < 3; - auto m = apply_strategy(arena, do_unsplit, false); + auto m = apply_strategy(arena, false, false); m->prop_universal(true); - if ((0 < gi.minimize_lvl) && (gi.minimize_lvl < 3)) - reduce_mealy_here(m, gi.minimize_lvl == 2); - else if (gi.minimize_lvl >= 3) - m = minimize_mealy(m, gi.minimize_lvl - 4); - if (gi.bv) { + auto sp = get_state_players(m); + auto n_s_env = sp.size() - std::accumulate(sp.begin(), + sp.end(), + 0u); + auto n_e_env = 0u; + std::for_each(m->edges().begin(), m->edges().end(), + [&n_e_env, &sp](const auto& e) + { + n_e_env += sp[e.src]; + }); gi.bv->strat2aut_time += sw.stop(); - gi.bv->nb_strat_states += m->num_states(); - gi.bv->nb_strat_edges += m->num_edges(); + gi.bv->nb_strat_states += n_s_env; + gi.bv->nb_strat_edges += n_e_env; } assert(is_mealy(m)); @@ -1200,7 +1203,8 @@ namespace spot { *vs << "direct strategy was found.\n" << "direct strat has " << strat->num_states() - << " states and " << strat->num_sets() << " colors\n"; + << " states, " << strat->num_edges() + << " edges and " << strat->num_sets() << " colors\n"; } return mealy_like{ mealy_like::realizability_code::REALIZABLE_REGULAR, diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 95590504c..46c0bc2bd 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -96,11 +96,14 @@ namespace spot double paritize_time = 0.0; double solve_time = 0.0; double strat2aut_time = 0.0; + double simplify_strat_time = 0.0; double aig_time = 0.0; unsigned nb_states_arena = 0; unsigned nb_states_arena_env = 0; unsigned nb_strat_states = 0; unsigned nb_strat_edges = 0; + unsigned nb_simpl_strat_states = 0; + unsigned nb_simpl_strat_edges = 0; unsigned nb_latches = 0; unsigned nb_gates = 0; bool realizable = false; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 215143df2..335c1b01e 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -195,7 +195,7 @@ cat >exp < GFb tanslating formula done in X seconds direct strategy was found. -direct strat has 1 states and 0 colors +direct strat has 1 states, 2 edges and 0 colors EOF ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx @@ -205,9 +205,8 @@ cat >exp < GFb tanslating formula done in X seconds direct strategy was found. -direct strat has 1 states and 0 colors -final strategy has 1 states and 2 edges -minimization took X seconds +direct strat has 1 states, 2 edges and 0 colors +simplification took X seconds EOF ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx @@ -217,7 +216,7 @@ cat >exp < GFe tanslating formula done in X seconds direct strategy was found. -direct strat has 16 states and 0 colors +direct strat has 16 states, 81 edges and 0 colors EOF ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \ --verbose --realizability --algo=lar 2> out @@ -561,9 +560,8 @@ cat >exp < GFb tanslating formula done in X seconds direct strategy was found. -direct strat has 1 states and 0 colors -final strategy has 1 states and 2 edges -minimization took X seconds +direct strat has 1 states, 2 edges and 0 colors +simplification took X seconds trying to create strategy directly for Gc direct strategy might exist but was not found. translating formula done in X seconds @@ -574,6 +572,7 @@ split inputs and outputs done in X seconds automaton has 2 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds EOF ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx @@ -588,9 +587,8 @@ cat >exp < out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx @@ -615,9 +613,8 @@ cat >exp < GFa) & G((a & c) | (!a & !c)) tanslating formula done in X seconds direct strategy was found. -direct strat has 1 states and 0 colors -final strategy has 1 states and 2 edges -minimization took X seconds +direct strat has 1 states, 2 edges and 0 colors +simplification took X seconds EOF ltlsynt -f '(GFb <-> GFa) && (G((a&c)|(!a&!c)))' --outs=b,c --verbose\ --verify --decompose=0 2> out @@ -630,9 +627,8 @@ cat >exp < FGb tanslating formula done in X seconds direct strategy was found. -direct strat has 2 states and 0 colors -final strategy has 2 states and 3 edges -minimization took X seconds +direct strat has 2 states, 3 edges and 0 colors +simplification took X seconds EOF ltlsynt -f "Fa <-> FGb" --outs=b,c --verbose --decompose=0 --verify 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx @@ -651,6 +647,7 @@ split inputs and outputs done in X seconds automaton has 9 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f "Ga <-> Gb" --outs=b --verbose --decompose=0 --verify --aiger 2> out @@ -668,6 +665,7 @@ split inputs and outputs done in X seconds automaton has 4 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds trying to create strategy directly for (a | x) -> x direct strategy might exist but was not found. translating formula done in X seconds @@ -678,6 +676,7 @@ split inputs and outputs done in X seconds automaton has 4 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f '((a|x) & (b | y) & b) => (x & y)' --outs="x,y" --aiger=ite\ @@ -697,6 +696,7 @@ split inputs and outputs done in X seconds automaton has 2 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds trying to create strategy directly for Gy direct strategy might exist but was not found. translating formula done in X seconds @@ -707,6 +707,7 @@ split inputs and outputs done in X seconds automaton has 2 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f 'G!(!x | !y)' --outs="x, y" --aiger=ite --verify --verbose 2> out @@ -760,6 +761,7 @@ split inputs and outputs done in X seconds automaton has 5 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f '(a & b) U (b & c)' --outs=b,c --decompose=yes --aiger --verbose\ @@ -780,6 +782,7 @@ split inputs and outputs done in X seconds automaton has 4 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds trying to create strategy directly for a -> c direct strategy might exist but was not found. translating formula done in X seconds @@ -790,6 +793,7 @@ split inputs and outputs done in X seconds automaton has 4 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds trying to create strategy directly for a -> d direct strategy might exist but was not found. translating formula done in X seconds @@ -800,6 +804,7 @@ split inputs and outputs done in X seconds automaton has 4 states solving game with acceptance: Streett 1 game solved in X seconds +simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f 'a => (b & c & d)' --outs=b,c,d, --decompose=yes\ diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb index 3a91415e9..5866057a1 100644 --- a/tests/python/_synthesis.ipynb +++ b/tests/python/_synthesis.ipynb @@ -3,6 +3,7 @@ { "cell_type": "code", "execution_count": 1, + "id": "c54c43ba", "metadata": {}, "outputs": [], "source": [ @@ -12,6 +13,7 @@ }, { "cell_type": "markdown", + "id": "0576f64a", "metadata": {}, "source": [ "Additional testing for synthesis" @@ -19,6 +21,7 @@ }, { "cell_type": "markdown", + "id": "e25b7989", "metadata": {}, "source": [ "Testing the different methods to solve" @@ -27,6 +30,7 @@ { "cell_type": "code", "execution_count": 2, + "id": "007107a6", "metadata": {}, "outputs": [ { @@ -50,6 +54,7 @@ { "cell_type": "code", "execution_count": 3, + "id": "a7859f19", "metadata": {}, "outputs": [ { @@ -57,43 +62,72 @@ "output_type": "stream", "text": [ "HOA: v1\n", - "States: 7\n", + "States: 21\n", "Start: 0\n", "AP: 3 \"i1\" \"i0\" \"o0\"\n", "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", + "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n", "controllable-AP: 2\n", "--BODY--\n", "State: 0\n", - "[!0&!1] 1\n", - "[!0&1] 2\n", - "[0&!1] 3\n", - "[0&1] 4\n", + "[!0&!1] 2\n", + "[!0&1] 4\n", + "[0&!1] 6\n", + "[0&1] 8\n", "State: 1\n", - "[0&1&!2] 4\n", - "[0&!1&!2] 3\n", - "[!0&1&!2] 2\n", - "[!0&!1&!2] 1\n", + "[0&1] 13\n", + "[0&!1] 18\n", + "[!0&1] 19\n", + "[!0&!1] 20\n", "State: 2\n", - "[0&!2] 4\n", - "[!0&!2] 2\n", + "[t] 1\n", "State: 3\n", - "[!0&1&2] 5\n", - "[0&1&2] 4\n", - "[!0&!1&2] 6\n", - "[0&!1&2] 3\n", + "[0] 13\n", + "[!0] 19\n", "State: 4\n", - "[!0&2] 5\n", - "[0&2] 4\n", + "[t] 3\n", "State: 5\n", - "[!0&!2] 5\n", - "[0&!2] 4\n", + "[!0&1] 10\n", + "[0&1] 11\n", + "[!0&!1] 15\n", + "[0&!1] 16\n", "State: 6\n", - "[!0&1&!2] 5\n", - "[0&1&!2] 4\n", - "[!0&!1&!2] 6\n", - "[0&!1&!2] 3\n", + "[t] 5\n", + "State: 7\n", + "[!0] 10\n", + "[0] 11\n", + "State: 8\n", + "[t] 7\n", + "State: 9\n", + "[!0] 12\n", + "[0] 13\n", + "State: 10\n", + "[2] 9\n", + "State: 11\n", + "[2] 7\n", + "State: 12\n", + "[!2] 9\n", + "State: 13\n", + "[!2] 7\n", + "State: 14\n", + "[!0&1] 12\n", + "[0&1] 13\n", + "[!0&!1] 17\n", + "[0&!1] 18\n", + "State: 15\n", + "[2] 14\n", + "State: 16\n", + "[2] 5\n", + "State: 17\n", + "[!2] 14\n", + "State: 18\n", + "[!2] 5\n", + "State: 19\n", + "[!2] 3\n", + "State: 20\n", + "[!2] 1\n", "--END--\n", "HOA: v1\n", "States: 7\n", @@ -141,163 +175,137 @@ "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", - "spot-state-player: 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1\n", + "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n", "controllable-AP: 2\n", "--BODY--\n", "State: 0\n", - "[!0&!1] 7\n", - "[!0&1] 8\n", - "[0&!1] 9\n", - "[0&1] 10\n", + "[!0&!1] 2\n", + "[!0&1] 4\n", + "[0&!1] 6\n", + "[0&1] 8\n", "State: 1\n", - "[0&1] 11\n", - "[0&!1] 12\n", - "[!0&1] 13\n", - "[!0&!1] 14\n", + "[0&1] 13\n", + "[0&!1] 18\n", + "[!0&1] 19\n", + "[!0&!1] 20\n", "State: 2\n", - "[0] 11\n", - "[!0] 13\n", + "[t] 1\n", "State: 3\n", - "[!0&1] 15\n", - "[0&1] 16\n", + "[0] 13\n", + "[!0] 19\n", + "State: 4\n", + "[t] 3\n", + "State: 5\n", + "[!0&1] 10\n", + "[0&1] 11\n", + "[!0&!1] 15\n", + "[0&!1] 16\n", + "State: 6\n", + "[t] 5\n", + "State: 7\n", + "[!0] 10\n", + "[0] 11\n", + "State: 8\n", + "[t] 7\n", + "State: 9\n", + "[!0] 12\n", + "[0] 13\n", + "State: 10\n", + "[2] 9\n", + "State: 11\n", + "[2] 7\n", + "State: 12\n", + "[!2] 9\n", + "State: 13\n", + "[!2] 7\n", + "State: 14\n", + "[!0&1] 12\n", + "[0&1] 13\n", "[!0&!1] 17\n", "[0&!1] 18\n", - "State: 4\n", - "[!0] 15\n", - "[0] 16\n", - "State: 5\n", - "[!0] 19\n", - "[0] 11\n", - "State: 6\n", - "[!0&1] 19\n", - "[0&1] 11\n", - "[!0&!1] 20\n", - "[0&!1] 12\n", - "State: 7\n", - "[t] 1\n", - "State: 8\n", - "[t] 2\n", - "State: 9\n", - "[t] 3\n", - "State: 10\n", - "[t] 4\n", - "State: 11\n", - "[!2] 4\n", - "State: 12\n", - "[!2] 3\n", - "State: 13\n", - "[!2] 2\n", - "State: 14\n", - "[!2] 1\n", "State: 15\n", - "[2] 5\n", + "[2] 14\n", "State: 16\n", - "[2] 4\n", + "[2] 5\n", "State: 17\n", - "[2] 6\n", + "[!2] 14\n", "State: 18\n", - "[2] 3\n", - "State: 19\n", "[!2] 5\n", + "State: 19\n", + "[!2] 3\n", "State: 20\n", - "[!2] 6\n", + "[!2] 1\n", "--END--\n", "HOA: v1\n", - "States: 2\n", - "Start: 1\n", + "States: 21\n", + "Start: 0\n", "AP: 3 \"i1\" \"i0\" \"o0\"\n", "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", + "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n", "controllable-AP: 2\n", "--BODY--\n", "State: 0\n", - "[0&1&!2] 1\n", - "[0&!1&!2] 1\n", - "[!0&1&!2] 0\n", - "[!0&!1&!2] 0\n", - "State: 1\n", - "[!0&1&2] 0\n", - "[0&1&2] 1\n", - "[!0&!1&2] 0\n", - "[0&!1&2] 1\n", - "--END--\n", - "HOA: v1\n", - "States: 2\n", - "Start: 1\n", - "AP: 3 \"i1\" \"i0\" \"o0\"\n", - "acc-name: all\n", - "Acceptance: 0 t\n", - "properties: trans-labels explicit-labels state-acc deterministic\n", - "controllable-AP: 2\n", - "--BODY--\n", - "State: 0\n", - "[0&1&!2] 1\n", - "[0&!1&!2] 1\n", - "[!0&1&!2] 0\n", - "[!0&!1&!2] 0\n", - "State: 1\n", - "[!0&1&2] 0\n", - "[0&1&2] 1\n", - "[!0&!1&2] 0\n", - "[0&!1&2] 1\n", - "--END--\n", - "HOA: v1\n", - "States: 6\n", - "Start: 1\n", - "AP: 3 \"i1\" \"i0\" \"o0\"\n", - "acc-name: all\n", - "Acceptance: 0 t\n", - "properties: trans-labels explicit-labels state-acc deterministic\n", - "spot-state-player: 0 0 1 1 1 1\n", - "controllable-AP: 2\n", - "--BODY--\n", - "State: 0\n", - "[0&1] 2\n", - "[0&!1] 2\n", - "[!0&1] 3\n", - "[!0&!1] 3\n", - "State: 1\n", + "[!0&!1] 2\n", "[!0&1] 4\n", - "[0&1] 5\n", - "[!0&!1] 4\n", - "[0&!1] 5\n", - "State: 2\n", - "[!2] 1\n", - "State: 3\n", - "[!2] 0\n", - "State: 4\n", - "[2] 0\n", - "State: 5\n", - "[2] 1\n", - "--END--\n", - "HOA: v1\n", - "States: 6\n", - "Start: 1\n", - "AP: 3 \"i1\" \"i0\" \"o0\"\n", - "acc-name: all\n", - "Acceptance: 0 t\n", - "properties: trans-labels explicit-labels state-acc deterministic\n", - "spot-state-player: 0 0 1 1 1 1\n", - "controllable-AP: 2\n", - "--BODY--\n", - "State: 0\n", - "[0] 2\n", - "[!0] 3\n", + "[0&!1] 6\n", + "[0&1] 8\n", "State: 1\n", - "[0] 4\n", - "[!0] 5\n", + "[0&1] 13\n", + "[0&!1] 18\n", + "[!0&1] 19\n", + "[!0&!1] 20\n", "State: 2\n", - "[!2] 1\n", + "[t] 1\n", "State: 3\n", - "[!2] 0\n", + "[0] 13\n", + "[!0] 19\n", "State: 4\n", - "[2] 1\n", + "[t] 3\n", "State: 5\n", - "[2] 0\n", + "[!0&1] 10\n", + "[0&1] 11\n", + "[!0&!1] 15\n", + "[0&!1] 16\n", + "State: 6\n", + "[t] 5\n", + "State: 7\n", + "[!0] 10\n", + "[0] 11\n", + "State: 8\n", + "[t] 7\n", + "State: 9\n", + "[!0] 12\n", + "[0] 13\n", + "State: 10\n", + "[2] 9\n", + "State: 11\n", + "[2] 7\n", + "State: 12\n", + "[!2] 9\n", + "State: 13\n", + "[!2] 7\n", + "State: 14\n", + "[!0&1] 12\n", + "[0&1] 13\n", + "[!0&!1] 17\n", + "[0&!1] 18\n", + "State: 15\n", + "[2] 14\n", + "State: 16\n", + "[2] 5\n", + "State: 17\n", + "[!2] 14\n", + "State: 18\n", + "[!2] 5\n", + "State: 19\n", + "[!2] 3\n", + "State: 20\n", + "[!2] 1\n", "--END--\n", "HOA: v1\n", - "States: 2\n", + "States: 7\n", "Start: 0\n", "AP: 3 \"i1\" \"i0\" \"o0\"\n", "acc-name: all\n", @@ -306,36 +314,277 @@ "controllable-AP: 2\n", "--BODY--\n", "State: 0\n", - "[0&2] 0\n", - "[!0&2] 1\n", + "[!0&!1] 1\n", + "[!0&1] 2\n", + "[0&!1] 3\n", + "[0&1] 4\n", "State: 1\n", - "[0&!2] 0\n", - "[!0&!2] 1\n", + "[0&1&!2] 4\n", + "[0&!1&!2] 3\n", + "[!0&1&!2] 2\n", + "[!0&!1&!2] 1\n", + "State: 2\n", + "[0&!2] 4\n", + "[!0&!2] 2\n", + "State: 3\n", + "[!0&1&2] 5\n", + "[0&1&2] 4\n", + "[!0&!1&2] 6\n", + "[0&!1&2] 3\n", + "State: 4\n", + "[!0&2] 5\n", + "[0&2] 4\n", + "State: 5\n", + "[!0&!2] 5\n", + "[0&!2] 4\n", + "State: 6\n", + "[!0&1&!2] 5\n", + "[0&1&!2] 4\n", + "[!0&!1&!2] 6\n", + "[0&!1&!2] 3\n", "--END--\n", "HOA: v1\n", - "States: 6\n", - "Start: 1\n", + "States: 21\n", + "Start: 0\n", "AP: 3 \"i1\" \"i0\" \"o0\"\n", "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", - "spot-state-player: 0 0 1 1 1 1\n", + "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n", "controllable-AP: 2\n", "--BODY--\n", "State: 0\n", - "[0] 2\n", - "[!0] 3\n", + "[!0&!1] 2\n", + "[!0&1] 4\n", + "[0&!1] 6\n", + "[0&1] 8\n", "State: 1\n", - "[0] 4\n", - "[!0] 5\n", + "[0&1] 13\n", + "[0&!1] 18\n", + "[!0&1] 19\n", + "[!0&!1] 20\n", "State: 2\n", - "[!2] 1\n", + "[t] 1\n", "State: 3\n", - "[!2] 0\n", + "[0] 13\n", + "[!0] 19\n", "State: 4\n", - "[2] 1\n", + "[t] 3\n", "State: 5\n", - "[2] 0\n", + "[!0&1] 10\n", + "[0&1] 11\n", + "[!0&!1] 15\n", + "[0&!1] 16\n", + "State: 6\n", + "[t] 5\n", + "State: 7\n", + "[!0] 10\n", + "[0] 11\n", + "State: 8\n", + "[t] 7\n", + "State: 9\n", + "[!0] 12\n", + "[0] 13\n", + "State: 10\n", + "[2] 9\n", + "State: 11\n", + "[2] 7\n", + "State: 12\n", + "[!2] 9\n", + "State: 13\n", + "[!2] 7\n", + "State: 14\n", + "[!0&1] 12\n", + "[0&1] 13\n", + "[!0&!1] 17\n", + "[0&!1] 18\n", + "State: 15\n", + "[2] 14\n", + "State: 16\n", + "[2] 5\n", + "State: 17\n", + "[!2] 14\n", + "State: 18\n", + "[!2] 5\n", + "State: 19\n", + "[!2] 3\n", + "State: 20\n", + "[!2] 1\n", + "--END--\n", + "HOA: v1\n", + "States: 21\n", + "Start: 0\n", + "AP: 3 \"i1\" \"i0\" \"o0\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc deterministic\n", + "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n", + "controllable-AP: 2\n", + "--BODY--\n", + "State: 0\n", + "[!0&!1] 2\n", + "[!0&1] 4\n", + "[0&!1] 6\n", + "[0&1] 8\n", + "State: 1\n", + "[0&1] 13\n", + "[0&!1] 18\n", + "[!0&1] 19\n", + "[!0&!1] 20\n", + "State: 2\n", + "[t] 1\n", + "State: 3\n", + "[0] 13\n", + "[!0] 19\n", + "State: 4\n", + "[t] 3\n", + "State: 5\n", + "[!0&1] 10\n", + "[0&1] 11\n", + "[!0&!1] 15\n", + "[0&!1] 16\n", + "State: 6\n", + "[t] 5\n", + "State: 7\n", + "[!0] 10\n", + "[0] 11\n", + "State: 8\n", + "[t] 7\n", + "State: 9\n", + "[!0] 12\n", + "[0] 13\n", + "State: 10\n", + "[2] 9\n", + "State: 11\n", + "[2] 7\n", + "State: 12\n", + "[!2] 9\n", + "State: 13\n", + "[!2] 7\n", + "State: 14\n", + "[!0&1] 12\n", + "[0&1] 13\n", + "[!0&!1] 17\n", + "[0&!1] 18\n", + "State: 15\n", + "[2] 14\n", + "State: 16\n", + "[2] 5\n", + "State: 17\n", + "[!2] 14\n", + "State: 18\n", + "[!2] 5\n", + "State: 19\n", + "[!2] 3\n", + "State: 20\n", + "[!2] 1\n", + "--END--\n", + "HOA: v1\n", + "States: 7\n", + "Start: 0\n", + "AP: 3 \"i1\" \"i0\" \"o0\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc deterministic\n", + "controllable-AP: 2\n", + "--BODY--\n", + "State: 0\n", + "[!0&!1] 1\n", + "[!0&1] 2\n", + "[0&!1] 3\n", + "[0&1] 4\n", + "State: 1\n", + "[0&1&!2] 4\n", + "[0&!1&!2] 3\n", + "[!0&1&!2] 2\n", + "[!0&!1&!2] 1\n", + "State: 2\n", + "[0&!2] 4\n", + "[!0&!2] 2\n", + "State: 3\n", + "[!0&1&2] 5\n", + "[0&1&2] 4\n", + "[!0&!1&2] 6\n", + "[0&!1&2] 3\n", + "State: 4\n", + "[!0&2] 5\n", + "[0&2] 4\n", + "State: 5\n", + "[!0&!2] 5\n", + "[0&!2] 4\n", + "State: 6\n", + "[!0&1&!2] 5\n", + "[0&1&!2] 4\n", + "[!0&!1&!2] 6\n", + "[0&!1&!2] 3\n", + "--END--\n", + "HOA: v1\n", + "States: 21\n", + "Start: 0\n", + "AP: 3 \"i1\" \"i0\" \"o0\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc deterministic\n", + "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n", + "controllable-AP: 2\n", + "--BODY--\n", + "State: 0\n", + "[!0&!1] 2\n", + "[!0&1] 4\n", + "[0&!1] 6\n", + "[0&1] 8\n", + "State: 1\n", + "[0&1] 13\n", + "[0&!1] 18\n", + "[!0&1] 19\n", + "[!0&!1] 20\n", + "State: 2\n", + "[t] 1\n", + "State: 3\n", + "[0] 13\n", + "[!0] 19\n", + "State: 4\n", + "[t] 3\n", + "State: 5\n", + "[!0&1] 10\n", + "[0&1] 11\n", + "[!0&!1] 15\n", + "[0&!1] 16\n", + "State: 6\n", + "[t] 5\n", + "State: 7\n", + "[!0] 10\n", + "[0] 11\n", + "State: 8\n", + "[t] 7\n", + "State: 9\n", + "[!0] 12\n", + "[0] 13\n", + "State: 10\n", + "[2] 9\n", + "State: 11\n", + "[2] 7\n", + "State: 12\n", + "[!2] 9\n", + "State: 13\n", + "[!2] 7\n", + "State: 14\n", + "[!0&1] 12\n", + "[0&1] 13\n", + "[!0&!1] 17\n", + "[0&!1] 18\n", + "State: 15\n", + "[2] 14\n", + "State: 16\n", + "[2] 5\n", + "State: 17\n", + "[!2] 14\n", + "State: 18\n", + "[!2] 5\n", + "State: 19\n", + "[!2] 3\n", + "State: 20\n", + "[!2] 1\n", "--END--\n" ] } @@ -345,7 +594,7 @@ "mm0 = spot.solved_game_to_mealy(game, si)\n", "msep0 = spot.solved_game_to_separated_mealy(game, si)\n", "msplit0 = spot.solved_game_to_split_mealy(game, si)\n", - "assert(spot.is_separated_mealy(mm0)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\n", + "assert(spot.is_mealy(mm0))\n", "assert(spot.is_separated_mealy(msep0))\n", "assert(spot.is_split_mealy(msplit0))\n", "print(mm0.to_str(\"hoa\"))\n", @@ -355,7 +604,7 @@ "mm2 = spot.solved_game_to_mealy(game, si)\n", "msep2 = spot.solved_game_to_separated_mealy(game, si)\n", "msplit2 = spot.solved_game_to_split_mealy(game, si)\n", - "assert(spot.is_separated_mealy(mm2)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\n", + "assert(spot.is_mealy(mm2))\n", "assert(spot.is_separated_mealy(msep2))\n", "assert(spot.is_split_mealy(msplit2))\n", "print(mm2.to_str(\"hoa\"))\n", @@ -365,7 +614,7 @@ "mm3 = spot.solved_game_to_mealy(game, si)\n", "msep3 = spot.solved_game_to_separated_mealy(game, si)\n", "msplit3 = spot.solved_game_to_split_mealy(game, si)\n", - "assert(spot.is_split_mealy(mm3)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\n", + "assert(spot.is_mealy(mm3))\n", "assert(spot.is_separated_mealy(msep3))\n", "assert(spot.is_split_mealy(msplit3))\n", "print(mm3.to_str(\"hoa\"))\n", @@ -376,31 +625,48 @@ { "cell_type": "code", "execution_count": 4, + "id": "fb57ac53", "metadata": {}, "outputs": [], "source": [ "mus0 = spot.unsplit_mealy(msplit0)\n", "mus2 = spot.unsplit_mealy(msplit2)\n", - "mus3 = spot.unsplit_mealy(msplit3)\n", - "mmus3 = spot.unsplit_mealy(mm3)" + "mus3 = spot.unsplit_mealy(msplit3)" ] }, { "cell_type": "code", "execution_count": 5, + "id": "40fc65b5", "metadata": {}, "outputs": [], "source": [ - "assert(mm0.equivalent_to(msep0))\n", - "assert(mm0.equivalent_to(mus0))\n", - "assert(mm2.equivalent_to(msep2))\n", - "assert(mm2.equivalent_to(mus2))\n", - "assert(mmus3.equivalent_to(msep3))\n", - "assert(mmus3.equivalent_to(mus3))" + "assert(mus0.equivalent_to(msep0))" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "f6d8b29c", + "metadata": {}, + "outputs": [], + "source": [ + "assert(mus2.equivalent_to(msep2))" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "db8d47f2", + "metadata": {}, + "outputs": [], + "source": [ + "assert(mus3.equivalent_to(msep3))" ] }, { "cell_type": "markdown", + "id": "c19beeb0", "metadata": {}, "source": [ "Testing related to #495" @@ -408,7 +674,8 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 8, + "id": "3736cd1b", "metadata": {}, "outputs": [ { @@ -470,10 +737,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fee3716f7b0> >" + " *' at 0x7f7458055570> >" ] }, - "execution_count": 6, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -486,7 +753,8 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 9, + "id": "da6a7802", "metadata": {}, "outputs": [ { @@ -552,10 +820,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fee3716f7b0> >" + " *' at 0x7f7458055570> >" ] }, - "execution_count": 7, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -567,7 +835,8 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 10, + "id": "987219a4", "metadata": {}, "outputs": [ { @@ -675,10 +944,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fee3716f630> >" + " *' at 0x7f74580553c0> >" ] }, - "execution_count": 8, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -691,7 +960,8 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 11, + "id": "958d81f2", "metadata": {}, "outputs": [ { @@ -772,10 +1042,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fee36703f60> >" + " *' at 0x7f743a5ca6c0> >" ] }, - "execution_count": 9, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -798,7 +1068,8 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 12, + "id": "078bb43e", "metadata": {}, "outputs": [ { @@ -939,10 +1210,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fee3716f930> >" + " *' at 0x7f7458059f90> >" ] }, - "execution_count": 10, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -955,7 +1226,8 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 13, + "id": "05b4a138", "metadata": {}, "outputs": [ { @@ -1147,10 +1419,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fee3716fa20> >" + " *' at 0x7f7458055870> >" ] }, - "execution_count": 11, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -1164,7 +1436,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 7ec181ebe..47cafbf41 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -9,7 +9,8 @@ "source": [ "import spot\n", "spot.setup()\n", - "from spot.jupyter import display_inline" + "from spot.jupyter import display_inline\n", + "import time" ] }, { @@ -696,7 +697,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f05083f22a0> >" + " *' at 0x7f7a0c2640c0> >" ] }, "metadata": {}, @@ -1668,7 +1669,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7f7a0c264e40> >" ] }, "metadata": {}, @@ -1855,7 +1856,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7f7a0c264d50> >" ] }, "metadata": {}, @@ -1992,7 +1993,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7f7a0c2643c0> >" ] }, "metadata": {}, @@ -2085,7 +2086,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7f7a0c264a20> >" ] }, "metadata": {}, @@ -2178,7 +2179,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7f7a0c264ea0> >" ] }, "metadata": {}, @@ -2315,7 +2316,7 @@ "\n" ], "text/plain": [ - "" + " *' at 0x7f7a0c2646f0> >" ] }, "metadata": {}, @@ -2342,8 +2343,9 @@ "for i in range(6):\n", " print(\"simplification lvl \", descr[i])\n", " si.minimize_lvl = i\n", - " mealy = spot.solved_game_to_separated_mealy(game, si)\n", - " display(mealy.show())" + " mealy = spot.solved_game_to_mealy(game, si)\n", + " spot.simplify_mealy_here(mealy, si.minimize_lvl, False)\n", + " display(mealy)" ] }, { @@ -2714,7 +2716,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3027,7 +3029,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f05082c7a20> >" + " *' at 0x7f7a0c009f00> >" ] }, "metadata": {}, @@ -3042,6 +3044,203 @@ "\n", "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "i0\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!i0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f7a0c009180> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "i0\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!i0\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -3099,10 +3298,11 @@ "!o0\n", "\n", "\n", - "\n" + "\n", + "
" ], "text/plain": [ - " *' at 0x7f05083f2300> >" + "" ] }, "metadata": {}, @@ -3179,7 +3379,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3191,8 +3391,10 @@ "spot.solve_game(game)\n", "spot.highlight_strategy(game)\n", "display(game)\n", - "mealy = spot.solved_game_to_separated_mealy(game)\n", + "mealy = spot.solved_game_to_mealy(game)\n", "display(mealy)\n", + "spot.simplify_mealy_here(mealy, 2, True)\n", + "display_inline(mealy, spot.unsplit_mealy(mealy))\n", "aig = spot.mealy_machine_to_aig(mealy, \"isop\")\n", "display(aig)" ] @@ -3306,7 +3508,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3738,7 +3940,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3803,7 +4005,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f05082c7ba0> >" + " *' at 0x7f7a0c009de0> >" ] }, "metadata": {}, @@ -3916,7 +4118,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4096,7 +4298,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4220,7 +4422,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f05082c7690> >" + " *' at 0x7f7a0c2640c0> >" ] }, "execution_count": 16,