diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index 8af04121c..fb2a498e9 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -79,36 +79,48 @@ namespace spot assert(sprod); // What follow is a way to compute whether an SCC is useless in - // prod, without having to call - // scc_map::determine_unknown_acceptance() on scc_map(prod), - // because prod has potentially a large acceptance condition. - // - // We know that an SCC of the product is accepting iff it is the - // combination of two accepting SCCs of the original automaton. - // - // So we can just compute the acceptance of each SCC this way, and - // derive the usefulness from that. + // prod, avoiding scc_info::determine_unknown_acceptance() on the + // product, because prod may have a large acceptance condition. scc_info sccmap_prod(prod); unsigned psc = sccmap_prod.scc_count(); std::vector useful(psc); for (unsigned n = 0; n < psc; ++n) { - unsigned one_state = sccmap_prod.states_of(n).front(); - bool accepting = - v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second]; - if (accepting && !sccmap_prod.is_trivial(n)) + // If scc_info could determinate acceptance easily, use it. + // An accepting SCC is useful. + bool uf = sccmap_prod.is_accepting_scc(n); + // If any of the successor is useful, this SCC is useful as + // well regardless of its acceptance. + if (!uf) + for (unsigned j: sccmap_prod.succ(n)) + if (useful[j]) + { + uf = true; + break; + } + if (uf) { useful[n] = true; continue; } - bool uf = false; - for (unsigned j: sccmap_prod.succ(n)) - if (useful[j]) - { - uf = true; - break; - } - useful[n] = uf; + if (!sccmap_prod.is_rejecting_scc(n)) + { + // This SCC has no useful successors, but we still do not + // known if it is accepting. + // + // A necessary condition for the SCC to be accepting is that + // its it the combination of two accepting SCCs. So let's + // test that first. + unsigned one_state = sccmap_prod.states_of(n).front(); + bool accepting = + v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second]; + 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); + } } // Now we just have to count the number of states && edges that diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 567b9f1bd..032444842 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -421,6 +421,20 @@ namespace spot return support; } + bool scc_info::check_scc_emptiness(unsigned n, std::vector* k) + { + 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(); + } + void scc_info::determine_unknown_acceptance() { std::vector k; @@ -436,15 +450,8 @@ namespace spot throw std::runtime_error( "scc_info::determine_unknown_acceptance() " "does not support alternating automata"); - if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) - report_need_track_states(); auto& node = node_[s]; - if (k.empty()) - k.resize(aut_->num_states()); - for (auto i: node.states_) - k[i] = true; - if (mask_keep_accessible_states(aut_, k, node.one_state_) - ->is_empty()) + if (check_scc_emptiness(s, &k)) node.rejecting_ = true; else node.accepting_ = true; diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 684a6e9c8..f44531b2d 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -583,10 +583,20 @@ namespace spot return node(scc).is_rejecting(); } - // Study the SCC that are currently reported neither as accepting - // nor rejecting because of the presence of Fin sets + /// \brief Study the SCCs that are currently reported neither as + /// accepting nor as rejecting because of the presence of Fin sets + /// + /// This simply calls check_scc_emptiness() on undeterminate SCCs. void determine_unknown_acceptance(); + /// \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); + bool is_useful_scc(unsigned scc) const { if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC))) diff --git a/tests/core/unambig.test b/tests/core/unambig.test index ebeb65dd6..ba85960d1 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -285,6 +285,7 @@ EOF run 1 autfilt -q --is-unambiguous smaller.hoa # These automata come from Simon Jantsch and David Müller. +# They exposed bugs in the optimized version of our unambiguous check. cat >sjdb.hoa <ambig.hoa<