From 5af687b2c8cce1ca21c2bf3b3f6ce93620affa19 Mon Sep 17 00:00:00 2001
From: martinez <martinez>
Date: Mon, 13 Sep 2004 15:25:13 +0000
Subject: [PATCH] * src/tgbatest/spotlbtt.test, src/tgbatest/reductgba.cc,
 src/tgbatest/ltl2tgba.cc: Add option for reduction of TGBA.

* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc,
src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
Remove some bugs.

src/tgbaalgos/gtec/ce.cc:
Modification of construction of counter example.

* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim_del.cc,
src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
Modification for delayed simulation.


* src/tgbaalgos/gtec/ce.hh,
* src/tgbatest/ltl2tgba.cc,
---
 ChangeLog                          |  27 ++-
 src/ltltest/reduc.test             |   5 +-
 src/tgba/tgbareduc.cc              |  97 ++++++---
 src/tgba/tgbareduc.hh              |  27 ++-
 src/tgbaalgos/Makefile.am          |   2 +
 src/tgbaalgos/colordfs.cc          | 223 +++++++++++++++++----
 src/tgbaalgos/colordfs.hh          |   3 +
 src/tgbaalgos/gtec/ce.cc           |  41 ++--
 src/tgbaalgos/minimalce.cc         | 266 ++++++++++++++++++++-----
 src/tgbaalgos/minimalce.hh         |  21 +-
 src/tgbaalgos/nesteddfs.cc         |  75 ++-----
 src/tgbaalgos/nesteddfs.hh         |   8 +-
 src/tgbaalgos/reductgba_sim.cc     |  24 +--
 src/tgbaalgos/reductgba_sim.hh     |  34 ++--
 src/tgbaalgos/reductgba_sim_del.cc |  45 ++++-
 src/tgbaalgos/tarjan_on_fly.cc     |  76 ++------
 src/tgbaalgos/tarjan_on_fly.hh     |   2 +-
 src/tgbatest/emptchk.test          |  16 +-
 src/tgbatest/ltl2tgba.cc           | 303 +++++++++++++++++++----------
 src/tgbatest/reductgba.cc          |  48 +++--
 src/tgbatest/spotlbtt.test         |   6 +-
 21 files changed, 931 insertions(+), 418 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 4b72521c4..6bacd07b3 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,26 @@
+2004-09-13  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* src/tgbatest/spotlbtt.test,
+	src/tgbatest/reductgba.cc,
+	src/tgbatest/ltl2tgba.cc:
+	Add option for reduction of TGBA.
+
+	* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
+	src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc,
+	src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc,
+	src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc,
+	src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
+	Remove some bugs.
+
+	src/tgbaalgos/gtec/ce.cc:
+	Modification of construction of counter example.
+
+	* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
+	src/tgbaalgos/reductgba_sim_del.cc,
+	src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
+	Modification for delayed simulation.
+
+
 2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>
 
 	* src/tgbaalgos/tarjan_on_fly.hh,
@@ -9,11 +32,11 @@
 	src/tgbaalgos/colordfs.hh,
 	src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check.
 
-	src/tgbaalgos/gtec/ce.hh,
+	* src/tgbaalgos/gtec/ce.hh,
 	src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
 	object in minimalce.hh.
 
-	src/tgbatest/ltl2tgba.cc,
+	* src/tgbatest/ltl2tgba.cc,
 	src/tgbatest/emptchk.test,
 	src/tgbaalgos/Makefile.am: Add files for emptyness-check.
 
diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test
index 858b2337f..40aff093c 100755
--- a/src/ltltest/reduc.test
+++ b/src/ltltest/reduc.test
@@ -22,11 +22,12 @@
 
 
 # Check for the reduc visitor.
-. ./defs || exit 1
+# . ./defs || exit 1
 
 set -e
 
-FICH=${1-$srcdir/formulae.txt}
+#FICH=${1-$srcdir/formulae.txt}
+FICH=${1-$srcdir/formules3.ltl}
 
 for opt in 0 1 2 3; do
   rm -f result.data
diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc
index 622ae74a7..137384a5a 100644
--- a/src/tgba/tgbareduc.cc
+++ b/src/tgba/tgbareduc.cc
@@ -35,7 +35,7 @@ namespace spot
       tgba_reachable_iterator_breadth_first(a),
       h_(nshf->build())
   {
-    dict_->register_all_variables_of(a, this); // useful ??
+    dict_->register_all_variables_of(a, this);
 
     run();
     all_acceptance_conditions_ = a->all_acceptance_conditions();
@@ -57,12 +57,12 @@ namespace spot
   }
 
   void
-  tgba_reduc::prune_automata(simulation_relation* rel)
+  tgba_reduc::quotient_state(direct_simulation_relation* rel)
   {
-    // Remember that for each state couple (*i)->second
-    // simulate (*i)->first.
+    // Remember that for each state couple
+    // (*i)->second simulate (*i)->first.
 
-    for (simulation_relation::iterator i = rel->begin();
+    for (direct_simulation_relation::iterator i = rel->begin();
 	 i != rel->end(); ++i)
       {
 
@@ -72,28 +72,29 @@ namespace spot
 
 	// We check if the two state are co-simulate.
 	bool recip = false;
-	for (spot::simulation_relation::iterator j = i;
+	for (direct_simulation_relation::iterator j = i;
 	     j != rel->end(); ++j)
 	  if ((((*i)->first)->compare((*j)->second) == 0) &&
 	      (((*j)->first)->compare((*i)->second) == 0))
 	    recip = true;
 
-	if (!recip)
-	    this->redirect_transition((*i)->first, (*i)->second);
-	else
-	    this->merge_state((*i)->first, (*i)->second);
+	if (recip)
+	  //this->redirect_transition((*i)->first, (*i)->second);
+	  this->merge_state((*i)->first, (*i)->second);
       }
 
     this->merge_transitions();
   }
 
   void
-  tgba_reduc::quotient_state(simulation_relation* rel)
+  tgba_reduc::quotient_state(delayed_simulation_relation* rel)
   {
-    // Remember that for each state couple (*i)->second
-    // simulate (*i)->first.
+    if (nb_set_acc_cond() > 1)
+      return;
 
-    for (simulation_relation::iterator i = rel->begin();
+    //this->quotient_state(rel);
+
+    for (delayed_simulation_relation::iterator i = rel->begin();
 	 i != rel->end(); ++i)
       {
 
@@ -103,7 +104,7 @@ namespace spot
 
 	// We check if the two state are co-simulate.
 	bool recip = false;
-	for (spot::simulation_relation::iterator j = i;
+	for (delayed_simulation_relation::iterator j = i;
 	     j != rel->end(); ++j)
 	  if ((((*i)->first)->compare((*j)->second) == 0) &&
 	      (((*j)->first)->compare((*i)->second) == 0))
@@ -116,6 +117,19 @@ namespace spot
     this->merge_transitions();
   }
 
+  void
+  tgba_reduc::delete_transitions(simulation_relation* rel)
+  {
+    for (simulation_relation::iterator i = rel->begin();
+	 i != rel->end(); ++i)
+      {
+	if (((*i)->first)->compare((*i)->second) == 0)
+	  continue;
+	this->redirect_transition((*i)->first, (*i)->second);
+      }
+    this->merge_transitions();
+  }
+
   void
   tgba_reduc::prune_scc()
   {
@@ -146,6 +160,7 @@ namespace spot
   }
 
   ////////////////////////////////////////////
+  // for build tgba_reduc
 
   void
   tgba_reduc::start()
@@ -430,10 +445,12 @@ namespace spot
   tgba_reduc::merge_state_delayed(const spot::state*,
 				  const spot::state*)
   {
+    // TO DO
   }
 
   /////////////////////////////////////////
   /////////////////////////////////////////
+  // Compute SCC
 
   // From gtec.cc
   void
@@ -604,24 +621,24 @@ namespace spot
 		 i != s1->end(); ++i)
 	      (*i)->acceptance_conditions = bddfalse;
 	  }
-	else
+	/*
+	  else
 	  {
-	    // FIXME
-	    /*
-	      tgba_succ_iterator* si = this->succ_iter(sm->first);
-	      spot::state* s2 = si->current_state();
-	      seen_map::iterator sm2 = si_.find(s2);
-	      if (sm2->second == n)
-	      {
-	      s1 = name_state_map_[tgba_explicit::format_state(sm2->first)];
-	      for (state::iterator i = s1->begin();
-	      i != s1->end(); ++i)
-	      (*i)->acceptance_conditions = bddfalse;
-	      }
-	      delete s2;
-	      delete si;
-	    */
+	  // FIXME
+	  tgba_succ_iterator* si = this->succ_iter(sm->first);
+	  spot::state* s2 = si->current_state();
+	  seen_map::iterator sm2 = si_.find(s2);
+	  if (sm2->second == n)
+	  {
+	  s1 = name_state_map_[tgba_explicit::format_state(sm2->first)];
+	  for (state::iterator i = s1->begin();
+	  i != s1->end(); ++i)
+	  (*i)->acceptance_conditions = bddfalse;
 	  }
+	  delete s2;
+	  delete si;
+	  }
+	*/
 
       }
   }
@@ -825,6 +842,7 @@ namespace spot
 
   }
 
+  /*
   void
   tgba_reduc::remove_scc_depth_first(spot::state* s, int n)
   {
@@ -853,7 +871,9 @@ namespace spot
 	seen_ = 0;
       }
   }
+  */
 
+  /*
   bool
   tgba_reduc::is_alpha_ball(const spot::state* s, bdd label, int n)
   {
@@ -909,6 +929,21 @@ namespace spot
 
     return ret;
   }
+  */
+
+  int
+  tgba_reduc::nb_set_acc_cond() const
+  {
+    bdd acc, all;
+    acc = all = this->all_acceptance_conditions();
+    int count = 0;
+    while (all != bddfalse)
+      {
+	all -= bdd_satone(all);
+	count++;
+      }
+    return count;
+  }
 
   //////// JUST FOR DEBUG //////////
 
diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh
index 91b4a4482..29b6b557a 100644
--- a/src/tgba/tgbareduc.hh
+++ b/src/tgba/tgbareduc.hh
@@ -34,6 +34,15 @@ namespace spot
   typedef Sgi::pair<const spot::state*, const spot::state*> state_couple;
   typedef Sgi::vector<state_couple*> simulation_relation;
 
