From 3f333792ffac814d6961e2de55a95f568581a241 Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Wed, 22 Jun 2022 10:25:35 +0200 Subject: [PATCH] Add a procedure that detects if an automaton is parity-type * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: add detection of edges that are in at least one accepting cycle. * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: add parity_type_to_parity and buchi_type_to_buchi. --- spot/twaalgos/genem.cc | 77 +++++++++++ spot/twaalgos/genem.hh | 30 +++++ spot/twaalgos/toparity.cc | 276 ++++++++++++++++++++++++++++++++++++++ spot/twaalgos/toparity.hh | 28 +++- 4 files changed, 410 insertions(+), 1 deletion(-) diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 51b2ea903..237b10118 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -309,5 +309,82 @@ namespace spot return !scc_split_check_filtered(upper_si, forced_acc, callback, {}); } + // return ⊤ if there exists at least one accepting transition. + static bool + accepting_transitions_aux(const scc_info &si, unsigned scc, + const acc_cond acc, + acc_cond::mark_t removed_colors, + acc_cond::mark_t tocut, + std::vector &accepting_transitions, + const bitvect& kept) + { + bool result = false; + scc_and_mark_filter filt(si, scc, tocut, kept); + filt.override_acceptance(acc); + scc_info upper_si(filt, scc_info_options::ALL); + for (unsigned sc = 0; sc < upper_si.scc_count(); ++sc) + result |= accepting_transitions_scc(upper_si, sc, acc, removed_colors, + accepting_transitions, kept); + return result; + } + bool + accepting_transitions_scc(const scc_info &si, unsigned scc, + const acc_cond aut_acc, + acc_cond::mark_t removed_colors, + std::vector& accepting_transitions, + const bitvect& kept) + { + // The idea is the same as in is_scc_empty() + bool result = false; + acc_cond::mark_t sets = si.acc_sets_of(scc); + acc_cond acc = aut_acc.restrict_to(sets); + acc = acc.remove(si.common_sets_of(scc), false); + + auto inner_edges = si.inner_edges_of(scc); + + if (si.is_trivial(scc)) + return false; + if (acc.is_t() || acc.accepting(acc.get_acceptance().used_sets())) + { + for (auto& e : inner_edges) + if ((e.acc & removed_colors) == acc_cond::mark_t {}) + accepting_transitions[si.get_aut()->edge_number(e)] = true; + return true; + } + else if (acc.is_f()) + return false; + acc_cond::acc_code rest = acc_cond::acc_code::f(); + for (const acc_cond& disjunct: acc.top_disjuncts()) + if (acc_cond::mark_t fu = disjunct.fin_unit()) + result |= accepting_transitions_aux(si, scc, acc.remove(fu, true), + (removed_colors | fu), fu, + accepting_transitions, kept); + else + rest |= disjunct.get_acceptance(); + if (!rest.is_f()) + { + acc_cond::mark_t m = { (unsigned) acc.fin_one() }; + result |= accepting_transitions_aux(si, scc, acc.remove(m, true), + (removed_colors | m), m, accepting_transitions, + kept); + result |= accepting_transitions_scc(si, scc, acc.remove(m, false), + removed_colors, accepting_transitions, + kept); + } + return result; + } + + std::vector + accepting_transitions(const const_twa_graph_ptr aut, acc_cond cond) + { + auto aut_vector_size = aut->edge_vector().size(); + std::vector result(aut_vector_size, false); + auto kept = make_bitvect(aut_vector_size); + scc_info si(aut); + for (unsigned scc = 0; scc < si.scc_count(); ++scc) + accepting_transitions_scc(si, scc, cond, {}, result, *kept); + delete kept; + return result; + } } diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index 3c3e5de51..3fefcdc77 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -110,4 +110,34 @@ namespace spot SPOT_API void generic_emptiness_check_select_version(const char* emversion = nullptr); + /// \ingroup emptiness_check_algorithms + /// + /// Give the set of transitions contained in + /// an accepting cycle of the SCC \a scc of \a aut. + /// + /// \param si scc_info used to describle the automaton + /// \param scc SCC to consider + /// \param aut_acc Acceptance condition used for this SCC + /// \param removed_colors A set of colors that can't appear on a transition + /// \param accepting_transitions The result. Must be a vector of size at least + /// the max index + 1 of a transition of the SCC scc and the value of each + /// index of a transition of this SCC must be set to false + /// \param kept A list of booleans that say if a transition is kept even if + /// it does not have an element of removed_colors + /// \return True if there is an accepting transition + SPOT_API bool + accepting_transitions_scc(const scc_info &si, unsigned scc, + const acc_cond aut_acc, + acc_cond::mark_t removed_colors, + std::vector& accepting_transitions, + const bitvect& kept); + + /// \ingroup emptiness_check_algorithms + /// + /// Give the set of transitions contained in an accepting cycle of \a aut. + /// \param aut Automaton to process + /// \param cond Acceptance condition associated + SPOT_API std::vector + accepting_transitions(const const_twa_graph_ptr aut, acc_cond cond); + } diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 0b46e6224..3c3f03607 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -26,6 +26,7 @@ #include #include #include +#include #include #include #include @@ -39,6 +40,281 @@ namespace spot { + inline void + assign_color(acc_cond::mark_t &mark, unsigned col) + { + if (col < SPOT_MAX_ACCSETS) + mark.set(col); + else + acc_cond::mark_t{SPOT_MAX_ACCSETS}; + } + + // Describes if we want to test if it is a Büchi, co-Büchi,… type automaton. + enum cond_kind + { + BUCHI, + CO_BUCHI, + // A parity condition with a Inf as outermost term + INF_PARITY, + // A parity condition with a Fin as outermost term + FIN_PARITY + }; + + // This enum describes the status of an edge + enum edge_status + { + NOT_MARKED, + MARKED, + IMPOSSIBLE, + LINK_SCC + }; + + static bool + cond_type_main_aux(const twa_graph_ptr &aut, const cond_kind kind, + const bool need_equivalent, + std::vector &status, + std::vector &res_colors, + acc_cond &new_cond, bool &was_able_to_color) + { + auto &ev = aut->edge_vector(); + const auto ev_size = ev.size(); + const auto aut_init = aut->get_init_state_number(); + was_able_to_color = false; + status = std::vector(ev_size, NOT_MARKED); + res_colors = std::vector(ev_size); + // Used by accepting_transitions_scc. + auto keep = std::unique_ptr(make_bitvect(ev_size)); + keep->set_all(); + + // Number of edges colored by the procedure, used to test equivalence for + // parity + unsigned nb_colored = 0; + + // We need to say that a transition between 2 SCC doesn't have to get a + // color. + scc_info si(aut, aut_init, nullptr, nullptr, scc_info_options::NONE); + status[0] = LINK_SCC; + if (si.scc_count() > 1) + { + for (unsigned edge_number = 1; edge_number < ev_size; ++edge_number) + { + auto &e = ev[edge_number]; + if (si.scc_of(e.src) != si.scc_of(e.dst)) + { + status[edge_number] = LINK_SCC; + ++nb_colored; + } + } + } + + // If we need to convert to (co-)Büchi, we have to search one accepting + // set. With parity there is no limit. + bool want_parity = kind == cond_kind::FIN_PARITY || + kind == cond_kind::INF_PARITY; + unsigned max_iter = want_parity ? -1U : 1; + + unsigned color = want_parity ? SPOT_MAX_ACCSETS - 1 : 0; + // Do we want always accepting transitions? + // Don't consider CO_BUCHI as it is done by Büchi + bool search_inf = kind != cond_kind::FIN_PARITY; + + using filter_data_t = std::pair &>; + + scc_info::edge_filter filter = + [](const twa_graph::edge_storage_t &t, unsigned, void *data) + -> scc_info::edge_filter_choice + { + auto &d = *static_cast(data); + // We only keep transitions that can be marked + if (d.second[d.first->edge_number(t)] == NOT_MARKED) + return scc_info::edge_filter_choice::keep; + else + return scc_info::edge_filter_choice::cut; + }; + std::vector not_decidable_transitions(ev_size, false); + auto aut_acc = aut->get_acceptance(); + auto aut_acc_comp = aut_acc.complement(); + for (unsigned iter = 0; iter < max_iter; ++iter) + { + // Share the code with Büchi-type + if (kind == CO_BUCHI) + std::swap(aut_acc, aut_acc_comp); + std::fill(not_decidable_transitions.begin(), + not_decidable_transitions.end(), false); + auto cond = acc_cond(search_inf ? aut_acc_comp : aut_acc); + auto filter_data = filter_data_t{aut, status}; + scc_info si(aut, aut_init, filter, &filter_data, + scc_info_options::TRACK_STATES); + bool worked = false; + unsigned ssc_size = si.scc_count(); + for (unsigned scc = 0; scc < ssc_size; ++scc) + { + // scc_info can detect that we will not be able to find an + // accepting/rejecting cycle. + if (!((search_inf && !si.is_accepting_scc(scc)) || + (!search_inf && !si.is_rejecting_scc(scc)))) + { + accepting_transitions_scc(si, scc, cond, {}, + not_decidable_transitions, *keep); + for (auto &e : si.inner_edges_of(scc)) + { + auto edge_number = aut->edge_number(e); + if (!not_decidable_transitions[edge_number]) + { + assert(!res_colors[edge_number]); + if (color != -1U) + assign_color(res_colors[edge_number], color); + was_able_to_color = true; + status[edge_number] = MARKED; + ++nb_colored; + keep->clear(edge_number); + worked = true; + } + } + } + } + + if (color-- == -1U) + break; + search_inf = !search_inf; + // If we were not able to add color, we have to add status 2 to + // remaining transitions. + if (!worked && !need_equivalent) + { + std::replace(status.begin(), status.end(), NOT_MARKED, IMPOSSIBLE); + break; + } + } + + acc_cond::acc_code new_code; + switch (kind) + { + case cond_kind::BUCHI: + new_code = acc_cond::acc_code::buchi(); + break; + case cond_kind::CO_BUCHI: + new_code = acc_cond::acc_code::cobuchi(); + break; + case cond_kind::INF_PARITY: + case cond_kind::FIN_PARITY: + new_code = acc_cond::acc_code::parity_max( + kind == cond_kind::INF_PARITY, SPOT_MAX_ACCSETS); + break; + } + + // We check parity + if (need_equivalent) + { + // For parity, it's equivalent if every transition has a color + // (status 1) or links 2 SCCs. + if (kind == cond_kind::INF_PARITY || kind == cond_kind::FIN_PARITY) + return nb_colored == ev_size - 1; + else + { + // For Büchi, we remove the transitions that have {0} in the + // result from aut and if there is an accepting cycle, res is not + // equivalent to aut. + // For co-Büchi, it's the same but we don't want to find a + // rejecting cycle. + using filter_data_t = std::pair; + + scc_info::edge_filter filter = + [](const twa_graph::edge_storage_t &t, unsigned, void *data) + -> scc_info::edge_filter_choice + { + auto &d = *static_cast(data); + if (d.second.get(d.first->edge_number(t))) + return scc_info::edge_filter_choice::keep; + else + return scc_info::edge_filter_choice::cut; + }; + + if (kind == CO_BUCHI) + aut->set_acceptance(acc_cond(aut_acc)); + + filter_data_t filter_data = {aut, *keep}; + scc_info si(aut, aut_init, filter, &filter_data); + si.determine_unknown_acceptance(); + const auto num_scc = si.scc_count(); + for (unsigned scc = 0; scc < num_scc; ++scc) + if (si.is_accepting_scc(scc)) + { + if (kind == CO_BUCHI) + aut->set_acceptance(acc_cond(aut_acc_comp)); + return false; + } + if (kind == CO_BUCHI) + aut->set_acceptance(acc_cond(aut_acc_comp)); + } + } + new_cond = acc_cond(new_code); + return true; + } + + static twa_graph_ptr + cond_type_main(const twa_graph_ptr &aut, const cond_kind kind, + bool &was_able_to_color) + { + std::vector res_colors; + std::vector status; + acc_cond new_cond; + if (cond_type_main_aux(aut, kind, true, status, res_colors, new_cond, + was_able_to_color)) + { + auto res = make_twa_graph(aut, twa::prop_set::all()); + auto &res_vector = res->edge_vector(); + unsigned rv_size = res_vector.size(); + for (unsigned i = 1; i < rv_size; ++i) + res_vector[i].acc = res_colors[i]; + res->set_acceptance(new_cond); + return res; + } + return nullptr; + } + + twa_graph_ptr + parity_type_to_parity(const twa_graph_ptr &aut) + { + bool odd_cond, max_cond; + bool parit = aut->acc().is_parity(max_cond, odd_cond); + // If it is parity, we just copy + if (parit) + { + if (!max_cond) + return change_parity(aut, parity_kind_max, parity_style_any); + auto res = make_twa_graph(aut, twa::prop_set::all()); + res->copy_acceptance_of(aut); + return res; + } + bool was_able_to_color; + // If the automaton is parity-type with a condition that has Inf as + // outermost term + auto res = cond_type_main(aut, cond_kind::INF_PARITY, was_able_to_color); + + // If it was impossible to find an accepting edge, it is perhaps possible + // to find a rejecting transition + if (res == nullptr && !was_able_to_color) + res = cond_type_main(aut, cond_kind::FIN_PARITY, was_able_to_color); + if (res) + reduce_parity_here(res); + return res; + } + + twa_graph_ptr + buchi_type_to_buchi(const twa_graph_ptr &aut) + { + bool useless; + return cond_type_main(aut, cond_kind::BUCHI, useless); + } + + twa_graph_ptr + co_buchi_type_to_co_buchi(const twa_graph_ptr &aut) + { + bool useless; + return cond_type_main(aut, cond_kind::CO_BUCHI, useless); + } + // Old version of IAR. namespace { diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index 7d2701581..6aecf7659 100644 --- a/spot/twaalgos/toparity.hh +++ b/spot/twaalgos/toparity.hh @@ -156,4 +156,30 @@ namespace spot SPOT_API twa_graph_ptr // deprecated since Spot 2.9 iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false); -} // namespace spot + /// \ingroup twa_acc_transform + /// \brief Convert an automaton into a parity max automaton preserving + /// structure when possible. + /// + /// Return nullptr if no such automaton is found. + /// \param aut Automaton that we want to convert + SPOT_API twa_graph_ptr + parity_type_to_parity(const twa_graph_ptr &aut); + + /// \ingroup twa_acc_transform + /// \brief Convert an automaton into a Büchi automaton preserving structure + /// when possible. + /// + /// Return nullptr if no such automaton is found. + /// \param aut Automaton that we want to convert + SPOT_API twa_graph_ptr + buchi_type_to_buchi(const twa_graph_ptr &aut); + + /// \ingroup twa_acc_transform + /// \brief Convert an automaton into a co-Büchi automaton preserving structure + /// when possible. + /// + /// Return nullptr if no such automaton is found. + /// \param aut Automaton that we want to convert + SPOT_API twa_graph_ptr + co_buchi_type_to_co_buchi(const twa_graph_ptr &aut); +}