From 967b1a4192940853b9cff0822d6eaf57cacb7415 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 30 May 2017 15:31:49 +0200 Subject: [PATCH] remfin: use an scc_info filter to avoid copying automata * spot/twaalgos/remfin.cc (is_scc_ba_type): Replace the call to mask_keep_states by the use of an scc_info filter. --- spot/twaalgos/remfin.cc | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 3f99f25c9..17c7194d9 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -101,12 +101,10 @@ namespace spot // 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); - } + if (aut->state_acc_sets(s) & i) + final[s] = true; + else + unknown.insert(s); // Check whether it is possible to build non-accepting cycles // using only the "unknown" states. while (!unknown.empty()) @@ -115,7 +113,18 @@ namespace spot for (auto s: unknown) keep[s] = true; - scc_info si(mask_keep_states(aut, keep, *unknown.begin())); + 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; + }; + + scc_info si(aut, *unknown.begin(), filter, &keep); unsigned scc_max = si.scc_count(); for (unsigned scc = 0; scc < scc_max; ++scc) {