diff --git a/NEWS b/NEWS index b63630d6a..66ecc5bc1 100644 --- a/NEWS +++ b/NEWS @@ -224,6 +224,10 @@ New in spot 2.4.4.dev (net yet released) - The test suite is now using v4 of the Jupyter Notebook format. + - The function rabin_is_buchi_realizable() as its name suggests checks + if a rabin aut. is Büchi realizable. It is heavily based on + tra_to_tba() algorithm. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 08ff27a52..2991e081b 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -67,17 +67,16 @@ namespace spot p.set_type(spot::postprocessor::Generic); p.set_pref(spot::postprocessor::Deterministic); p.set_level(spot::postprocessor::Low); - auto dra = p.run(aut); - if (dra->acc().is_generalized_buchi()) + auto dpa = p.run(aut); + if (dpa->acc().is_generalized_buchi()) { - assert(is_deterministic(dra)); + assert(is_deterministic(dpa)); return true; } else { - auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra)); - assert(ba); - return is_deterministic(ba); + auto dra = to_generalized_rabin(dpa); + return rabin_is_buchi_realizable(dra); } } } diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 344e5d31a..2206d8741 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -220,7 +220,8 @@ namespace spot 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, init, filter, &filter_data, + scc_info_options::TRACK_STATES); for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc) { @@ -274,8 +275,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); @@ -785,6 +786,31 @@ namespace spot } } + bool + rabin_is_buchi_realizable(const const_twa_graph_ptr& inaut) + { + auto aut = cleanup_acceptance(inaut); + + std::vector pairs; + if (!aut->acc().is_rabin_like(pairs)) + return false; + + auto aut_pairs = rs_pairs_view(pairs); + if (aut->get_acceptance().is_t()) + return false; + + // if is TBA type + scc_info si(aut, scc_info_options::TRACK_STATES); + 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) + if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final)) + return false; + + return true; + } + twa_graph_ptr rabin_to_buchi_maybe(const const_twa_graph_ptr& aut) { diff --git a/spot/twaalgos/remfin.hh b/spot/twaalgos/remfin.hh index 6444eba46..7eb26b6eb 100644 --- a/spot/twaalgos/remfin.hh +++ b/spot/twaalgos/remfin.hh @@ -23,6 +23,13 @@ namespace spot { + /// \ingroup twa_acc_transform + /// \brief Check if \aut is Büchi-realizable. This is inspired + /// from rabin_to_buchi_maybe()'s algorithm. The main difference is that + /// here, no automaton is built. + SPOT_API bool + rabin_is_buchi_realizable(const const_twa_graph_ptr& aut); + /// \ingroup twa_acc_transform /// \brief Convert a Rabin automaton to Büchi automaton, preserving /// determinism when possible.