* src/tgbaalgos/emptiness_stats.hh (ars_statistics): Distinguish

states visited to compute the prefix and those for the cycle.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/gtec/ce.cc: Adjust.
* src/tgbatest/randtgba.cc: Print both statistics.

ChangeLog

@@ -1,3 +1,11 @@
+2005-01-24  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/emptiness_stats.hh (ars_statistics): Distinguish
+	states visited to compute the prefix and those for the cycle.
+	* src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx,
+	src/tgbaalgos/gtec/ce.cc: Adjust.
+	* src/tgbatest/randtgba.cc: Print both statistics.
+
 2005-01-24  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
 
 	* src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add options

src/tgbaalgos/emptiness_stats.hh

@@ -125,24 +125,37 @@ namespace spot
   {
   public:
     ars_statistics()
-      : states_(0)
+      : prefix_states_(0), cycle_states_(0)
     {
     }
 
     void
-    inc_ars_states()
+    inc_ars_prefix_states()
     {
-      ++states_;
+      ++prefix_states_;
     }
 
     int
-    ars_states() const
+    ars_prefix_states() const
     {
-      return states_;
+      return prefix_states_;
+    }
+
+    void
+    inc_ars_cycle_states()
+    {
+      ++cycle_states_;
+    }
+
+    int
+    ars_cycle_states() const
+    {
+      return cycle_states_;
     }
 
   private:
-    unsigned states_;	/// number of states visited
+    unsigned prefix_states_;	/// states visited to construct the prefix
+    unsigned cycle_states_;	/// states visited to construct the cycle
   };
 
   /// @}

src/tgbaalgos/gtec/ce.cc

