* src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc

(couvreur99_check_shy::couvreur99_check_shy): Add the group option,
and redefine todo as a list so it can be iterated over.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce
couvreur99_shy- (for group=false) in addition to couvreur99_shy
(for group=true).
* iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi,
couvreur99_check_ssp_shy): Use group=true;

ChangeLog

@@ -1,5 +1,14 @@
 2004-12-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
+	(couvreur99_check_shy::couvreur99_check_shy): Add the group option,
+	and redefine todo as a list so it can be iterated over.
+	* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce
+	couvreur99_shy- (for group=false) in addition to couvreur99_shy
+	(for group=true).
+	* iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi,
+	couvreur99_check_ssp_shy): Use group=true;
+
 	* src/tgbaalgos/randomgraph.cc (random_graph): Do not use the
 	pointer of the state created as keys in sets; otherwise the graph
 	created depends on the memory layout.

iface/gspn/ssp.cc

@@ -900,6 +900,7 @@ namespace spot
   public:
     couvreur99_check_shy_ssp(const tgba* a)
       : couvreur99_check_shy(a,
+			     true,
 			     numbered_state_heap_ssp_factory_semi::instance())
     {
     }
@@ -944,7 +945,7 @@ namespace spot
 			{
 			  State* succ_tgba_ = 0;
 			  size_t size_tgba_ = 0;
-			  succ_queue& queue = todo.top().second;
+			  succ_queue& queue = todo.back().second;
 
 			  Diff_succ(old_state->left(), new_state->left(),
 				    &succ_tgba_, &size_tgba_);
@@ -991,6 +992,7 @@ namespace spot
     return
       new couvreur99_check_shy
       (ssp_automata,
+       true,
        numbered_state_heap_ssp_factory_semi::instance());
   }
 

src/tgbaalgos/gtec/gtec.cc

@@ -256,14 +256,15 @@ namespace spot
   //////////////////////////////////////////////////////////////////////
 
   couvreur99_check_shy::couvreur99_check_shy(const tgba* a,
+					     bool group,
 					     const numbered_state_heap_factory*
 					     nshf)