+  /*
+    typedef Sgi::vector<state_couple*> direct_simulation_relation;
+    typedef Sgi::vector<state_couple*> delayed_simulation_relation;
+  */
+
+  class direct_simulation_relation : public simulation_relation{};
+  class delayed_simulation_relation : public simulation_relation{};
+
+
   class tgba_reduc: public tgba_explicit,
 		    public tgba_reachable_iterator_breadth_first
   {
@@ -46,11 +55,15 @@ namespace spot
 
     /// Reduce the automata using a relation simulation
     /// Do not call this method with a delayed simulation relation.
-    void prune_automata(simulation_relation* rel);
+    void quotient_state(direct_simulation_relation* rel);
 
     /// Build the quotient automata. Call this method
     /// when use to a delayed simulation relation.
-    void quotient_state(simulation_relation* rel);
+    void quotient_state(delayed_simulation_relation* rel);
+
+    /// \brief Delete some transitions with help of a simulation
+    /// relation.
+    void delete_transitions(simulation_relation* rel);
 
     /// Remove all state which not lead to an accepting cycle.
     void prune_scc();
@@ -144,9 +157,9 @@ namespace spot
     ///  publisher	= {Springer-Verlag}
     /// }
     /// \endverbatim
-    bool is_alpha_ball(const spot::state* s,
-		       bdd label = bddfalse,
-		       int n = -1);
+    // bool is_alpha_ball(const spot::state* s,
+    // bdd label = bddfalse,
+    // int n = -1);
 
     // Return true if we can't reach a state with
     // an other value of scc.
@@ -165,11 +178,13 @@ namespace spot
     void remove_scc(spot::state* s);
 
     /// Same as remove_scc but more efficient.
-    void remove_scc_depth_first(spot::state* s, int n = -1);
+    // void remove_scc_depth_first(spot::state* s, int n = -1);
 
     /// For compute_scc.
     void remove_component(const spot::state* from);
 
+    int tgba_reduc::nb_set_acc_cond() const;
+
   };
 }
 
diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index 518c968ae..49b1b0ff4 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -36,6 +36,7 @@ tgbaalgos_HEADERS = \
   magic.hh \
   minimalce.hh \
   nesteddfs.hh \
+  nesteddfsgen.hh \
   neverclaim.hh \
   powerset.hh \
   reachiter.hh \
@@ -55,6 +56,7 @@ libtgbaalgos_la_SOURCES = \
   magic.cc \
   minimalce.cc \
   nesteddfs.cc \
+  nesteddfsgen.cc \
   neverclaim.cc \
   powerset.cc \
   reachiter.cc \
diff --git a/src/tgbaalgos/colordfs.cc b/src/tgbaalgos/colordfs.cc
index 83ef8f6d0..e953640c5 100644
--- a/src/tgbaalgos/colordfs.cc
+++ b/src/tgbaalgos/colordfs.cc
@@ -30,6 +30,7 @@ namespace spot
   colordfs_search::colordfs_search(const tgba_tba_proxy* a)
     : a(a), x(0), counter_(0)
   {
+    Maxdepth = -1;
   }
 
   colordfs_search::~colordfs_search()
@@ -111,9 +112,7 @@ namespace spot
     int n = 0;
     for (i->first(); !i->done(); i->next(), n++)
       {
-	//std::cout << "iter : " << n << std::endl;
 	s2 = i->current_state();
-	//std::cout << a->format_state(s2) << std::endl;
 	hi = h.find(s2);
 	if (hi != h.end())
 	  return_value &= (hi->second.c == black);
@@ -123,8 +122,6 @@ namespace spot
       }
     delete i;
 
-    //std::cout << "End Loop" << std::endl;
-
     hi = h.find(s);
     assert(hi != h.end());
     if (return_value)
