From 3c17c418a23c086d899bcc5b4f7c30b94a724830 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 21 Sep 2012 15:09:08 +0200 Subject: [PATCH] Speedup is_weak_scc() if all transitions in the SCC are accepting. * src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Speedup when all transitions are accepting. --- src/tgbaalgos/isweakscc.cc | 4 ++++ src/tgbaalgos/isweakscc.hh | 8 +++++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 19e1e7526..e29ee6bbe 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -71,6 +71,10 @@ namespace spot // If no cycle is accepting, the SCC is weak. if (!map.accepting(scc)) return true; + // If all transitions use all acceptance conditions, the SCC is weak. + if (map.useful_acc_of(scc) == + bdd_support(map.get_aut()->neg_acceptance_conditions())) + return true; // If the SCC is accepting, but one cycle is not, the SCC is not // weak. weak_checker w(map); diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index d28a4b205..83d195e78 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -35,9 +35,11 @@ namespace spot /// /// The scc_map \a map should have been built already. The absence /// of accepting cycle is easy to check (the scc_map can tell - /// whether the SCC is non-accepting already). For the accepting - /// SCCs, this function enumerates all cycles in the given SCC (it - /// stops if it find a non-accepting cycle). + /// whether the SCC is non-accepting already). Similarly, an SCC in + /// which all transitions belong to all acceptance sets is + /// necessarily weak. + /// For other accepting SCCs, this function enumerates all cycles in + /// the given SCC (it stops if it find a non-accepting cycle). bool is_weak_scc(scc_map& map, unsigned scc); /// @}