From f965894a7fb7af8c461383f6efe715a883dc529a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 22 Nov 2004 17:41:38 +0000
Subject: [PATCH] * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
 couvreur99_check_shy::check): Compute more statistics for randtgba.
 (couvreur99_check::print_stats): Print these here too.

---
 ChangeLog                  |  5 +++++
 src/tgbaalgos/gtec/gtec.cc | 30 +++++++++++++++++++++++-------
 2 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 1cc9f3b7c..6d7feead7 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,10 @@
 2004-11-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
+	couvreur99_check_shy::check): Compute more statistics for
+	randtgba.
+	(couvreur99_check::print_stats): Print these here too.
+
 	* src/sanity/style.test: Allow "'" after ",".
 
 	* src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly
diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc
index 01de5b7fe..5f04112ff 100644
--- a/src/tgbaalgos/gtec/gtec.cc
+++ b/src/tgbaalgos/gtec/gtec.cc
@@ -63,6 +63,8 @@ namespace spot
 	// Remove each destination of this iterator.
 	for (i->first(); !i->done(); i->next())
 	  {
+	    inc_transitions();
+
 	    state* s = i->current_state();
 	    numbered_state_heap::state_index_p spi = ecs_->h->index(s);
 
@@ -116,6 +118,7 @@ namespace spot
       tgba_succ_iterator* iter = ecs_->aut->succ_iter(init);
       iter->first();
       todo.push(pair_state_iter(init, iter));
+      inc_depth();
     }
 
     while (!todo.empty())
@@ -133,6 +136,7 @@ namespace spot
 
 	    // Backtrack TODO.
 	    todo.pop();
+	    dec_depth();
 
 	    // When backtracking the root of an SCC, we must also
 	    // remove that SCC from the ARC/ROOT stacks.  We must
@@ -153,9 +157,10 @@ namespace spot
 	    continue;
 	  }
 
-	// We have a successor to look at.  Fetch the values
-	// (destination state, acceptance conditions of the arc)
-	// we are interested in...
+	// We have a successor to look at.
+	inc_transitions();
+	// Fetch the values (destination state, acceptance conditions
+	// of the arc) we are interested in...
 	const state* dest = succ->current_state();
 	bdd acc = succ->current_acceptance_conditions();
 	// ... and point the iterator to the next successor, for
@@ -175,6 +180,7 @@ namespace spot
 	    tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest);
 	    iter->first();
 	    todo.push(pair_state_iter(dest, iter));
+	    inc_depth();
 	    continue;
 	  }
 
@@ -220,12 +226,14 @@ namespace spot
 	      {
 		delete todo.top().second;
 		todo.pop();
+		dec_depth();
 	      }
             set_states(ecs_->states());
 	    return new couvreur99_check_result(ecs_);
 	  }
       }
     // This automaton recognizes no word.
+    set_states(ecs_->states());
     return 0;
   }
 
@@ -239,6 +247,8 @@ namespace spot
   couvreur99_check::print_stats(std::ostream& os) const
   {
     ecs_->print_stats(os);
+    os << transitions() << " transitions explored" << std::endl;
+    os << max_depth() << " items max in DFS search stack" << std::endl;
     return os;
   }
 
@@ -251,6 +261,7 @@ namespace spot
   {
     // Setup depth-first search from the initial state.
     todo.push(pair_state_successors(0, succ_queue()));
+    inc_depth();
     todo.top().second.push_front(successor(bddtrue,
 					   ecs_->aut->get_init_state()));
   }
@@ -262,7 +273,6 @@ namespace spot
   emptiness_check_result*
   couvreur99_check_shy::check()
   {
-
     for (;;)
       {
 	assert(ecs_->root.size() == arc.size());
@@ -344,6 +354,7 @@ namespace spot
 			      delete q->s;
 			  }
 			todo.pop();
+			dec_depth();
 		      }
                     set_states(ecs_->states());
 		    return new couvreur99_check_result(ecs_);
@@ -362,9 +373,13 @@ namespace spot
 	    const state* curr = todo.top().first;
 	    // Backtrack TODO.
 	    todo.pop();
+	    dec_depth();
 	    if (todo.empty())
-	      // This automaton recognizes no word.
-	      return 0;
+	      {
+		// This automaton recognizes no word.
+		set_states(ecs_->states());
+		return 0;
+	      }
 
 	    // When backtracking the root of an SCC, we must also
 	    // remove that SCC from the ARC/ROOT stacks.  We must
@@ -393,9 +408,10 @@ namespace spot
 	ecs_->root.push(num);
 	arc.push(succ.acc);
 	todo.push(pair_state_successors(succ.s, succ_queue()));
+	inc_depth();
 	succ_queue& new_queue = todo.top().second;
 	tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
-	for (iter->first(); !iter->done(); iter->next())
+	for (iter->first(); !iter->done(); iter->next(), inc_transitions())
 	  new_queue.push_back(successor(iter->current_acceptance_conditions(),
 					iter->current_state()));
 	delete iter;