@@ -138,8 +135,8 @@ namespace spot
   {
     clock();
     counter_ = new ce::counter_example(a);
-    const state* s = a->get_init_state();
-    if (dfs_blue(s))
+    const state *s = a->get_init_state();
+    if (dfs_blue_min(s))
       counter_->build_cycle(x);
     else
       {
@@ -154,49 +151,60 @@ namespace spot
   bool
   colordfs_search::dfs_blue(const state* s, bdd)
   {
-    //std::cout << "dfs_blue : " << a->format_state(s) << std::endl;
-    if (!push(s, blue))
-      return false;
+    std::cout << "dfs_blue : " << std::endl;
 
-    hash_type::iterator hi;
-    tgba_succ_iterator* i = a->succ_iter(s);
-    int n = 0;
-    for (i->first(); !i->done(); i->next(), n++)
+    if (stack.empty())
+      // It's a new search.
+      push(a->get_init_state(), blue);
+    else
+      tstack.pop_front();
+
+    while (!stack.empty())
       {
-	const state* s2 = i->current_state();
-	//std::cout << "s2 : " << a->format_state(s2) << std::endl;
-	hi = h.find(s2);
-	if (a->state_is_accepting(s2) &&
-	    (hi != h.end() && hi->second.is_in_cp))
+      recurse:
+	tgba_succ_iterator *i = stack.front().second;
+	hash_type::iterator hi;
+
+	//std::cout << a->format_state(p.first) << std::endl;
+	while (!i->done())
 	  {
-	    ce::state_ce ce;
-	    ce = ce::state_ce(s2, i->current_condition());
-	    x = const_cast<state*>(s2);
-	    delete i;
-	    return true;// a counter example is found !!
-	  }
-	else if (hi == h.end() || hi->second.c == white)
-	  {
-	    int res = dfs_blue(s2, i->current_acceptance_conditions());
-	    if (res == 1)
+	    const state* s2 = i->current_state();
+	    hi = h.find(s2);
+	    if (a->state_is_accepting(s2) &&
+		(hi != h.end() && hi->second.is_in_cp))
 	      {
-		delete i;
-		return true;
+		//ce::state_ce ce;
+		//ce = ce::state_ce(s2, i->current_condition());
+		x = const_cast<state*>(s2);
+		//push(s2, blue); //
+		//delete i;
+		return true;// a counter example is found !!
 	      }
+	    else if (hi == h.end() || hi->second.c == white)
+	      {
+		push(s2, blue);
+		goto recurse;
+	      }
+	    else
+	      delete s2;
+	    i->next();
 	  }
-	else
-	  delete s2; // FIXME
-      }
-    delete i;
 
-    pop();
+	s = stack.front().first;
+	pop();
 
-    if (!all_succ_black(s) &&
-	a->state_is_accepting(s))
-      {
-	if (dfs_red(s))
-	  return 1;
-	dfs_black(s);
+	if (!all_succ_black(s) &&
+	    a->state_is_accepting(s))
+	  {
+	    if (dfs_red(s))
+	      return true;
+
+	    hash_type::iterator hi = h.find(s);
+	    assert(hi == h.end());
+	    hi->second.c = black;
+	  }
+
+	delete s; //
       }
 
     return false;
@@ -205,7 +213,7 @@ namespace spot
   bool
   colordfs_search::dfs_red(const state* s)
   {
-    //std::cout << "dfs_red : " << a->format_state(s) << std::endl;
+    std::cout << "dfs_red : " << a->format_state(s) << std::endl;
     if (!push(s, red))
       return false;
 
@@ -240,12 +248,143 @@ namespace spot
       }
     delete i;
 
+    hi = h.find(s);
+    assert(hi == h.end());
+    hi->second.c = black;
     //std::cout << "dfs_red : pop" << std::endl;
     pop();
 
     return false;
   }
 
+  ///////////////////////////////////////////////////////////////////////
+  // for minimisation
+
+  bool
+  colordfs_search::dfs_blue_min(const state* s, bdd)
+  {
+    //std::cout << "dfs_blue : " << a->format_state(s) << std::endl;
+    if (!push(s, blue))
+      return false;
+
+    hash_type::iterator hi = h.find(s);
+    if (hi != h.end())
+      {
+	if (((int)stack.size() + 1) < hi->second.depth)
+	  hi->second.depth = stack.size(); // for minimize
+      }
+    else
+      {
+	assert(0);
+      }
+
+    if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth))
+      {
+	tgba_succ_iterator* i = a->succ_iter(s);
+	int n = 0;
+	for (i->first(); !i->done(); i->next(), n++)
+	  {
+	    const state* s2 = i->current_state();
+	    //std::cout << "s2 : " << a->format_state(s2) << std::endl;
+	    hi = h.find(s2);
+
+	    if (a->state_is_accepting(s2) &&
+		(hi != h.end() && hi->second.is_in_cp))
+	      {
+		Maxdepth = stack.size();
+		ce::state_ce ce;
+		ce = ce::state_ce(s2, i->current_condition());
+		x = const_cast<state*>(s2);
+		delete i;
+		return true;// a counter example is found !!
+	      }
+	    else if (hi == h.end() || hi->second.c == white)
+	      {
+		int res = dfs_blue_min(s2, i->current_acceptance_conditions());
+		if (res == 1)
+		  {
+		    delete i;
+		    return true;
+		  }
+	      }
+	    else
+	      delete s2; // FIXME
+	  }
+	delete i;
+
+
+	pop();
+
+	if (!all_succ_black(s) &&
+	    a->state_is_accepting(s))
+	  {
+	    if (dfs_red_min(s))
+	      return 1;
+	    dfs_black(s);
+	  }
+      }
+
+    return false;
+  }
+
+  bool
+  colordfs_search::dfs_red_min(const state* s)
+  {
+    //std::cout << "dfs_red : " << a->format_state(s) << std::endl;
+    if (!push(s, red))
+      return false;
+
+    hash_type::iterator hi = h.find(s);
+    if (hi != h.end())
+      {
+	if (((int)stack.size() + 1) < hi->second.depth)
+	  hi->second.depth = stack.size(); // for minimize
+      }
+    else
+      assert(0);
+
+    if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth))
+      {
+	tgba_succ_iterator* i = a->succ_iter(s);
+	int n = 0;
+	for (i->first(); !i->done(); i->next(), n++)
+	  {
+	    const state* s2 = i->current_state();
+	    hi = h.find(s2);
+	    if (hi != h.end() && hi->second.is_in_cp &&
+		(a->state_is_accepting(s2) ||
+		 (hi->second.c == blue)))
+	      {
+		Maxdepth = stack.size();
+		ce::state_ce ce;
+		ce = ce::state_ce(s2->clone(), i->current_condition());
+		x = const_cast<state*>(s2);
+		delete i;
+		return true;// a counter example is found !!
+	      }
+	    if (hi != h.end() &&
+		(hi->second.c == blue))
+	      // || ((int)stack.size() + 1) < hi->second.depth))
+	      {
+		delete s2; // FIXME
+		if (dfs_red_min(hi->first))
+		  {
+		    delete i;
+		    return true;
+		  }
+	      }
+	    else
+	      delete s2;
+	  }
+	delete i;
+
+	//std::cout << "dfs_red : pop" << std::endl;
+	pop();
+      }
+    return false;
+  }
+
+
   void
   colordfs_search::dfs_black(const state* s)
   {
diff --git a/src/tgbaalgos/colordfs.hh b/src/tgbaalgos/colordfs.hh
index a7fa97aac..c748c9409 100644
--- a/src/tgbaalgos/colordfs.hh
+++ b/src/tgbaalgos/colordfs.hh
@@ -97,6 +97,8 @@ namespace spot
     /// Pages = "92-108")
     bool dfs_blue(const state* s, bdd acc = bddfalse);
     bool dfs_red(const state* s);
+    bool dfs_blue_min(const state* s, bdd acc = bddfalse);
+    bool dfs_red_min(const state* s);
     void dfs_black(const state* s);
 
     /// Append a new state to the current path.
@@ -110,6 +112,7 @@ namespace spot
     const tgba_tba_proxy* a;	///< The automata to check.
     /// The state for which we are currently seeking an SCC.
     const state* x;
+    int Maxdepth; ///< The size of the current counter example.
 
     ce::counter_example* counter_;
     clock_t tps_;
diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc
index ede0507da..0f6961636 100644
--- a/src/tgbaalgos/gtec/ce.cc
+++ b/src/tgbaalgos/gtec/ce.cc
@@ -35,7 +35,10 @@ namespace spot
 				   eccf)
     : ecs_(ecs)
   {
-    counter_ = new ce::counter_example(ecs->aut);
+
+    std::cout << "counter_example" << std::endl;
+
+    //counter_ = new ce::counter_example(ecs->aut);
 
     assert(!ecs_->root.empty());
     assert(suffix.empty());
@@ -79,7 +82,7 @@ namespace spot
     suffix.push_front(spi.first);
 
     /////
-    counter_->prefix.push_front(ce::state_ce(spi.first->clone(), bddfalse));
+    // counter_->prefix.push_front(ce::state_ce(spi.first->clone(), bddfalse));
     ////
 
     // We build a path trough each SCC in the stack.  For the
@@ -127,14 +130,15 @@ namespace spot
 			state_sequence seq;
 
 			///
-			ce::l_state_ce seq_count;
+			// ce::l_state_ce seq_count;
 			///
 
 			seq.push_front(h_dest);
 			while (src->compare(start))
 			  {
 			    ///
-			    seq_count.push_front(ce::state_ce(src->clone(), bddfalse));
+			    // seq_count.push_front(ce::state_ce(src->clone(),
+			    // bddfalse));
 			    ///
 
 			    seq.push_front(src);
@@ -144,8 +148,8 @@ namespace spot
 			suffix.splice(suffix.end(), seq);
 
 			///
-			counter_->prefix.splice(counter_->prefix.end(),
-						seq_count);
+			// counter_->prefix.splice(counter_->prefix.end(),
+			// seq_count);
 			///
 
 			// Exit this BFS for this SCC.
@@ -186,6 +190,8 @@ namespace spot
 				  const state* from,
 				  const state* to)
   {
+    //std::cout << "complete_cycle" << std::endl;
+
     // If by change or period already ends on the state we have
     // to reach back, we are done.
     if (from == to
@@ -233,8 +239,8 @@ namespace spot
 		cycle_path p;
 
 		///
-		ce::l_state_ce p_counter;
-		p_counter.push_front(ce::state_ce(h_dest->clone(), cond));
+		// ce::l_state_ce p_counter;
+		// p_counter.push_front(ce::state_ce(h_dest->clone(), cond));
 		///
 
 		p.push_front(state_proposition(h_dest, cond));
@@ -242,15 +248,16 @@ namespace spot
 		  {
 		    const state_proposition& psi = father[src];
 		    ///
-		    p_counter.push_front(ce::state_ce(src->clone(), psi.second));
+		    // p_counter.push_front(ce::state_ce(src->clone(),
+		    // psi.second));
 		    ///
 		    p.push_front(state_proposition(src, psi.second));
 		    src = psi.first;
 		  }
 		period.splice(period.end(), p);
 		///
-		counter_->cycle.splice(counter_->cycle.end(),
-				       p_counter);
+		// counter_->cycle.splice(counter_->cycle.end(),
+		// p_counter);
 		///
 
 		// Exit the BFS, but release all iterators first.
@@ -441,6 +448,8 @@ namespace spot
   counter_example::accepting_path(const explicit_connected_component* scc,
 				  const state* start, bdd acc_to_traverse)
   {
+    //std::cout << "accepting_path" << std::endl;
+
     // State seen during the DFS.
     typedef Sgi::hash_set<const state*,
                           state_ptr_hash, state_ptr_equal> set_type;
@@ -450,6 +459,9 @@ namespace spot
 
     while (acc_to_traverse != bddfalse)
       {
+	//std::cout << "accepting_path : while (acc_to_traverse != bddfalse)"
+	// << std::endl;
+
 	// Initial state.
 	{
 	  tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
@@ -467,6 +479,9 @@ namespace spot
 
 	while (!todo.empty())
 	  {
+	    // std::cout << "accepting_path : while (!todo.empty())"
+	    // << std::endl;
+
 	    tgba_succ_iterator* iter = todo.top().iter;
 	    const state* s = todo.top().s;
 
@@ -563,8 +578,8 @@ namespace spot
 	     it != best_path.end(); ++it)
 	  {
 	    period.push_back(*it);
-	    ce::state_ce ce(it->first->clone(), it->second);
-	    counter_->cycle.push_back(ce);
+	    //ce::state_ce ce(it->first->clone(), it->second);
+	    //counter_->cycle.push_back(ce);
 	    //counter_->cycle.push_back(*it);
 	  }
 
diff --git a/src/tgbaalgos/minimalce.cc b/src/tgbaalgos/minimalce.cc
index a2453f722..f8e157370 100644
--- a/src/tgbaalgos/minimalce.cc
+++ b/src/tgbaalgos/minimalce.cc
@@ -223,14 +223,15 @@ namespace spot
   /////////////////////////////////////////////////////////////////////////////
   // minimal_search
 
-  minimalce_search::minimalce_search(const tgba_tba_proxy *a)
+  minimalce_search::minimalce_search(const tgba_tba_proxy *a,
+				     bool mode)
     : a(a), min_ce(0)
   {
+    mode_ = mode;
   }
 
   minimalce_search::~minimalce_search()
   {
-
     hash_type::const_iterator s = h_lenght.begin();
     while (s != h_lenght.end())
       {
@@ -244,11 +245,13 @@ namespace spot
 	 i != l_ce.end();)
       {
 	//std::cout << "delete a counter" << std::endl;
-	if (*i == min_ce)
+	/*
+	  if (*i == min_ce)
 	  {
-	    ++i;
-	    continue;
+	  ++i;
+	  continue;
 	  }
+	*/
 	ce::counter_example* ce = *i;
 	++i;
 	delete ce;
@@ -262,11 +265,22 @@ namespace spot
   {
     clock();
     nb_found = 0;
-    min_ce = new ce::counter_example(a);
+
+    if ((!min_ce && mode_) ||
+	!mode_)
+      min_ce = new ce::counter_example(a);
+
+    if (mode_)
+      {
+	min_ce = find();
+	tps_ = clock();
+	return min_ce;
+      }
+
     std::ostringstream os;
     const state* s = a->get_init_state();
     recurse_find(s, os);
-    std::cout << "nb_found : " << nb_found << std::endl;
+    //std::cout << "nb_found : " << nb_found << std::endl;
 
     if (min_ce->size() == 0)
       {
@@ -279,45 +293,212 @@ namespace spot
   }
 
   ce::counter_example*
-  minimalce_search::check(ce::counter_example*)
+  minimalce_search::check(ce::counter_example* ce)
   {
-    min_ce = new ce::counter_example(a);
+    min_ce = ce;
 
-    /*
-    ce::l_state_ce::iterator i;
-    int depth = 0;
-    for (i = min_ce->prefix.begin();
-	 i != min_ce->prefix.end(); ++i, ++depth)
-      {
-	stack.push_front(i->first);
-	//if (h_lenght.find(i->first) == h_lenght.end())
-	h_lenght[i->first] = depth;
-      }
-    for (i = min_ce->cycle.begin();
-	 i != min_ce->cycle.end(); ++i, ++depth)
-      {
-	stack.push_front(i->first);
-	if (h_lenght.find(i->first) == h_lenght.end())
-	  h_lenght[i->first] = depth;
-      }
-    */
-
-    const state* s = a->get_init_state();
     std::ostringstream os;
+    const state* s = a->get_init_state();
     recurse_find(s, os);
-    //if (recurse_find(s))
-    //return min_ce;
-    //else
+    //std::cout << "nb_found : " << nb_found << std::endl;
+    tps_ = clock();
     return min_ce;
   }
 
+  ce::counter_example*
+  minimalce_search::find()
+  {
+    /// FIXME
+    std::ostringstream os;
+
+    int mode = normal;
+    int depth_mode = 0;
+    int depth_mode_memory = -1;
+    const state* s = 0;
+    hash_type::iterator i;
+    tgba_succ_iterator* iter = 0;
+
+    if (!h_lenght.size())
+      {
+	// it's a new search
+	//std::cout << "it's a new search" << std::endl;
+	s = a->get_init_state();
+	i = h_lenght.find(s);
+	if (i != h_lenght.end())
+	  {
+	    delete s;
+	    s = i->first;
+	    if (((int)stack.size() + 1) < i->second)
+	      i->second = stack.size() + 1;
+	  }
+	else
+	  h_lenght[s] = stack.size();
+	iter = a->succ_iter(s);
+	iter->first();
+	stack.push_front(state_pair(s, iter));
+	depth_mode++;
+      }
+    else
+      s = stack.front().first;
+
+    while (!stack.empty())
+      {
+      recurse:
+	//std::cout << "recurse: " << a->format_state(s) << std::endl;
+	/*
+	  if (iter)
+	  delete iter;
+	*/
+
+	iter = stack.front().second;
+	while (!iter->done())
+	  {
+	    //std::cout << "iter" << std::endl;
+
+	    //stack_type::iterator j = stack.begin();
+	    //j->second = iter->current_condition();
+
+	    const state* succ = iter->current_state();
+
+	    if ((min_ce->size() == 0) ||
+		((int)stack.size() + 1 <= min_ce->size()))
+	      {
+		int depth = in_stack(succ, os);
+		if (depth != -1)
+		  {
+		    if (closes_accepting(succ, depth, os))
+		      {
+			// New counter example is found !!
+			//std::cout << "CE found !!" << std::endl;
+			save_counter(succ, os);
+
+			i = h_lenght.find(succ);
+			if (i == h_lenght.end())
+			  h_lenght[succ] = stack.size() + 1;
+			else
+			  {
+			    delete succ;
+			    if (((int)stack.size() + 1) < i->second)
+			      i->second = stack.size() + 1;
+			  }
+
+			iter->next();
+			return min_ce;
+		      }
+		    else
+		      delete succ;
+		  }
+
+		else if ((mode == careful) ||
+			 a->state_is_accepting(succ))
+		  {
+		    s = succ;
+		    iter->next();
+
+		    if (mode != careful)
+		      depth_mode_memory = depth_mode;
+		    mode = careful;
+		    hash_type::iterator i = h_lenght.find(s);
+		    if (i != h_lenght.end())
+		      {
+			delete s;
+			s = i->first;
+			if (((int)stack.size() + 1) < i->second)
+			  i->second = stack.size() + 1;
+		      }
+		    else
+		      h_lenght[s] = stack.size();
+
+		    iter = a->succ_iter(s);
+		    iter->first();
+		    stack.push_front(state_pair(s, iter));
+		    depth_mode++;
+		    goto recurse;
+		  }
+
+		else if (h_lenght.find(succ) == h_lenght.end())
+		  {
+		    s = succ;
+		    iter->next();
+
+		    hash_type::iterator i = h_lenght.find(s);
+		    if (i != h_lenght.end())
+		      {
+			delete s;
+			s = i->first;
+			if (((int)stack.size() + 1) < i->second)
+			  i->second = stack.size() + 1;
+		      }
+		    else
+		      h_lenght[s] = stack.size();
+
+		    iter = a->succ_iter(s);
+		    iter->first();
+		    stack.push_front(state_pair(s, iter));
+		    depth_mode++;
+		    goto recurse;
+		  }
+
+		else if ((h_lenght[succ] > (int)stack.size() + 1) &&
+			 (min_ce->size() != 0))
+		  {
+		    s = succ;
+		    iter->next();
+
+		    if (mode != careful)
+		      depth_mode_memory = depth_mode;
+		    mode = careful;
+		    hash_type::iterator i = h_lenght.find(s);
+		    if (i != h_lenght.end())
+		      {
+			delete s;
+			s = i->first;
+			if (((int)stack.size() + 1) < i->second)
+			  i->second = stack.size() + 1;
+		      }
+		    else
+		      h_lenght[s] = stack.size();
+
+		    iter = a->succ_iter(s);
+		    iter->first();
+		    stack.push_front(state_pair(s, iter));
+		    depth_mode++;
+		    goto recurse;
+		  }
+		else
+		  delete succ;
+	      }
+	    else
+	      delete succ;
+
+	    iter->next();
+	  }
+
+	delete iter;
+
+	depth_mode--;
+	if (depth_mode_memory == depth_mode)
+	  {
+	    depth_mode_memory = -1;
+	    mode = normal;
+	  }
+
+	stack.pop_front();
+	s = stack.front().first;
+      }
+
+    return 0;
+  }
+
   void
   minimalce_search::recurse_find(const state* s,
 				 std::ostringstream& os,
 				 int mode)
   {
+    /*
     std::cout << os.str() << "recurse find : "
 	      << a->format_state(s) << std::endl;
+    */
 
     hash_type::iterator i = h_lenght.find(s);
     if (i != h_lenght.end())
@@ -328,22 +509,20 @@ namespace spot
 	  i->second = stack.size() + 1;
       }
     else
-      h_lenght[s] = stack.size();
+      h_lenght[s] = stack.size() + 1;
 
-    stack.push_front(state_pair(s, bddfalse));
-    //stack.push_front(s);
+    //stack.push_front(state_pair(s, bddfalse));
 
     tgba_succ_iterator* iter = a->succ_iter(s);
+    stack.push_front(state_pair(s, iter));
     iter->first();
     while (!iter->done())
       {
-	stack_type::iterator j = stack.begin();
-	j->second = iter->current_condition();
+	//stack_type::iterator j = stack.begin();
+	//j->second = iter->current_condition();
 
 	const state* succ = iter->current_state();
 
-	std::cout << "stack.size() +1: " << (int)stack.size() + 1
-		  << "min_ce->size() : " << min_ce->size()<< std::endl;
 	if ((min_ce->size() == 0) ||
 	    ((int)stack.size() + 1 <= min_ce->size()))
 	  {
@@ -479,9 +658,7 @@ namespace spot
     //std::cout << os.str() << "save counter" << std::endl;
 
     nb_found++;
-    if (min_ce->size())
-      l_ce.push_front(min_ce);
-    else
+    if (!min_ce->size())
       delete min_ce;
 
     min_ce = new ce::counter_example(a);
@@ -489,8 +666,8 @@ namespace spot
     for (stack_type::iterator i = stack.begin();
 	 i != stack.end(); ++i)
       {
-	ce = ce::state_ce(i->first->clone(), i->second);
-	//ce = ce::state_ce((*i)->clone(), bddfalse);
+	//ce = ce::state_ce(i->first->clone(), i->second->current_condition());
+	ce = ce::state_ce(i->first->clone(), bddfalse);
 	min_ce->prefix.push_front(ce);
       }
 
@@ -500,6 +677,7 @@ namespace spot
 
     //const state* s = *i;
     min_ce->build_cycle(s);
+    l_ce.push_front(min_ce);
   }
 
   std::ostream&
diff --git a/src/tgbaalgos/minimalce.hh b/src/tgbaalgos/minimalce.hh
index bde6e7005..a3c6e4bb8 100644
--- a/src/tgbaalgos/minimalce.hh
+++ b/src/tgbaalgos/minimalce.hh
@@ -58,7 +58,7 @@ namespace spot
 
       /// \brief Project a counter example on a tgba.
       void project_ce(const tgba* aut, std::ostream& os = std::cout);
-      // \brief Build a tgba from a counter example.
+      /// \brief Build a tgba from a counter example.
       tgba* ce2tgba();
 
       l_state_ce prefix;
@@ -89,7 +89,7 @@ namespace spot
   class minimalce_search: public emptyness_search
   {
   public:
-    minimalce_search(const tgba_tba_proxy *a);
+    minimalce_search(const tgba_tba_proxy *a, bool mode = false);
 
     virtual ~minimalce_search();
 
@@ -99,6 +99,8 @@ namespace spot
     /// \brief Find a counter example shorter than \a min_ce.
     ce::counter_example* check(ce::counter_example* min_ce);
 
+    ce::counter_example* find();
+
     /// \brief Print Stat.
     std::ostream& print_stat(std::ostream& os) const;
 
@@ -119,7 +121,8 @@ namespace spot
 			  state_ptr_hash, state_ptr_equal> hash_type;
     hash_type h_lenght;		///< Map of visited states.
 
-    typedef std::pair<const state*, bdd> state_pair;
+    typedef std::pair<const state*, tgba_succ_iterator*> state_pair;
+    //typedef std::pair<const state*, bdd> state_pair;
     typedef std::list<state_pair> stack_type;
     //typedef std::list<const state*> stack_type;
     stack_type stack;		///< Stack of visited states on the path.
@@ -130,8 +133,20 @@ namespace spot
     ce::counter_example* min_ce;
     std::list<ce::counter_example*> l_ce;
     int nb_found;
+    bool mode_;
     clock_t tps_;
 
+    /// \brief Perform the minimal search as explain in
+    /// @InProceedings(GaMoZe04spin,
+    /// Author = "Gastin, P. and Moro, P. and Zeitoun, M.",
+    /// Title = "Minimization of counterexamples in {SPIN}",
+    /// BookTitle = "Proceedings of the 11th SPIN Workshop (SPIN'04)",
+    /// Editor = "Graf, S. and Mounier, L.",
+    /// Publisher = SPRINGER,
+    /// Series = LNCS,
+    /// Number = 2989,
+    /// Year = 2004,
+    /// Pages = "92-108")
     void recurse_find(const state* it,
 		      std::ostringstream& os,
 		      int mode = normal);
diff --git a/src/tgbaalgos/nesteddfs.cc b/src/tgbaalgos/nesteddfs.cc
index 4a20d365d..7f5d2dce4 100644
--- a/src/tgbaalgos/nesteddfs.cc
+++ b/src/tgbaalgos/nesteddfs.cc
@@ -37,6 +37,7 @@ namespace spot
       nested_ = true;
     if (opt == my_nested)
       my_nested_ = true;
+    Maxsize = 0;
   }
 
   nesteddfs_search::~nesteddfs_search()
@@ -62,13 +63,20 @@ namespace spot
   bool
   nesteddfs_search::push(const state* s, bool m)
   {
+    /*
+      if ((Maxsize != 0) && // for minimize
+      (stack.size() + 1 > Maxsize))
+      return false;
+    */
+
     tgba_succ_iterator* i = a->succ_iter(s);
     i->first();
 
     hash_type::iterator hi = h.find(s);
     if (hi == h.end())
       {
-	magic d = { !m, m, true };
+	//magic d = { !m, m, true, stack.size() + 1};
+	magic d = { !m, m, true, };
 	h[s] = d;
       }
     else
@@ -76,31 +84,18 @@ namespace spot
 	hi->second.seen_without |= !m;
 	hi->second.seen_with |= m;
 	hi->second.seen_path = true; // for nested search
+	/*
+	  if ((stack.size() + 1) < hi->second.depth) // for minimize
+	  hi->second.depth = stack.size() + 1;
+	*/
 	if (hi->first != s)
 	  delete s;
 	s = hi->first;
-
-	/*
-	if (hi->second.depth != -1 &&
-	    hi->second.depth > (int)stack.size())
-	  return false;
-	*/
-
       }
 
     magic_state ms = { s, m };
     stack.push_front(state_iter_pair(ms, i));
 
-    // We build the counter example.
-    /*
-      bdd b = bddfalse;
-      if (!i->done()) // if the state is dead.
-      b = i->current_condition();
-      ce::state_ce ce;
-      ce = ce::state_ce(s->clone(), b);
-      counter_->prefix.push_back(ce);
-    */
-
     return true;
   }
 
@@ -146,29 +141,6 @@ namespace spot
   ce::counter_example*
   nesteddfs_search::check()
   {
-
-    ///
-    hash_type::const_iterator s = h.begin();
-    while (s != h.end())
-      {
-	// Advance the iterator before deleting the "key" pointer.
-	const state* ptr = s->first;
-	++s;
-	delete ptr;
-      }
-    if (x)
-      delete x;
-    while (!stack.empty())
-      {
-	delete stack.front().second;
-	stack.pop_front();
-      }
-    ///
-
-    //counter_ = new ce::counter_example(a);
-
-    clock();
-
     if (my_nested_)
       {
 	accepted_path_ = false;
@@ -215,8 +187,8 @@ namespace spot
 		assert(stack.size() == tstack.size());
 
 		build_counter();
+		//Maxsize = stack.size();
 		//counter_->build_cycle(x);
-		tps_ = clock();
 		return counter_;
 	      }
 	    if (!has(s_prime, magic))
@@ -226,9 +198,12 @@ namespace spot
 		    accepted_path_ = true;
 		    accepted_depth_ = stack.size();
 		  }
-		push(s_prime, magic);
-		tstack.push_front(c);
-		goto recurse;
+		if (push(s_prime, magic))
+		  {
+		    tstack.push_front(c);
+		    goto recurse;
+		  }
+		// for minimize
 	      }
 	    delete s_prime;
 	  }
@@ -242,10 +217,6 @@ namespace spot
 	    hi->second.seen_path = false;
 	  }
 	stack.pop_front();
-	/*
-	  delete (counter_->prefix.back()).first;
-	  counter_->prefix.pop_back();
-	*/
 
 	if (!magic && a->state_is_accepting(s))
 	  {
@@ -265,9 +236,6 @@ namespace spot
     std::cout << "END CHECK" << std::endl;
 
     assert(tstack.empty());
-    //delete counter_;
-
-    tps_ = clock();
 
     return 0;
   }
@@ -322,8 +290,7 @@ namespace spot
     if (counter_)
       ce_size = counter_->size();
     os << "Size of Counter Example : " << ce_size << std::endl
-       << "States explored : " << h.size() << std::endl
-       << "Computed time : " << tps_ << " microseconds" << std::endl;
+       << "States explored : " << h.size() << std::endl;
     return os;
   }
 
diff --git a/src/tgbaalgos/nesteddfs.hh b/src/tgbaalgos/nesteddfs.hh
index f15b564ee..802aeb8f2 100644
--- a/src/tgbaalgos/nesteddfs.hh
+++ b/src/tgbaalgos/nesteddfs.hh
@@ -45,11 +45,11 @@ namespace spot
   public:
 
     /// Initialize the Nesteddfs Search algorithm on the automaton \a a.
-    nesteddfs_search(const tgba_tba_proxy *a, int opt = my_nested);
+    nesteddfs_search(const tgba_tba_proxy *a, int opt = nested);
 
     virtual ~nesteddfs_search();
 
-    /// \brief Perform a Nested DFS Search.
+    /// \brief Perform a Magic or a Nested DFS Search.
     ///
     /// \return true iff the algorithm has found a new accepting
     ///    path.
@@ -79,6 +79,7 @@ namespace spot
       bool seen_without : 1;
       bool seen_with    : 1;
       bool seen_path    : 1;
+      //unsigned int depth;
     };
 
     /// \brief A state for the spot::magic_search algorithm.
@@ -127,8 +128,9 @@ namespace spot
     bool accepted_path_;
     int accepted_depth_;
 
+    unsigned int Maxsize;
+
     ce::counter_example* counter_;
-    clock_t tps_;
 
   };
 
diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc
index f9539382e..dd08c1dda 100644
--- a/src/tgbaalgos/reductgba_sim.cc
+++ b/src/tgbaalgos/reductgba_sim.cc
@@ -562,10 +562,10 @@ namespace spot
       }
   }
 
-  simulation_relation*
+  direct_simulation_relation*
   parity_game_graph_direct::get_relation()
   {
-    simulation_relation* rel = new simulation_relation();
+    direct_simulation_relation* rel = new direct_simulation_relation;
     state_couple* p = 0;
     seen_map::iterator j;
 
@@ -611,13 +611,13 @@ namespace spot
 
   ///////////////////////////////////////////////////////////////////////
 
-  simulation_relation*
+  direct_simulation_relation*
   get_direct_relation_simulation(const tgba* f,
 				 std::ostream& os,
 				 int opt)
   {
     parity_game_graph_direct* G = new parity_game_graph_direct(f);
-    simulation_relation* rel = G->get_relation();
+    direct_simulation_relation* rel = G->get_relation();
     if (opt == 1)
       G->print(os);
     delete G;
@@ -625,7 +625,7 @@ namespace spot
   }
 
   void
-  free_relation_simulation(simulation_relation* rel)
+  free_relation_simulation(direct_simulation_relation* rel)
   {
     if (rel == 0)
       return;
@@ -668,24 +668,26 @@ namespace spot
   {
     spot::tgba_reduc* automatareduc = new  spot::tgba_reduc(f);
 
-    if (opt & Reduce_Dir_Sim)
+    if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim))
       {
-	simulation_relation* rel
+	direct_simulation_relation* rel
 	  = get_direct_relation_simulation(automatareduc, std::cout);
 
 	automatareduc->display_rel_sim(rel, std::cout);
-	automatareduc->prune_automata(rel);
+	automatareduc->quotient_state(rel);
+	automatareduc->delete_transitions(rel);
 
 	free_relation_simulation(rel);
       }
     else
-      if (opt & Reduce_Del_Sim)
+      if (opt & (Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim))
 	{
-	  simulation_relation* rel
+	  delayed_simulation_relation* rel
 	    = get_delayed_relation_simulation(automatareduc, std::cout);
 
 	  automatareduc->display_rel_sim(rel, std::cout);
-	  automatareduc->prune_automata(rel);
+	  automatareduc->quotient_state(rel);
+	  automatareduc->delete_transitions(rel);
 
 	  free_relation_simulation(rel);
 	}
diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh
index 5a0d65808..f073b030f 100644
--- a/src/tgbaalgos/reductgba_sim.hh
+++ b/src/tgbaalgos/reductgba_sim.hh
@@ -37,12 +37,16 @@ namespace spot
     {
       /// No reduction.
       Reduce_None = 0,
-      /// Reduction using direct simulation relation.
-      Reduce_Dir_Sim = 1,
-      /// Reduction using delayed simulation relation.
-      Reduce_Del_Sim = 2,
+      /// Reduction of state using direct simulation relation.
+      Reduce_quotient_Dir_Sim = 1,
+      /// Reduction of transitions using direct simulation relation.
+      Reduce_transition_Dir_Sim = 2,
+      /// Reduction of state using delayed simulation relation.
+      Reduce_quotient_Del_Sim = 4,
+      /// Reduction of transition using delayed simulation relation.
+      Reduce_transition_Del_Sim = 8,
       /// Reduction using SCC.
-      Reduce_Scc = 4,
+      Reduce_Scc = 16,
       /// All reductions.
       Reduce_All = -1U
     };
@@ -57,19 +61,21 @@ namespace spot
   tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All);
 
   /// \brief Compute a direct simulation relation on state of tgba \a f.
-  simulation_relation* get_direct_relation_simulation(const tgba* a,
-						      std::ostream& os,
-						      int opt = -1);
+  direct_simulation_relation* get_direct_relation_simulation(const tgba* a,
+							     std::ostream& os,
+							     int opt = -1);
 
   /// Compute a delayed simulation relation on state of tgba \a f.
   // FIXME: This method is correct but it builds sometime (when there are more
   // than one acceptance condition) only a part of the simulation relation.
-  simulation_relation* get_delayed_relation_simulation(const tgba* a,
-						       std::ostream& os,
-						       int opt = -1);
+  delayed_simulation_relation* get_delayed_relation_simulation(const tgba* a,
+							       std::ostream& os,
+							       int opt = -1);
 
   /// To free a simulation relation.
-  void free_relation_simulation(simulation_relation* rel);
+  void free_relation_simulation(direct_simulation_relation* rel);
+  /// To free a simulation relation.
+  void free_relation_simulation(delayed_simulation_relation* rel);
 
   ///////////////////////////////////////////////////////////////////////
   // simulation.
@@ -185,7 +191,7 @@ namespace spot
     parity_game_graph_direct(const tgba* a);
     ~parity_game_graph_direct();
 
-    virtual simulation_relation* get_relation();
+    virtual direct_simulation_relation* get_relation();
 
   protected:
     virtual void build_graph();
@@ -282,7 +288,7 @@ namespace spot
     parity_game_graph_delayed(const tgba* a);
     ~parity_game_graph_delayed();
 
-    virtual simulation_relation* get_relation();
+    virtual delayed_simulation_relation* get_relation();
 
   private:
 
diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc
index 6319d6e03..c02528674 100644
--- a/src/tgbaalgos/reductgba_sim_del.cc
+++ b/src/tgbaalgos/reductgba_sim_del.cc
@@ -622,15 +622,17 @@ namespace spot
     //std::cout << "lift::change = false" << std::endl;
   }
 
