diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 33d35d632..4da23a865 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -476,7 +476,7 @@ namespace if (opt_merge) aut->merge_transitions(); if (opt_clean_acc || opt_rem_fin) - cleanup_acceptance(aut); + cleanup_acceptance_here(aut); if (opt_complement_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().complement()); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index d4ebef7c4..67e0de9f6 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1110,7 +1110,7 @@ namespace { #define DO(x, prefix, suffix) if (x[i]) \ { \ - cleanup_acceptance(x[i]); \ + cleanup_acceptance_here(x[i]); \ if (x[i]->acc().uses_fin_acceptance()) \ { \ auto st = x[i]->num_states(); \ diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc index 5ee8027fc..e6523f53a 100644 --- a/src/tgbaalgos/cleanacc.cc +++ b/src/tgbaalgos/cleanacc.cc @@ -21,11 +21,11 @@ namespace spot { - void cleanup_acceptance(tgba_digraph_ptr& aut) + tgba_digraph_ptr cleanup_acceptance_here(tgba_digraph_ptr aut) { auto& acc = aut->acc(); if (acc.num_sets() == 0) - return; + return aut; auto& c = aut->get_acceptance(); acc_cond::mark_t used_in_cond = c.used_sets(); @@ -39,7 +39,7 @@ namespace spot auto useless = acc.comp(useful); if (!useless) - return; + return aut; // Remove useless marks from the automaton for (auto& t: aut->transitions()) @@ -50,7 +50,14 @@ namespace spot // This may in turn cause even more set to be unused, because of // some simplifications, so do it again. - return cleanup_acceptance(aut); + return cleanup_acceptance_here(aut); } + tgba_digraph_ptr cleanup_acceptance(const_tgba_digraph_ptr aut) + { + return cleanup_acceptance_here(make_tgba_digraph(aut, + tgba::prop_set::all())); + } + + } diff --git a/src/tgbaalgos/cleanacc.hh b/src/tgbaalgos/cleanacc.hh index b52de35aa..148ab8c34 100644 --- a/src/tgbaalgos/cleanacc.hh +++ b/src/tgbaalgos/cleanacc.hh @@ -24,6 +24,11 @@ namespace spot { /// \brief Remove useless acceptance sets - SPOT_API void - cleanup_acceptance(tgba_digraph_ptr& aut); + /// @{ + SPOT_API tgba_digraph_ptr + cleanup_acceptance_here(tgba_digraph_ptr aut); + + SPOT_API tgba_digraph_ptr + cleanup_acceptance(const_tgba_digraph_ptr aut); + /// @} } diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index 2069cd29e..b4091c705 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -173,8 +173,7 @@ namespace spot { // Simply complete the automaton, and complement its // acceptance. - auto res = tgba_complete(aut); - cleanup_acceptance(res); + auto res = cleanup_acceptance_here(tgba_complete(aut)); res->set_acceptance(res->acc().num_sets(), res->get_acceptance().complement()); return res; diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc index 7619f16fa..088dc53c6 100644 --- a/src/tgbaalgos/remfin.cc +++ b/src/tgbaalgos/remfin.cc @@ -333,7 +333,7 @@ namespace spot } res->purge_dead_states(); trace << "before cleanup: " << res->get_acceptance() << '\n'; - cleanup_acceptance(res); + cleanup_acceptance_here(res); trace << "after cleanup: " << res->get_acceptance() << '\n'; return res; }