From d45b60a4e57b7402ebf359c7b6b35f6d1cd616e9 Mon Sep 17 00:00:00 2001 From: xlauko Date: Thu, 29 Jun 2017 22:11:17 +0200 Subject: [PATCH] remfin: Use tra2tba as new rabin strategy in remove_fin Move implementation of tra2tba to remfin. * python/spot/impl.i: Remove tra2tba python bindings * spot/twaalgos/Makefile.am: Remove tra2tba * spot/twaalgos/remfin.cc: Update rabin_strategy * spot/twaalgos/tra2tba.cc: Delete the file * spot/twaalgos/tra2tba.hh: Delete the file * tests/core/remfin.test: Update tests * tests/python/tra2tba.py: Update tests --- python/spot/impl.i | 2 - spot/twaalgos/Makefile.am | 2 - spot/twaalgos/remfin.cc | 493 ++++++++++++++++++-------------------- spot/twaalgos/tra2tba.cc | 318 ------------------------ spot/twaalgos/tra2tba.hh | 37 --- tests/core/remfin.test | 130 ++++------ tests/python/tra2tba.py | 107 ++++++--- 7 files changed, 363 insertions(+), 726 deletions(-) delete mode 100644 spot/twaalgos/tra2tba.cc delete mode 100644 spot/twaalgos/tra2tba.hh diff --git a/python/spot/impl.i b/python/spot/impl.i index 90bf39e82..956ec8fb7 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -151,7 +151,6 @@ #include #include #include -#include #include #include #include @@ -582,7 +581,6 @@ def state_is_accepting(self, src) -> "bool": %include %include %include -%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index df8c1ae3d..38cc4136b 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -84,7 +84,6 @@ twaalgos_HEADERS = \ tau03.hh \ tau03opt.hh \ totgba.hh \ - tra2tba.hh \ translate.hh \ word.hh @@ -146,7 +145,6 @@ libtwaalgos_la_SOURCES = \ tau03.cc \ tau03opt.cc \ totgba.cc \ - tra2tba.cc \ translate.cc \ word.cc diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 6d5c06462..16e8b9239 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -38,9 +38,53 @@ namespace spot { namespace { - // Check whether the SCC composed of all states STATES, and - // visiting all acceptance marks in SETS contains non-accepting - // cycles. + enum class strategy_t : unsigned + { + trivial = 1, + weak = 2, + alternation = 4, + street = 8, + rabin = 16 + }; + + using strategy_flags = strong_enum_flags; + using strategy = + std::function; + + twa_graph_ptr + remove_fin_impl(const const_twa_graph_ptr&, const strategy_flags); + + using EdgeMask = std::vector; + + template< typename Edges, typename Apply > + void for_each_edge(const_twa_graph_ptr aut, + const Edges& edges, + const EdgeMask& mask, + Apply apply) + { + for (const auto& e: edges) + { + unsigned edge_id = aut->edge_number(e); + if (mask[edge_id]) + apply(edge_id); + } + } + + 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 = 0U; + for_each_edge(aut, edges, mask, [&] (unsigned e) + { + const auto& ed = aut->edge_data(e); + scc_mark |= ed.acc; + }); + return scc_mark; + } + + // Check whether the SCC contains non-accepting cycles. // // A cycle is accepting (in a Rabin automaton) if there exists an // acceptance pair (Fᵢ, Iᵢ) such that some states from Iᵢ are @@ -50,257 +94,244 @@ namespace spot // pairs (Fᵢ, Iᵢ), either no states from Iᵢ are visited or some // states from Fᵢ are visited. (This corresponds to an accepting // cycle with Streett acceptance.) - static bool - is_scc_ba_type(const const_twa_graph_ptr& aut, - const std::vector& states, - std::vector& final, - acc_cond::mark_t inf_pairs, - acc_cond::mark_t inf_alone, - acc_cond::mark_t sets) + // + // final are those edges which are used in the resulting tba + // acceptance condition. + bool is_scc_tba_type(const_twa_graph_ptr aut, + const scc_info& si, + const unsigned scc, + std::vector keep, + const rs_pairs_view& aut_pairs, + std::vector& final) { - // Consider the SCC as one large cycle and check its - // intersection with all Fᵢs and Iᵢs: This is the SETS - // variable. - // - // Let f=[F₁,F₂,...] and i=[I₁,I₂,...] be bitvectors where bit - // Fᵢ (resp. Iᵢ) indicates that Fᵢ (resp. Iᵢ) has been visited - // in the SCC. - acc_cond::mark_t f = (sets << 1U) & inf_pairs; - acc_cond::mark_t i = sets & inf_pairs; - // If we have i&!f = [0,0,...] that means that the cycle formed + if (si.is_rejecting_scc(scc)) + return true; + + auto scc_acc = scc_acc_marks(aut, si.inner_edges_of(scc), keep); + 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. + if (scc_pairs.fins_alone().proper_subset(aut_pairs.fins_alone())) + { + for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e) + { + final[e] = true; + }); + return true; + } + + auto scc_infs_alone = scc_pairs.infs_alone(); + // Firstly consider whole SCC as one large cycle. + // If there is no inf without matching fin then the cycle formed // by the entire SCC is not accepting. However that does not // 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 states. - i -= f; - i |= inf_alone & sets; - if (!i) + 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. - std::vector keep(aut->num_states(), false); + auto& states = si.states_of(scc); + std::vector keep_states(aut->num_states(), false); for (auto s: states) - keep[s] = true; - auto sccaut = mask_keep_accessible_states(aut, keep, states.front()); - // Force SBA to false. It does not affect the emptiness - // check result, however it prevent recurring into this - // procedure, because is_empty() will call - // to_generalized_buchi() which will call remove_fin()... - sccaut->prop_state_acc(false); + keep_states[s] = true; + auto sccaut = mask_keep_accessible_states(aut, + keep_states, + states.front()); + + // Prevent recurring into this function, by skipping the rabin straegy + 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 sccaut->is_empty(); + // is not BA type + return remove_fin_impl(sccaut, skip)->is_empty(); } - // The bits remaining sets in i corresponds to I₁s that have - // been seen with seeing the matching F₁. In this SCC any state - // 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 do not visit Fᵢ. + + // Remaining infs corresponds to I₁s that have been seen with seeing + // the mathing F₁.cIn 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 do not visit Fᵢ. std::set unknown; - for (auto s: states) - if (aut->state_acc_sets(s) & i) - final[s] = true; - else - unknown.insert(s); + for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e) + { + const auto& ed = aut->edge_data(e); + if (ed.acc & scc_infs_alone) + final[e] = true; + else + unknown.insert(e); + }); // Check whether it is possible to build non-accepting cycles - // using only the "unknown" states. + // using only the "unknown" edges. + keep.assign(aut->edge_vector().size(), false); + + // Erase edges that cannot form cycle, ie. that edge whose 'dst' + // is not 'src' of any unknown edges. + std::vector remove; + do + { + remove.clear(); + std::set srcs; + for (auto e: unknown) + srcs.insert(aut->edge_storage(e).src); + for (auto e: unknown) + if (!srcs.count(aut->edge_storage(e).dst)) + remove.push_back(e); + for (auto r: remove) + unknown.erase(r); + } + while (!remove.empty()); + + // Check whether it is possible to build non-accepting cycles + // using only the "unknown" edges. + using filter_data_t = std::pair< const_twa_graph_ptr, std::vector >; + + scc_info::edge_filter filter = + [](const twa_graph::edge_storage_t& t, unsigned, void* data) + -> scc_info::edge_filter_choice + { + const_twa_graph_ptr aut; + std::vector keep; + std::tie(aut, keep) = *static_cast(data); + + if (keep[aut->edge_number(t)]) + return scc_info::edge_filter_choice::keep; + else + return scc_info::edge_filter_choice::ignore; + }; + while (!unknown.empty()) { - std::vector keep(aut->num_states(), false); - for (auto s: unknown) - keep[s] = true; + std::vector keep(aut->edge_vector().size(), false); + for (auto e: unknown) + keep[e] = true; - scc_info::edge_filter filter = - [](const twa_graph::edge_storage_t&, unsigned dst, - void* filter_data) -> scc_info::edge_filter_choice - { - auto& keepref = *reinterpret_cast(filter_data); - if (keepref[dst]) - return scc_info::edge_filter_choice::keep; - else - return scc_info::edge_filter_choice::ignore; - }; + auto filter_data = filter_data_t{aut, keep}; + auto init = aut->edge_storage(*unknown.begin()).src; + scc_info si(aut, init, filter, &filter_data); - scc_info si(aut, *unknown.begin(), filter, &keep); - unsigned scc_max = si.scc_count(); - for (unsigned scc = 0; scc < scc_max; ++scc) + for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc) { - for (auto s: si.states_of(scc)) - unknown.erase(s); - if (si.is_rejecting_scc(scc)) // this includes trivial SCCs + for_each_edge(aut, si.edges_of(uscc), keep, [&](unsigned e) + { + unknown.erase(e); + }); + if (si.is_rejecting_scc(uscc)) continue; - if (!is_scc_ba_type(aut, si.states_of(scc), - final, inf_pairs, 0U, si.acc(scc))) + if (!is_scc_tba_type(aut, si, uscc, keep, aut_pairs, final)) return false; } } return true; } - // Specialized conversion from Rabin acceptance to Büchi acceptance. - // Is able to detect SCCs that are Büchi-type (i.e., they can be + // Specialized conversion from transition based Rabin acceptance to + // transition based Büchi acceptance. + // Is able to detect SCCs that are TBA-type (i.e., they can be // converted to Büchi acceptance without chaning their structure). - // Currently only works with state-based acceptance. // // See "Deterministic ω-automata vis-a-vis Deterministic Büchi // Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for // some details about detecting Büchi-typeness. // - // We essentially apply this method SCC-wise. The paper is + // We essentially apply this method SCC-wise. The paper is // concerned about *deterministic* automata, but we apply the // algorithm on non-deterministic automata as well: in the worst - // case it is possible that a Büchi-type SCC with some - // non-deterministim has one accepting and one rejecting run for + // case it is possible that a TBA-type SCC with some + // non-deterministic has one accepting and one rejecting run for // the same word. In this case we may fail to detect the - // Büchi-typeness of the SCC, but the resulting automaton should + // TBA-typeness of the SCC, but the resulting automaton should // be correct nonetheless. - static twa_graph_ptr - ra_to_ba(const const_twa_graph_ptr& aut, - acc_cond::mark_t inf_pairs, - acc_cond::mark_t inf_alone, - acc_cond::mark_t fin_alone) + twa_graph_ptr + tra_to_tba(const const_twa_graph_ptr& inaut) { - assert((bool)aut->prop_state_acc()); + // cleanup acceptance for easy detection of alone fins and infs + auto aut = cleanup_acceptance(inaut); - scc_info si(aut); - // For state-based Rabin automata, we check each SCC for - // BA-typeness. If an SCC is BA-type, its final states are stored - // in BA_FINAL_STATES. - std::vector scc_is_ba_type(si.scc_count(), false); - bool ba_type = false; - std::vector ba_final_states; + std::vector pairs; + if (!aut->acc().is_rabin_like(pairs)) + return nullptr; -#ifdef DEBUG - acc_cond::mark_t fin; - acc_cond::mark_t inf; - std::tie(inf, fin) = aut->get_acceptance().used_inf_fin_sets(); - assert(inf == (inf_pairs | inf_alone)); - assert(fin == ((inf_pairs >> 1U) | fin_alone)); -#endif - ba_final_states.resize(aut->num_states(), false); - ba_type = true; // until proven otherwise - unsigned scc_max = si.scc_count(); - for (unsigned scc = 0; scc < scc_max; ++scc) - { - if (si.is_rejecting_scc(scc)) // this includes trivial SCCs - { - scc_is_ba_type[scc] = true; - continue; - } - bool scc_ba_type = false; - auto sets = si.acc(scc); - // If there is one fin_alone that is not in the SCC, - // any cycle in the SCC is accepting. Mark all states - // as final. - if ((sets & fin_alone) != fin_alone) - { - for (auto s: si.states_of(scc)) - ba_final_states[s] = true; - scc_ba_type = true; - } - // In the general case, we need a dedicated check. Note - // that the used fin_alone sets can be ignored, as they - // cannot contribute to Büchi-typeness, - else - { - scc_ba_type = is_scc_ba_type(aut, si.states_of(scc), - ba_final_states, - inf_pairs, inf_alone, si.acc(scc)); - } - ba_type &= scc_ba_type; - scc_is_ba_type[scc] = scc_ba_type; - } + auto aut_pairs = rs_pairs_view(pairs); + auto code = aut->get_acceptance(); + if (code.is_t()) + return nullptr; -#ifdef TRACE - trace << "SCC DBA-realizibility\n"; - for (unsigned scc = 0; scc < scc_max; ++scc) - { - trace << scc << ": " << scc_is_ba_type[scc] << " {"; - for (auto s: si.states_of(scc)) - trace << ' ' << s; - trace << " }\n"; - } -#endif + // if is TBA type + scc_info si{aut}; + std::vector scc_is_tba_type(si.scc_count(), false); + std::vector final(aut->edge_vector().size(), false); + 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); - unsigned nst = aut->num_states(); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, false, false, true }); - res->new_states(nst); + res->prop_copy(aut, { false, false, false, false, false, true }); + res->new_states(aut->num_states()); res->set_buchi(); res->set_init_state(aut->get_init_state_number()); trival deterministic = aut->prop_universal(); trival complete = aut->prop_complete(); std::vector state_map(aut->num_states()); - for (unsigned n = 0; n < scc_max; ++n) + for (unsigned scc = 0; scc < si.scc_count(); ++scc) { - auto states = si.states_of(n); + auto states = si.states_of(scc); - if (scc_is_ba_type[n]) + if (scc_is_tba_type[scc]) { - // If the SCC is BA-type, we know exactly what state need to - // be marked as accepting. - for (auto s: states) + for (const auto& e: si.edges_of(scc)) { - bool acc = ba_final_states[s]; - for (auto& t: aut->out(s)) - res->new_acc_edge(s, t.dst, t.cond, acc); + bool acc = final[aut->edge_number(e)]; + res->new_acc_edge(e.src, e.dst, e.cond, acc); } } else { - deterministic = false; complete = trival::maybe(); // The main copy is only accepting for inf_alone // and for all Inf sets that have no matching Fin // sets in this SCC. - acc_cond::mark_t sccsets = si.acc(n); - acc_cond::mark_t f = (sccsets << 1U) & inf_pairs; - acc_cond::mark_t i = sccsets & (inf_pairs | inf_alone); - i -= f; - for (auto s: states) + auto scc_pairs = rs_pairs_view(pairs, si.acc(scc)); + auto scc_infs_alone = scc_pairs.infs_alone(); + + for (const auto& e: si.edges_of(scc)) { - bool acc{aut->state_acc_sets(s) & i}; - for (auto& t: aut->out(s)) - res->new_acc_edge(s, t.dst, t.cond, acc); + bool acc{e.acc & scc_infs_alone}; + res->new_acc_edge(e.src, e.dst, e.cond, acc); } - auto rem = sccsets & ((inf_pairs >> 1U) | fin_alone); - assert(rem != 0U); - auto sets = rem.sets(); + auto fins_alone = aut_pairs.fins_alone(); - unsigned ss = states.size(); - - for (auto r: sets) + for (auto r: scc_pairs.fins().sets()) { - unsigned base = res->new_states(ss); - for (auto s: states) - state_map[s] = base++; + unsigned base = res->new_states(states.size()); for (auto s: states) + state_map[s] = base++; + for (const auto& e: si.inner_edges_of(scc)) { - auto ns = state_map[s]; - acc_cond::mark_t acc = aut->state_acc_sets(s); - if (acc.has(r)) + if (e.acc.has(r)) continue; - bool jacc{acc & inf_alone}; - bool cacc = fin_alone.has(r) || acc.has(r + 1); - for (auto& t: aut->out(s)) + auto src = state_map[e.src]; + auto dst = state_map[e.dst]; + bool cacc = fins_alone.has(r) + ? true + : ((scc_pairs.paired_with(r) & e.acc) != 0); + res->new_acc_edge(src, dst, e.cond, cacc); + // We need only one non-deterministic jump per + // cycle. As an approximation, we only do + // them on back-links. + if (e.dst <= e.src) { - if (si.scc_of(t.dst) != n) - continue; - auto nd = state_map[t.dst]; - res->new_acc_edge(ns, nd, t.cond, cacc); - // We need only one non-deterministic jump per - // cycle. As an approximation, we only do - // them on back-links. - if (t.dst <= s) - res->new_acc_edge(s, nd, t.cond, jacc); + deterministic = false; + bool jacc = ((e.acc & scc_infs_alone) != 0); + res->new_acc_edge(e.src, dst, e.cond, jacc); } } } @@ -309,9 +340,27 @@ namespace spot res->prop_complete(complete); res->prop_universal(deterministic); res->purge_dead_states(); + res->merge_edges(); + return res; } + // Transforms automaton from transition based acceptance to state based + // acceptance. + void make_state_acc(twa_graph_ptr & aut) + { + unsigned nst = aut->num_states(); + for (unsigned s = 0; s < nst; ++s) + { + acc_cond::mark_t acc = 0U; + for (auto& t: aut->out(s)) + acc |= t.acc; + for (auto& t: aut->out(s)) + t.acc = acc; + } + aut->prop_state_acc(true); + } + // If the DNF is // Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) | // Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4) @@ -710,19 +759,6 @@ namespace spot return res; } - enum class strategy_t : unsigned - { - trivial = 1, - weak = 2, - alternation = 4, - street = 8, - rabin = 16, - }; - - using strategy_flags = strong_enum_flags; - using strategy = - std::function; - twa_graph_ptr remove_fin_impl(const const_twa_graph_ptr& aut, const strategy_flags skip = {}) { @@ -748,72 +784,11 @@ namespace spot twa_graph_ptr rabin_to_buchi_maybe(const const_twa_graph_ptr& aut) { - if (!aut->prop_state_acc().is_true()) - return nullptr; - - auto code = aut->get_acceptance(); - - if (code.is_t()) - return nullptr; - - acc_cond::mark_t inf_pairs = 0U; - acc_cond::mark_t inf_alone = 0U; - acc_cond::mark_t fin_alone = 0U; - - auto s = code.back().sub.size; - - // Rabin 1 - if (code.back().sub.op == acc_cond::acc_op::And && s == 4) - goto start_and; - // Co-Büchi - else if (code.back().sub.op == acc_cond::acc_op::Fin && s == 1) - goto start_fin; - // Rabin >1 - else if (code.back().sub.op != acc_cond::acc_op::Or) - return nullptr; - - while (s) - { - --s; - if (code[s].sub.op == acc_cond::acc_op::And) - { - start_and: - auto o1 = code[--s].sub.op; - auto m1 = code[--s].mark; - auto o2 = code[--s].sub.op; - auto m2 = code[--s].mark; - // We expect - // Fin({n}) & Inf({n+1}) - if (o1 != acc_cond::acc_op::Fin || - o2 != acc_cond::acc_op::Inf || - m1.count() != 1 || - m2.count() != 1 || - m2 != (m1 << 1U)) - return nullptr; - inf_pairs |= m2; - } - else if (code[s].sub.op == acc_cond::acc_op::Fin) - { - start_fin: - fin_alone |= code[--s].mark; - } - else if (code[s].sub.op == acc_cond::acc_op::Inf) - { - auto m1 = code[--s].mark; - if (m1.count() != 1) - return nullptr; - inf_alone |= m1; - } - else - { - return nullptr; - } - } - - trace << "inf_pairs: " << inf_pairs << '\n'; - trace << "inf_alone: " << inf_alone << '\n'; - trace << "fin_alone: " << fin_alone << '\n'; - return ra_to_ba(aut, inf_pairs, inf_alone, fin_alone); + bool is_state_acc = aut->prop_state_acc().is_true(); + auto res = tra_to_tba(aut); + if (res && is_state_acc) + make_state_acc(res); + return res; } twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut) diff --git a/spot/twaalgos/tra2tba.cc b/spot/twaalgos/tra2tba.cc deleted file mode 100644 index 1dc0b59e6..000000000 --- a/spot/twaalgos/tra2tba.cc +++ /dev/null @@ -1,318 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include -#include -#include -#include - -namespace spot -{ - namespace - { - std::vector scc_edges(const const_twa_graph_ptr& aut, - const scc_info& si, - const unsigned scc) - { - std::vector edges; - for (unsigned s : si.states_of(scc)) - for (const auto& t: aut->succ(aut->state_from_number(s))) - edges.push_back(aut->edge_number(t)); - return edges; - - } - // - std::vector scc_inner_edges(const const_twa_graph_ptr& aut, - const scc_info& si, - const unsigned scc) - { - auto edges = scc_edges(aut, si, scc); - edges.erase(std::remove_if(edges.begin(), edges.end(), - [&](unsigned e) - { - return si.scc_of(aut->edge_storage(e).dst) != scc; - }), - edges.end()); - return edges; - } - - twa_graph_ptr mask_keep_edges(const const_twa_graph_ptr& aut, - std::vector& to_keep, - unsigned int init) - { - if (to_keep.size() < aut->edge_vector().size()) - to_keep.resize(aut->edge_vector().size(), false); - - auto res = make_twa_graph(aut->get_dict()); - res->copy_ap_of(aut); - res->prop_copy(aut, { false, true, false, true, false, false }); - res->copy_acceptance_of(aut); - - size_t states = aut->num_states(); - std::vector> edges; - edges.resize(states); - for (size_t i = 0; i < states; ++i) - edges[i].resize(states, false); - - for (size_t i = 0; i < aut->edge_vector().size(); ++i) - { - if (to_keep[i]) - { - const auto& es = aut->edge_storage(i); - edges[es.src][es.dst] = true; - } - } - - transform_copy(aut, res, - [&](unsigned src, bdd& cond, acc_cond::mark_t&, - unsigned dst) - { - if (!edges[src][dst]) - cond = bddfalse; - }, - init); - return res; - } - - // Check whether the SCC contains non-accepting cycles. - // - // A cycle is accepting (in a Rabin automaton) if there exists an - // acceptance pair (Fᵢ, Iᵢ) such that some states from Iᵢ are - // visited while no states from Fᵢ are visited. - // - // Consequently, a cycle is non-accepting if for all acceptance - // pairs (Fᵢ, Iᵢ), either no states from Iᵢ are visited or some - // states from Fᵢ are visited. (This corresponds to an accepting - // cycle with Streett acceptance.) - // - // final are those edges which are used in the resulting tba - // acceptance condition. - bool is_scc_tba_type(const const_twa_graph_ptr& aut, - const scc_info& si, - const unsigned scc, - const acc_cond::mark_t fin_alone, - std::vector& final) - { - if (si.is_rejecting_scc(scc)) - return true; - - auto acc_pairs = aut->get_acceptance().used_inf_fin_sets(); - auto infs = si.acc(scc) & acc_pairs.first; - auto fins = si.acc(scc) & acc_pairs.second; - auto infs_with_fins = (si.acc(scc) << 1U) & acc_pairs.first; - infs -= infs_with_fins; - - // If there is one fin_alone that is not in the SCC, - // any cycle in the SCC is accepting. - if ((fins & fin_alone) != fin_alone) - { - for (auto e: scc_edges(aut, si, scc)) - final[e] = true; - return true; - } - auto& states = si.states_of(scc); - // Firstly consider whole SCC as one large cycle. - // If there is no inf without matching fin then the cycle formed - // by the entire SCC is not accepting. However that does not - // 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 states. - if (!infs) - { - // 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. - std::vector keep(aut->num_states(), false); - for (auto s: states) - keep[s] = true; - auto sccaut = mask_keep_accessible_states(aut, - keep, - states.front()); - sccaut->prop_state_acc(false); - return sccaut->is_empty(); - } - - // Remaining infs corresponds to I₁s that have been seen with seeing - // the mathing 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 do not visit Fᵢ. - std::set unknown; - for (auto e: scc_inner_edges(aut, si, scc)) - if (aut->edge_data(e).acc & infs) - final[e] = true; - else - unknown.insert(e); - // Check whether it is possible to build non-accepting cycles - // using only the "unknown" edges. - std::vector keep(aut->edge_vector().size(), false); - for (auto e: unknown) - keep[e] = true; - - while (!unknown.empty()) - { - unsigned init = aut->edge_storage(*unknown.begin()).src; - scc_info si(mask_keep_edges(aut, keep, init)); - unsigned scc_max = si.scc_count(); - for (unsigned uscc = 0; uscc < scc_max; ++uscc) - { - for (auto e: scc_edges(aut, si, uscc)) - { - unknown.erase(e); - keep[e] = false; - } - if (si.is_rejecting_scc(uscc)) - continue; - if (!is_scc_tba_type(aut, si, uscc, fin_alone, final)) - return false; - } - } - return true; - } - } - - // Specialized conversion from transition based Rabin acceptance to - // transition based Büchi acceptance. - // Is able to detect SCCs that are TBA-type (i.e., they can be - // converted to Büchi acceptance without chaning their structure). - // - // See "Deterministic ω-automata vis-a-vis Deterministic Büchi - // Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for - // some details about detecting Büchi-typeness. - // - // We essentially apply this method SCC-wise. The paper is - // concerned about *deterministic* automata, but we apply the - // algorithm on non-deterministic automata as well: in the worst - // case it is possible that a TBA-type SCC with some - // non-deterministic has one accepting and one rejecting run for - // the same word. In this case we may fail to detect the - // TBA-typeness of the SCC, but the resulting automaton should - // be correct nonetheless. - twa_graph_ptr - tra_to_tba(const const_twa_graph_ptr& aut) - { - if (aut->prop_state_acc().is_true()) - return nullptr; - - std::vector pairs; - if (!aut->acc().is_rabin_like(pairs)) - return nullptr; - - auto code = aut->get_acceptance(); - if (code.is_t()) - return nullptr; - - // if is TBA type - scc_info si{aut}; - std::vector scc_is_tba_type(si.scc_count(), false); - std::vector final(aut->edge_vector().size(), false); - - acc_cond::mark_t inf_alone = 0U; - acc_cond::mark_t fin_alone = 0U; - for (const auto& p: pairs) - if (!p.fin) - inf_alone &= p.inf; - else if (!p.inf) - fin_alone &= p.fin; - - for (unsigned scc = 0; scc < si.scc_count(); ++scc) - { - scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, fin_alone, final); - } - // compute final edges - auto res = make_twa_graph(aut->get_dict()); - res->copy_ap_of(aut); - res->prop_copy(aut, { false, false, false, false, false, true }); - res->new_states(aut->num_states()); - res->set_buchi(); - res->set_init_state(aut->get_init_state_number()); - trival deterministic = aut->prop_universal(); - trival complete = aut->prop_complete(); - - std::vector state_map(aut->num_states()); - for (unsigned scc = 0; scc < si.scc_count(); ++scc) - { - auto states = si.states_of(scc); - - if (scc_is_tba_type[scc]) - { - for (unsigned e: scc_edges(aut, si, scc)) - { - const auto& ed = aut->edge_data(e); - const auto& es = aut->edge_storage(e); - bool acc = final[e]; - res->new_acc_edge(es.src, es.dst, ed.cond, acc); - } - } - else - { - deterministic = false; - complete = trival::maybe(); - - auto acc_pairs = aut->get_acceptance().used_inf_fin_sets(); - auto infs = si.acc(scc) & acc_pairs.first; - auto infs_with_fins = (si.acc(scc) << 1U) & acc_pairs.first; - infs -= infs_with_fins; - - for (auto e: scc_edges(aut, si, scc)) - { - const auto& ed = aut->edge_data(e); - const auto& es = aut->edge_storage(e); - bool acc{ ed.acc & infs }; - res->new_acc_edge(es.src, es.dst, ed.cond, acc); - } - - auto rem = si.acc(scc) & acc_pairs.second; - assert(rem != 0U); - for (auto r: rem.sets()) - { - unsigned base = res->new_states(states.size()); - for (auto s: states) - state_map[s] = base++; - for (auto e: scc_inner_edges(aut, si, scc)) - { - const auto& ed = aut->edge_data(e); - const auto& es = aut->edge_storage(e); - if (ed.acc.has(r)) - continue; - auto src = state_map[es.src]; - auto dst = state_map[es.dst]; - res->new_acc_edge(src, dst, ed.cond, ed.acc.has(r + 1)); - // We need only one non-deterministic jump per - // cycle. As an approximation, we only do - // them on back-links. - bool jacc{ed.acc & inf_alone}; - if (es.dst <= es.src) - res->new_acc_edge(es.src, dst, ed.cond, jacc); - } - } - } - } - res->prop_complete(complete); - res->prop_universal(deterministic); - res->purge_dead_states(); - res->merge_edges(); - - return res; - } - -} diff --git a/spot/twaalgos/tra2tba.hh b/spot/twaalgos/tra2tba.hh deleted file mode 100644 index 3f812a7e1..000000000 --- a/spot/twaalgos/tra2tba.hh +++ /dev/null @@ -1,37 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement -// de l'Epita. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include - -namespace spot -{ - /// \brief Convert a transition-based Rabin automaton to Büchi automaton, - /// preserving determinism when possible. - /// - /// Return nullptr if the input is not a Rabin automaton, or is not - /// transition-based. - /// - /// This modifies the algorithm from "Deterministic - /// ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan, - /// A. Puri, and R. Brayton (ISAAC'94), but SCC-wise. - SPOT_API twa_graph_ptr - tra_to_tba(const const_twa_graph_ptr& aut); -} diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 007e0ff96..7f279753e 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -353,8 +353,7 @@ State: 0 [!0] 0 [0] 1 State: 1 {0} -[!0] 1 -[0] 1 +[t] 1 --END-- HOA: v1 States: 10 @@ -402,80 +401,72 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 {0} -[!0&!1] 12 -[0&!1] 11 -[!0&1] 1 [0&1] 0 +[!0&1] 1 +[0&!1] 11 +[!0&!1] 12 State: 1 {0} -[!0&!1] 12 -[0&!1] 11 -[!0&1] 1 [0&1] 0 -State: 2 {0} -[!0&!1] 10 +[!0&1] 1 [0&!1] 11 +[!0&!1] 12 +State: 2 {0} [!0&1] 2 [0&1] 9 +[!0&!1] 10 +[0&!1] 11 State: 3 {0} -[!0&!1] 12 -[0&!1] 11 [!0&1] 1 [0&1] 3 +[0&!1] 11 +[!0&!1] 12 State: 4 {0} -[!0&!1] 12 -[0&!1] 12 [!0&1] 4 [0&1] 7 +[!1] 12 State: 5 {0} -[!0&!1] 10 -[0&!1] 12 [!0&1] 5 [0&1] 8 +[!0&!1] 10 +[0&!1] 12 State: 6 {0} -[!0&!1] 12 -[0&!1] 11 [!0&1] 4 [0&1] 6 -State: 7 {0} +[0&!1] 11 [!0&!1] 12 -[0&!1] 12 +State: 7 {0} [!0&1] 4 [0&1] 7 +[!1] 12 State: 8 -[!0&!1] 12 -[0&!1] 12 -[!0&1] 8 -[0&1] 8 -[!0&1] 14 -[0&1] 14 +[1] 8 +[!1] 12 +[1] 14 State: 9 -[!0&!1] 12 -[0&!1] 11 [!0&1] 1 [0&1] 3 +[0&!1] 11 +[!0&!1] 12 State: 10 {0} -[!0&!1] 10 -[0&!1] 12 [!0&1] 5 [0&1] 8 -State: 11 {0} -[!0&!1] 12 -[0&!1] 11 -[!0&1] 8 -[0&1] 6 -State: 12 -[!0&!1] 12 -[0&!1] 12 -[!0&1] 8 -[0&1] 8 -State: 13 [!0&!1] 10 +[0&!1] 12 +State: 11 {0} +[0&1] 6 +[!0&1] 8 [0&!1] 11 +[!0&!1] 12 +State: 12 +[1] 8 +[!1] 12 +State: 13 [!0&1] 2 [0&1] 3 +[!0&!1] 10 +[0&!1] 11 State: 14 {0} -[!0&1] 14 -[0&1] 14 +[1] 14 --END-- HOA: v1 States: 4 @@ -511,35 +502,21 @@ properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 -[!0&!1] 0 -[0&!1] 0 -[!0&1] 0 -[0&1] 0 +[t] 0 State: 1 -[!0&!1] 0 -[0&!1] 2 -[!0&1] 0 -[0&1] 2 +[!0] 0 +[0] 2 State: 2 {0} -[!0&!1] 2 -[0&!1] 2 -[!0&1] 2 -[0&1] 2 +[t] 2 State: 3 {0} -[!0&!1] 3 -[0&!1] 2 [!0&1] 1 -[0&1] 2 +[0] 2 +[!0&!1] 3 State: 4 -[!0&!1] 3 -[0&!1] 3 -[!0&1] 1 -[0&1] 1 +[1] 1 +[!1] 3 State: 5 -[!0&!1] 4 -[0&!1] 4 -[!0&1] 4 -[0&1] 4 +[t] 4 --END-- HOA: v1 States: 5 @@ -550,24 +527,18 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 -[!0&!1] 2 [0&!1] 0 -[!0&1] 2 +[!0] 2 [0&1] 3 State: 1 -[!0&!1] 2 [0&!1] 1 -[!0&1] 2 -[0&1] 2 +[!0 | 1] 2 State: 2 {0} -[!0&!1] 2 [0&!1] 0 -[!0&1] 2 -[0&1] 2 +[!0 | 1] 2 State: 3 -[!0&!1] 2 [0&!1] 0 -[!0&1] 2 +[!0] 2 [0&1] 3 [0&1] 4 State: 4 {0} @@ -578,7 +549,8 @@ States: 37 Start: 0 AP: 2 "a" "b" acc-name: generalized-Buchi 12 -Acceptance: 12 $acctwelve +Acceptance: 12 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)\ +&Inf(7)&Inf(8)&Inf(9)&Inf(10)&Inf(11) properties: trans-labels explicit-labels state-acc complete --BODY-- State: 0 @@ -737,11 +709,11 @@ properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 -[0] 1 [!0] 0 +[0] 1 State: 1 {0} -[0] 1 [!0] 0 +[0] 1 --END-- EOF diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index ed1b48fbd..0f7852f3d 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -31,7 +31,7 @@ State: 1 [0] 1 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 2. @@ -51,7 +51,6 @@ State: 2 [!0] 1 {} [0] 2 {1} --END-- -EOF """) exp = """HOA: v1 @@ -72,7 +71,7 @@ State: 2 [0] 2 {0} --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 3. @@ -106,7 +105,7 @@ State: 1 [0] 1 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 4. @@ -146,7 +145,7 @@ State: 2 {0} [t] 2 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 5. @@ -192,7 +191,7 @@ State: 3 {0} [t] 3 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 6. @@ -222,26 +221,26 @@ Start: 0 AP: 2 "p3" "p2" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels trans-acc +properties: trans-labels explicit-labels state-acc --BODY-- State: 0 [!1] 0 [1] 1 [0&!1] 2 -State: 1 -[!1] 0 {0} -[1] 1 {0} +State: 1 {0} +[!1] 0 +[1] 1 +[0&!1] 2 +[0&1] 3 +State: 2 {0} +[0&!1] 2 +[0&1] 3 +State: 3 {0} [0&!1] 2 [0&1] 3 -State: 2 -[0&!1] 2 {0} -[0&1] 3 {0} -State: 3 -[0&!1] 2 {0} -[0&1] 3 {0} --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 7. @@ -276,7 +275,7 @@ State: 1 {0} [0] 1 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 8. @@ -355,7 +354,7 @@ State: 7 [0&2] 7 {0} --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 9. @@ -391,7 +390,7 @@ State: 1 [1&!2] 1 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 10. @@ -430,7 +429,7 @@ State: 2 {0} [0&1] 2 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 11. @@ -467,7 +466,8 @@ State: 1 [0] 1 {0} --END--""" -res = spot.tra_to_tba(aut) + +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 12. @@ -506,13 +506,13 @@ State: 1 [!0] 0 [0] 1 [!0] 3 -State: 2 +State: 2 {0} [!0] 2 State: 3 {0} [!0] 3 --END--""" -res = spot.tra_to_tba(aut) +res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) # Test 13. @@ -538,8 +538,57 @@ State: 0 "F(Gp3|GFp2)" --END-- """) -res = spot.tra_to_tba(aut) -tba = spot.tgba_determinize(res) -a = spot.dtwa_complement(aut).intersects(tba) -b = spot.dtwa_complement(tba).intersects(aut) -assert(a == b) +exp = """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p3" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!1] 0 {0} +[1] 1 +State: 1 +[!1] 0 {0} +[1] 1 {0} +--END--""" + +res = spot.remove_fin(aut) +assert(res.to_str('hoa') == exp) + +# Test 14. +aut = spot.automaton(""" +HOA: v1 +States: 1 +Start: 0 +Acceptance: 4 (Fin(0)&Inf(1)) | (Fin(2)&Inf(3)) +AP: 2 "b" "a" +--BODY-- +State: 0 + 0 {3} /*{}*/ + 0 {1 3} /*{b}*/ + 0 {2} /*{a}*/ + 0 {2 1} /*{b, a}*/ +--END--""") + +exp = """HOA: v1 +States: 2 +Start: 0 +AP: 2 "b" "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 0 {0} +[!0] 0 +[0&!1] 1 {0} +[!0&!1] 1 +State: 1 +[!1] 1 {0} +--END--""" + +res = spot.remove_fin(aut) +assert(res.to_str('hoa') == exp)