-  simulation_relation*
+  delayed_simulation_relation*
   parity_game_graph_delayed::get_relation()
   {
-    simulation_relation* rel = new simulation_relation();
+    delayed_simulation_relation* rel = new delayed_simulation_relation;
     state_couple* p = 0;
     seen_map::iterator j;
 
-    if (this->nb_set_acc_cond() > 1)
+    /*
+      if (this->nb_set_acc_cond() > 1)
       return rel;
+    */
 
     for (Sgi::vector<spoiler_node*>::iterator i
 	   = spoiler_vertice_.begin();
@@ -674,15 +676,48 @@ namespace spot
   }
 
   ///////////////////////////////////////////
-  simulation_relation*
+  delayed_simulation_relation*
   get_delayed_relation_simulation(const tgba* f, std::ostream& os, int opt)
   {
     parity_game_graph_delayed* G = new parity_game_graph_delayed(f);
-    simulation_relation* rel = G->get_relation();
+    delayed_simulation_relation* rel = G->get_relation();
     if (opt == 1)
       G->print(os);
     delete G;
     return rel;
   }
 
+  void
+  free_relation_simulation(delayed_simulation_relation* rel)
+  {
+    if (rel == 0)
+      return;
+
+    Sgi::hash_map<const spot::state*, int,
+      state_ptr_hash, state_ptr_equal> seen;
+    Sgi::hash_map<const spot::state*, int,
+      state_ptr_hash, state_ptr_equal>::iterator j;
+
+    delayed_simulation_relation::iterator i;
+    for (i = rel->begin(); i != rel->end(); ++i)
+      {
+	if ((j = seen.find((*i)->first)) == seen.end())
+	    seen[(*i)->first] = 0;
+
+	if ((j = seen.find((*i)->second)) == seen.end())
+	    seen[(*i)->second] = 0;
+
+	delete *i;
+      }
+    delete rel;
+    rel = 0;
+
+    for (j = seen.begin(); j != seen.end();)
+      {
+	const state* ptr = j->first;
+	++j;
+	delete ptr;
+      }
+  }
+
 }
