From 7998fff056856d793697eb0f30bda146a509a8dd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 11 Dec 2008 13:06:58 +0100
Subject: [PATCH] Compute more statistics about SCCs.

---
 ChangeLog            | 10 +++++++
 src/tgbaalgos/scc.cc | 67 ++++++++++++++++++++++++++++++++++++++++++++
 src/tgbaalgos/scc.hh | 18 ++++++++++++
 3 files changed, 95 insertions(+)

diff --git a/ChangeLog b/ChangeLog
index ee06c0690..35c1ea4f8 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,13 @@
+2008-12-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Compute more statistics about SCCs.
+
+	* src/tgbaalgos/scc.hh (scc_stats): Add new attributes:
+	acc_scc, dead_scc, acc_paths, dead_paths.
+	* src/tgbaalgos/scc.hh (scc_stats::dump): Display them.
+	(build_scc_stats): Compute them.
+	(scc_recurse_data, scc_recurse): New helper structure and function.
+
 2008-12-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix tracking of SCCs on the search stack.
diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc
index 29e243db5..5bd6c19f1 100644
--- a/src/tgbaalgos/scc.cc
+++ b/src/tgbaalgos/scc.cc
@@ -30,6 +30,10 @@ namespace spot
   scc_stats::dump(std::ostream& out) const
   {
     out << "total SCCs: " << scc_total << std::endl;
+    out << "accepting SCCs: " << acc_scc << std::endl;
+    out << "dead SCCs: " << dead_scc << std::endl;
+    out << "accepting paths: " << acc_paths << std::endl;
+    out << "dead paths: " << dead_paths << std::endl;
     return out;
   }
 
@@ -243,10 +247,73 @@ namespace spot
     return -scc_num_;
   }
 
+  namespace
+  {
+    struct scc_recurse_data
+    {
+      scc_recurse_data() : acc_scc(0), dead_scc(0) {};
+      typedef std::map<int, unsigned> graph_counter;
+      graph_counter acc_paths;
+      graph_counter dead_paths;
+      unsigned acc_scc;
+      unsigned dead_scc;
+    };
+
+    bool scc_recurse(const scc_map& m, int state, scc_recurse_data& data)
+    {
+      const scc_map::succ_type& succ = m.succ(state);
+
+      bool accepting = m.accepting(state);
+      scc_map::succ_type::const_iterator it;
+      int acc_paths = 0;
+      int dead_paths = 0;
+
+      bool paths_accepting = false;
+      for (it = succ.begin(); it != succ.end(); ++it)
+	{
+	  int dest = it->first;
+	  bool path_accepting = scc_recurse(m, dest, data);
+	  paths_accepting |= path_accepting;
+
+	  if (path_accepting)
+	    acc_paths += data.acc_paths[dest];
+	  else
+	    dead_paths += data.dead_paths[dest];
+	}
+
+      if (accepting)
+	{
+	  ++data.acc_scc;
+	  if (!paths_accepting)
+	    acc_paths = 1;
+	}
+      else if (!paths_accepting)
+	{
+	  ++data.dead_scc;
+	}
+
+      data.acc_paths[state] = acc_paths;
+      data.dead_paths[state] = dead_paths;
+
+      return accepting | paths_accepting;
+    }
+
+  }
+
   scc_stats build_scc_stats(const scc_map& m)
   {
     scc_stats res;
     res.scc_total = m.scc_count();
+
+    scc_recurse_data d;
+    int init = m.initial();
+    scc_recurse(m, init, d);
+
+    res.acc_scc = d.acc_scc;
+    res.dead_scc = d.dead_scc;
+    res.acc_paths = d.acc_paths[init];
+    res.dead_paths = d.dead_paths[init];
+
     return res;
   }
 
diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh
index 25e583a73..825cc8d94 100644
--- a/src/tgbaalgos/scc.hh
+++ b/src/tgbaalgos/scc.hh
@@ -31,7 +31,25 @@ namespace spot
 
   struct scc_stats
   {
+    /// Total number of SCCs.
     unsigned scc_total;
+    /// Total number of accepting SCC.
+    unsigned acc_scc;
+    /// Total number of dead SCC.
+    ///
+    /// An SCC is dead if no accepting SCC is reachable from it.
+    /// Note that an SCC can be neither dead nor accepting.
+    unsigned dead_scc;
+
+    /// Number of path to a terminal accepting SCC.
+    ///
+    /// A terminal accepting SCC is an accepting SCC that has
+    /// only dead successors (or no successors at all).
+    unsigned acc_paths;
+    /// Number of paths to a terminal dead SCC.
+    ///
+    /// A terminal dead SCC is a dead SCC without successors.
+    unsigned dead_paths;
 
     std::ostream& dump(std::ostream& out) const;
   };