From e6a5a743f79b4049c56aa1ac14a2305ae12bccd2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Jul 2015 12:07:40 +0200 Subject: [PATCH] remfin: avoid some loops in SCC that do not intersect any Fin * src/twaalgos/remfin.cc: Here. --- src/twaalgos/remfin.cc | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc index 228647dd5..cbe319320 100644 --- a/src/twaalgos/remfin.cc +++ b/src/twaalgos/remfin.cc @@ -283,12 +283,17 @@ namespace spot // What to keep and add into the main copy acc_cond::mark_t main_sets = 0U; acc_cond::mark_t main_add = 0U; + bool intersects_fin = false; for (unsigned i = 0; i < cs; ++i) if (!(m & rem[i])) { main_sets |= keep[i]; main_add |= add[i]; } + else + { + intersects_fin = true; + } trace << "main_sets " << main_sets << "\nmain_add " << main_add << '\n'; // Create the main copy @@ -296,7 +301,9 @@ namespace spot for (auto& t: aut->out(s)) res->new_edge(s, t.dst, t.cond, (t.acc & main_sets) | main_add); - if (si.is_rejecting_scc(n)) + // We do not need any other copy if the SCC is non-accepting, + // of if it does not intersect any Fin. + if (!intersects_fin || si.is_rejecting_scc(n)) continue; // Create clones