diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index c4e541f72..0fb7f0bb3 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -75,8 +75,6 @@ namespace spot else { int fo = acc.fin_one(); - if (fo < 0) - std::cerr << autacc << acc << '\n'; assert(fo >= 0); // Try to accept when Fin(fo) == true acc_cond::mark_t fo_m = {(unsigned) fo}; @@ -162,6 +160,8 @@ namespace spot bool generic_emptiness_check_for_scc(const scc_info& si, unsigned scc) { + if (si.is_accepting_scc(scc)) + return false; return is_scc_empty(si, scc, si.get_aut()->acc(), nullptr); } diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 18f16a9f3..54d72e4c0 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -38,21 +38,6 @@ namespace spot { namespace { - enum strategy_t - { - trivial = 1U, - weak = 2U, - alternation = 4U, - rabin = 8U, - streett = 16U, - }; - - using strategy = - std::function; - - twa_graph_ptr - remove_fin_impl(const const_twa_graph_ptr&, const strategy_t); - using EdgeMask = std::vector; template< typename Edges, typename Apply > @@ -69,19 +54,6 @@ namespace spot } } - template< typename Edges > - acc_cond::mark_t scc_acc_marks(const_twa_graph_ptr aut, - const Edges& edges, - const EdgeMask& mask) - { - acc_cond::mark_t scc_mark = {}; - for_each_edge(aut, edges, mask, [&] (unsigned e) - { - scc_mark |= aut->edge_data(e).acc; - }); - return scc_mark; - } - // Transforms automaton from transition based acceptance to state based // acceptance. void make_state_acc(twa_graph_ptr & aut) @@ -122,7 +94,7 @@ namespace spot if (si.is_rejecting_scc(scc)) return true; - auto scc_acc = scc_acc_marks(aut, si.inner_edges_of(scc), keep); + auto scc_acc = si.acc_sets_of(scc); auto scc_pairs = rs_pairs_view(aut_pairs.pairs(), scc_acc); // If there is one aut_fin_alone that is not in the SCC, // any cycle in the SCC is accepting. @@ -143,31 +115,14 @@ namespace spot // necessarily imply that all cycles in the SCC are also // non-accepting. We may have a smaller cycle that is // accepting, but which becomes non-accepting when extended with - // more edges. + // more edges. In that case (which we can detect by checking + // whether the SCC has a non-empty language), the SCC is the + // not TBA-realizable. if (!scc_infs_alone) - { - // Check whether the SCC is accepting. We do that by simply - // converting that SCC into a TGBA and running our emptiness - // check. This is not a really smart implementation and - // could be improved. - auto& states = si.states_of(scc); - std::vector keep_states(aut->num_states(), false); - for (auto s: states) - keep_states[s] = true; - auto sccaut = mask_keep_accessible_states(aut, - keep_states, - states.front()); - // Prevent recurring into this function by skipping the - // Rabin strategy - auto skip = strategy_t::rabin; - // If SCCAUT is empty, the SCC is BA-type (and none of its - // states are final). If SCCAUT is nonempty, the SCC is not - // BA type - return remove_fin_impl(sccaut, skip)->is_empty(); - } + return si.check_scc_emptiness(scc); - // Remaining infs corresponds to I₁s that have been seen without seeing - // the matching F₁. In this SCC any edge in these I₁ is therefore + // Remaining infs corresponds to Iᵢs that have been seen without seeing + // the matching Fᵢ. In this SCC any edge in these Iᵢ is therefore // final. Otherwise we do not know: it is possible that there is // a non-accepting cycle in the SCC that does not visit Fᵢ. std::set unknown; @@ -180,7 +135,7 @@ namespace spot unknown.insert(e); }); - // Erase edges that cannot belong to a cycle, i.e., that edges + // Erase edges that cannot belong to a cycle, i.e., the edges // whose 'dst' is not 'src' of any unknown edges. std::vector remove; do @@ -277,8 +232,8 @@ namespace spot std::vector keep(aut->edge_vector().size(), true); for (unsigned scc = 0; scc < si.scc_count(); ++scc) - scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep, - aut_pairs, final); + scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep, + aut_pairs, final); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); @@ -783,21 +738,14 @@ namespace spot return res; } - twa_graph_ptr remove_fin_impl(const const_twa_graph_ptr& aut, - const strategy_t skip = {}) + twa_graph_ptr remove_fin_impl(const_twa_graph_ptr aut) { auto simp = simplify_acceptance(aut); - - auto handle = [&](strategy stra, strategy_t type) -> twa_graph_ptr - { - return (type & skip) ? nullptr : stra(simp); - }; - - if (auto maybe = handle(trivial_strategy, strategy_t::trivial)) + if (auto maybe = trivial_strategy(simp)) return maybe; - if (auto maybe = handle(weak_strategy, strategy_t::weak)) + if (auto maybe = weak_strategy(simp)) return maybe; - if (auto maybe = handle(alternation_strategy, strategy_t::alternation)) + if (auto maybe = alternation_strategy(simp)) return maybe; // The order between Rabin and Streett matters because for // instance "Streett 1" (even generalized Streett 1) is @@ -810,9 +758,9 @@ namespace spot // Note that SPOT_STREETT_CONV_MIN default to 3, which means // that regardless of this order, Rabin 1 is not handled by // streett_strategy unless SPOT_STREETT_CONV_MIN is changed. - if (auto maybe = handle(rabin_strategy, strategy_t::rabin)) + if (auto maybe = rabin_strategy(simp)) return maybe; - if (auto maybe = handle(streett_strategy, strategy_t::streett)) + if (auto maybe = streett_strategy(simp)) return maybe; return default_strategy(simp); } diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 773582ea1..cf0d7a71a 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -438,7 +438,7 @@ namespace spot return support; } - bool scc_info::check_scc_emptiness(unsigned n) + bool scc_info::check_scc_emptiness(unsigned n) const { if (SPOT_UNLIKELY(!aut_->is_existential())) throw std::runtime_error("scc_info::check_scc_emptiness() " @@ -832,4 +832,27 @@ namespace spot return res; } + + scc_info::edge_filter_choice + scc_and_mark_filter::filter_scc_and_mark_ + (const twa_graph::edge_storage_t& e, unsigned dst, void* data) + { + auto& d = *reinterpret_cast(data); + if (d.lower_si_->scc_of(dst) != d.lower_scc_) + return scc_info::edge_filter_choice::ignore; + if (d.cut_sets_ & e.acc) + return scc_info::edge_filter_choice::cut; + return scc_info::edge_filter_choice::keep; + } + + scc_info::edge_filter_choice + scc_and_mark_filter::filter_mark_ + (const twa_graph::edge_storage_t& e, unsigned, void* data) + { + auto& d = *reinterpret_cast(data); + if (d.cut_sets_ & e.acc) + return scc_info::edge_filter_choice::cut; + return scc_info::edge_filter_choice::keep; + } + } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index edae2ac84..ff10c9d89 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -478,6 +478,11 @@ namespace spot return options_; } + edge_filter get_filter() const + { + return filter_; + } + const void* get_filter_data() const { return filter_data_; @@ -623,7 +628,7 @@ namespace spot /// /// This is an internal function of /// determine_unknown_acceptance(). - bool check_scc_emptiness(unsigned n); + bool check_scc_emptiness(unsigned n) const; /// \brief Retrieves an accepting run of the automaton whose cycle is in the /// SCC. @@ -733,24 +738,9 @@ namespace spot static scc_info::edge_filter_choice filter_scc_and_mark_(const twa_graph::edge_storage_t& e, - unsigned dst, void* data) - { - auto& d = *reinterpret_cast(data); - if (d.lower_si_->scc_of(dst) != d.lower_scc_) - return scc_info::edge_filter_choice::ignore; - if (d.cut_sets_ & e.acc) - return scc_info::edge_filter_choice::cut; - return scc_info::edge_filter_choice::keep; - }; - + unsigned dst, void* data); static scc_info::edge_filter_choice - filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data) - { - auto& d = *reinterpret_cast(data); - if (d.cut_sets_ & e.acc) - return scc_info::edge_filter_choice::cut; - return scc_info::edge_filter_choice::keep; - }; + filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data); public: /// \brief Specify how to restrict scc_info to some SCC and acceptance sets @@ -764,9 +754,10 @@ namespace spot : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets), aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance()) { - const void* data = lower_si.get_filter_data(); - if (data) + auto f = lower_si.get_filter(); + if (f == &filter_mark_ || f == &filter_scc_and_mark_) { + const void* data = lower_si.get_filter_data(); auto& d = *reinterpret_cast(data); cut_sets_ |= d.cut_sets_; } diff --git a/tests/python/genem.py b/tests/python/genem.py index a2741a2fc..01f98344d 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -298,4 +298,4 @@ def run_bench(automata): assert run3.replay(spot.get_cout()) is True -run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11, a360]) +run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360])