@@ -48,7 +48,7 @@ namespace spot
       const state*
       filter(const state* s)
       {
-	r->inc_ars_states();
+	r->inc_ars_prefix_states();
 	numbered_state_heap::state_index_p sip = ecs->h->find(s);
 	// Ignore unknown states ...
 	if (!sip.first)
@@ -180,7 +180,7 @@ namespace spot
 	  virtual const state*
 	  filter(const state* s)
 	  {
-	    r->inc_ars_states();
+	    r->inc_ars_cycle_states();
 	    numbered_state_heap::state_index_p sip = ecs->h->find(s);
 	    // Ignore unknown states.
 	    if (!sip.first)

src/tgbaalgos/gv04.cc

@@ -339,7 +339,7 @@ namespace spot
 	    virtual const state*
 	    filter(const state* s)
 	    {
-	      r->inc_ars_states();
+	      r->inc_ars_cycle_states();
 	      // Do not escape the SCC
 	      hash_type::const_iterator j = data.h.find(s);
 	      if (// This state was never visited so far.

src/tgbaalgos/ndfs_result.hxx

@@ -272,7 +272,7 @@ namespace spot
           if (!f.it->done())
             {
               const state *s_prime = f.it->current_state();
-	      inc_ars_states();
+	      inc_ars_cycle_states();
               ndfsr_trace << "  Visit the successor: "
                           << a_->format_state(s_prime) << std::endl;
               bdd label = f.it->current_condition();
@@ -398,7 +398,7 @@ namespace spot
 
       const state* filter(const state* s)
       {
-	ars->inc_ars_states();
+	ars->inc_ars_cycle_states();
         if (!h.has_been_visited(s)
 	    || seen.find(s) != seen.end()
 	    || dead.find(s) != dead.end())
@@ -459,6 +459,7 @@ namespace spot
     typedef Sgi::hash_multimap<const state*, transition,
 			       state_ptr_hash, state_ptr_equal> m_source_trans;
 
+    template<bool cycle>
     class min_path: public bfs_steps
     {
     public:
@@ -490,7 +491,11 @@ namespace spot
 
       const state* filter(const state* s)
       {
-	ars->inc_ars_states();
+	if (cycle)
+	  ars->inc_ars_cycle_states();
+	else
+	  ars->inc_ars_prefix_states();
+
         ndfsr_trace << "filter: " << a_->format_state(s);
         if (!h.has_been_visited(s) || seen.find(s) != seen.end())
           {
@@ -568,7 +573,7 @@ namespace spot
 	  typename m_source_trans::iterator i = target.find(current.dest);
 	  if (i == target.end())
 	    {
-	      min_path s(this, a_, target, h_);
+	      min_path<true> s(this, a_, target, h_);
 	      const state* res = s.search(current.dest->clone(), run->cycle);
 	      // init current to the corresponding transition.
 	      assert(res);
@@ -598,7 +603,7 @@ namespace spot
 		      << a_->format_state(begin) << std::endl;
 	  transition tmp;
 	  target.insert(std::make_pair(begin, tmp));
-	  min_path s(this, a_, target, h_);
+	  min_path<true> s(this, a_, target, h_);
 	  const state* res = s.search(current.dest->clone(), run->cycle);
 	  assert(res);
 	  assert(res->compare(begin) == 0);
@@ -633,7 +638,7 @@ namespace spot
       else
         {
           // This initial state is outside the cycle.  Compute the prefix.
-          min_path s(this, a_, target, h_);
+          min_path<false> s(this, a_, target, h_);
           cycle_entry_point = s.search(prefix_start, run->prefix);
           assert(cycle_entry_point);
           cycle_entry_point = cycle_entry_point->clone();

src/tgbatest/randtgba.cc

@@ -336,9 +336,12 @@ struct acss_stat
 
 struct ars_stat
 {
-  int min_states;
+  int min_prefix_states;
-  int max_states;
+  int max_prefix_states;
-  int tot_states;
+  int tot_prefix_states;
+  int min_cycle_states;
+  int max_cycle_states;
+  int tot_cycle_states;
   int n;
 
   ars_stat()
@@ -349,21 +352,25 @@ struct ars_stat
   void
   count(const spot::ars_statistics* acss)
   {
-    int s = acss->ars_states();
+    int p = acss->ars_prefix_states();
+    int c = acss->ars_cycle_states();
     if (n++)
       {
-	min_states = std::min(min_states, s);
+	min_prefix_states = std::min(min_prefix_states, p);
-	max_states = std::max(max_states, s);
+	max_prefix_states = std::max(max_prefix_states, p);
-	tot_states += s;
+	tot_prefix_states += p;
+	min_cycle_states = std::min(min_cycle_states, c);
+	max_cycle_states = std::max(max_cycle_states, c);
+	tot_cycle_states += c;
       }
     else
       {
-	min_states = max_states = tot_states = s;
+	min_prefix_states = max_prefix_states = tot_prefix_states = p;
+	min_cycle_states = max_cycle_states = tot_cycle_states = c;
       }
   }
 };
 
-
 struct ar_stat
 {
   int min_prefix;
@@ -1259,7 +1266,7 @@ main(int argc, char** argv)
       std::cout << "Statistics about accepting run computation:"
 		<< std::endl;
       std::cout << std::setw(22) << ""
-		<< " |      (non unique) states      |"
+		<< " |(non unique) states for prefix |"
 		<< std::endl << std::setw(22) << "algorithm"
 		<< " |   min   < mean  < max | total |  n"
 		<< std::endl
@@ -1268,14 +1275,37 @@ main(int argc, char** argv)
       for (ars_stats_type::const_iterator i = ars_stats.begin();
 	   i != ars_stats.end(); ++i)
 	std::cout << std::setw(22) << i->first << " |"
-		  << std::setw(6) << i->second.min_states
+		  << std::setw(6) << i->second.min_prefix_states
 		  << " "
 		  << std::setw(8)
-		  << static_cast<float>(i->second.tot_states) / i->second.n
+		  << (static_cast<float>(i->second.tot_prefix_states)
+		      / i->second.n)
 		  << " "
-		  << std::setw(6) << i->second.max_states
+		  << std::setw(6) << i->second.max_prefix_states
 		  << " |"
-		  << std::setw(6) << i->second.tot_states
+		  << std::setw(6) << i->second.tot_prefix_states
+		  << " |"
+		  << std::setw(4) << i->second.n
+		  << std::endl;
+      std::cout << std::setw(22) << ""
+		<< " | (non unique) states for cycle |"
+		<< std::endl << std::setw(22) << "algorithm"
+		<< " |   min   < mean  < max | total |  n"
+		<< std::endl
+		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
+		<< std::endl;
+      for (ars_stats_type::const_iterator i = ars_stats.begin();
+	   i != ars_stats.end(); ++i)
+	std::cout << std::setw(22) << i->first << " |"
+		  << std::setw(6) << i->second.min_cycle_states
+		  << " "
+		  << std::setw(8)
+		  << (static_cast<float>(i->second.tot_cycle_states)
+		      / i->second.n)
+		  << " "
+		  << std::setw(6) << i->second.max_cycle_states
+		  << " |"
+		  << std::setw(6) << i->second.tot_cycle_states
 		  << " |"
 		  << std::setw(4) << i->second.n
 		  << std::endl;