diff --git a/src/tgbaalgos/tarjan_on_fly.cc b/src/tgbaalgos/tarjan_on_fly.cc
index 104fc2cc0..fc676d29d 100644
--- a/src/tgbaalgos/tarjan_on_fly.cc
+++ b/src/tgbaalgos/tarjan_on_fly.cc
@@ -35,20 +35,19 @@ namespace spot
     for (stack_type::iterator i = stack.begin();
 	 i != stack.end(); ++i)
       {
-	if ((*i).s)
-	  delete (*i).s;
-	if ((*i).lasttr)
-	  delete (*i).lasttr;
+	//if ((*i).s)
+	delete (*i).s;
+	//if ((*i).lasttr)
+	delete (*i).lasttr;
       }
   }
 
   ce::counter_example*
   tarjan_on_fly::check()
   {
-    std::cout << "tarjan_on_fly::check()" << std::endl;
-
-    clock();
-
+    tgba_succ_iterator* iter = 0;
+    const state* succ = 0;
+    int pos = 0;
     top = dftop = -1;
     violation = false;
 
@@ -57,24 +56,20 @@ namespace spot
 
     while (!violation && dftop >= 0)
       {
-	//std::cout << "iter while" << std::endl;
 	s = stack[dftop].s;
-	std::cout << "s : " << a->format_state(s) << std::endl;
-	tgba_succ_iterator* iter = stack[dftop].lasttr;
+	iter = stack[dftop].lasttr;
 	if (iter == 0)
 	  {
 	    iter = a->succ_iter(s);
-	    //std::cout << "iter->first" << std::endl;
 	    iter->first();
 	    stack[dftop].lasttr = iter;
 	  }
 	else
 	  {
-	    //std::cout << "iter->next" << std::endl;
 	    iter->next();
 	  }
 
-	const state* succ = 0;
+	succ = 0;
 	if (!iter->done())
 	  {
 	    succ = iter->current_state();
@@ -82,7 +77,7 @@ namespace spot
 	      push(succ);
 	    else
 	      {
-		int pos = in_stack(succ);
+		pos = in_stack(succ);
 		delete succ;
 		if (pos != -1) // succ is in stack
 		  lowlinkupdate(dftop, pos);
@@ -92,7 +87,6 @@ namespace spot
 	  pop();
       }
 
-    tps_ = clock();
     if (violation)
       return build_counter();
 
@@ -104,9 +98,6 @@ namespace spot
   void
   tarjan_on_fly::push(const state* s)
   {
-    std::cout << "tarjan_on_fly::push() : "
-	      << a->format_state(s) << " : " << std::endl;
-
     h[s] = 1;
     top++;
 
@@ -122,33 +113,19 @@ namespace spot
     else
       ss.acc = -1;
 
-    /*
-    std::cout << "    lowlink : " << ss.lowlink << std::endl;
-    std::cout << "    pre     : " << ss.pre << std::endl;
-    std::cout << "    acc     : " << ss.acc << std::endl;
-    */
-
     if (top < (int)stack.size())
       {
-	std::cout << "MAJ" << std::endl;
-
-	/*
 	const state* sdel = stack[top].s;
 	tgba_succ_iterator* iter = stack[top].lasttr;
-	*/
-
-	stack[top] = ss;
-
-	/*
 	delete sdel;
 	if (iter)
 	  delete iter;
-	*/
 
+
+	stack[top] = ss;
       }
     else
       {
-	std::cout << "INS" << std::endl;
 	stack.push_back(ss);
       }
 
@@ -158,8 +135,6 @@ namespace spot
   void
   tarjan_on_fly::pop()
   {
-    std::cout << "tarjan_on_fly::pop()" << std::endl;
-
     int p = stack[dftop].pre;
 
     if (p >= 0)
@@ -174,20 +149,11 @@ namespace spot
   void
   tarjan_on_fly::lowlinkupdate(int f, int t)
   {
-    /*
-    std::cout << "tarjan_on_fly::lowlinkupdate() : " << std::endl
-	      << "     stack[t].lowlink : " << stack[t].lowlink
-	      << "     stack[f].lowlink : " << stack[f].lowlink
-	      << "     stack[f].acc     : " << stack[f].acc
-	      << std::endl;
-    */
-
     if (stack[t].lowlink <= stack[f].lowlink)
       {
 	if (stack[t].lowlink <= stack[f].acc)
 	  {
 	    violation = true;
-	    std::cout << "VIOLATION DETECTED" << std::endl;
 	  }
 	stack[f].lowlink = stack[t].lowlink;
       }
@@ -196,9 +162,6 @@ namespace spot
   int
   tarjan_on_fly::in_stack(const state* s) const
   {
-    std::cout << "tarjan_on_fly::in_stack() : "
-	      << a->format_state(s) << std::endl;
-
     int n = 0;
     stack_type::const_iterator i;
     for (i = stack.begin(); i != stack.end(); ++i, ++n)
@@ -214,8 +177,6 @@ namespace spot
   ce::counter_example*
   tarjan_on_fly::build_counter()
   {
-    std::cout << "tarjan_on_fly::build_counter()" << std::endl;
-
     ce = new ce::counter_example(a);
 
     stack_type::iterator i;
@@ -224,20 +185,14 @@ namespace spot
 	if (x && x->compare((*i).s) == 0)
 	  break;
 
-	//os << "  " << a->format_state(i->first) << std::endl;
-
 	ce->prefix.push_back(ce::state_ce((*i).s->clone(),
-					   //bddtrue));
-					   (*i).lasttr->current_condition()));
+					  (*i).lasttr->current_condition()));
       }
 
     for (; i != stack.end(); ++i)
       {
-	//os << "  " << a->format_state(i->first) << std::endl;
-
 	ce->cycle.push_back(ce::state_ce((*i).s->clone(),
-					   //bddtrue));
-					   (*i).lasttr->current_condition()));
+					 (*i).lasttr->current_condition()));
       }
 
     return ce;
@@ -250,8 +205,7 @@ namespace spot
     if (ce)
       ce_size = ce->size();
     os << "Size of Counter Example : " << ce_size << std::endl
-       << "States explored : " << h.size() << std::endl
-       << "Computed time : " << tps_ << " microseconds" << std::endl;
+       << "States explored : " << h.size() << std::endl;
     return os;
   }
 
diff --git a/src/tgbaalgos/tarjan_on_fly.hh b/src/tgbaalgos/tarjan_on_fly.hh
index f59e266e6..6a175800a 100644
--- a/src/tgbaalgos/tarjan_on_fly.hh
+++ b/src/tgbaalgos/tarjan_on_fly.hh
@@ -85,7 +85,7 @@ namespace spot
     int in_stack(const state* s) const;
 
     ce::counter_example* build_counter();
-    clock_t tps_;
+    //clock_t tps_;
 
   };
 
diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test
index 183d3d8c2..d97ec1b1a 100755
--- a/src/tgbatest/emptchk.test
+++ b/src/tgbatest/emptchk.test
@@ -27,12 +27,15 @@ set -e
 
 expect_ce()
 {
-  run 0 ./ltl2tgba -ms -f "$1"
   run 0 ./ltl2tgba -m -f "$1"
   run 0 ./ltl2tgba -ndfs -f "$1"
-  #run 0 ./ltl2tgba -ndfs2 -f "$1"
   run 0 ./ltl2tgba -tj -f "$1"
   run 0 ./ltl2tgba -c -f "$1"
+  run 0 ./ltl2tgba -ndfs2 -f "$1"
+  run 0 ./ltl2tgba -ng -f "$1"
+
+  #run 0 ./ltl2tgba -ms -f "$1"
+  #run 0 ./ltl2tgba -msit -f "$1"
 
   run 0 ./ltl2tgba -e "$1"
   run 0 ./ltl2tgba -e -D "$1"
@@ -48,12 +51,14 @@ expect_ce()
 
 expect_no()
 {
-  run 0 ./ltl2tgba -Ms -f "$1"
   run 0 ./ltl2tgba -M -f "$1"
   run 0 ./ltl2tgba -Ndfs -f "$1"
-  run 0 ./ltl2tgba -Ndfs2 -f "$1"
   run 0 ./ltl2tgba -TJ -f "$1"
   run 0 ./ltl2tgba -C -f "$1"
+  run 0 ./ltl2tgba -Ndfs2 -f "$1"
+  run 0 ./ltl2tgba -NG -f "$1"
+
+  #run 0 ./ltl2tgba -Ms -f "$1"
 
   run 0 ./ltl2tgba -E "$1"
   run 0 ./ltl2tgba -E -D "$1"
@@ -67,8 +72,7 @@ expect_no()
   run 0 ./ltl2tgba -M -f "$1"
 }
 
-#expect_no '!((FF a) <=> (F a))'
-#expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+expect_ce 'Fa & Xb & GFc & Gd'
 
 expect_ce 'a'
 expect_ce 'a U b'
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 25135ecf6..4635e8a1e 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -36,6 +36,7 @@
 #include "tgba/tgbatba.hh"
 #include "tgbaalgos/magic.hh"
 #include "tgbaalgos/nesteddfs.hh"
+#include "tgbaalgos/nesteddfsgen.hh"
 #include "tgbaalgos/colordfs.hh"
 #include "tgbaalgos/tarjan_on_fly.hh"
 //#include "tgbaalgos/minimalce.hh"
@@ -81,12 +82,18 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -ms   minmimal-search (implies -D), expect a counter-example"
 	    << std::endl
+	    << "  -msit minmimal-search (implies -D), expect a counter-example"
+	    << std::endl
 	    << "  -mold magic-search (implies -D), expect a counter-example"
 	    << std::endl
 	    << "  -M    magic-search (implies -D), expect no counter-example"
 	    << std::endl
 	    << "  -Mold magic-search (implies -D), expect no counter-example"
 	    << std::endl
+	    << "  -n    same as -m, but display more counter-examples"
+	    << std::endl
+	    << "  -N    display the never clain for Spin "
+	    << "(implies -D)" << std::endl
 	    << "  -ndfs nesteddfs-search (implies -D), expect a "
 	    << "counter-example"
 	    << std::endl
@@ -99,10 +106,12 @@ syntax(char* prog)
 	    << "  -Ndfs2 modify-nesteddfs-search (implies -D), "
 	    << "expect no counter-example"
 	    << std::endl
-	    << "  -n    same as -m, but display more counter-examples"
+	    << "  -ng   nesteddfs-search generalized (implies -D), expect a "
+	    << "counter-example"
+	    << std::endl
+	    << "  -NG   nesteddfs-search generalized (implies -D), expect no "
+	    << "counter-example"
 	    << std::endl
-	    << "  -N    display the never clain for Spin "
-	    << "(implies -D)" << std::endl
             << "  -p    branching postponement (implies -f)" << std::endl
 	    << "  -r    display the relation BDD, not the reachability graph"
 	    << std::endl
@@ -114,12 +123,18 @@ syntax(char* prog)
 	    << "  -r4   reduce formula using all rules" << std::endl
 	    << "  -rd   display the reduce formula" << std::endl
 	    << "  -R    same as -r, but as a set" << std::endl
-	    << "  -R1   use direct simulation to reduce the automata "
+	    << "  -R1q  use direct simulation to merge some state "
 	    << "(use -L for more reduction)"
 	    << std::endl
-	    << "  -R2   use delayed simulation to reduce the automata "
+	    << "  -R1t  use direct simulation to remove some transition "
 	    << "(use -L for more reduction)"
 	    << std::endl
+	    << "  -R2q  use delayed simulation to merge some state "
+	    << "(the automaton must be degeneralised)"
+	    << std::endl
+	    << "  -R2t  use delayed simulation to remove some transition "
+	    << "(the automaton must be degeneralised)"
+	    << std::endl
 	    << "  -R3   use SCC to reduce the automata"
 	    << std::endl
 	    << "  -Rd   display the simulation relation"
@@ -163,9 +178,9 @@ main(int argc, char** argv)
   int formula_index = 0;
   enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld,
 	 NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
-	 TarjanOnFly, MinimalSearch} echeck = None;
+	 TarjanOnFly, MinimalSearch, MinimalSearchIterative,
+	 NestedGeneSearch} echeck = None;
   spot::emptyness_search* es = 0;
