diff --git a/NEWS b/NEWS index f838b27a0..baa3f5d0a 100644 --- a/NEWS +++ b/NEWS @@ -23,7 +23,9 @@ New in spot 2.6.0.dev (not yet released) emptiness checks of twa_graph_ptr (i.e., automata not built on-the-fly) with an *arbitrary* acceptance condition. Its sister spot::generic_emptiness_check_scc() can be used to decide the - emptiness of an SCC. + emptiness of an SCC. This is now used by + twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and + scc_info::determine_unknown_acceptance(). New in spot 2.6 (2018-07-04) diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 8c0cb1a7d..b8ba5cb86 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -31,6 +31,8 @@ #include #include #include +#include +#include #include namespace spot @@ -53,10 +55,26 @@ namespace spot namespace { + const_twa_graph_ptr is_twa_graph(const const_twa_ptr& a) + { + return std::dynamic_pointer_cast(a); + } + + // Make sure automata using Fin acceptance are twa_graph_ptr + const_twa_graph_ptr fin_to_twa_graph_maybe(const const_twa_ptr& a) + { + if (!a->acc().uses_fin_acceptance()) + return nullptr; + auto aa = is_twa_graph(a); + if (!aa) + aa = make_twa_graph(a, twa::prop_set::all()); + return remove_alternation(aa); + } + // Remove Fin-acceptance and alternation. const_twa_ptr remove_fin_maybe(const const_twa_ptr& a) { - auto aa = std::dynamic_pointer_cast(a); + auto aa = is_twa_graph(a); if ((!aa || aa->is_existential()) && !a->acc().uses_fin_acceptance()) return a; if (!aa) @@ -77,6 +95,9 @@ namespace spot bool twa::is_empty() const { + const_twa_ptr a = shared_from_this(); + if (const_twa_graph_ptr ag = fin_to_twa_graph_maybe(a)) + return generic_emptiness_check(ag); return !couvreur99_new_check(remove_fin_maybe(shared_from_this())); } @@ -111,7 +132,18 @@ namespace spot bool twa::intersects(const_twa_ptr other) const { - auto a1 = remove_fin_maybe(shared_from_this()); + auto self = shared_from_this(); + // If the two operands are explicit automata (twa_graph_ptr) and one + // of them uses Fin acceptance, make a regular product and check it + // with the generic emptiness. + if (acc().uses_fin_acceptance() || other->acc().uses_fin_acceptance()) + { + const_twa_graph_ptr g1 = is_twa_graph(self); + const_twa_graph_ptr g2 = is_twa_graph(other); + if (g1 && g2 && g1->is_existential() && g2->is_existential()) + return !generic_emptiness_check(product(g1, g2)); + } + auto a1 = remove_fin_maybe(self); auto a2 = remove_fin_maybe(other); return !otf_product(a1, a2)->is_empty(); } diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 0bcec63b8..109c5b700 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -207,6 +207,9 @@ namespace spot bool generic_emptiness_check(const const_twa_graph_ptr& aut) { + if (SPOT_UNLIKELY(!aut->is_existential())) + throw std::runtime_error("generic_emptiness_check() " + "does not support alternating automata"); auto aut_ = std::const_pointer_cast(aut); acc_cond old = aut_->acc(); bool res = generic_emptiness_check_main_nocopy(aut_); @@ -217,6 +220,9 @@ namespace spot bool generic_emptiness_check_for_scc(const scc_info& si, unsigned scc) { + if (SPOT_UNLIKELY(!si.get_aut()->is_existential())) + throw std::runtime_error("generic_emptiness_check_for_scc() " + "does not support alternating automata"); return generic_emptiness_check_for_scc_nocopy(si, scc); } } diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index 442177232..01497edcc 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -118,9 +118,8 @@ namespace spot if (!accepting) continue; // We can't avoid it any more, we have to check the - // acceptance if the SCC. - std::vector k; - useful[n] = !sccmap_prod.check_scc_emptiness(n, &k); + // acceptance of the SCC. + useful[n] = !sccmap_prod.check_scc_emptiness(n); } } diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index a9597a2dc..16dbd1c7e 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -24,6 +24,7 @@ #include #include #include +#include #include @@ -423,23 +424,18 @@ namespace spot return support; } - bool scc_info::check_scc_emptiness(unsigned n, std::vector* k) + bool scc_info::check_scc_emptiness(unsigned n) { if (SPOT_UNLIKELY(!aut_->is_existential())) throw std::runtime_error("scc_info::check_scc_emptiness() " "does not support alternating automata"); if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) report_need_track_states(); - k->assign(aut_->num_states(), false); - auto& node = node_[n]; - for (auto i: node.states_) - (*k)[i] = true; - return mask_keep_accessible_states(aut_, *k, node.one_state_)->is_empty(); + return generic_emptiness_check_for_scc(*this, n); } void scc_info::determine_unknown_acceptance() { - std::vector k; unsigned s = scc_count(); bool changed = false; // iterate over SCCs in topological order @@ -453,7 +449,7 @@ namespace spot "scc_info::determine_unknown_acceptance() " "does not support alternating automata"); auto& node = node_[s]; - if (check_scc_emptiness(s, &k)) + if (check_scc_emptiness(s)) node.rejecting_ = true; else node.accepting_ = true; diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 955cf6ba2..392d1235f 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -592,10 +592,8 @@ namespace spot /// \brief Recompute whether an SCC is accepting or not. /// /// This is an internal function of - /// determine_unknown_acceptance(). The Boolean vector k will be - /// used by the method to mark the state that belong to the SCC. - /// It can be shared between multiple calls. - bool check_scc_emptiness(unsigned n, std::vector* k); + /// determine_unknown_acceptance(). + bool check_scc_emptiness(unsigned n); bool is_useful_scc(unsigned scc) const {