From 98ebbea17e2edd734e29b1b112e4833f666abdb4 Mon Sep 17 00:00:00 2001 From: philipp Date: Thu, 4 Nov 2021 00:24:17 +0100 Subject: [PATCH] Renaming and clean up "Strategy" was used for mealy machines and game strategies a like. Introduced the notion of mealy machine in three different flavors: mealy machine: twa_graph with synthesis-outputs separated mealy machine: mealy machine and all transitions have conditions of the form (bdd over inputs)&(bdd over outputs) split mealy machine: mealy machine that alternates between env and player states. Needs state-players * bin/ltlsynt.cc: renaming * python/spot/impl.i: Add vector for const_twa_graph_ptr * spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Adapting functions * spot/twaalgos/mealy_machine.cc, spot/twaalgos/mealy_machine.hh: Add test functions and propagate properties correctly. Adjust for names * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Removing unnecessary functions and adapt to new names * tests/python/aiger.py, tests/python/_mealy.ipynb, tests/python/mealy.py, tests/python/synthesis.ipynb: Adjust --- bin/ltlsynt.cc | 122 +- python/spot/impl.i | 3 + spot/twaalgos/aiger.cc | 207 +- spot/twaalgos/aiger.hh | 44 +- spot/twaalgos/mealy_machine.cc | 505 ++-- spot/twaalgos/mealy_machine.hh | 121 +- spot/twaalgos/synthesis.cc | 864 +++---- spot/twaalgos/synthesis.hh | 82 +- tests/python/_mealy.ipynb | 109 +- tests/python/aiger.py | 7 +- tests/python/mealy.py | 50 +- tests/python/synthesis.ipynb | 4300 +++++++++++++++++--------------- 12 files changed, 3376 insertions(+), 3038 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 98cd49bc0..bd15d9be5 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -36,6 +36,7 @@ #include #include #include +#include #include #include #include @@ -344,7 +345,7 @@ namespace auto sub_f = sub_form.begin(); auto sub_o = sub_outs_str.begin(); - std::vector strategies; + std::vector mealy_machines; auto print_game = want_game ? [](const spot::twa_graph_ptr& game)->void @@ -359,27 +360,27 @@ namespace for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) { - spot::strategy_like_t strat + spot::mealy_like m_like { - spot::strategy_like_t::realizability_code::UNKNOWN, + spot::mealy_like::realizability_code::UNKNOWN, nullptr, bddfalse }; // If we want to print a game, // we never use the direct approach if (!want_game) - strat = + m_like = spot::try_create_direct_strategy(*sub_f, *sub_o, *gi); - switch (strat.success) + switch (m_like.success) { - case spot::strategy_like_t::realizability_code::UNREALIZABLE: + case spot::mealy_like::realizability_code::UNREALIZABLE: { std::cout << "UNREALIZABLE" << std::endl; safe_tot_time(); return 1; } - case spot::strategy_like_t::realizability_code::UNKNOWN: + case spot::mealy_like::realizability_code::UNKNOWN: { auto arena = spot::ltl_to_game(*sub_f, *sub_o, *gi); if (gi->bv) @@ -404,55 +405,75 @@ namespace // only if we need it if (!opt_real) { - spot::strategy_like_t sl; - sl.success = - spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR; - sl.strat_like = spot::create_strategy(arena, *gi); - sl.glob_cond = bddfalse; - strategies.push_back(sl); + spot::mealy_like ml; + ml.success = + spot::mealy_like::realizability_code::REALIZABLE_REGULAR; + ml.mealy_like = + spot::solved_game_to_separated_mealy(arena, *gi); + ml.glob_cond = bddfalse; + mealy_machines.push_back(ml); } break; } - case spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR: + case spot::mealy_like::realizability_code::REALIZABLE_REGULAR: { // the direct approach yielded a strategy // which can now be minimized // We minimize only if we need it - assert(strat.strat_like && "Expected success but found no strat!"); + assert(m_like.mealy_like && "Expected success but found no mealy!"); if (!opt_real) { - spot::stopwatch sw_min; - sw_min.start(); - unsigned simplify = gi->minimize_lvl; - bool do_split = 3 <= simplify; - if (do_split) - strat.strat_like = - split_2step(strat.strat_like, - spot::get_synthesis_outputs(strat.strat_like), - false); - minimize_strategy_here(strat.strat_like, simplify); - if (do_split) - strat.strat_like = spot::unsplit_2step(strat.strat_like); - auto delta = sw_min.stop(); + 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(); + } + + // 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 " - << strat.strat_like->num_states() - << " states and " - << strat.strat_like->num_edges() - << " edges\n" - << "minimization took " << delta - << " seconds\n"; + << m_like.mealy_like->num_states() + << " states and " + << m_like.mealy_like->num_edges() + << " edges\n" + << "minimization took " << delta + << " seconds\n"; } SPOT_FALLTHROUGH; } - case spot::strategy_like_t::realizability_code::REALIZABLE_DTGBA: + case spot::mealy_like::realizability_code::REALIZABLE_DTGBA: if (!opt_real) - strategies.push_back(strat); + mealy_machines.push_back(m_like); break; default: - error(2, 0, "unexpected success code during strategy generation " + error(2, 0, "unexpected success code during mealy machine generation " "(please send bug report)"); } } @@ -472,8 +493,9 @@ namespace } // If we reach this line // a strategy was found for each subformula - assert(strategies.size() == sub_form.size() - && "Strategies are missing"); + assert(mealy_machines.size() == sub_form.size() + && "There are subformula for which no mealy like object" + "has been created."); spot::aig_ptr saig = nullptr; spot::twa_graph_ptr tot_strat = nullptr; @@ -485,9 +507,9 @@ namespace spot::stopwatch sw2; if (gi->bv) sw2.start(); - saig = spot::strategies_to_aig(strategies, opt_print_aiger, - input_aps, - sub_outs_str); + saig = spot::mealy_machines_to_aig(mealy_machines, opt_print_aiger, + input_aps, + sub_outs_str); if (gi->bv) { gi->bv->aig_time = sw2.stop(); @@ -507,14 +529,14 @@ namespace else { assert(std::all_of( - strategies.begin(), strategies.end(), - [](const auto& sl) - {return sl.success == - spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR; }) - && "ltlsynt: Can not handle TGBA as strategy."); - tot_strat = strategies.front().strat_like; - for (size_t i = 1; i < strategies.size(); ++i) - tot_strat = spot::product(tot_strat, strategies[i].strat_like); + mealy_machines.begin(), mealy_machines.end(), + [](const auto& ml) + {return ml.success == + spot::mealy_like::realizability_code::REALIZABLE_REGULAR; }) + && "ltlsynt: Cannot handle TGBA as strategy."); + tot_strat = mealy_machines.front().mealy_like; + for (size_t i = 1; i < mealy_machines.size(); ++i) + tot_strat = spot::product(tot_strat, mealy_machines[i].mealy_like); printer.print(tot_strat, timer_printer_dummy); } diff --git a/python/spot/impl.i b/python/spot/impl.i index 1e7497244..63d6b25e2 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -461,6 +461,8 @@ static void handle_any_exception() %include %implicitconv std::vector; +%implicitconv std::vector; +%implicitconv std::vector; %implicitconv spot::formula; %implicitconv std::vector; @@ -670,6 +672,7 @@ def state_is_accepting(self, src) -> "bool": %template(scc_info_scc_edges) spot::internal::scc_edges const, spot::internal::keep_all>; %template(scc_info_inner_scc_edges) spot::internal::scc_edges const, spot::internal::keep_inner_scc>; %template(vector_twa_graph) std::vector; +%template(vector_const_twa_graph) std::vector; %include %include %include diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 60336be33..5b04d1f11 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -34,6 +34,7 @@ #include #include #include +#include #include #define STR(x) #x @@ -1201,12 +1202,20 @@ namespace spot }; std::vector outbddvec; + outbddvec.reserve(output_names_.size()); for (auto& ao : output_names_) outbddvec.push_back(bdd_ithvar(aut->register_ap(ao))); // Also register the ins for (auto& ai : input_names_) aut->register_ap(ai); + // Set the named prop + set_synthesis_outputs(aut, + std::accumulate(outbddvec.begin(), outbddvec.end(), + (bdd) bddtrue, + [](const bdd& b1, const bdd& b2) -> bdd + {return b1 & b2; })); + std::vector outcondbddvec; for (auto ov : outputs_) outcondbddvec.push_back(aigvar2bdd(ov)); @@ -1387,8 +1396,6 @@ namespace { assert(e.cond != bddfalse); bdd bout = bdd_exist(e.cond, all_inputs); - assert(((bout & bdd_existcomp(e.cond, all_inputs)) == e.cond) && - "Precondition (in) & (out) == cond violated"); // low is good, dc is ok, high is bad this_outc[astrat.first->edge_number(e)] = bdd_satoneshortest(bout, 0, 1, 5); @@ -1447,9 +1454,9 @@ namespace const std::vector& unused_ins = {}, const std::vector& unused_outs = {}) { - // The aiger circuit cannot encode the acceptance condition - // Test that the acceptance condition is true - for (auto&& astrat : strat_vec) + // The aiger circuit can currently noly encode separated mealy machines + + for (const auto& astrat : strat_vec) if (!astrat.first->acc().is_t()) { std::cerr << "Acc cond must be true not " << astrat.first->acc() @@ -1457,6 +1464,10 @@ namespace throw std::runtime_error("Cannot turn automaton into " "aiger circuit"); } + // This checks the acc again, but does more and is to + // costly for non-debug mode + assert(std::all_of(strat_vec.begin(), strat_vec.end(), + [](const auto& p){ return is_separated_mealy(p.first); })); // get the propositions std::vector input_names; @@ -1840,56 +1851,40 @@ namespace spot { aig_ptr - strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode) + mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode) { - if (!aut) - throw std::runtime_error("aut cannot be null"); + if (!m) + throw std::runtime_error("mealy_machine_to_aig(): " + "m cannot be null"); - return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode); + return auts_to_aiger({{m, get_synthesis_outputs(m)}}, mode); } aig_ptr - strategies_to_aig(const std::vector& strat_vec, - const char *mode) + mealy_machine_to_aig(const mealy_like& m, const char* mode) { - std::for_each(strat_vec.begin()+1, strat_vec.end(), - [usedbdd = strat_vec.at(0)->get_dict()](const auto& s) - { - if (usedbdd != s->get_dict()) - throw std::runtime_error("All strategies have to " - "share a bdd_dict!\n"); - }); + if (m.success != mealy_like::realizability_code::REALIZABLE_REGULAR) + throw std::runtime_error("mealy_machine_to_aig(): " + "Can only handle regular mealy machine, TBD"); - std::vector> new_vec; - new_vec.reserve(strat_vec.size()); - - bdd all_outputs = bddtrue; - for (auto& astrat : strat_vec) - { - bdd this_outputs = get_synthesis_outputs(astrat); - // Check if outs do not overlap - if (bdd_and(bdd_not(this_outputs), all_outputs) == bddfalse) - throw std::runtime_error("\"outs\" of strategies are not " - "distinct!.\n"); - all_outputs &= this_outputs; - new_vec.emplace_back(astrat, this_outputs); - } - return auts_to_aiger(new_vec, mode); + return mealy_machine_to_aig(m.mealy_like, mode); } aig_ptr - strategy_to_aig(const twa_graph_ptr &aut, const char *mode, + mealy_machine_to_aig(const twa_graph_ptr &m, const char *mode, const std::vector& ins, const std::vector& outs) { - if (!aut) - throw std::runtime_error("aut cannot be null"); + if (!m) + throw std::runtime_error("mealy_machine_to_aig(): " + "m cannot be null"); // Make sure ins and outs are disjoint { std::vector all_ap = ins; all_ap.insert(all_ap.end(), outs.begin(), outs.end()); - check_double_names(all_ap, "Atomic propositions appears in input " + check_double_names(all_ap, "mealy_machine_to_aig(): " + "Atomic propositions appears in input " "and output propositions; "); } // Check if there exist outs or ins that are not used by the @@ -1900,7 +1895,7 @@ namespace spot std::vector unused_ins; { std::set used_aps; - for (const auto& f : aut->ap()) + for (const auto& f : m->ap()) used_aps.insert(f.ap_name()); for (const auto& ao : outs) if (!used_aps.count(ao)) @@ -1910,25 +1905,90 @@ namespace spot unused_ins.push_back(ai); } // todo Some additional checks? - return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode, + return auts_to_aiger({{m, get_synthesis_outputs(m)}}, mode, unused_ins, unused_outs); } + aig_ptr + mealy_machine_to_aig(mealy_like& m, const char *mode, + const std::vector& ins, + const std::vector& outs) + { + if (m.success != mealy_like::realizability_code::REALIZABLE_REGULAR) + throw std::runtime_error("mealy_machine_to_aig(): " + "Can only handle regular mealy machine, TBD"); + + return mealy_machine_to_aig(m.mealy_like, mode, ins, outs); + } + + aig_ptr + mealy_machines_to_aig(const std::vector& m_vec, + const char *mode) + { + std::for_each(m_vec.begin()+1, m_vec.end(), + [usedbdd = m_vec.at(0)->get_dict()](const auto& s) + { + if (usedbdd != s->get_dict()) + throw std::runtime_error("mealy_machines_to_aig(): " + "All machines have to " + "share a bdd_dict!\n"); + }); + + std::vector> new_vec; + new_vec.reserve(m_vec.size()); + + bdd all_outputs = bddtrue; + for (auto& am : m_vec) + { + bdd this_outputs = get_synthesis_outputs(am); + // Check if outs do not overlap + if (bdd_and(bdd_not(this_outputs), all_outputs) == bddfalse) + throw std::runtime_error("mealy_machines_to_aig(): " + "\"outs\" of the machines are not " + "distinct!.\n"); + all_outputs &= this_outputs; + new_vec.emplace_back(am, this_outputs); + } + return auts_to_aiger(new_vec, mode); + } + + aig_ptr + mealy_machines_to_aig(const std::vector& m_vec, + const char *mode) + { + if (std::any_of(m_vec.cbegin(), m_vec.cend(), + [](const auto& m) + {return m.success != + mealy_like::realizability_code::REALIZABLE_REGULAR; })) + throw std::runtime_error("mealy_machines_to_aig(): " + "Can only handle regular mealy machine for " + "the moment, TBD"); + auto new_vec = std::vector(); + new_vec.reserve(m_vec.size()); + std::transform(m_vec.cbegin(), m_vec.cend(), + std::back_inserter(new_vec), + [](const auto& m){return m.mealy_like; }); + + return mealy_machines_to_aig(new_vec, mode); + } + // Note: This ignores the named property aig_ptr - strategies_to_aig(const std::vector& strat_vec, - const char *mode, - const std::vector& ins, - const std::vector>& outs) + mealy_machines_to_aig(const std::vector& m_vec, + const char *mode, + const std::vector& ins, + const std::vector>& outs) { - if (strat_vec.size() != outs.size()) - throw std::runtime_error("Expected as many outs as strategies!\n"); + if (m_vec.size() != outs.size()) + throw std::runtime_error("mealy_machines_to_aig(): " + "Expected as many outs as strategies!\n"); - std::for_each(strat_vec.begin()+1, strat_vec.end(), - [usedbdd = strat_vec.at(0)->get_dict()](auto&& it) + std::for_each(m_vec.begin()+1, m_vec.end(), + [usedbdd = m_vec.at(0)->get_dict()](auto&& it) { if (usedbdd != it->get_dict()) - throw std::runtime_error("All strategies have to " + throw std::runtime_error("mealy_machines_to_aig(): " + "All strategies have to " "share a bdd_dict!\n"); }); @@ -1944,17 +2004,17 @@ namespace spot } std::vector> new_vec; - new_vec.reserve(strat_vec.size()); + new_vec.reserve(m_vec.size()); std::set used_aps; - for (size_t i = 0; i < strat_vec.size(); ++i) + for (size_t i = 0; i < m_vec.size(); ++i) { - for (const auto& f : strat_vec[i]->ap()) + for (const auto& f : m_vec[i]->ap()) used_aps.insert(f.ap_name()); // todo Some additional checks? - new_vec.emplace_back(strat_vec[i], - get_synthesis_outputs(strat_vec[i])); + new_vec.emplace_back(m_vec[i], + get_synthesis_outputs(m_vec[i])); } // Check if there exist outs or ins that are not used by the @@ -1975,15 +2035,15 @@ namespace spot } aig_ptr - strategies_to_aig(const std::vector& strat_vec, - const char *mode, - const std::vector& ins, - const std::vector>& outs) + mealy_machines_to_aig(const std::vector& strat_vec, + const char* mode, + const std::vector& ins, + const std::vector>& outs) { // todo extend to TGBA and possibly others const unsigned ns = strat_vec.size(); - std::vector strategies; - strategies.reserve(ns); + std::vector m_machines; + m_machines.reserve(ns); std::vector> outs_used; outs_used.reserve(ns); @@ -1991,27 +2051,28 @@ namespace spot { switch (strat_vec[i].success) { - case strategy_like_t::realizability_code::UNREALIZABLE: - throw std::runtime_error("strategies_to_aig(): Partial strat is " - "not feasible!"); - case strategy_like_t::realizability_code::UNKNOWN: - throw std::runtime_error("strategies_to_aig(): Partial strat has " - "unknown status!"); - case strategy_like_t::realizability_code::REALIZABLE_REGULAR: + case mealy_like::realizability_code::UNREALIZABLE: + throw std::runtime_error("mealy_machines_to_aig(): One of the " + "mealy like machines is not realizable."); + case mealy_like::realizability_code::UNKNOWN: + throw std::runtime_error("mealy_machines_to_aig(): One of the" + "mealy like objects has " + "status \"unkwnown\""); + case mealy_like::realizability_code::REALIZABLE_REGULAR: { - strategies.push_back(strat_vec[i].strat_like); + m_machines.push_back(strat_vec[i].mealy_like); outs_used.push_back(outs[i]); break; } - case strategy_like_t::realizability_code::REALIZABLE_DTGBA: - throw std::runtime_error("strategies_to_aig(): TGBA not " - "yet supported."); + case mealy_like::realizability_code::REALIZABLE_DTGBA: + throw std::runtime_error("mealy_machines_to_aig(): TGBA not " + "yet supported - TBD"); default: - throw std::runtime_error("strategies_to_aig(): Unknown " + throw std::runtime_error("mealy_machines_to_aig(): Unknown " "success identifier."); } } - return strategies_to_aig(strategies, mode, ins, outs_used); + return mealy_machines_to_aig(m_machines, mode, ins, outs_used); } std::ostream & @@ -2073,7 +2134,7 @@ namespace spot print_aiger(std::ostream& os, const const_twa_graph_ptr& aut, const char* mode) { - print_aiger(os, strategy_to_aig(aut, mode)); + print_aiger(os, mealy_machine_to_aig(aut, mode)); return os; } } diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 4ba831b61..b58a687da 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -36,7 +36,7 @@ namespace spot { // Forward for synthesis - struct strategy_like_t; + struct mealy_like; class aig; @@ -415,8 +415,8 @@ namespace spot }; /// \ingroup synthesis - /// \brief Convert a strategy into an aig relying on the transformation - /// described by \a mode. + /// \brief Convert a mealy (like) machine into an aig relying on + /// the transformation described by \a mode. /// \param mode This param has to be of the form /// `ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2]` /// Where `ite` means encoded via if-then-else normal form, @@ -437,11 +437,18 @@ namespace spot /// outs are guaranteed to appear in the aiger circuit. ///@{ SPOT_API aig_ptr - strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode); + mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode); SPOT_API aig_ptr - strategy_to_aig(const twa_graph_ptr& aut, const char *mode, - const std::vector& ins, - const std::vector& outs); + mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode, + const std::vector& ins, + const std::vector& outs); + + SPOT_API aig_ptr + mealy_machine_to_aig(const mealy_like& m, const char* mode); + SPOT_API aig_ptr + mealy_machine_to_aig(mealy_like& m, const char *mode, + const std::vector& ins, + const std::vector& outs); ///@} /// \ingroup synthesis @@ -459,18 +466,21 @@ namespace spot /// guaranteed to appear in the aiger circuit. /// @{ SPOT_API aig_ptr - strategies_to_aig(const std::vector& strat_vec, - const char* mode); + mealy_machines_to_aig(const std::vector& m_vec, + const char* mode); SPOT_API aig_ptr - strategies_to_aig(const std::vector& strat_vec, - const char* mode, - const std::vector& ins, - const std::vector>& outs); + mealy_machines_to_aig(const std::vector& m_vec, + const char* mode); SPOT_API aig_ptr - strategies_to_aig(const std::vector& strat_vec, - const char* mode, - const std::vector& ins, - const std::vector>& outs); + mealy_machines_to_aig(const std::vector& m_vec, + const char* mode, + const std::vector& ins, + const std::vector>& outs); + SPOT_API aig_ptr + mealy_machines_to_aig(const std::vector& m_vec, + const char* mode, + const std::vector& ins, + const std::vector>& outs); /// @} diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index f19a474a2..f4b15b9d4 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -33,6 +33,7 @@ #include #include #include +#include #include #include @@ -52,11 +53,245 @@ # define dotimeprint while (0) std::cerr #endif +namespace +{ + bool is_deterministic_(const std::vector& ins) + { + const unsigned n_ins = ins.size(); + for (unsigned idx1 = 0; idx1 < n_ins - 1; ++idx1) + for (unsigned idx2 = idx1 + 1; idx2 < n_ins; ++idx2) + if (bdd_have_common_assignment(ins[idx1], ins[idx2])) + return false; + return true; + } +} +namespace spot +{ + + bool + is_mealy(const const_twa_graph_ptr& m) + { + if (!m->acc().is_t()) + { + trace << "is_mealy(): Mealy machines must have " + "true acceptance condition.\n"; + return false; + } + + if (!m->get_named_prop("synthesis-outputs")) + { + trace << "is_mealy(): \"synthesis-outputs\" not found!\n"; + return false; + } + + return true; + } + + bool + is_separated_mealy(const const_twa_graph_ptr& m) + { + if (!is_mealy(m)) + return false; + + auto outs = get_synthesis_outputs(m); + + for (const auto& e : m->edges()) + if ((bdd_exist(e.cond, outs) & bdd_existcomp(e.cond, outs)) != e.cond) + { + trace << "is_separated_mealy_machine(): Edge number " + << m->edge_number(e) << " from " << e.src << " to " << e.dst + << " with " << e.cond << " is not separated!\n"; + return false; + } + + return true; + } + + bool + is_split_mealy(const const_twa_graph_ptr& m) + { + if (!is_mealy(m)) + return false; + + if (m->get_named_prop("state-player") == nullptr) + { + 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()) + { + trace << "\"state-player\" has not the same size as the " + "automaton!\n"; + return false; + } + + if (sp[m->get_init_state_number()]) + { + trace << "is_split_mealy(): Initial state must be owned by env!\n"; + return false; + } + + auto outs = get_synthesis_outputs(m); + + for (const auto& e : m->edges()) + { + if (sp[e.src] == sp[e.dst]) + { + trace << "is_split_mealy(): Edge number " + << m->edge_number(e) << " from " << e.src << " to " << e.dst + << " is not alternating!\n"; + return false; + } + if (sp[e.src] && (bdd_exist(e.cond, outs) != bddtrue)) + { + trace << "is_split_mealy(): Edge number " + << m->edge_number(e) << " from " << e.src << " to " << e.dst + << " depends on inputs, but should be labeled by outputs!\n"; + return false; + } + if (!sp[e.src] && (bdd_existcomp(e.cond, outs) != bddtrue)) + { + trace << "is_split_mealy(): Edge number " + << m->edge_number(e) << " from " << e.src << " to " << e.dst + << " depends on outputs, but should be labeled by inputs!\n"; + return false; + } + } + return true; + } + + bool + is_input_deterministic_mealy(const const_twa_graph_ptr& m) + { + if (!is_mealy(m)) + return false; + + const unsigned N = m->num_states(); + + auto sp_ptr = m->get_named_prop("state-player"); + // Unsplit mealy -> sp_ptr == nullptr + if (sp_ptr && !is_split_mealy(m)) + return false; + + auto outs = get_synthesis_outputs(m); + + std::vector ins; + for (unsigned s = 0; s < N; ++s) + { + if (sp_ptr && (*sp_ptr)[s]) + continue; + ins.clear(); + for (const auto& e : m->out(s)) + ins.push_back(sp_ptr ? e.cond + : bdd_exist(e.cond, outs)); + if (!is_deterministic_(ins)) + { + trace << "is_input_deterministic_mealy(): State number " + << s << " is not input determinisc!\n"; + return false; + } + } + return true; + } + + void + split_separated_mealy_here(const twa_graph_ptr& m) + { + assert(is_mealy(m)); + + auto output_bdd = get_synthesis_outputs(m); + + struct dst_cond_color_t + { + std::pair dst_cond; + acc_cond::mark_t color; + }; + + auto hasher = [](const dst_cond_color_t& dcc) noexcept + { + return dcc.color.hash() ^ pair_hash()(dcc.dst_cond); + }; + auto equal = [](const dst_cond_color_t& dcc1, + const dst_cond_color_t& dcc2) noexcept + { + return (dcc1.dst_cond == dcc2.dst_cond) + && (dcc1.color == dcc2.color); + }; + + std::unordered_map player_map(m->num_edges(), + hasher, equal); + + auto get_ps = [&](unsigned dst, const bdd& ocond, + acc_cond::mark_t color) + { + dst_cond_color_t key{std::make_pair(dst, ocond.id()), + color}; + auto [it, inserted] = + player_map.try_emplace(key, m->num_states()); + if (!inserted) + return it->second; + unsigned ns = m->new_state(); + assert(ns == it->second); + m->new_edge(ns, dst, ocond, color); + return ns; + }; + + unsigned ne = m->edge_vector().size(); + for (unsigned eidx = 1; eidx < ne; ++eidx) + { + const auto& e = m->edge_storage(eidx); + if (e.next_succ == eidx) // dead edge + continue; + bdd incond = bdd_exist(e.cond, output_bdd); + bdd outcond = bdd_existcomp(e.cond, output_bdd); + assert(((incond&outcond) == e.cond) && "Precondition violated"); + // Create new state and trans + // this may invalidate "e". + unsigned new_dst = get_ps(e.dst, outcond, e.acc); + // redirect + auto& e2 = m->edge_storage(eidx); + e2.dst = new_dst; + e2.cond = incond; + } + + auto* sp_ptr = m->get_or_set_named_prop("state-player"); + + sp_ptr->resize(m->num_states()); + std::fill(sp_ptr->begin(), sp_ptr->end(), false); + for (const auto& eit : player_map) + (*sp_ptr)[eit.second] = true; + //Done + } + + twa_graph_ptr + split_separated_mealy(const const_twa_graph_ptr& m) + { + assert(is_mealy((m))); + auto m2 = make_twa_graph(m, twa::prop_set::all()); + m2->copy_acceptance_of(m); + set_synthesis_outputs(m2, get_synthesis_outputs(m)); + split_separated_mealy_here(m2); + return m2; + } + + twa_graph_ptr + unsplit_mealy(const const_twa_graph_ptr& m) + { + assert(is_split_mealy(m)); + return unsplit_2step(m); + } + +} + namespace { - // Anonymous for minimize_mealy_fast + // Anonymous for reduce_mealy using namespace spot; // Used to get the signature of the state. @@ -478,84 +713,33 @@ namespace namespace spot { - twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm, - bool use_inclusion) + twa_graph_ptr reduce_mealy(const const_twa_graph_ptr& mm, + bool output_assignment) { - bool orig_is_split = true; - bdd* outsptr = nullptr; - bdd outs = bddfalse; + assert(is_mealy(mm)); + if (mm->get_named_prop>("state-player")) + throw std::runtime_error("reduce_mealy(): " + "Only works on unsplit machines.\n"); - twa_graph_ptr mmc; - if (mm->get_named_prop>("state-player") != nullptr) - { - outsptr = mm->get_named_prop("synthesis-outputs"); - assert(outsptr && "If the original strat is split, " - "we need \"synthesis-outputs\"."); - outs = *outsptr; - mmc = unsplit_2step(mm); - } - else - { - mmc = make_twa_graph(mm, twa::prop_set::all()); - mmc->copy_ap_of(mm); - mmc->copy_acceptance_of(mm); - orig_is_split = false; - } + auto mmc = make_twa_graph(mm, twa::prop_set::all()); + mmc->copy_ap_of(mm); + mmc->copy_acceptance_of(mm); + set_synthesis_outputs(mmc, get_synthesis_outputs(mm)); - minimize_mealy_fast_here(mmc, use_inclusion); - - // Split if the initial aut was split - if (orig_is_split) - { - mmc = split_2step(mmc, outs, false); - bool orig_init_player = - mm->get_named_prop>("state-player") - ->at(mm->get_init_state_number()); - alternate_players(mmc, orig_init_player, false); - } - // Try to set outputs - if (outsptr) - mmc->set_named_prop("synthesis-outputs", new bdd(outs)); + reduce_mealy_here(mmc, output_assignment); + assert(is_mealy(mmc)); return mmc; } - void minimize_mealy_fast_here(twa_graph_ptr& mm, bool use_inclusion) + void reduce_mealy_here(twa_graph_ptr& mm, bool output_assignment) { - - bool orig_is_split = false; - bdd* outsptr = nullptr; - bdd outs = bddfalse; - - auto sp_ptr = mm->get_named_prop>("state-player"); - - bool init_player = sp_ptr ? sp_ptr->at(mm->get_init_state_number()) - : false; + assert(is_mealy(mm)); // Only consider infinite runs mm->purge_dead_states(); - if (mm->get_named_prop>("state-player") != nullptr) - { - // Check if done - if (std::count(sp_ptr->begin(), sp_ptr->end(), false) == 1) - return; - outsptr = mm->get_named_prop("synthesis-outputs"); - assert(outsptr && "If the original strat is split, " - "we need \"synthesis-outputs\"."); - outs = *outsptr; - init_player = - mm->get_named_prop>("state-player")->at( - mm->get_init_state_number()); - mm = unsplit_2step(mm); - orig_is_split = true; - } - else - // Check if done - if (mm->num_states() == 1) - return; - - auto repr = get_repres(mm, use_inclusion); + auto repr = get_repres(mm, output_assignment); if (repr[0] == -1U) return; @@ -567,25 +751,20 @@ namespace spot std::vector done(mm->num_states(), false); todo.emplace(init); while (!todo.empty()) - { - auto current = todo.top(); - todo.pop(); - done[current] = true; - for (auto& e : mm->out(current)) { - auto repr_dst = repr[e.dst]; - e.dst = repr_dst; - if (!done[repr_dst]) - todo.emplace(repr_dst); + auto current = todo.top(); + todo.pop(); + done[current] = true; + for (auto& e : mm->out(current)) + { + auto repr_dst = repr[e.dst]; + e.dst = repr_dst; + if (!done[repr_dst]) + todo.emplace(repr_dst); + } } - } mm->purge_unreachable_states(); - if (orig_is_split) - { - mm = split_2step(mm, outs, false); - alternate_players(mm, init_player, false); - mm->set_named_prop("synthesis-outputs", new bdd(outs)); - } + assert(is_mealy(mm)); } } @@ -639,7 +818,7 @@ namespace template size_t find_first_index_of(const CONT& c, PRED pred) { - size_t s = c.size(); + const size_t s = c.size(); for (unsigned i = 0; i < s; ++i) if (pred(c[i])) return i; @@ -874,8 +1053,8 @@ namespace std::vector spnew(n_new, true); std::fill(spnew.begin(), spnew.begin()+n_env, false); - omm->set_named_prop("state-player", - new std::vector(std::move(spnew))); + set_state_players(omm, std::move(spnew)); + set_synthesis_outputs(omm, get_synthesis_outputs(mm)); // Make sure we have a proper strategy, // that is each player state has only one successor @@ -1217,7 +1396,7 @@ namespace #ifdef TRACE trace << "We found " << n_group << " groups.\n"; for (unsigned s = 0; s < n_env; ++s) - trace << s << " : " << which_group[s] << '\n'; + trace << s << " : " << which_group.at(s) << '\n'; #endif return std::make_pair(n_group, which_group); } @@ -1640,7 +1819,7 @@ namespace split_mmw->get_graph().chain_edges_(); #ifdef TRACE trace << "Orig split aut\n"; - print_hoa(std::cerr, split_mmw) << '\n'; + print_hoa(std::cerr, mmw) << '\n'; { auto ss = make_twa_graph(split_mmw, twa::prop_set::all()); for (unsigned group = 0; group < red.n_groups; ++group) @@ -1652,10 +1831,9 @@ namespace bdd_ithvar(ss->register_ap("g"+std::to_string(group) +"e"+std::to_string(i)))); } - const unsigned ns = ss->num_states(); - for (unsigned s = 0; s < ns; ++s) + for (unsigned s = 0; s < n_env; ++s) { - if (red.which_group[s] != group) + if (red.which_group.at(s) != group) continue; for (auto& e : ss->out(s)) e.cond = @@ -1676,8 +1854,8 @@ namespace for (const auto& idx_vec : red.bisim_letters[i]) trace << red.minimal_letters_vec[i][idx_vec.front()].id() << '\n'; trace << "ids in the edge of the group\n"; - for (unsigned s = 0; s < split_mmw->num_states(); ++s) - if (red.which_group[s] == i) + for (unsigned s = 0; s < n_env; ++s) + if (red.which_group.at(s) == i) for (const auto& e : split_mmw->out(s)) trace << e.src << "->" << e.dst << ':' << e.cond.id() << '\n'; } @@ -2763,64 +2941,14 @@ namespace return gmm2cond; } - void cstr_unsplit(twa_graph_ptr& minmach, - const reduced_alphabet_t& red, - const std::vector>>& - x_in_class, - std::unordered_map& used_ziaj_map) - { - const unsigned n_groups = red.n_groups; - // For each minimal letter, create the (input) condition that it represents - // This has to be created for each minimal letters - // and might be shared between alphabets - std::vector> gmm2cond - = comp_represented_cond(red); - // Use a new map to reduce the number of edges created - // iaj.i: src_class or 0 - // iaj.a: id of out condition - // iaj.j: dst_class - std::unordered_map - edge_map(2*used_ziaj_map.size(), iaj_hash, iaj_eq); - - for (unsigned group = 0; group < n_groups; ++group) - { - edge_map.clear(); - - // Attention the a in used_ziaj corresponds to the index - for (const auto& [iaj, outcond] : used_ziaj_map) - { - if (x_in_class[iaj.i].first != group) - continue; - - const bdd& repr_cond = gmm2cond[group].at(iaj.a); - - // Check if there already exists a suitable edge - auto [itedge, inserted] = - edge_map.try_emplace({iaj.i, (unsigned) outcond.id(), iaj.j}, - repr_cond); - if (!inserted) - itedge->second |= repr_cond; - } - // Create the actual edges - - for (const auto& ep : edge_map) - minmach->new_edge(ep.first.i, ep.first.j, - ep.second & bdd_from_int((int) ep.first.a)); - } - } - - void cstr_keep_split(twa_graph_ptr& minmach, - const reduced_alphabet_t& red, - const std::vector>>& - x_in_class, - std::unordered_map& used_ziaj_map) + void cstr_split_mealy(twa_graph_ptr& minmach, + const reduced_alphabet_t& red, + const std::vector>>& + x_in_class, + std::unordered_map& used_ziaj_map) { const unsigned n_env_states = minmach->num_states(); // For each minimal letter, create the (input) condition that it represents @@ -2895,11 +3023,10 @@ namespace } // Set the state-player - std::vector sp(minmach->num_states(), true); + auto* sp = new std::vector(minmach->num_states(), true); for (unsigned i = 0; i < n_env_states; ++i) - sp[i] = false; - minmach->set_named_prop("state-player", - new std::vector(std::move(sp))); + (*sp)[i] = false; + minmach->set_named_prop("state-player", sp); } // This function refines the sat constraints in case the @@ -3185,7 +3312,6 @@ namespace const reduced_alphabet_t& red, const part_sol_t& psol, const unsigned n_env, - bool keep_split, stopwatch& sw) { const auto& psolv = psol.psol; @@ -3432,10 +3558,7 @@ namespace continue; //retry } - if (keep_split) - cstr_keep_split(minmach, red, x_in_class, used_ziaj_map); - else - cstr_unsplit(minmach, red, x_in_class, used_ziaj_map); + cstr_split_mealy(minmach, red, x_in_class, used_ziaj_map); // todo: What is the impact of chosing one of the possibilities minmach->set_init_state(init_class_v.front()); @@ -3447,26 +3570,17 @@ namespace namespace spot { twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm, - int premin, bool keep_split) + int premin) { + assert(is_split_mealy(mm)); + stopwatch sw; sw.start(); if ((premin < -1) || (premin > 1)) throw std::runtime_error("premin has to be -1, 0 or 1"); - if (!mm->acc().is_t()) - throw std::runtime_error("Mealy machine needs true acceptance!\n"); - auto orig_spref = get_state_players(mm); - if (orig_spref.size() != mm->num_states()) - throw std::runtime_error("Inconsistent \"state-player\""); - - if (std::any_of(mm->edges().begin(), mm->edges().end(), - [&](const auto& e){return orig_spref[e.src] - == orig_spref[e.dst]; })) - throw std::runtime_error("Arena is not alternating!"); - // Check if finite traces exist // If so, deactivate fast minimization @@ -3491,10 +3605,18 @@ namespace spot if (premin == -1) return mm; else - return minimize_mealy_fast(mm, premin == 1); + { + // 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; + } }; const_twa_graph_ptr mmw = do_premin(); + assert(is_split_mealy(mmw)); dotimeprint << "Done premin " << sw.stop() << '\n'; // 0 -> "Env" next is input props @@ -3508,6 +3630,7 @@ namespace spot // second black : player-states unsigned n_env = -1u; std::tie(mmw, n_env) = reorganize_mm(mmw, spref); + assert(is_split_mealy(mmw)); #ifdef TRACE print_hoa(std::cerr, mmw); #endif @@ -3530,15 +3653,9 @@ namespace spot auto early_exit = [&]() { - if (keep_split) - return std::const_pointer_cast(mmw); - else - { - auto mmw_u = unsplit_2step(mmw); - // todo correct unsplit to avoid this - mmw_u->purge_unreachable_states(); - return mmw_u; - } + // Always keep machines split + assert(is_split_mealy_specialization(mm, mmw)); + return std::const_pointer_cast(mmw); }; // If the partial solution has the same number of @@ -3576,7 +3693,6 @@ namespace spot minmachine = try_build_min_machine(mm_pb, mmw, reduced_alphabet, partsol, n_env, - keep_split, sw); dotimeprint << "Done try_build " << n_classes << " - " << sw.stop() << '\n'; @@ -3591,35 +3707,32 @@ namespace spot // Set state players! if (!minmachine) return early_exit(); - // Try to set outputs - if (bdd* outptr = mm->get_named_prop("synthesis-outputs")) - minmachine->set_named_prop("synthesis-outputs", new bdd(*outptr)); + set_synthesis_outputs(minmachine, get_synthesis_outputs(mm)); dotimeprint << "Done minimizing - " << minmachine->num_states() << " - " << sw.stop() << '\n'; + + assert(is_split_mealy_specialization(mm, minmachine)); return minmachine; } } namespace spot { - bool is_mealy_specialization(const_twa_graph_ptr left, - const_twa_graph_ptr right, - bool verbose) + bool is_split_mealy_specialization(const_twa_graph_ptr left, + const_twa_graph_ptr right, + bool verbose) { + assert(is_split_mealy(left)); + assert(is_split_mealy(right)); + auto& spl = get_state_players(left); auto& spr = get_state_players(right); const unsigned initl = left->get_init_state_number(); const unsigned initr = right->get_init_state_number(); - if (spl[initl]) - throw std::runtime_error("left: Mealy machine must have an " - "environment controlled initial state."); - if (spr[initr]) - throw std::runtime_error("right: Mealy machine must have an " - "environment controlled initial state."); - #ifndef NDEBUG + // todo auto check_out = [](const const_twa_graph_ptr& aut, const auto& sp) { diff --git a/spot/twaalgos/mealy_machine.hh b/spot/twaalgos/mealy_machine.hh index 0c555534b..139f7cce2 100644 --- a/spot/twaalgos/mealy_machine.hh +++ b/spot/twaalgos/mealy_machine.hh @@ -23,48 +23,109 @@ namespace spot { - /// \brief Minimizes an (in)completely specified mealy machine + /// todo + /// Comment je faire au mieux pour expliquer mealy dans les doc + + /// \brief Checks whether or not the automaton is a mealy machine + /// + /// \param m The automaton to be verified + /// \note A mealy machine must have the named property \"synthesis-outputs\" + /// and have a \"true\" as acceptance condition + SPOT_API bool + is_mealy(const const_twa_graph_ptr& m); + + /// \brief Checks whether or not the automaton is a separated mealy machine + /// + /// \param m The automaton to be verified + /// \note A separated mealy machine is a mealy machine machine with all + /// transitions having the form (in)&(out) where in[out] is a bdd over + /// input[output] propositions of m + SPOT_API bool + is_separated_mealy(const const_twa_graph_ptr& m); + + /// \brief Checks whether or not the automaton is a split mealy machine + /// + /// \param m The automaton to be verified + /// \note A split mealy machine is a mealy machine machine with the named + /// property \"state-player\". Moreover the underlying automaton + /// must be alternating between the player and the env. Transitions + /// leaving env[player] states can only be labeled by + /// input[output] propositions. + SPOT_API bool + is_split_mealy(const const_twa_graph_ptr& m); + + /// \brief Checks whether or not a mealy machine is input deterministic + /// + /// \param m The automaton to be verified + /// \note works all mealy machines, no matter whether they are split + /// or separated or neither of neither of them. + /// \note A machine is input deterministic if none of the states + /// has two outgoing transitions that can agree on a assignement + /// of the input propositions. + SPOT_API bool + is_input_deterministic_mealy(const const_twa_graph_ptr& m); + + + /// \brief make each transition in a separated mealy machine a + /// 2-step transition. + /// + /// \param m separated mealy machine to be split + /// \return returns the equivalent split mealy machine if not done inplace + /// @{ + SPOT_API twa_graph_ptr + split_separated_mealy(const const_twa_graph_ptr& m); + + SPOT_API void + split_separated_mealy_here(const twa_graph_ptr& m); + /// @} + + /// \brief the inverse of split_separated_mealy + SPOT_API twa_graph_ptr + unsplit_mealy(const const_twa_graph_ptr& m); + + /// \brief reduce an (in)completely specified mealy machine /// Based on signature inclusion or equality. This is not guaranteed /// to find the minimal number of states but is usually faster. /// This also comes at another drawback: /// All applicable sequences have to be infinite. Finite /// traces are disregarded - /// \Note The graph does not have to be split into env and player - /// states as for minimize_mealy - SPOT_API - void minimize_mealy_fast_here(twa_graph_ptr& mm, - bool use_inclusion = false); + /// \param mm The mealy machine to be minimized, has to be unsplit + /// \param output_assignment Whether or not to use output assignment + /// \return A specialization of \c mm. Note that if mm is separated, + /// the returned machine is separated as well. + /// \note See todo TACAS22 Effective reductions of mealy machines + /// @{ + SPOT_API twa_graph_ptr + reduce_mealy(const const_twa_graph_ptr& mm, + bool output_assignment = false); - /// \brief Like minimize_mealy_fast_here - SPOT_API - twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm, - bool use_inclusion = false); + SPOT_API void + reduce_mealy_here(twa_graph_ptr& mm, + bool output_assignment = false); + /// @} - /// \brief Minimizes an (in)completely specified mealy machine - /// The approach is basically described in \cite abel2015memin - /// \param premin Use minimize_mealy_fast before applying the + /// \brief Minimizes a split (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 /// the original machine has no finite trace. /// -1 : Do not use; - /// 0 : Use without inclusion; - /// 1 : Use with inclusion - /// \param keep_split Whether or not to keep the automaton states - /// partitioned into player and env states - /// \pre Graph must be split into env states and player states, - /// such that they alternate. Edges leaving env states must be labeled - /// with input proposition and edges leaving player states must be - /// labeled with output propositions. - SPOT_API - twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm, - int premin = -1, - bool keep_split = true); + /// 0 : Use without output assignment; + /// 1 : Use with output assignment + /// \return Returns a split mealy machines which is a minimal + /// speciliazation of the original machine + SPOT_API twa_graph_ptr + minimize_mealy(const const_twa_graph_ptr& mm, int premin = -1); - /// \brief Test if the mealy machine \a right is a specialization of - /// the mealy machine \a left. That is all input sequences valid for left + /// \brief Test if the split mealy machine \a right is a specialization of + /// the split mealy machine \a left. + /// + /// That is all input sequences valid for left /// must be applicable for right and the induced sequence of output signals /// of right must imply the ones of left - SPOT_API bool is_mealy_specialization(const_twa_graph_ptr left, - const_twa_graph_ptr right, - bool verbose = false); + SPOT_API bool + is_split_mealy_specialization(const_twa_graph_ptr left, + const_twa_graph_ptr right, + bool verbose = false); } \ No newline at end of file diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 45de43928..ca176dfcd 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -39,6 +39,7 @@ // Helper function/structures for split_2step namespace{ + using namespace spot; // Computes and stores the restriction // of each cond to the input domain and the support // This is useful as it avoids recomputation @@ -47,9 +48,9 @@ namespace{ struct small_cacher_t { //e to e_in and support - std::unordered_map, spot::bdd_hash> cond_hash_; + std::unordered_map, bdd_hash> cond_hash_; - void fill(const spot::const_twa_graph_ptr& aut, bdd output_bdd) + void fill(const const_twa_graph_ptr& aut, bdd output_bdd) { cond_hash_.reserve(aut->num_edges()/5+1); // 20% is about lowest number of different edge conditions @@ -79,28 +80,28 @@ namespace{ // of the state. struct e_info_t { - e_info_t(const spot::twa_graph::edge_storage_t& e, + e_info_t(const twa_graph::edge_storage_t& e, const small_cacher_t& sm) : dst(e.dst), econd(e.cond), einsup(sm[e.cond]), acc(e.acc) { - pre_hash = (spot::wang32_hash(dst) - ^ std::hash()(acc)) - * spot::fnv::prime; + pre_hash = (wang32_hash(dst) + ^ std::hash()(acc)) + * fnv::prime; } inline size_t hash() const { - return spot::wang32_hash(spot::bdd_hash()(econdout)) ^ pre_hash; + return wang32_hash(bdd_hash()(econdout)) ^ pre_hash; } unsigned dst; bdd econd; mutable bdd econdout; std::pair einsup; - spot::acc_cond::mark_t acc; + acc_cond::mark_t acc; size_t pre_hash; }; // We define an order between the edges to avoid creating multiple @@ -129,6 +130,313 @@ namespace{ < std::tie(rhs->dst, rhs->acc, r_id); } }less_info_ptr; + + // Improved apply strat, that reduces the number of edges/states + // while keeping the needed edge-properties + // Note, this only deals with deterministic strategies + // Note, assumes that env starts playing + twa_graph_ptr + apply_strategy(const twa_graph_ptr& arena, + bool unsplit, bool keep_acc) + { + const auto& win = get_state_winners(arena); + const auto& strat = get_strategy(arena); + const auto& sp = get_state_players(arena); + auto outs = get_synthesis_outputs(arena); + + if (!win[arena->get_init_state_number()]) + throw std::runtime_error("Player does not win initial state, strategy " + "is not applicable"); + + assert((sp[arena->get_init_state_number()] == false) + && "Env needs to have first turn!"); + + assert(std::none_of(arena->edges().begin(), arena->edges().end(), + [&sp](const auto& e) + { bool same_player = sp.at(e.src) == sp.at(e.dst); + if (same_player) + std::cerr << e.src << " and " << e.dst << " belong to same " + << "player, arena not alternating!\n"; + return same_player; })); + + auto strat_split = make_twa_graph(arena->get_dict()); + strat_split->copy_ap_of(arena); + if (keep_acc) + strat_split->copy_acceptance_of(arena); + else + strat_split->acc().set_acceptance(acc_cond::acc_code::t()); + + std::stack todo; + todo.push(arena->get_init_state_number()); + + struct dca{ + unsigned dst; + unsigned condvar; + acc_cond::mark_t acc; + }; + struct dca_hash + { + size_t operator()(const dca& d) const noexcept + { + return pair_hash()(std::make_pair(d.dst, d.condvar)) + ^ wang32_hash(d.acc.hash()); + } + }; + struct dca_equal + { + bool operator()(const dca& d1, const dca& d2) const noexcept + { + return std::tie(d1.dst, d1.condvar, d1.acc) + == std::tie(d2.dst, d2.condvar, d2.acc); + } + }; + + //env dst + player cond + acc -> p stat + std::unordered_map p_map; + + constexpr unsigned unseen_mark = std::numeric_limits::max(); + std::vector env_map(arena->num_states(), unseen_mark); + strat_split->set_init_state(strat_split->new_state()); + env_map[arena->get_init_state_number()] = + strat_split->get_init_state_number(); + + // The states in the new graph are qualified local + // Get a local environment state + auto get_sel = [&](unsigned s) + { + if (SPOT_UNLIKELY(env_map[s] == unseen_mark)) + env_map[s] = strat_split->new_state(); + return env_map[s]; + }; + + // local dst + // Check if there exists already a local player state + // that has the same dst, cond and (if keep_acc is true) acc + auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc) + { + dca d{dst, (unsigned) cond.id(), acc}; + auto it = p_map.find(d); + if (it != p_map.end()) + return it->second; + unsigned ns = strat_split->new_state(); + p_map[d] = ns; + strat_split->new_edge(ns, dst, cond, acc); + return ns; + }; + + while (!todo.empty()) + { + unsigned src_env = todo.top(); + unsigned src_envl = get_sel(src_env); + todo.pop(); + // All env edges + for (const auto& e_env : arena->out(src_env)) + { + // Get the corresponding strat + const auto& e_strat = arena->edge_storage(strat[e_env.dst]); + // Check if already explored + if (env_map[e_strat.dst] == unseen_mark) + todo.push(e_strat.dst); + unsigned dst_envl = get_sel(e_strat.dst); + // The new env edge, player is constructed automatically + auto used_acc = keep_acc ? e_strat.acc : acc_cond::mark_t({}); + strat_split->new_edge(src_envl, + get_spl(dst_envl, e_strat.cond, used_acc), + e_env.cond, used_acc); + } + } + // All states exists, we can try to further merge them + // Specialized merge + std::vector spnew(strat_split->num_states(), false); + for (const auto& p : p_map) + spnew[p.second] = true; + + // Sorting edges in place + auto comp_edge = [](const auto& e1, const auto& e2) + { + return std::tuple(e1.dst, e1.acc, e1.cond.id()) + < std::tuple(e2.dst, e2.acc, e2.cond.id()); + }; + // todo, replace with sort_edges_of_ in graph + auto sort_edges_of = + [&, &split_graph = strat_split->get_graph()](unsigned s) + { + static std::vector edge_nums; + edge_nums.clear(); + + auto eit = strat_split->out(s); + const auto eit_e = eit.end(); + // 0 Check if it is already sorted + if (std::is_sorted(eit.begin(), eit_e, comp_edge)) + return false; // No change + // 1 Get all edges numbers and sort them + std::transform(eit.begin(), eit_e, std::back_inserter(edge_nums), + [&](const auto& e) + { return strat_split->edge_number(e); }); + std::sort(edge_nums.begin(), edge_nums.end(), + [&](unsigned ne1, unsigned ne2) + { return comp_edge(strat_split->edge_storage(ne1), + strat_split->edge_storage(ne2)); }); + // 2 Correct the order + auto& sd = split_graph.state_storage(s); + sd.succ = edge_nums.front(); + sd.succ_tail = edge_nums.back(); + const unsigned n_edges_p = edge_nums.size()-1; + for (unsigned i = 0; i < n_edges_p; ++i) + split_graph.edge_storage(edge_nums[i]).next_succ = edge_nums[i+1]; + split_graph.edge_storage(edge_nums.back()).next_succ = 0; //terminal + // All nicely chained + return true; + }; + auto merge_edges_of = [&](unsigned s) + { + // Call this after sort edges of + // Mergeable edges are nicely chained + bool changed = false; + auto eit = strat_split->out_iteraser(s); + unsigned idx_last = strat_split->edge_number(*eit); + ++eit; + while (eit) + { + auto& e_last = strat_split->edge_storage(idx_last); + if (std::tie(e_last.dst, e_last.acc) + == std::tie(eit->dst, eit->acc)) + { + //Same dest and acc -> or condition + e_last.cond |= eit->cond; + eit.erase(); + changed = true; + } + else + { + idx_last = strat_split->edge_number(*eit); + ++eit; + } + } + return changed; + }; + auto merge_able = [&](unsigned s1, unsigned s2) + { + auto eit1 = strat_split->out(s1); + auto eit2 = strat_split->out(s2); + // Note: No self-loops here + return std::equal(eit1.begin(), eit1.end(), + eit2.begin(), eit2.end(), + [](const auto& e1, const auto& e2) + { + return std::tuple(e1.dst, e1.acc, e1.cond.id()) + == std::tuple(e2.dst, e2.acc, e2.cond.id()); + }); + }; + + const unsigned n_sstrat = strat_split->num_states(); + std::vector remap(n_sstrat, -1u); + bool changed_any; + std::vector to_check; + to_check.reserve(n_sstrat); + // First iteration -> all env states are candidates + for (unsigned i = 0; i < n_sstrat; ++i) + if (!spnew[i]) + to_check.push_back(i); + + while (true) + { + changed_any = false; + std::for_each(to_check.begin(), to_check.end(), + [&](unsigned s){ sort_edges_of(s); merge_edges_of(s); }); + // Check if we can merge env states + for (unsigned s1 : to_check) + for (unsigned s2 = 0; s2 < n_sstrat; ++s2) + { + if (spnew[s2] || (s1 == s2)) + continue; // Player state or s1 == s2 + if ((remap[s2] < s2)) + continue; //s2 is already remapped + if (merge_able(s1, s2)) + { + changed_any = true; + if (s1 < s2) + remap[s2] = s1; + else + remap[s1] = s2; + break; + } + } + + if (!changed_any) + break; + // Redirect changed targets and set possibly mergeable states + to_check.clear(); + for (auto& e : strat_split->edges()) + if (remap[e.dst] != -1u) + { + e.dst = remap[e.dst]; + to_check.push_back(e.src); + assert(spnew[e.src]); + } + + // Now check the player states + // We can skip sorting -> only one edge + // todo change when multistrat + changed_any = false; + for (unsigned s1 : to_check) + for (unsigned s2 = 0; s2 < n_sstrat; ++s2) + { + if (!spnew[s2] || (s1 == s2)) + continue; // Env state or s1 == s2 + if ((remap[s2] < s2)) + continue; //s2 is already remapped + if (merge_able(s1, s2)) + { + changed_any = true; + if (s1 < s2) + remap[s2] = s1; + else + remap[s1] = s2; + break; + } + } + + if (!changed_any) + break; + // Redirect changed targets and set possibly mergeable states + to_check.clear(); + for (auto& e : strat_split->edges()) + if (remap[e.dst] != -1u) + { + e.dst = remap[e.dst]; + to_check.push_back(e.src); + assert(!spnew[e.src]); + } + } + + // Defrag and alternate + if (remap[strat_split->get_init_state_number()] != -1u) + strat_split->set_init_state(remap[strat_split->get_init_state_number()]); + unsigned st = 0; + for (auto& s: remap) + if (s == -1U) + s = st++; + else + s = -1U; + + strat_split->defrag_states(remap, st); + + alternate_players(strat_split, false, false); + // What we do now depends on whether we unsplit or not + if (unsplit) + { + auto final = unsplit_2step(strat_split); + set_synthesis_outputs(final, outs); + return final; + } + + set_synthesis_outputs(strat_split, outs); + return strat_split; + } } namespace spot @@ -142,7 +450,7 @@ namespace spot split->copy_acceptance_of(aut); split->new_states(aut->num_states()); split->set_init_state(aut->get_init_state_number()); - split->set_named_prop("synthesis-output", new bdd(output_bdd)); + split->set_named_prop("synthesis-outputs", new bdd(output_bdd)); auto [is_unsat, unsat_mark] = aut->acc().unsat_mark(); if (!is_unsat && complete_env) @@ -318,89 +626,13 @@ namespace spot if (sink_env != -1u) owner->at(sink_env) = false; split->set_named_prop("state-player", owner); + split->set_named_prop("synthesis-outputs", + new bdd(output_bdd)); // Done return split; } - void - split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd) - { - struct dst_cond_color_t - { - std::pair dst_cond; - acc_cond::mark_t color; - }; - - auto hasher = [](const dst_cond_color_t& dcc) noexcept - { - return dcc.color.hash() ^ pair_hash()(dcc.dst_cond); - }; - auto equal = [](const dst_cond_color_t& dcc1, - const dst_cond_color_t& dcc2) noexcept - { - return (dcc1.dst_cond == dcc2.dst_cond) - && (dcc1.color == dcc2.color); - }; - - std::unordered_map player_map(aut->num_edges(), - hasher, equal); - - auto get_ps = [&](unsigned dst, const bdd& ocond, - acc_cond::mark_t color) - { - dst_cond_color_t key{std::make_pair(dst, ocond.id()), - color}; - auto [it, inserted] = - player_map.try_emplace(key, aut->num_states()); - if (!inserted) - return it->second; - unsigned ns = aut->new_state(); - assert(ns == it->second); - aut->new_edge(ns, dst, ocond, color); - return ns; - }; - - unsigned ne = aut->edge_vector().size(); - for (unsigned eidx = 1; eidx < ne; ++eidx) - { - const auto& e = aut->edge_storage(eidx); - if (e.next_succ == eidx) // dead edge - continue; - bdd incond = bdd_exist(e.cond, output_bdd); - bdd outcond = bdd_existcomp(e.cond, output_bdd); - assert(((incond&outcond) == e.cond) && "Precondition violated"); - // Create new state and trans - // this may invalidate "e". - unsigned new_dst = get_ps(e.dst, outcond, e.acc); - // redirect - auto& e2 = aut->edge_storage(eidx); - e2.dst = new_dst; - e2.cond = incond; - } - - auto* sp_ptr = - aut->get_or_set_named_prop>("state-player"); - - sp_ptr->resize(aut->num_states()); - std::fill(sp_ptr->begin(), sp_ptr->end(), false); - for (auto& eit : player_map) - (*sp_ptr)[eit.second] = true; - //Done - } - - twa_graph_ptr - split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd) - { - auto aut2 = make_twa_graph(aut, twa::prop_set::all()); - aut2->copy_acceptance_of(aut); - aut2->set_named_prop("synthesis-output", new bdd(output_bdd)); - split_2step_fast_here(aut2, output_bdd); - return aut2; - } - twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut) { @@ -453,321 +685,6 @@ namespace spot return out; } - // Improved apply strat, that reduces the number of edges/states - // while keeping the needed edge-properties - // Note, this only deals with deterministic strategies - // Note, assumes that env starts playing - spot::twa_graph_ptr - apply_strategy(const spot::twa_graph_ptr& arena, - bool unsplit, bool keep_acc) - { - const auto& win = get_state_winners(arena); - const auto& strat = get_strategy(arena); - const auto& sp = get_state_players(arena); - auto outs = get_synthesis_outputs(arena); - - if (!win[arena->get_init_state_number()]) - throw std::runtime_error("Player does not win initial state, strategy " - "is not applicable"); - - assert((sp[arena->get_init_state_number()] == false) - && "Env needs to have first turn!"); - - assert(std::none_of(arena->edges().begin(), arena->edges().end(), - [&sp](const auto& e) - { bool same_player = sp.at(e.src) == sp.at(e.dst); - if (same_player) - std::cerr << e.src << " and " << e.dst << " belong to same " - << "player, arena not alternating!\n"; - return same_player; })); - - auto strat_split = spot::make_twa_graph(arena->get_dict()); - strat_split->copy_ap_of(arena); - if (keep_acc) - strat_split->copy_acceptance_of(arena); - - std::stack todo; - todo.push(arena->get_init_state_number()); - - struct dca{ - unsigned dst; - unsigned condvar; - acc_cond::mark_t acc; - }; - struct dca_hash - { - size_t operator()(const dca& d) const noexcept - { - return pair_hash()(std::make_pair(d.dst, d.condvar)) - ^ wang32_hash(d.acc.hash()); - } - }; - struct dca_equal - { - bool operator()(const dca& d1, const dca& d2) const noexcept - { - return std::tie(d1.dst, d1.condvar, d1.acc) - == std::tie(d2.dst, d2.condvar, d2.acc); - } - }; - - //env dst + player cond + acc -> p stat - std::unordered_map p_map; - - constexpr unsigned unseen_mark = std::numeric_limits::max(); - std::vector env_map(arena->num_states(), unseen_mark); - strat_split->set_init_state(strat_split->new_state()); - env_map[arena->get_init_state_number()] = - strat_split->get_init_state_number(); - - // The states in the new graph are qualified local - // Get a local environment state - auto get_sel = [&](unsigned s) - { - if (SPOT_UNLIKELY(env_map[s] == unseen_mark)) - env_map[s] = strat_split->new_state(); - return env_map[s]; - }; - - // local dst - // Check if there exists already a local player state - // that has the same dst, cond and (if keep_acc is true) acc - auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc) - { - dca d{dst, (unsigned) cond.id(), acc}; - auto it = p_map.find(d); - if (it != p_map.end()) - return it->second; - unsigned ns = strat_split->new_state(); - p_map[d] = ns; - strat_split->new_edge(ns, dst, cond, acc); - return ns; - }; - - while (!todo.empty()) - { - unsigned src_env = todo.top(); - unsigned src_envl = get_sel(src_env); - todo.pop(); - // All env edges - for (const auto& e_env : arena->out(src_env)) - { - // Get the corresponding strat - const auto& e_strat = arena->edge_storage(strat[e_env.dst]); - // Check if already explored - if (env_map[e_strat.dst] == unseen_mark) - todo.push(e_strat.dst); - unsigned dst_envl = get_sel(e_strat.dst); - // The new env edge, player is constructed automatically - auto used_acc = keep_acc ? e_strat.acc : acc_cond::mark_t({}); - strat_split->new_edge(src_envl, - get_spl(dst_envl, e_strat.cond, used_acc), - e_env.cond, used_acc); - } - } - // All states exists, we can try to further merge them - // Specialized merge - std::vector spnew(strat_split->num_states(), false); - for (const auto& p : p_map) - spnew[p.second] = true; - - // Sorting edges in place - auto comp_edge = [](const auto& e1, const auto& e2) - { - return std::tuple(e1.dst, e1.acc, e1.cond.id()) - < std::tuple(e2.dst, e2.acc, e2.cond.id()); - }; - auto sort_edges_of = - [&, &split_graph = strat_split->get_graph()](unsigned s) - { - static std::vector edge_nums; - edge_nums.clear(); - - auto eit = strat_split->out(s); - const auto eit_e = eit.end(); - // 0 Check if it is already sorted - if (std::is_sorted(eit.begin(), eit_e, comp_edge)) - return false; // No change - // 1 Get all edges numbers and sort them - std::transform(eit.begin(), eit_e, std::back_inserter(edge_nums), - [&](const auto& e) - { return strat_split->edge_number(e); }); - std::sort(edge_nums.begin(), edge_nums.end(), - [&](unsigned ne1, unsigned ne2) - { return comp_edge(strat_split->edge_storage(ne1), - strat_split->edge_storage(ne2)); }); - // 2 Correct the order - auto& sd = split_graph.state_storage(s); - sd.succ = edge_nums.front(); - sd.succ_tail = edge_nums.back(); - const unsigned n_edges_p = edge_nums.size()-1; - for (unsigned i = 0; i < n_edges_p; ++i) - split_graph.edge_storage(edge_nums[i]).next_succ = edge_nums[i+1]; - split_graph.edge_storage(edge_nums.back()).next_succ = 0; //terminal - // All nicely chained - return true; - }; - auto merge_edges_of = [&](unsigned s) - { - // Call this after sort edges of - // Mergeable edges are nicely chained - bool changed = false; - auto eit = strat_split->out_iteraser(s); - unsigned idx_last = strat_split->edge_number(*eit); - ++eit; - while (eit) - { - auto& e_last = strat_split->edge_storage(idx_last); - if (std::tie(e_last.dst, e_last.acc) - == std::tie(eit->dst, eit->acc)) - { - //Same dest and acc -> or condition - e_last.cond |= eit->cond; - eit.erase(); - changed = true; - } - else - { - idx_last = strat_split->edge_number(*eit); - ++eit; - } - } - return changed; - }; - auto merge_able = [&](unsigned s1, unsigned s2) - { - auto eit1 = strat_split->out(s1); - auto eit2 = strat_split->out(s2); - // Note: No self-loops here - return std::equal(eit1.begin(), eit1.end(), - eit2.begin(), eit2.end(), - [](const auto& e1, const auto& e2) - { - return std::tuple(e1.dst, e1.acc, e1.cond.id()) - == std::tuple(e2.dst, e2.acc, e2.cond.id()); - }); - }; - - const unsigned n_sstrat = strat_split->num_states(); - std::vector remap(n_sstrat, -1u); - bool changed_any; - std::vector to_check; - to_check.reserve(n_sstrat); - // First iteration -> all env states are candidates - for (unsigned i = 0; i < n_sstrat; ++i) - if (!spnew[i]) - to_check.push_back(i); - - while (true) - { - changed_any = false; - std::for_each(to_check.begin(), to_check.end(), - [&](unsigned s){ sort_edges_of(s); merge_edges_of(s); }); - // Check if we can merge env states - for (unsigned s1 : to_check) - for (unsigned s2 = 0; s2 < n_sstrat; ++s2) - { - if (spnew[s2] || (s1 == s2)) - continue; // Player state or s1 == s2 - if ((remap[s2] < s2)) - continue; //s2 is already remapped - if (merge_able(s1, s2)) - { - changed_any = true; - if (s1 < s2) - remap[s2] = s1; - else - remap[s1] = s2; - break; - } - } - - if (!changed_any) - break; - // Redirect changed targets and set possibly mergeable states - to_check.clear(); - for (auto& e : strat_split->edges()) - if (remap[e.dst] != -1u) - { - e.dst = remap[e.dst]; - to_check.push_back(e.src); - assert(spnew[e.src]); - } - - // Now check the player states - // We can skip sorting -> only one edge - // todo change when multistrat - changed_any = false; - for (unsigned s1 : to_check) - for (unsigned s2 = 0; s2 < n_sstrat; ++s2) - { - if (!spnew[s2] || (s1 == s2)) - continue; // Env state or s1 == s2 - if ((remap[s2] < s2)) - continue; //s2 is already remapped - if (merge_able(s1, s2)) - { - changed_any = true; - if (s1 < s2) - remap[s2] = s1; - else - remap[s1] = s2; - break; - } - } - - if (!changed_any) - break; - // Redirect changed targets and set possibly mergeable states - to_check.clear(); - for (auto& e : strat_split->edges()) - if (remap[e.dst] != -1u) - { - e.dst = remap[e.dst]; - to_check.push_back(e.src); - assert(!spnew[e.src]); - } - } - - // Defrag and alternate - if (remap[strat_split->get_init_state_number()] != -1u) - strat_split->set_init_state(remap[strat_split->get_init_state_number()]); - unsigned st = 0; - for (auto& s: remap) - if (s == -1U) - s = st++; - else - s = -1U; - - strat_split->defrag_states(remap, st); - - alternate_players(strat_split, false, false); - // What we do now depends on whether we unsplit or not - if (unsplit) - { - auto final = unsplit_2step(strat_split); - set_synthesis_outputs(final, outs); - return final; - } - // Keep the splitted version - set_state_winners(strat_split, region_t(strat_split->num_states(), true)); - - std::vector new_strat(strat_split->num_states(), -1u); - - for (unsigned i = 0; i < strat_split->num_states(); ++i) - { - if (!sp[i]) - continue; - new_strat[i] = strat_split->edge_number(*strat_split->out(i).begin()); - } - set_strategy(strat_split, std::move(new_strat)); - set_synthesis_outputs(strat_split, outs); - return strat_split; - } - std::ostream& operator<<(std::ostream& os, synthesis_info::algo s) { using algo = synthesis_info::algo; @@ -1059,7 +976,7 @@ namespace spot } //end switch solver // Set the named properties assert(dpa->get_named_prop>("state-player") - && "DPA has no state-players"); + && "DPA has no \"state-player\""); set_synthesis_outputs(dpa, outs); return dpa; } @@ -1087,78 +1004,15 @@ namespace spot return ltl_to_game(parse_formula(f), all_outs, gi); } - void - minimize_strategy_here(twa_graph_ptr& strat, int min_lvl) - { - if (!strat->acc().is_t()) - throw std::runtime_error("minimize_strategy_here(): strategy is expected " - "to accept all runs! Otherwise it does not " - "correspond to a mealy machine and can not be " - "optimized this way."); - // 0 -> No minimization - // 1 -> Regular monitor/DFA minimization - // 2 -> Mealy minimization based on language inclusion - // with output assignement - // 3 -> Exact Mealy minimization using SAT - // 4 -> Monitor min then exact minimization - // 5 -> Mealy minimization based on language inclusion then exact - // minimization - bdd outs = get_synthesis_outputs(strat); - - switch (min_lvl) - { - case 0: - return; - case 1: - { - minimize_mealy_fast_here(strat, false); - break; - } - case 2: - { - minimize_mealy_fast_here(strat, true); - break; - } - case 3: - { - strat = minimize_mealy(strat, -1); - break; - } - case 4: - { - strat = minimize_mealy(strat, 0); - break; - } - case 5: - { - strat = minimize_mealy(strat, 1); - break; - } - default: - throw std::runtime_error("Unknown minimization option"); - } - set_synthesis_outputs(strat, outs); - } - twa_graph_ptr - minimize_strategy(const_twa_graph_ptr& strat, int min_lvl) - { - auto strat_dup = spot::make_twa_graph(strat, spot::twa::prop_set::all()); - set_synthesis_outputs(strat_dup, - get_synthesis_outputs(strat)); - if (auto sp_ptr = strat->get_named_prop("state-player")) - set_state_players(strat_dup, *sp_ptr); - minimize_strategy_here(strat_dup, min_lvl); - return strat_dup; - } - - twa_graph_ptr - create_strategy(twa_graph_ptr arena, synthesis_info& gi) + solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi) { + assert(arena->get_named_prop("state-player") + && "Need prop \"state-player\""); if (!arena) throw std::runtime_error("Arena can not be null"); - spot::stopwatch sw; + stopwatch sw; if (gi.bv) sw.start(); @@ -1168,32 +1022,34 @@ namespace spot // If we use minimizations 0,1 or 2 -> unsplit const bool do_unsplit = gi.minimize_lvl < 3; - twa_graph_ptr strat_aut = apply_strategy(arena, do_unsplit, false); + auto m = apply_strategy(arena, do_unsplit, false); - strat_aut->prop_universal(true); + m->prop_universal(true); - minimize_strategy_here(strat_aut, gi.minimize_lvl); + 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); - assert(do_unsplit - || strat_aut->get_named_prop>("state-player")); if (!do_unsplit) - strat_aut = unsplit_2step(strat_aut); + m = unsplit_mealy(m); if (gi.bv) { gi.bv->strat2aut_time += sw.stop(); - gi.bv->nb_strat_states += strat_aut->num_states(); - gi.bv->nb_strat_edges += strat_aut->num_edges(); + gi.bv->nb_strat_states += m->num_states(); + gi.bv->nb_strat_edges += m->num_edges(); } - return strat_aut; + assert(is_separated_mealy(m)); + return m; } twa_graph_ptr - create_strategy(twa_graph_ptr arena) + solved_game_to_separated_mealy(twa_graph_ptr arena) { synthesis_info dummy; - return create_strategy(arena, dummy); + return solved_game_to_separated_mealy(arena, dummy); } } @@ -1241,7 +1097,7 @@ namespace spot }; } - strategy_like_t + mealy_like try_create_direct_strategy(formula f, const std::vector& output_aps, synthesis_info &gi) @@ -1253,41 +1109,41 @@ namespace spot *vs << "trying to create strategy directly for " << f << '\n'; auto ret_sol_maybe = [&vs]() - { - if (vs) - *vs << "direct strategy might exist but was not found.\n"; - return strategy_like_t{ - strategy_like_t::realizability_code::UNKNOWN, - nullptr, - bddfalse}; - }; + { + if (vs) + *vs << "direct strategy might exist but was not found.\n"; + return mealy_like{ + mealy_like::realizability_code::UNKNOWN, + nullptr, + bddfalse}; + }; auto ret_sol_none = [&vs]() { if (vs) *vs << "no strategy exists.\n"; - return strategy_like_t{ - strategy_like_t::realizability_code::UNREALIZABLE, + return mealy_like{ + mealy_like::realizability_code::UNREALIZABLE, nullptr, bddfalse}; }; auto ret_sol_exists = [&vs](auto strat) - { - if (vs) { - *vs << "direct strategy was found.\n" - << "direct strat has " << strat->num_states() - << " states and " << strat->num_sets() << " colors\n"; - } - return strategy_like_t{ - strategy_like_t::realizability_code::REALIZABLE_REGULAR, - strat, - bddfalse}; - }; + if (vs) + { + *vs << "direct strategy was found.\n" + << "direct strat has " << strat->num_states() + << " states and " << strat->num_sets() << " colors\n"; + } + return mealy_like{ + mealy_like::realizability_code::REALIZABLE_REGULAR, + strat, + bddfalse}; + }; formula_2_inout_props form2props(output_aps); auto output_aps_set = std::set(output_aps.begin(), - output_aps.end()); + output_aps.end()); formula f_g = formula::tt(), f_left, f_right; diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index e69d2982c..f9e0d6cf5 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -58,29 +58,13 @@ namespace spot split_2step(const const_twa_graph_ptr& aut, const bdd& output_bdd, bool complete_env); - /// \ingroup synthesis - /// \brief make each transition a 2-step transition. - /// - /// This algorithm is only applicable if all transitions of the - /// graph have the form p -- ins & outs --> q. - /// That is they are a conjunction of a condition over the input - /// propositions ins and a condition over the output propositions outs - /// - /// \param aut automaton to be transformed - /// \param output_bdd conjunction of all output AP, all APs not present - /// are treated as inputs - /// @{ - SPOT_API void - split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd); - - SPOT_API twa_graph_ptr - split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd); - /// @} - - /// \ingroup synthesis - /// \brief the reverse of split_2step + /// \brief the inverse of split_2step /// + /// \pre aut is an alternating arena + /// \post All edge conditions in the returned automaton are of the form + /// ins&outs, with ins/outs being a condition over the input/output + /// propositions /// \note This function relies on the named property "state-player" SPOT_API twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut); @@ -174,57 +158,23 @@ namespace spot /// @} /// \ingroup synthesis - /// \brief Takes a solved game and restricts the automaton to the - /// winning strategy of the player - /// - /// \param arena twa_graph with named properties "state-player", - /// "strategy" and "state-winner" - /// \param unsplit Whether or not to unsplit the automaton - /// \param keep_acc Whether or not keep the acceptance condition - /// \return the resulting twa_graph - SPOT_API spot::twa_graph_ptr - apply_strategy(const spot::twa_graph_ptr& arena, - bool unsplit, bool keep_acc); - - /// \ingroup synthesis - /// \brief Minimizes a strategy. Strategies are infact - /// Mealy machines. So we can use techniques designed for them - /// - /// \param strat The machine to minimize - /// \param min_lvl How to minimize the machine: - /// 0: No minimization, 1: Minimizing it like an DFA, - /// means the language is preserved, 2: Inclusion with - /// output assignement, 3: Exact minimization using - /// SAT solving, 4: SAT solving with DFA minimization as - /// preprocessing, 5: SAT solving using inclusion based - /// minimization with output assignment as preprocessing - /// \note min_lvl 1 and 2 work more efficiently on UNSPLIT strategies, - /// whereas min_lvl 3, 4 and 5 mandate a SPLIT strategy + /// \brief creates a separated mealy machine from a solved game + /// taking into account the options given in \a gi. + /// This concerns in particular whether or not the machine is to be reduced + /// and how. /// @{ - SPOT_API void - minimize_strategy_here(twa_graph_ptr& strat, int min_lvl); - SPOT_API twa_graph_ptr - minimize_strategy(const_twa_graph_ptr& strat, int min_lvl); + solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi); + SPOT_API twa_graph_ptr + solved_game_to_separated_mealy(twa_graph_ptr arena); /// @} /// \ingroup synthesis - /// \brief creates a strategy from a solved game taking into account the - /// options given in \a gi - /// @{ - SPOT_API twa_graph_ptr - create_strategy(twa_graph_ptr arena, synthesis_info& gi); - SPOT_API twa_graph_ptr - create_strategy(twa_graph_ptr arena); - /// @} - - /// \ingroup synthesis - /// \brief A struct that represents different types of strategy like + /// \brief A struct that represents different types of mealy like /// objects struct SPOT_API - strategy_like_t + mealy_like { - enum class realizability_code { UNREALIZABLE, @@ -235,7 +185,7 @@ namespace spot }; realizability_code success; - twa_graph_ptr strat_like; + twa_graph_ptr mealy_like; bdd glob_cond; }; @@ -272,7 +222,7 @@ namespace spot /// \param f The formula to synthesize a strategy for /// \param output_aps A vector with the name of all output properties. /// All APs not named in this vector are treated as inputs - SPOT_API strategy_like_t + SPOT_API mealy_like try_create_direct_strategy(formula f, const std::vector& output_aps, synthesis_info& gi); diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb index 96a95b09e..0fbad3d08 100644 --- a/tests/python/_mealy.ipynb +++ b/tests/python/_mealy.ipynb @@ -3,7 +3,6 @@ { "cell_type": "code", "execution_count": 1, - "id": "99baf49c", "metadata": {}, "outputs": [], "source": [ @@ -13,7 +12,6 @@ }, { "cell_type": "markdown", - "id": "066489fd", "metadata": {}, "source": [ "Test the Mealy printer." @@ -22,7 +20,6 @@ { "cell_type": "code", "execution_count": 2, - "id": "08d7d512", "metadata": {}, "outputs": [], "source": [ @@ -32,7 +29,6 @@ { "cell_type": "code", "execution_count": 3, - "id": "4e5b66f4", "metadata": {}, "outputs": [ { @@ -53,7 +49,6 @@ { "cell_type": "code", "execution_count": 4, - "id": "ce2ff962", "metadata": {}, "outputs": [ { @@ -140,7 +135,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3d8c04f720> >" + " *' at 0x7f300caabba0> >" ] }, "execution_count": 4, @@ -155,17 +150,15 @@ { "cell_type": "code", "execution_count": 5, - "id": "3bcbeef2", "metadata": {}, "outputs": [], "source": [ - "x = spot.apply_strategy(g, True, False)" + "x = spot.solved_game_to_separated_mealy(g)" ] }, { "cell_type": "code", "execution_count": 6, - "id": "47d298f0", "metadata": {}, "outputs": [ { @@ -220,7 +213,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3d8c04f630> >" + " *' at 0x7f300c179300> >" ] }, "execution_count": 6, @@ -235,7 +228,6 @@ { "cell_type": "code", "execution_count": 7, - "id": "f0d098ac", "metadata": {}, "outputs": [], "source": [ @@ -245,7 +237,6 @@ { "cell_type": "code", "execution_count": 8, - "id": "adf92ac7", "metadata": {}, "outputs": [ { @@ -294,7 +285,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3d8c04f630> >" + " *' at 0x7f300c179300> >" ] }, "execution_count": 8, @@ -305,96 +296,6 @@ "source": [ "x" ] - }, - { - "cell_type": "code", - "execution_count": 9, - "id": "6e8cd892", - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "❸\n", - ") | (Fin(\n", - "❷\n", - ") & (Inf(\n", - "❶\n", - ") | Fin(\n", - "⓿\n", - ")))\n", - "[parity max odd 4]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "\n", - "!a & !c\n", - "/\n", - "\n", - "!b & !d\n", - "❸\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "\n", - "a | c\n", - "/\n", - "\n", - "b | d\n", - "❸\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7f3d76e561e0> >" - ] - }, - "execution_count": 9, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "spot.apply_strategy(g, True, True)" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "5948f923", - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -413,7 +314,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.8.10" } }, "nbformat": 4, diff --git a/tests/python/aiger.py b/tests/python/aiger.py index d6c8f2c93..5148fef5f 100644 --- a/tests/python/aiger.py +++ b/tests/python/aiger.py @@ -3339,9 +3339,10 @@ for strat_string, (ins_str, outs_str) in strats: for ss in [""] + [f"+sub{ii}" for ii in range(3)]: for ddx in ["", "+dc"]:# todo prob here for uud in ["", "+ud"]: - aig = spot.strategy_to_aig(strat, m+ss+ddx+uud) + aig = spot.mealy_machine_to_aig(strat, m+ss+ddx+uud) strat2_s = aig.as_automaton(True) - if not spot.is_mealy_specialization(strat_s, strat2_s): + if not spot.is_split_mealy_specialization(strat_s, + strat2_s): print(f"Mode is {m+ss+ddx+uud}") print(f"""Strat is \n{strat_s.to_str("hoa")}""") print(f"""Aig as aut is \n{strat2_s.to_str("hoa")}""") @@ -3361,7 +3362,7 @@ for aout in outs_str: outs &= buddy.bdd_ithvar(strat.register_ap(aout)) spot.set_synthesis_outputs(strat, outs) -aig = spot.strategy_to_aig(strat, "isop") +aig = spot.mealy_machine_to_aig(strat, "isop") ins = [True, False, False, False, True, True, True, True, True, True] exp_latches = [(False, False), diff --git a/tests/python/mealy.py b/tests/python/mealy.py index 6c84ac2bc..74ea2ea23 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -43,9 +43,10 @@ spot.set_synthesis_outputs(a, o1&o2) b = spot.minimize_mealy(a) assert(list(spot.get_state_players(b)).count(False) == 2) -assert(spot.is_mealy_specialization(a, b)) +assert(spot.is_split_mealy_specialization(a, b)) -test_auts = [("""HOA: v1 +test_auts = [ +("""HOA: v1 States: 22 Start: 0 AP: 6 "i0" "i1" "i2" "i3" "o0" "o1" @@ -360,13 +361,6 @@ for (mealy_str, nenv_min) in test_auts: mealy = spot.automaton(mealy_str) mealy.merge_edges() - mealy_min_ks = spot.minimize_mealy(mealy, -1, True) - mealy_min_us = spot.minimize_mealy(mealy, -1, False) - - n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)]) - assert(n_e == nenv_min) - assert(mealy_min_us.num_states() == nenv_min) - assert(spot.is_mealy_specialization(mealy, mealy_min_ks, True)) outs = buddy.bddtrue ins = buddy.bddtrue @@ -378,8 +372,20 @@ for (mealy_str, nenv_min) in test_auts: ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name())) else: assert("""Aps must start with either "i" or "o".""") - mealy_min_us_s = spot.split_2step(mealy_min_us, outs, False) - assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True)) + + spot.set_synthesis_outputs(mealy, outs) + + mealy_min_ks = spot.minimize_mealy(mealy, -1) + + n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)]) + assert(n_e == nenv_min) + assert(spot.is_split_mealy_specialization(mealy, mealy_min_ks)) + + # Test un- and resplit + tmp = spot.unsplit_2step(mealy_min_ks) + mealy_min_rs = spot.split_2step(tmp, spot.get_synthesis_outputs(tmp), False) + assert(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True)) + assert(spot.are_equivalent(mealy_min_ks, mealy_min_rs)) # Testing bisimulation (with output assignment) @@ -498,13 +504,23 @@ State: 16 --END--""") # Build an equivalent deterministic monitor -min_equiv = spot.minimize_mealy_fast(aut, False) +# ; +# ; +# +spot.set_synthesis_outputs(aut, + buddy.bdd_ithvar( + aut.register_ap("u02alarm29control02alarm29control"))\ + & buddy.bdd_ithvar( + aut.register_ap("u02alarm29control0f1d2alarm29turn2on1b"))\ + & buddy.bdd_ithvar( + aut.register_ap("u02alarm29control0f1d2alarm29turn2off1b"))) +min_equiv = spot.reduce_mealy(aut, False) assert min_equiv.num_states() == 6 assert spot.are_equivalent(min_equiv, aut) # Build an automaton that recognizes a subset of the language of the original # automaton -min_sub = spot.minimize_mealy_fast(aut, True) +min_sub = spot.reduce_mealy(aut, True) assert min_sub.num_states() == 5 prod = spot.product(spot.complement(aut), min_sub) assert spot.generic_emptiness_check(prod) @@ -531,6 +547,8 @@ State: 3 --END-- """) +spot.set_synthesis_outputs(aut, buddy.bdd_ithvar(aut.register_ap("b"))) + exp = """HOA: v1 States: 1 Start: 0 @@ -544,7 +562,7 @@ State: 0 --END--""" # An example that shows that we should not build a tree when we use inclusion. -res = spot.minimize_mealy_fast(aut, True) +res = spot.reduce_mealy(aut, True) assert res.to_str() == exp aut = spot.automaton(""" @@ -569,6 +587,8 @@ State: 3 --END-- """) +spot.set_synthesis_outputs(aut, buddy.bdd_ithvar(aut.register_ap("b"))) + exp = """HOA: v1 States: 2 Start: 0 @@ -585,7 +605,7 @@ State: 1 [0&1] 1 --END--""" -res = spot.minimize_mealy_fast(aut, True) +res = spot.reduce_mealy(aut, True) assert res.to_str() == exp diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 5a9d3f29e..5e175ee71 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -7,7 +7,8 @@ "outputs": [], "source": [ "import spot\n", - "spot.setup()" + "spot.setup()\n", + "from spot.jupyter import display_inline" ] }, { @@ -51,649 +52,649 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "❸\n", - ") | (Fin(\n", - "❷\n", - ") & (Inf(\n", - "❶\n", - ") | Fin(\n", - "⓿\n", - ")))\n", - "[parity max odd 4]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "!i0 & !i1\n", - "❶\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "i0 & !i1\n", - "❶\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "!i0 & i1\n", - "❶\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "i0 & i1\n", - "❶\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "!i1\n", - "❶\n", + "\n", + "\n", + "!i1\n", + "❶\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "i1\n", - "❶\n", + "\n", + "\n", + "i1\n", + "❶\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "!i1\n", - "❶\n", + "\n", + "\n", + "!i1\n", + "❶\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "i1\n", - "❶\n", + "\n", + "\n", + "i1\n", + "❶\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "i1\n", - "❶\n", + "\n", + "\n", + "i1\n", + "❶\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "!i1\n", - "❶\n", + "\n", + "\n", + "!i1\n", + "❶\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "1\n", - "❷\n", + "\n", + "\n", + "1\n", + "❷\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", - "❶\n", + "\n", + "\n", + "i1\n", + "❶\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "!i1\n", - "❶\n", + "\n", + "\n", + "!i1\n", + "❶\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "i0\n", - "❶\n", + "\n", + "\n", + "i0\n", + "❶\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "!i0\n", - "❶\n", + "\n", + "\n", + "!i0\n", + "❶\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "i0 & i1\n", - "❶\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "i0 & !i1\n", - "❶\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "!i0 & i1\n", - "❶\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "!i0 & !i1\n", - "❶\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "i0 & !i1\n", - "❶\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "i0 & i1\n", - "❶\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", - "❶\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "!i0 & i1\n", - "❶\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "i0 & !i1\n", - "❶\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "i0 & i1\n", - "❶\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", - "❶\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "!i0 & i1\n", - "❶\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "i0 & i1\n", - "❶\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "i0 & !i1\n", - "❶\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "!i0 & i1\n", - "❶\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "!i0 & !i1\n", - "❶\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "o0\n", - "❸\n", + "\n", + "\n", + "o0\n", + "❸\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "!o0\n", - "❸\n", + "\n", + "\n", + "!o0\n", + "❸\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "1\n", - "❸\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "1\n", - "❷\n", + "\n", + "\n", + "1\n", + "❷\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f4d60cb1540> >" + " *' at 0x7f494811f630> >" ] }, "metadata": {}, @@ -735,588 +736,588 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "❸\n", - ") | (Fin(\n", - "❷\n", - ") & (Inf(\n", - "❶\n", - ") | Fin(\n", - "⓿\n", - ")))\n", - "[parity max odd 4]\n", + " viewBox=\"0.00 0.00 650.45 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "❷\n", + "\n", + "\n", + "❷\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "❶\n", + "\n", + "\n", + "❶\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "❸\n", + "\n", + "\n", + "❸\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "❷\n", + "\n", + "\n", + "❷\n", "\n", "\n", "\n" @@ -1352,7 +1353,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "simplification lvl 0\n" + "simplification lvl 0 : No simplification\n" ] }, { @@ -1361,303 +1362,303 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" @@ -1673,7 +1674,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "simplification lvl 1\n" + "simplification lvl 1 : bisimulation-based reduction\n" ] }, { @@ -1682,169 +1683,169 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n" @@ -1860,7 +1861,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "simplification lvl 2\n" + "simplification lvl 2 : bisimulation-based reduction with output output assignement\n" ] }, { @@ -1869,119 +1870,119 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" @@ -1997,7 +1998,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "simplification lvl 3\n" + "simplification lvl 3 : SAT-based exact minimization\n" ] }, { @@ -2006,75 +2007,75 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" @@ -2090,7 +2091,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "simplification lvl 4\n" + "simplification lvl 4 : First 1 then 3 (exact)\n" ] }, { @@ -2099,75 +2100,75 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n" @@ -2183,7 +2184,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "simplification lvl 5\n" + "simplification lvl 5 : First 2 then 3 (not exact)\n" ] }, { @@ -2192,75 +2193,119 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", - "\n", + "\n", "1->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" @@ -2281,18 +2326,29 @@ "# 3 : SAT-based exact minimization\n", "# 4 : First 1 then 3 (exact)\n", "# 5 : First 2 then 3 (not exact)\n", + "\n", + "descr = [\"0 : No simplification\", \n", + " \"1 : bisimulation-based reduction\", \n", + " \"2 : bisimulation-based reduction with output output assignement\",\n", + " \"3 : SAT-based exact minimization\",\n", + " \"4 : First 1 then 3 (exact)\",\n", + " \"5 : First 2 then 3 (not exact)\"]\n", + "\n", + "\n", "for i in range(6):\n", - " print(\"simplification lvl\", i)\n", + " print(\"simplification lvl \", descr[i])\n", " si.minimize_lvl = i\n", - " strat = spot.create_strategy(game, si)\n", - " display(strat.show())" + " mealy = spot.solved_game_to_separated_mealy(game, si)\n", + " display(mealy.show())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Alternatively, the `apply_strategy` is a more low-level function that can be used to restrict the automaton to the part where player 1 is winning, without simplifying it. It's second argument controls whether pairs of transitions corresponding to each player should be fused back into a single transition. The third argument controls whether the game's acceptance condition should be copied." + "The machines returned by 'solved_game_to_separated_mealy' are (obviously) separated.\n", + "If we need a split mealy machine, we can call the dedicated function, which is more efficient\n", + "than the general 'split_2step'." ] }, { @@ -2302,418 +2358,290 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", + "text/html": [ + "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "
\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", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", + "\n", "\n", - "0->6\n", - "\n", - "\n", - "!i0 & i1\n", + "0->2\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", - "\n", - "\n", - "8\n", - "\n", - "8\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", "\n", - "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", "\n", - "0->8\n", - "\n", - "\n", - "i0 & i1\n", + "0->3\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "o0\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "o0\n", "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", - "\n", + "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", - "\n", - "\n", - "6->5\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "8->7\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "13\n", - "\n", - "13\n", - "\n", - "\n", - "\n", - "1->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", - "\n", - "\n", - "18\n", - "\n", - "18\n", - "\n", - "\n", - "\n", - "1->18\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "19\n", - "\n", - "19\n", - "\n", - "\n", + "\n", "\n", - "1->19\n", - "\n", - "\n", - "i0 & !i1\n", + "1->5\n", + "\n", + "\n", + "i0 & !i1\n", "\n", - "\n", - "\n", - "20\n", - "\n", - "20\n", - "\n", - "\n", + "\n", "\n", - "1->20\n", - "\n", - "\n", - "!i0 & !i1\n", + "1->5\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", - "\n", - "\n", - "13->7\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "18->5\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "19->3\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "20->1\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "3->13\n", - "\n", - "\n", - "i1\n", - "\n", - "\n", + "\n", "\n", - "3->19\n", - "\n", - "\n", - "!i1\n", + "4->0\n", + "\n", + "\n", + "!o0\n", "\n", - "\n", - "\n", - "10\n", - "\n", - "10\n", - "\n", - "\n", - "\n", - "5->10\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "11\n", - "\n", - "11\n", - "\n", - "\n", - "\n", - "5->11\n", - "\n", - "\n", - "i0 & i1\n", - "\n", - "\n", - "\n", - "15\n", - "\n", - "15\n", - "\n", - "\n", - "\n", - "5->15\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", - "\n", - "\n", - "16\n", - "\n", - "16\n", - "\n", - "\n", - "\n", - "5->16\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "9\n", - "\n", - "9\n", - "\n", - "\n", - "\n", - "10->9\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "11->7\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "14\n", - "\n", - "14\n", - "\n", - "\n", - "\n", - "15->14\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "16->5\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "7->10\n", - "\n", - "\n", - "!i1\n", - "\n", - "\n", - "\n", - "7->11\n", - "\n", - "\n", - "i1\n", - "\n", - "\n", - "\n", - "9->13\n", - "\n", - "\n", - "i1\n", - "\n", - "\n", - "\n", - "12\n", - "\n", - "12\n", - "\n", - "\n", - "\n", - "9->12\n", - "\n", - "\n", - "!i1\n", - "\n", - "\n", - "\n", - "12->9\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "14->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", - "\n", - "\n", - "14->18\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "14->12\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "17\n", - "\n", - "17\n", - "\n", - "\n", - "\n", - "14->17\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", - "\n", - "\n", - "17->14\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "!o0\n", "\n", "\n", - "\n" + "\n", + "
" ], "text/plain": [ - " *' at 0x7f4d61543bd0> >" + "" ] }, - "execution_count": 5, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "spot.apply_strategy(game, False, False)" + "display_inline(mealy.show(), spot.split_separated_mealy(mealy).show())" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Converting the separated mealy machine to AIGER\n", + "\n", + "A separated mealy machine can be converted to a circuit in the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) using `strategy_to_aig()`. This takes a second argument specifying what type of encoding to use (exactly like `ltlsynt`'s `--aiger=...` option). \n", + "\n", + "In this case, the circuit is quite simple: `o0` should be the negation of previous value of `i1`. This is done by storing the value of `i1` in a latch. And the value if `i0` can be ignored." ] }, { @@ -2727,329 +2655,76 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "L0_out\n", "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "1\n", - "\n", - "1\n", + "o0\n", + "\n", + "o0\n", "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "6->o0:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "L0\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "i1\n", "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "2->L0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "5->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "6->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "6->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "i0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f4d61524e10> >" + " >" ] }, - "execution_count": 6, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "spot.apply_strategy(game, True, False)" + "aig = spot.mealy_machine_to_aig(mealy, \"isop\")\n", + "display(aig)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "# Converting the strategy to AIGER\n", - "\n", - "A strategy can be converted to a circuit in the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) using `strategy_to_aig()`. This takes a second argument specifying what type of encoding to use (exactly like `ltlsynt`'s `--aiger=...` option). \n", - "\n", - "In this case, the circuit is quite simple: `o0` should be the negation of previous value of `i1`. This is done by storing the value of `i1` in a latch. And the value of `i0` can be ignored." + "While we are at it, let us mention that you can render those circuits horizontally as follows:" ] }, { @@ -3063,137 +2738,54 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "L0_out\n", - "\n", - "\n", - "\n", - "o0\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "6->o0:s\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "L0\n", - "\n", - "L0_in\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "i1\n", - "\n", - "\n", - "\n", - "2->L0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "i0\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " >" - ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], - "source": [ - "aig = spot.strategy_to_aig(strat, \"isop\")\n", - "display(aig)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "While we are at it, let us mention that you can render those circuits horizontally as follows:" - ] - }, - { - "cell_type": "code", - "execution_count": 8, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:w\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "2\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "2->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n" @@ -3202,7 +2794,7 @@ "" ] }, - "execution_count": 8, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -3211,6 +2803,37 @@ "aig.show('h')" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To encode the circuit in the aig format (ASCII version) use:" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "aag 3 2 1 1 0\n", + "2\n", + "4\n", + "6 3\n", + "7\n", + "i0 i1\n", + "i1 i0\n", + "o0 o0\n" + ] + } + ], + "source": [ + "print(aig.to_str())" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -3239,167 +2862,167 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "❺\n", - ") | (Fin(\n", - "❹\n", - ") & (Inf(\n", - "❸\n", - ") | (Fin(\n", - "❷\n", - ") & (Inf(\n", - "❶\n", - ") | Fin(\n", - "⓿\n", - ")))))\n", - "[parity max odd 6]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❺\n", + ") | (Fin(\n", + "❹\n", + ") & (Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))))\n", + "[parity max odd 6]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "i0\n", - "❶\n", + "\n", + "\n", + "i0\n", + "❶\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!i0\n", - "❶\n", + "\n", + "\n", + "!i0\n", + "❶\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "1\n", - "❶\n", + "\n", + "\n", + "1\n", + "❶\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "1\n", - "❺\n", + "\n", + "\n", + "1\n", + "❺\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "1\n", - "❶\n", + "\n", + "\n", + "1\n", + "❶\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!o0\n", - "❺\n", + "\n", + "\n", + "!o0\n", + "❺\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "1\n", - "❶\n", + "\n", + "\n", + "1\n", + "❶\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "o0\n", - "❹\n", + "\n", + "\n", + "o0\n", + "❹\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!o0\n", - "❹\n", + "\n", + "\n", + "!o0\n", + "❹\n", "\n", "\n", "\n", "7->1\n", - "\n", - "\n", - "!o0\n", - "❹\n", + "\n", + "\n", + "!o0\n", + "❹\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f4d60cb1e10> >" + " *' at 0x7f4948141cc0> >" ] }, "metadata": {}, @@ -3411,72 +3034,147 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "L0_out\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "\n", - "6\n", - "\n", - "6\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "L0\n", - "\n", - "L0_in\n", - "\n", - "\n", - "\n", - "6->L0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "o0\n", - "\n", - "o0\n", - "\n", - "\n", + "\n", "\n", - "6->o0:s\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "i0\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "i0\n", + "/\n", + "\n", + "o0\n", "\n", - "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", "\n", - "2->6\n", - "\n", - "\n", + "0->1\n", + "\n", + "\n", + "\n", + "!i0\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " *' at 0x7f4948141de0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "L0_out\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "L0\n", + "\n", + "L0_in\n", + "\n", + "\n", + "\n", + "6->L0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "o0\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "6->o0:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "i0\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " >" ] }, "metadata": {}, @@ -3488,8 +3186,9 @@ "spot.solve_game(game)\n", "spot.highlight_strategy(game)\n", "display(game)\n", - "strat = spot.create_strategy(game)\n", - "aig = spot.strategy_to_aig(strat, \"isop\")\n", + "mealy = spot.solved_game_to_separated_mealy(game)\n", + "display(mealy)\n", + "aig = spot.mealy_machine_to_aig(mealy, \"isop\")\n", "display(aig)" ] }, @@ -3497,7 +3196,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "To force the presence of extra variables in the circuit, they can be passed to `strategy_to_aig()`." + "To force the presence of extra variables in the circuit, they can be passed to `mealy_machine_to_aig()`." ] }, { @@ -3511,96 +3210,96 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "6->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "8->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "8->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "0\n", - "\n", - "False\n", + "\n", + "False\n", "\n", "\n", "\n", "0->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3608,7 +3307,636 @@ } ], "source": [ - "display(spot.strategy_to_aig(strat, \"isop\", [\"i0\", \"i1\"], [\"o0\", \"o1\"]))" + "display(spot.mealy_machine_to_aig(mealy, \"isop\", [\"i0\", \"i1\"], [\"o0\", \"o1\"]))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Combining mealy machines\n", + "\n", + "It can happen that the complet specification of the controller can be separated into sub-specifications with DISJOINT output propositions, see Finkbeiner et al. Specification Decomposition for Reactive Synthesis.\n", + "This results in multiple mealy machines which have to be converted into one single aiger circuit.\n", + "\n", + "This can be done using the function `mealy_machines_to_aig()`, which takes a vector of separated mealy machines as argument.\n", + "In order for this to work, all mealy machines need to share the same `bdd_dict`. This can be ensured by passing a common options strucuture." + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "initial games\n" + ] + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\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", + "(!i0 & !i1) | (i0 & i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\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", + "(!i0 & !i1) | (i0 & i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "o1\n", + "❸\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!o1\n", + "❸\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "solved games\n" + ] + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\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", + "(!i0 & !i1) | (i0 & i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\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", + "(!i0 & !i1) | (i0 & i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "o1\n", + "❸\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!o1\n", + "❸\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "reduced strategies\n" + ] + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "o1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "!o1\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Circuit implementing both machines\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "6->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "8->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "o0\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "10->o0:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "o1\n", + "\n", + "o1\n", + "\n", + "\n", + "\n", + "10->o1:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "i0\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " >" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "g1 = spot.ltl_to_game(\"G((i0 xor i1) <-> o0)\", [\"o0\"], si)\n", + "g2 = spot.ltl_to_game(\"G((i0 xor i1) <-> (~o1))\", [\"o1\"], si)\n", + "print(\"initial games\")\n", + "display_inline(g1, g2)\n", + "spot.solve_game(g1)\n", + "spot.highlight_strategy(g1)\n", + "spot.solve_game(g2)\n", + "spot.highlight_strategy(g2)\n", + "print(\"solved games\")\n", + "display_inline(g1, g2)\n", + "strat1 = spot.solved_game_to_separated_mealy(g1)\n", + "strat2 = spot.solved_game_to_separated_mealy(g2)\n", + "print(\"reduced strategies\")\n", + "display_inline(strat1, strat2)\n", + "print(\"Circuit implementing both machines\")\n", + "m_vec = spot.vector_const_twa_graph()\n", + "m_vec.push_back(strat1)\n", + "m_vec.push_back(strat2)\n", + "aig = spot.mealy_machines_to_aig(m_vec, \"isop\")\n", + "display(aig)" ] }, { @@ -3619,14 +3947,14 @@ "\n", "Note that we do not support the full [AIGER syntax](http://fmv.jku.at/aiger/FORMAT.aiger). Our restrictions corresponds to the conventions used in the type of AIGER file we output:\n", "- Input variables start at index 2 and are consecutively numbered.\n", - "- Latch variables start at index (1 + #inputs) × 2 and are consecutively numbered.\n", + "- Latch variables start at index (1 + #inputs) × 2 and are consecutively numbered.\n", "- If some inputs or outputs are named in comments, all of them have to be named.\n", "- Gate number $n$ can only connect to latches, inputs, or previously defined gates ($\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "d\n", + "\n", + "d\n", "\n", "\n", "\n", "6->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "c\n", + "\n", + "c\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "a\n", + "\n", + "a\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "b\n", + "\n", + "b\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3770,7 +4098,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -3798,7 +4126,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -3822,7 +4150,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -3831,43 +4159,55 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "(!a & !b & !c & !d) | (!a & b & c & !d) | (a & !b & c & !d) | (a & b & !c & d)\n", + "\n", + "\n", + "\n", + "!a & !b\n", + "/\n", + "\n", + "!c & !d\n", + "\n", + "a & b\n", + "/\n", + "\n", + "!c & d\n", + "\n", + "(!a & b) | (a & !b)\n", + "/\n", + "\n", + "c & !d\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f4d61543b70> >" + " *' at 0x7f49481417b0> >" ] }, - "execution_count": 15, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -3893,7 +4233,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3" + "version": "3.8.10" } }, "nbformat": 4,