Compute more statistics about SCCs.

ChangeLog

+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.

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;
   }
 

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;
   };