-    : couvreur99_check(a, nshf), num(1)
+    : couvreur99_check(a, nshf), num(1), group_(group)
   {
     // Setup depth-first search from the initial state.
-    todo.push(pair_state_successors(0, succ_queue()));
+    todo.push_back(pair_state_successors(0, succ_queue()));
     inc_depth();
-    todo.top().second.push_front(successor(bddtrue,
+    todo.back().second.push_front(successor(bddtrue,
 					   ecs_->aut->get_init_state()));
   }
 
@@ -279,7 +280,7 @@ namespace spot
 	assert(ecs_->root.size() == arc.size());
 
 	// Get the successors of the current state.
-	succ_queue& queue = todo.top().second;
+	succ_queue& queue = todo.back().second;
 
 	// First, we process all successors that we have already seen.
 	// This is an idea from Soheib Baarir.  It helps to merge SCCs
@@ -342,7 +343,7 @@ namespace spot
 		    // unless they are used as keys in H.
 		    while (!todo.empty())
 		      {
-			succ_queue& queue = todo.top().second;
+			succ_queue& queue = todo.back().second;
 			for (succ_queue::iterator q = queue.begin();
 			     q != queue.end(); ++q)
 			  {
@@ -354,7 +355,7 @@ namespace spot
 			    if (spi.first == 0)
 			      delete q->s;
 			  }
-			todo.pop();
+			todo.pop_back();
 			dec_depth();
 		      }
                     set_states(ecs_->states());
@@ -367,13 +368,33 @@ namespace spot
 	    queue.erase(old);
 	  }
 
+	// Group the pending successors of formed SCC of requested.
+	if (group_ && todo.back().first != 0)
+	  {
+	    int top_index = *ecs_->h->index(todo.back().first).second;
+	    if (ecs_->root.top().index < top_index)
+	      {
+		do
+		  {
+		    todo_list::reverse_iterator prev = todo.rbegin();
+		    todo_list::reverse_iterator last = prev++;
+		    prev->second.splice(prev->second.end(), last->second);
+		    todo.pop_back();
+		    dec_depth();
+		    top_index = *ecs_->h->index(todo.back().first).second;
+		  }
+		while (ecs_->root.top().index < top_index);
+		continue;
+	      }
+	  }
+
 	// If there is no more successor, backtrack.
 	if (queue.empty())
 	  {
 	    // We have explored all successors of state CURR.
-	    const state* curr = todo.top().first;
+	    const state* curr = todo.back().first;
 	    // Backtrack TODO.
-	    todo.pop();
+	    todo.pop_back();
 	    dec_depth();
 	    if (todo.empty())
 	      {
@@ -408,9 +429,9 @@ namespace spot
 	ecs_->h->insert(succ.s, ++num);
 	ecs_->root.push(num);
 	arc.push(succ.acc);
-	todo.push(pair_state_successors(succ.s, succ_queue()));
+	todo.push_back(pair_state_successors(succ.s, succ_queue()));
 	inc_depth();
-	succ_queue& new_queue = todo.top().second;
+	succ_queue& new_queue = todo.back().second;
 	tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
 	for (iter->first(); !iter->done(); iter->next(), inc_transitions())
 	  new_queue.push_back(successor(iter->current_acceptance_conditions(),

src/tgbaalgos/gtec/gtec.hh

@@ -108,11 +108,17 @@ namespace spot
   /// \brief A version of spot::couvreur99_check that tries to visit
   /// known states first.
   ///
+  /// If \a group is true (the default), the successors of all the
+  /// states that belong to the same SCC will be considered when
+  /// choosing a successor.  Otherwise, only the successor of the
+  /// topmost state on the DFS stack are considered.
+  ///
   /// See the documentation for spot::couvreur99_check
   class couvreur99_check_shy : public couvreur99_check
   {
   public:
     couvreur99_check_shy(const tgba* a,
+			 bool group = true,
 			 const numbered_state_heap_factory* nshf
 			 = numbered_state_heap_hash_map_factory::instance());
     virtual ~couvreur99_check_shy();
@@ -140,7 +146,12 @@ namespace spot
     //   (ACCEPTANCE_CONDITIONS, STATE) pairs.
     typedef std::list<successor> succ_queue;
     typedef std::pair<const state*, succ_queue> pair_state_successors;
-    std::stack<pair_state_successors> todo;
+    typedef std::list<pair_state_successors> todo_list;
+    todo_list todo;
+
+    // Whether successors should be grouped for states in the same
+    // SCC.
+    bool group_;
 
     /// \brief find the SCC number of a unprocessed state.
     ///

src/tgbatest/ltl2tgba.cc

@@ -122,6 +122,7 @@ syntax(char* prog)
 	    << std::endl
 	    << "Where ALGO should be one of:" << std::endl
 	    << "  couvreur99 (the default)" << std::endl
+	    << "  couvreur99_shy-" << std::endl
 	    << "  couvreur99_shy" << std::endl
 	    << "  magic_search" << std::endl
 	    << "  magic_search_repeated" << std::endl
@@ -159,6 +160,7 @@ main(int argc, char** argv)
   enum { None, Couvreur, Couvreur2, MagicSearch, Se05Search,
 	 Tau03Search, Tau03OptSearch, Gv04 } echeck = None;
   enum { NoneDup, BFS, DFS } dupexp = NoneDup;
+  bool couv_group = true;
   bool search_many = false;
   bool bit_state_hashing = false;
   int heap_size = 10*1024*1024;
@@ -381,6 +383,12 @@ main(int argc, char** argv)
       else if (echeck_algo == "couvreur99_shy")
 	{
 	  echeck = Couvreur2;
+	  couv_group = true;
+	}
+      else if (echeck_algo == "couvreur99_shy-")
+	{
+	  echeck = Couvreur2;
+	  couv_group = false;
 	}
       else if (echeck_algo == "magic_search")
 	{
@@ -670,7 +678,7 @@ main(int argc, char** argv)
 	  break;
 
 	case Couvreur2:
-	  ec = new spot::couvreur99_check_shy(a);
+	  ec = new spot::couvreur99_check_shy(a, couv_group);
 	  break;
 
         case MagicSearch:

src/tgbatest/randtgba.cc

@@ -59,6 +59,12 @@ couvreur99_shy_cons(const spot::tgba* a)
   return new spot::couvreur99_check_shy(a);
 }
 
+spot::emptiness_check*
+couvreur99_shy_minus_cons(const spot::tgba* a)
+{
+  return new spot::couvreur99_check_shy(a, false);
+}
+
 spot::emptiness_check*
 bsh_ms_cons(const spot::tgba* a)
 {
@@ -82,6 +88,7 @@ struct ec_algo
 ec_algo ec_algos[] =
   {
     { "couvreur99",            couvreur99_cons,                 0, -1U, true },
+    { "couvreur99_shy-",       couvreur99_shy_minus_cons,       0, -1U, true },
     { "couvreur99_shy",        couvreur99_shy_cons,             0, -1U, true },
     { "explicit_magic_search", spot::explicit_magic_search,     0,   1, true },
     { "bit_state_hashing_magic_search",