-  //int opt_search = 0; //FIXME
   spot::search_opt opt_nested_search = spot::magic;
   enum { NoneDup, BFS, DFS } dupexp = NoneDup;
   bool magic_many = false;
@@ -197,7 +212,6 @@ main(int argc, char** argv)
       else if (!strcmp(argv[formula_index], "-c"))
 	{
 	  echeck = ColorDFSSearch;
-	  //opt_search = 0;
 	  degeneralize_opt = true;
 	  expect_counter_example = true;
 	  output = -1;
@@ -255,37 +269,14 @@ main(int argc, char** argv)
 	  fair_loop_approx = true;
 	  fm_opt = true;
 	}
-      else if (!strcmp(argv[formula_index], "-mold"))
-	{
-	  echeck = MagicSearchOld;
-	  //opt_search = 0;
-	  degeneralize_opt = true;
-	  expect_counter_example = true;
-	  output = -1;
-	}
       else if (!strcmp(argv[formula_index], "-m"))
 	{
 	  opt_nested_search = spot::magic;
 	  echeck = MagicSearch;
-	  //opt_search = 0;
 	  degeneralize_opt = true;
 	  expect_counter_example = true;
 	  output = -1;
-	  //magic_many = true;
-	}
-      else if (!strcmp(argv[formula_index], "-ms"))
-	{
-	  echeck = MinimalSearch;
-	  degeneralize_opt = true;
-	  expect_counter_example = true;
-	  output = -1;
-	}
-      else if (!strcmp(argv[formula_index], "-Mold"))
-	{
-	  echeck = MagicSearchOld; // FIXME
-	  degeneralize_opt = true;
-	  expect_counter_example = false;
-	  output = -1;
+	  magic_many = true;
 	}
       else if (!strcmp(argv[formula_index], "-M"))
 	{
@@ -295,6 +286,28 @@ main(int argc, char** argv)
 	  expect_counter_example = false;
 	  output = -1;
 	}
