From 99981153e613461f12c8e0d864d2e43ec8abb404 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 18 Nov 2009 15:18:40 +0100
Subject: [PATCH] Fix acceptance check in scc_map: trivial SCCs are not
 accepting. Also compute useless SCCs.

* src/tgbaalgos/scc.cc (scc_map::scc::trivial): New field.
(scc_stats::useless_scc_map): New field.
* src/tgbaalgos/scc.cc (scc_map::build_map): Mark SCCs that are
not trivial.
(scc_map::accepting): Always return false for trivial SCC.
(build_scc_stats): Fill in useless_scc_map.
---
 ChangeLog            | 12 ++++++++++++
 src/tgbaalgos/scc.cc |  8 ++++++++
 src/tgbaalgos/scc.hh |  8 +++++++-
 3 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/ChangeLog b/ChangeLog
index 4864f8c64..964d0f3eb 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,15 @@
+2009-11-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fix acceptance check in scc_map: trivial SCCs are not accepting.
+	Also compute useless SCCs.
+
+	* src/tgbaalgos/scc.cc (scc_map::scc::trivial): New field.
+	(scc_stats::useless_scc_map): New field.
+	* src/tgbaalgos/scc.cc (scc_map::build_map): Mark SCCs that are
+	not trivial.
+	(scc_map::accepting): Always return false for trivial SCC.
+	(build_scc_stats): Fill in useless_scc_map.
+
 2009-11-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Make it easy to filter states while iterating over an automaton.
diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc
index 048525ffa..d36b1770d 100644
--- a/src/tgbaalgos/scc.cc
+++ b/src/tgbaalgos/scc.cc
@@ -77,6 +77,8 @@ namespace spot
   bool
   scc_map::accepting(unsigned n) const
   {
+    if (scc_map_[n].trivial)
+      return false;
     return acc_set_of(n) == aut_->all_acceptance_conditions();
   }
 
@@ -288,6 +290,8 @@ namespace spot
 	root_.front().succ.insert(succs.begin(), succs.end());
 	root_.front().conds.insert(conds.begin(), conds.end());
 	root_.front().supp &= supp;
+	// This SCC is no longer trivial.
+	root_.front().trivial = false;
       }
 
     // recursively update supp_rec
@@ -417,6 +421,10 @@ namespace spot
     res.acc_paths = d.acc_paths[init];
     res.dead_paths = d.dead_paths[init];
 
+    res.useless_scc_map.reserve(res.scc_total);
+    for (unsigned n = 0; n < res.scc_total; ++n)
+      res.useless_scc_map[n] = !d.acc_paths[n];
+
     return res;
   }
 
diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh
index acd3e3970..ced5a2e9e 100644
--- a/src/tgbaalgos/scc.hh
+++ b/src/tgbaalgos/scc.hh
@@ -56,6 +56,9 @@ namespace spot
     unsigned dead_paths;
     unsigned self_loops;
 
+    /// A map of the useless SCCs.
+    std::vector<bool> useless_scc_map;
+
     std::ostream& dump(std::ostream& out) const;
   };
 
@@ -150,7 +153,8 @@ namespace spot
     {
     public:
       scc(int index) : index(index), acc(bddfalse),
-		       supp(bddtrue), supp_rec(bddfalse) {};
+		       supp(bddtrue), supp_rec(bddfalse),
+		       trivial(true) {};
       /// Index of the SCC.
       int index;
       /// The union of all acceptance conditions of transitions which
@@ -166,6 +170,8 @@ namespace spot
       bdd supp_rec;
       /// Successor SCC.
       succ_type succ;
+      /// Trivial SCC have one state and no self-loops.
+      bool trivial;
     };
 
     const tgba* aut_;		// Automata to decompose.