* src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class.

* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh
(couvreur99_check_result): Inherit from acss_statistics.
(couvreur99_check_result::acss_states): Implement it.
* src/tgbatest/randtgba.cc: Display statistics about accepting cycle
search space.

ChangeLog

@@ -1,5 +1,12 @@
 2005-01-03  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class.
+	* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh
+	(couvreur99_check_result): Inherit from acss_statistics.
+	(couvreur99_check_result::acss_states): Implement it.
+	* src/tgbatest/randtgba.cc: Display statistics about accepting cycle
+	search space.
+
 	* src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call
 	erase() after splice(), splice() already removes the elements.
 

src/tgbaalgos/emptiness_stats.hh

@@ -35,37 +35,53 @@ namespace spot
     : states_(0), transitions_(0), depth_(0), max_depth_(0)
     {
     }
-    void set_states(int n)
+
+    void
+    set_states(int n)
     {
       states_ = n;
     }
-    void inc_states()
+
+    void
+    inc_states()
     {
       ++states_;
     }
-    void inc_transitions()
+
+    void
+    inc_transitions()
     {
       ++transitions_;
     }
-    void inc_depth()
+
+    void
+    inc_depth()
     {
       ++depth_;
       if (depth_ > max_depth_)
 	max_depth_ = depth_;
     }
-    void dec_depth()
+
+    void
+    dec_depth()
     {
       --depth_;
     }
-    int states() const
+
+    int
+    states() const
     {
       return states_;
     }
-    int transitions() const
+
+    int
+    transitions() const
     {
       return transitions_;
     }
-    int max_depth() const
+
+    int
+    max_depth() const
     {
       return max_depth_;
     }
@@ -77,6 +93,13 @@ namespace spot
     unsigned max_depth_; /// maximal depth of the stack(s)
   };
 
+  /// Accepting Cycle Search Space statistics
+  class acss_statistics
+  {
+  public:
+    virtual int acss_states() const = 0;
+  };
+
   /// @}
 }
 

src/tgbaalgos/gtec/ce.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -78,6 +78,19 @@ namespace spot
   {
   }
 
+  int
+  couvreur99_check_result::acss_states() const
+  {
+    int count = 0;
+    int scc_root = ecs_->root.s.top().index;
+
+    numbered_state_heap_const_iterator* i = ecs_->h->iterator();
+    for (i->first(); !i->done(); i->next())
+      if (i->get_index() >= scc_root)
+	++count;
+    return count;
+  }
+
   tgba_run*
   couvreur99_check_result::accepting_run()
   {

src/tgbaalgos/gtec/ce.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -24,11 +24,14 @@
 
 #include "status.hh"
 #include "tgbaalgos/emptiness.hh"
+#include "tgbaalgos/emptiness_stats.hh"
 
 namespace spot
 {
   /// Compute a counter example from a spot::couvreur99_check_status
-  class couvreur99_check_result: public emptiness_check_result
+  class couvreur99_check_result:
+    public emptiness_check_result,
+    public acss_statistics
   {
   public:
     couvreur99_check_result(const couvreur99_check_status* ecs);
@@ -37,6 +40,8 @@ namespace spot
 
     void print_stats(std::ostream& os) const;
 
+    virtual int acss_states() const;
+
   protected:
     /// Called by accepting_run() to find a cycle which traverses all
     /// acceptance conditions in the accepted SCC.

src/tgbatest/randtgba.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -223,6 +223,35 @@ struct ec_stat
   }
 };
 
+struct acss_stat
+{
+  int min_states;
+  int max_states;
+  int tot_states;
+  int n;
+
+  acss_stat()
+    : n(0)
+  {
+  }
+
+  void
+  count(const spot::acss_statistics* acss)
+  {
+    int s = acss->acss_states();
+    if (n++)
+      {
+	min_states = std::min(min_states, s);
+	max_states = std::max(max_states, s);
+	tot_states += s;
+      }
+    else
+      {
+	min_states = max_states = tot_states = s;
+      }
+  }
+};
+
 struct ar_stat
 {
   int min_prefix;
@@ -268,6 +297,9 @@ struct ar_stat
 typedef std::map<std::string, ec_stat> ec_stats_type;
 ec_stats_type ec_stats;
 
+typedef std::map<std::string, acss_stat> acss_stats_type;
+acss_stats_type acss_stats;
+
 typedef std::map<std::string, ar_stat> ar_stats_type;
 ar_stats_type ar_stats;		// Statistics about accepting runs.
 ar_stats_type mar_stats;        // ... about minimized accepting runs.
@@ -547,6 +579,10 @@ main(int argc, char** argv)
 		{
 		  std::cout << "acc. run";
 		  ++n_non_empty;
+		  const spot::acss_statistics* acss =
+		    dynamic_cast<const spot::acss_statistics*>(res);
+		  if (opt_z && acss)
+		    acss_stats[algo].count(acss);
 		  if (opt_replay)
 		    {
 		      spot::tgba_run* run;
@@ -658,6 +694,7 @@ main(int argc, char** argv)
 
   if (!ec_stats.empty())
     {
+      std::cout << std::endl;
       std::ios::fmtflags old = std::cout.flags();
       std::cout << std::right << std::fixed << std::setprecision(1);
 
@@ -696,7 +733,7 @@ main(int argc, char** argv)
                 << std::setw(22) << "algorithm"
 		<< " |   min   < mean  < max |   n"
 		<< std::endl
-		<< std::setw(59) << std::setfill('-') << "" << std::setfill(' ')
+		<< std::setw(53) << std::setfill('-') << "" << std::setfill(' ')
 		<< std::endl;
       for (ec_stats_type::const_iterator i = ec_stats.begin();
 	   i != ec_stats.end(); ++i)
@@ -716,6 +753,38 @@ main(int argc, char** argv)
       std::cout << std::setiosflags(old);
     }
 
+  if (!acss_stats.empty())
+    {
+      std::cout << std::endl;
+      std::ios::fmtflags old = std::cout.flags();
+      std::cout << std::right << std::fixed << std::setprecision(1);
+
+      std::cout << "Statistics about accepting cycle search space:"
+		<< std::endl;
+      std::cout << std::setw(22) << ""
+		<< " |              states           |"
+		<< std::endl << std::setw(22) << "algorithm"
+		<< " |   min   < mean  < max | total |  n"
+		<< std::endl
+		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
+		<< std::endl;
+      for (acss_stats_type::const_iterator i = acss_stats.begin();
+	   i != acss_stats.end(); ++i)
+	std::cout << std::setw(22) << i->first << " |"
+		  << std::setw(6) << i->second.min_states
+		  << " "
+		  << std::setw(8)
+		  << static_cast<float>(i->second.tot_states) / i->second.n
+		  << " "
+		  << std::setw(6) << i->second.max_states
+		  << " |"
+		  << std::setw(6) << i->second.tot_states
+		  << " |"
+		  << std::setw(4) << i->second.n
+		  << std::endl;
+      std::cout << std::setiosflags(old);
+    }
+
   if (!ar_stats.empty())
     {
       std::cout << std::endl