+      else if (!strcmp(argv[formula_index], "-mold"))
+	{
+	  echeck = MagicSearchOld;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	  magic_many = true;
+	}
+      else if (!strcmp(argv[formula_index], "-Mold"))
+	{
+	  echeck = MagicSearchOld;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-ms"))
+	{
+	  echeck = MinimalSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	}
       else if (!strcmp(argv[formula_index], "-Ms"))
 	{
 	  echeck = MinimalSearch;
@@ -302,40 +315,12 @@ main(int argc, char** argv)
 	  expect_counter_example = false;
 	  output = -1;
 	}
-      else if (!strcmp(argv[formula_index], "-ndfs"))
+      else if (!strcmp(argv[formula_index], "-msit"))
 	{
-	  opt_nested_search = spot::nested;
-	  echeck = NestedDFSSearch;
-	  //opt_search = 1;
+	  echeck = MinimalSearchIterative;
 	  degeneralize_opt = true;
 	  expect_counter_example = true;
-	  output = -1;
-	}
-      else if (!strcmp(argv[formula_index], "-Ndfs"))
-	{
-	  opt_nested_search = spot::nested;
-	  echeck = NestedDFSSearch;
-	  //opt_search = 1;
-	  degeneralize_opt = true;
-	  expect_counter_example = false;
-	  output = -1;
-	}
-      else if (!strcmp(argv[formula_index], "-ndfs2"))
-	{
-	  opt_nested_search = spot::my_nested;
-	  echeck = NestedDFSSearchModify;
-	  //opt_search = 2;
-	  degeneralize_opt = true;
-	  expect_counter_example = true;
-	  output = -1;
-	}
-      else if (!strcmp(argv[formula_index], "-Ndfs2"))
-	{
-	  opt_nested_search = spot::my_nested;
-	  echeck = NestedDFSSearchModify;
-	  //opt_search = 2;
-	  degeneralize_opt = true;
-	  expect_counter_example = false;
+	  magic_many = true;
 	  output = -1;
 	}
       else if (!strcmp(argv[formula_index], "-n"))
@@ -351,6 +336,53 @@ main(int argc, char** argv)
 	  degeneralize_opt = true;
 	  output = 8;
 	}
+      else if (!strcmp(argv[formula_index], "-ndfs"))
+	{
+	  opt_nested_search = spot::nested;
+	  echeck = NestedDFSSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	  magic_many = true;
+	}
+      else if (!strcmp(argv[formula_index], "-Ndfs"))
+	{
+	  opt_nested_search = spot::nested;
+	  echeck = NestedDFSSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-ndfs2"))
+	{
+	  opt_nested_search = spot::my_nested;
+	  echeck = NestedDFSSearchModify;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-Ndfs2"))
+	{
+	  opt_nested_search = spot::my_nested;
+	  echeck = NestedDFSSearchModify;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-ng"))
+	{
+	  echeck = NestedGeneSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-NG"))
+	{
+	  echeck = NestedGeneSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
       else if (!strcmp(argv[formula_index], "-p"))
 	{
 	  post_branching = true;
@@ -380,15 +412,21 @@ main(int argc, char** argv)
 	{
 	  output = 3;
 	}
-      else if (!strcmp(argv[formula_index], "-R1"))
+      else if (!strcmp(argv[formula_index], "-R1q"))
 	{
-	  //degeneralize_opt = true; // FIXME
-	  reduc_aut |= spot::Reduce_Dir_Sim;
+	  reduc_aut |= spot::Reduce_quotient_Dir_Sim;
 	}
-      else if (!strcmp(argv[formula_index], "-R2"))
+      else if (!strcmp(argv[formula_index], "-R1t"))
 	{
-	  //degeneralize_opt = true; // FIXME
-	  reduc_aut |= spot::Reduce_Del_Sim;
+	  reduc_aut |= spot::Reduce_transition_Dir_Sim;
+	}
+      else if (!strcmp(argv[formula_index], "-R2q"))
+	{
+	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
+	}
+      else if (!strcmp(argv[formula_index], "-R2t"))
+	{
+	  reduc_aut |= spot::Reduce_transition_Del_Sim;
 	}
       else if (!strcmp(argv[formula_index], "-R3"))
 	{
@@ -542,36 +580,46 @@ main(int argc, char** argv)
 	  if (reduc_aut & spot::Reduce_Scc)
 	    aut_red->prune_scc();
 
-	  if ((reduc_aut & spot::Reduce_Dir_Sim) ||
-	      (reduc_aut & spot::Reduce_Del_Sim))
+	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
+			   spot::Reduce_transition_Dir_Sim |
+			   spot::Reduce_quotient_Del_Sim |
+			   spot::Reduce_transition_Del_Sim))
 	    {
-	      spot::simulation_relation* rel;
-	      if (reduc_aut & spot::Reduce_Dir_Sim)
-		rel = spot::get_direct_relation_simulation(a,
-							   std::cout,
-							   display_parity_game);
-	      else if (reduc_aut & spot::Reduce_Del_Sim)
-		rel = spot::get_delayed_relation_simulation(a,
-							    std::cout,
-							    display_parity_game);
-	      else
-		{
-		  assert(0);
-		  // Please GCC so it does not think REL is unused.
-		  rel = 0;
-		}
+	      spot::direct_simulation_relation* rel_dir = 0;
+	      spot::delayed_simulation_relation* rel_del = 0;
+
+	      if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
+			       spot::Reduce_transition_Dir_Sim))
+		rel_dir = spot::get_direct_relation_simulation(a,
+							       std::cout,
+							       display_parity_game);
+	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
+				    spot::Reduce_transition_Del_Sim))
+		rel_del = spot::get_delayed_relation_simulation(a,
+								std::cout,
+								display_parity_game);
 
 	      if (display_rel_sim)
-		aut_red->display_rel_sim(rel, std::cout);
+		{
+		  if (rel_dir)
+		    aut_red->display_rel_sim(rel_dir, std::cout);
+		  if (rel_del)
+		    aut_red->display_rel_sim(rel_del, std::cout);
+		}
 
-	      if (reduc_aut & spot::Reduce_Dir_Sim)
-		aut_red->prune_automata(rel);
-	      else if (reduc_aut & spot::Reduce_Del_Sim)
-		aut_red->quotient_state(rel);
-	      else
-		assert(0);
+	      if (reduc_aut & spot::Reduce_quotient_Dir_Sim)
+		aut_red->quotient_state(rel_dir);
+	      if (reduc_aut & spot::Reduce_transition_Dir_Sim)
+		aut_red->delete_transitions(rel_dir);
+	      if (reduc_aut & spot::Reduce_quotient_Del_Sim)
+		aut_red->quotient_state(rel_del);
+	      if (reduc_aut & spot::Reduce_transition_Del_Sim)
+		aut_red->delete_transitions(rel_del);
 
-	      spot::free_relation_simulation(rel);
+	      if (rel_dir)
+		spot::free_relation_simulation(rel_dir);
+	      if (rel_del)
+		spot::free_relation_simulation(rel_del);
 	    }
 	}
 
@@ -639,6 +687,7 @@ main(int argc, char** argv)
 	case Couvreur:
 	case Couvreur2:
 	  {
+	    std::cout << "Tarjan Couvreur" << std::endl;
 	    spot::emptiness_check* ec;
 	    if (echeck == Couvreur)
 	      ec = new spot::emptiness_check(a);
@@ -654,12 +703,16 @@ main(int argc, char** argv)
 		    break;
 		  }
 		spot::counter_example ce(ec->result());
-		//ce.print_result(std::cout);
-		spot::ce::counter_example* res2 = ce.get_counter_example();
-		spot::tgba* aut = res2->ce2tgba();
-		spot::dotty_reachable(std::cout, aut);
-		delete res2;
-		delete aut;
+		ce.print_result(std::cout);
+		ce.print_stats(std::cout);
+
+		//spot::ce::counter_example* res2 = ce.get_counter_example();
+		//spot::tgba* aut = res2->ce2tgba();
+		//spot::dotty_reachable(std::cout, aut);
+		//res2->print(std::cout);
+		//delete res2;
+		//delete aut;
+
 	      }
 	    else
 	      {
@@ -669,8 +722,28 @@ main(int argc, char** argv)
 	  }
 	  break;
 
+	case NestedGeneSearch:
+	  {
+	    std::cout << "Nested DFS generalized" << std::endl;
+	    spot::nesteddfsgen_search* ec = new spot::nesteddfsgen_search(a);
+	    bool res = ec->check();
+	    ec->print_stats(std::cout);
+	    if (expect_counter_example)
+	      {
+		if (!res)
+		  exit_code = 1;
+	      }
+	    else
+	      {
+		exit_code = res;
+	      }
+	    delete ec;
+	  }
+	  break;
+
 	case MagicSearchOld:
 	  {
+	    std::cout << "Magic Search" << std::endl;
 	    spot::magic_search ms(degeneralized);
 	    bool res = ms.check();
 	    if (expect_counter_example)
@@ -692,23 +765,46 @@ main(int argc, char** argv)
 	  break;
 
 	case ColorDFSSearch:
+	  std::cout << "Colored Search" << std::endl;
 	  es = new spot::colordfs_search(degeneralized);
 	  break;
 
 	case TarjanOnFly:
+	  std::cout << "Tarjan On Fly" << std::endl;
 	  es = new spot::tarjan_on_fly(degeneralized);
 	  break;
 
 	case MinimalSearch:
-	  es = new spot::minimalce_search(degeneralized);
+	  {
+	    std::cout << "Recursive Minimal Search" << std::endl;
+	    es = new spot::colordfs_search(degeneralized);
+	    spot::ce::counter_example* res = es->check();
+	    res->print(std::cout);
+	    std::cout << "Minimisation:" << std::endl;
+	    es = new spot::minimalce_search(degeneralized, false);
+	    res = es->check();
+	    res->print(std::cout);
+	  }
+	  break;
+
+	case MinimalSearchIterative:
+	    std::cout << "Iterative Minimal Search" << std::endl;
+	  es = new spot::minimalce_search(degeneralized, true);
 	  break;
 
 	case MagicSearch:
-	case NestedDFSSearch:
-	case NestedDFSSearchModify:
+	  std::cout << "Magic Search" << std::endl;
 	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
 	  break;
 
+	case NestedDFSSearch:
+	case NestedDFSSearchModify:
+	  std::cout << "Nested DFS" << std::endl;
+	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
+	  break;
+
+	default:
+	  assert(0);
 	}
 
       if (es)
@@ -750,6 +846,7 @@ main(int argc, char** argv)
 	    delete res;
 	}
 
+
       if (es)
 	delete es;
       if (f)
diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc
index c6a61b4b5..2a1b6be74 100644
--- a/src/tgbatest/reductgba.cc
+++ b/src/tgbatest/reductgba.cc
@@ -66,18 +66,28 @@ main(int argc, char** argv)
       o = spot::Reduce_Scc;
       break;
     case 1:
-      o = spot::Reduce_Dir_Sim;
+      o = spot::Reduce_quotient_Dir_Sim;
       break;
     case 2:
-      o = spot::Reduce_Del_Sim;
+      o = spot::Reduce_transition_Dir_Sim;
       break;
     case 3:
-      o = spot::Reduce_Dir_Sim | spot::Reduce_Scc;
+      o = spot::Reduce_quotient_Del_Sim;
       break;
     case 4:
-      o = spot::Reduce_Del_Sim | spot::Reduce_Scc;
+      o = spot::Reduce_transition_Del_Sim;
       break;
     case 5:
+      o = spot::Reduce_quotient_Dir_Sim |
+	spot::Reduce_transition_Dir_Sim |
+	spot::Reduce_Scc;
+      break;
+    case 6:
+      o = spot::Reduce_quotient_Del_Sim |
+	spot::Reduce_transition_Del_Sim |
+	spot::Reduce_Scc;
+      break;
+    case 7:
       // No Reduction
       break;
     default:
@@ -85,7 +95,8 @@ main(int argc, char** argv)
   }
 
   int exit_code = 0;
-  spot::simulation_relation* rel = 0;
+  spot::direct_simulation_relation* rel_dir = 0;
+  spot::delayed_simulation_relation* rel_del = 0;
   spot::tgba* automata = 0;
   spot::tgba_reduc* automatareduc = 0;
 
@@ -110,21 +121,30 @@ main(int argc, char** argv)
   spot::dotty_reachable(std::cout, automata);
   automatareduc = new spot::tgba_reduc(automata);
 
-  if (o & spot::Reduce_Dir_Sim)
+  if (o & spot::Reduce_quotient_Dir_Sim)
     {
-      rel = spot::get_direct_relation_simulation(automatareduc, std::cout);
-      automatareduc->prune_automata(rel);
+      rel_dir = spot::get_direct_relation_simulation(automatareduc, std::cout);
+      automatareduc->quotient_state(rel_dir);
     }
-  else if (o & spot::Reduce_Del_Sim)
+  else if (o & spot::Reduce_quotient_Del_Sim)
     {
-      rel = spot::get_delayed_relation_simulation(automatareduc, std::cout);
-      automatareduc->quotient_state(rel);
+      std::cout << "get delayed" << std::endl;
+      rel_del = spot::get_delayed_relation_simulation(automatareduc, std::cout);
+      std::cout << "quotient state" << std::endl;
+      automatareduc->quotient_state(rel_del);
+      std::cout << "end" << std::endl;
     }
 
-  if (rel != 0)
+  if (rel_dir != 0)
     {
-      automatareduc->display_rel_sim(rel, std::cout);
-      spot::free_relation_simulation(rel);
+      automatareduc->display_rel_sim(rel_dir, std::cout);
+      spot::free_relation_simulation(rel_dir);
+    }
+
+  if (rel_del != 0)
+    {
+      automatareduc->display_rel_sim(rel_del, std::cout);
+      spot::free_relation_simulation(rel_del);
     }
 
   if (o & spot::Reduce_Scc)
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 144334e7a..f087a71c9 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -104,7 +104,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), post reduction with direct simulation"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -R1 -F -f -t'"
+   Parameters = "--spot './ltl2tgba -R1q -R1t -F -f -t'"
    Enabled = yes
 }
 
@@ -112,7 +112,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), post reduction with delayed simulation"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -R2 -F -f -t'"
+   Parameters = "--spot './ltl2tgba -R2q -R2t -F -f -t'"
    Enabled = yes
 }
 
@@ -128,7 +128,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), pre + post reduction"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r4 -R1 -R3 -F -f -t'"
+   Parameters = "--spot './ltl2tgba -r4 -R1q -R1t -R3 -F -f -t'"
    Enabled = yes
 }