* 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: four new algorithms for emptyness check.

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/emptchk.test,
src/tgbaalgos/Makefile.am: Add files for emptyness-check.


* src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata.
* src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition
for scc reduce.

ChangeLog

@@ -1,3 +1,28 @@
+2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* 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: four new algorithms for emptyness check.
+
+	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/emptchk.test,
+	src/tgbaalgos/Makefile.am: Add files for emptyness-check.
+
+2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata.
+	* src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition
+	for scc reduce.
+
 2004-08-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* configure.ac, NEWS: Bump version to 0.0y.

src/tgba/tgbareduc.cc

@@ -123,6 +123,8 @@ namespace spot
       this->compute_scc();
     this->prune_acc();
     this->delete_scc();
+
+    this->merge_transitions();
   }
 
   std::string
@@ -424,6 +426,12 @@ namespace spot
 
   }
 
+  void
+  tgba_reduc::merge_state_delayed(const spot::state*,
+				  const spot::state*)
+  {
+  }
+
   /////////////////////////////////////////
   /////////////////////////////////////////
 
@@ -580,8 +588,6 @@ namespace spot
   void
   tgba_reduc::remove_acc(const spot::state* s)
   {
-    //std::cout << "remove_acc" << std::endl;
-
     tgba_explicit::state* s1;
     seen_map::iterator sm = si_.find(s);
     sm = si_.find(s);
@@ -624,7 +630,6 @@ namespace spot
   tgba_reduc::is_not_accepting(const spot::state* s,
 			       int n)
   {
-    //std::cout << "is not accepting" << std::endl;
     bool b = false;
 
     // First call of is_terminal //
@@ -726,8 +731,6 @@ namespace spot
   bool
   tgba_reduc::is_terminal(const spot::state* s, int n)
   {
-    // FIXME
-
     // a SCC is terminal if there are no transition
     // leaving the SCC AND she doesn't contain all
     // the acceptance condition.

src/tgba/tgbareduc.hh

@@ -117,6 +117,12 @@ namespace spot
     void merge_state(const spot::state* s1,
 		     const spot::state* s2);
 
+    /// Redirect all transition leading to s1 to s2.
+    /// Note that we can do the reverse because
+    /// s1 and s2 belong to a co-simulate relation.
+    void merge_state_delayed(const spot::state* s1,
+			     const spot::state* s2);
+
     /// Remove all the scc which are terminal and doesn't
     /// contains all the acceptance conditions.
     void delete_scc();

src/tgbaalgos/Makefile.am

@@ -27,33 +27,41 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 tgbaalgosdir = $(pkgincludedir)/tgbaalgos
 
 tgbaalgos_HEADERS = \
+  colordfs.hh \
   dotty.hh \
   dupexp.hh \
   lbtt.hh \
   ltl2tgba_fm.hh \
   ltl2tgba_lacim.hh \
   magic.hh \
+  minimalce.hh \
+  nesteddfs.hh \
   neverclaim.hh \
   powerset.hh \
   reachiter.hh \
   save.hh \
   stats.hh \
-  reductgba_sim.hh
+  reductgba_sim.hh \
+  tarjan_on_fly.hh
 
 noinst_LTLIBRARIES = libtgbaalgos.la
 libtgbaalgos_la_SOURCES = \
+  colordfs.cc \
   dotty.cc \
   dupexp.cc \
   lbtt.cc \
   ltl2tgba_fm.cc \
   ltl2tgba_lacim.cc \
   magic.cc \
+  minimalce.cc \
+  nesteddfs.cc \
   neverclaim.cc \
   powerset.cc \
   reachiter.cc \
   save.cc \
   stats.cc \
   reductgba_sim.cc \
-  reductgba_sim_del.cc
+  reductgba_sim_del.cc \
+  tarjan_on_fly.cc
 
 libtgbaalgos_la_LIBADD = gtec/libgtec.la

src/tgbaalgos/colordfs.cc

@@ -0,0 +1,296 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <iterator>
+#include <cassert>
+#include "colordfs.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+
+  colordfs_search::colordfs_search(const tgba_tba_proxy* a)
+    : a(a), x(0), counter_(0)
+  {
+  }
+
+  colordfs_search::~colordfs_search()
+  {
+    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;
+    // Release all iterators on the stack.
+    while (!stack.empty())
+      {
+	delete stack.front().second;
+	stack.pop_front();
+      }
+  }
+
+  bool
+  colordfs_search::push(const state* s, color c)
+  {
+    tgba_succ_iterator* i = a->succ_iter(s);
+    i->first();
+
+    /*
+    hash_type::iterator hi = h.find(s);
+    if (hi != h.end())
+      if (hi->second.depth <= (int)stack.size())
+	//return false; // FIXME
+	return true;
+    */
+
+    color_state cs = { c, true , stack.size() }; // FIXME
+    h[s] = cs;
+
+    stack.push_front(state_iter_pair(s, i));
+
+    // We build the counter example
+    bdd b = bddfalse;
+    if (!i->done()) // if the state is dead.
+      b = i->current_condition();
+    counter_->prefix.push_back(ce::state_ce(s->clone(), b));
+
+    return true;
+  }
+
+  void
+  colordfs_search::pop()
+  {
+    const state* s = stack.begin()->first;
+    tgba_succ_iterator* i = stack.begin()->second;
+    delete i;
+
+    //std::cout << "pop : " << a->format_state(s) << std::endl;
+
+    hash_type::iterator hi = h.find(s);
+    assert(hi != h.end());
+    hi->second.is_in_cp = false;
+    stack.pop_front();
+    //delete s;
+
+    // We build the counter example
+    delete counter_->prefix.back().first;
+    counter_->prefix.pop_back();
+  }
+
+  bool
+  colordfs_search::all_succ_black(const state* s)
+  {
+    bool return_value = true;
+    hash_type::iterator hi;
+
+    const state* s2;
+    tgba_succ_iterator* i = a->succ_iter(s);
+    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);
+	else
+	  return_value = false;
+	delete s2;
+      }
+    delete i;
+
+    //std::cout << "End Loop" << std::endl;
+
+    hi = h.find(s);
+    assert(hi != h.end());
+    if (return_value)
+      hi->second.c = black;
+
+    return return_value;
+  }
+
+  ce::counter_example*
+  colordfs_search::check()
+  {
+    clock();
+    counter_ = new ce::counter_example(a);
+    const state* s = a->get_init_state();
+    if (dfs_blue(s))
+      counter_->build_cycle(x);
+    else
+      {
+	delete counter_;
+	counter_ = 0;
+      }
+    tps_ = clock();
+
+    return counter_;
+  }
+
+  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;
+
+    hash_type::iterator hi;
+    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))
+	  {
+	    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)
+	      {
+		delete i;
+		return true;
+	      }
+	  }
+	else
+	  delete s2; // FIXME
+      }
+    delete i;
+
+    pop();
+
+    if (!all_succ_black(s) &&
+	a->state_is_accepting(s))
+      {
+	if (dfs_red(s))
+	  return 1;
+	dfs_black(s);
+      }
+
+    return false;
+  }
+
+  bool
+  colordfs_search::dfs_red(const state* s)
+  {
+    //std::cout << "dfs_red : " << a->format_state(s) << std::endl;
+    if (!push(s, red))
+      return false;
+
+    hash_type::iterator hi;
+    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)))
+	  {
+	    //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)
+	  {
+	    delete s2; // FIXME
+	    if (dfs_red(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)
+  {
+    //std::cout << "dfs_black" << a->format_state(s) << std::endl;
+    hash_type::iterator hi = h.find(s);
+    if (hi == h.end()) // impossible
+      {
+	color_state cs = { black, false, stack.size() };
+	h[s] = cs;
+      }
+    else
+      hi->second.c = black;
+
+    tgba_succ_iterator* i = a->succ_iter(s);
+    for (i->first(); !i->done(); i->next())
+      {
+	const state* s2 = i->current_state();
+	hi = h.find(s2);
+	if (hi == h.end())
+	  {
+	    color_state cs = { black, false, stack.size() };
+	    h[s2] = cs;
+	    dfs_black(s2);
+	  }
+	else
+	  {
+	    delete s2;
+	    if (hi->second.c != black)
+	      dfs_black(hi->first);
+	  }
+      }
+    delete i;
+
+  }
+
+  std::ostream&
+  colordfs_search::print_stat(std::ostream& os) const
+  {
+    int ce_size = 0;
+    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;
+    return os;
+  }
+
+}

src/tgbaalgos/colordfs.hh

@@ -0,0 +1,121 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_COLORDFS_HH
+# define SPOT_TGBAALGOS_COLORDFS_HH
+
+#include "misc/hash.hh"
+#include <list>
+#include <utility>
+#include <ostream>
+#include "tgba/tgbatba.hh"
+#include "tgbaalgos/minimalce.hh"
+
+namespace spot
+{
+  class colordfs_search: public emptyness_search
+  {
+  public:
+    /// Initialize the Colordfs Search algorithm on the automaton \a a.
+    colordfs_search(const tgba_tba_proxy *a);
+
+    virtual ~colordfs_search();
+
+    /// \brief Perform a Color DFS Search.
+    ///
+    /// \return a new accepting path if there exists one, NULL otherwise.
+    ///
+    /// check() can be called several times until it return false,
+    /// to enumerate all accepting paths.
+    virtual ce::counter_example* check();
+
+    /// \brief Print Stat.
+    std::ostream& print_stat(std::ostream& os) const;
+
+  private:
+
+    // The names "stack", "h", and "x", are those used in the paper.
+
+    /// \brief  Records the color of a state.
+    enum color
+      {
+	white = 0,
+	blue  = 1,
+	red   = 2,
+	black = 3
+      };
+
+    struct color_state
+    {
+      color c;
+      bool is_in_cp;
+      int depth;
+    };
+
+    typedef std::pair<const state*, tgba_succ_iterator*> state_iter_pair;
+    typedef std::list<state_iter_pair> stack_type;
+    stack_type stack;		///< Stack of visited states on the path.
+
+    typedef std::list<bdd> tstack_type;
+    /// \brief Stack of transitions.
+    ///
+    /// This is an addition to the data from the paper.
+    tstack_type tstack;
+
+    typedef Sgi::hash_map<const state*, color_state,
+			  state_ptr_hash, state_ptr_equal> hash_type;
+    hash_type h;		///< Map of visited states.
+
+    /// The three dfs 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")
+    bool dfs_blue(const state* s, bdd acc = bddfalse);
+    bool dfs_red(const state* s);
+    void dfs_black(const state* s);
+
+    /// Append a new state to the current path.
+    bool push(const state* s, color c);
+    /// Remove a state to the current path.
+    void pop();
+    /// Check if all successors of \a s are black and color
+    /// \a s in black if true.
+    bool all_succ_black(const state* s);
+
+    const tgba_tba_proxy* a;	///< The automata to check.
+    /// The state for which we are currently seeking an SCC.
+    const state* x;
+
+    ce::counter_example* counter_;
+    clock_t tps_;
+  };
+
+
+}
+
+#endif // SPOT_TGBAALGOS_COLORDFS_HH

src/tgbaalgos/gtec/ce.cc

@@ -35,6 +35,8 @@ namespace spot
 				   eccf)
     : ecs_(ecs)
   {
+    counter_ = new ce::counter_example(ecs->aut);
+
     assert(!ecs_->root.empty());
     assert(suffix.empty());
 
@@ -76,6 +78,10 @@ namespace spot
     assert(spi.first);
     suffix.push_front(spi.first);
 
+    /////
+    counter_->prefix.push_front(ce::state_ce(spi.first->clone(), bddfalse));
+    ////
+
     // We build a path trough each SCC in the stack.  For the
     // first SCC, the starting state is the initial state of the
     // automaton.  The destination state is the closest state
@@ -113,21 +119,35 @@ namespace spot
 		const state* h_dest = scc[k]->has_state(dest);
 		if (!h_dest)
 		  {
-		    // If we have found a state in the next SCC.
+		    // If we have found a state in greater SCC which.
 		    // Unwind the path and populate SUFFIX.
 		    h_dest = scc[k+1]->has_state(dest);
 		    if (h_dest)
 		      {
 			state_sequence seq;
 
+			///
+			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.push_front(src);
 			    src = father[src];
 			  }
 			// Append SEQ to SUFFIX.
 			suffix.splice(suffix.end(), seq);
+
+			///
+			counter_->prefix.splice(counter_->prefix.end(),
+						seq_count);
+			///
+
 			// Exit this BFS for this SCC.
 			while (!todo.empty())
 			  {
@@ -211,14 +231,27 @@ namespace spot
 	    if (h_dest == to)
 	      {
 		cycle_path p;
+
+		///
+		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));
 		while (src != from)
 		  {
 		    const state_proposition& psi = father[src];
+		    ///
+		    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);
+		///
 
 		// Exit the BFS, but release all iterators first.
 		while (!todo.empty())
@@ -256,6 +289,9 @@ namespace spot
 
   }
 
+  ////////////////////////////////////////////////////////////////////////
+  /*
+
   void
   counter_example::accepting_path(const explicit_connected_component* scc,
 				  const state* start, bdd acc_to_traverse)
@@ -380,7 +416,12 @@ namespace spot
 	// Append our best path to the period.
 	for (cycle_path::iterator it = best_path.begin();
 	     it != best_path.end(); ++it)
-	  period.push_back(*it);
+	  {
+	    period.push_back(*it);
+	    ce::state_ce ce(it->first, it->second);
+	    counter_->cycle.push_back(ce);
+	    counter_->cycle.push_back(*it);
+	  }
 
 	// Prepare to find another path for the remaining acceptance
 	// conditions.
@@ -393,6 +434,153 @@ namespace spot
     complete_cycle(scc, start, suffix.back());
   }
 
+  */
+  ////////////////////////////////////////////////////////////////////////
+
+  void
+  counter_example::accepting_path(const explicit_connected_component* scc,
+				  const state* start, bdd acc_to_traverse)
+  {
+    // State seen during the DFS.
+    typedef Sgi::hash_set<const state*,
+                          state_ptr_hash, state_ptr_equal> set_type;
+    set_type seen;
+    // DFS stack.
+    std::stack<triplet> todo;
+
+    while (acc_to_traverse != bddfalse)
+      {
+	// Initial state.
+	{
+	  tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
+	  i->first();
+	  todo.push(triplet(start, i, bddfalse));
+	  seen.insert(start);
+	}
+
+	// The path being explored currently.
+	cycle_path path;
+	// The best path seen so far.
+	cycle_path best_path;
+	// The acceptance conditions traversed by BEST_PATH.
+	bdd best_acc = bddfalse;
+
+	while (!todo.empty())
+	  {
+	    tgba_succ_iterator* iter = todo.top().iter;
+	    const state* s = todo.top().s;
+
+	    // Nothing more to explore, backtrack.
+	    if (iter->done())
+	      {
+		todo.pop();
+		delete iter;
+		seen.erase(s);
+		if (todo.size())
+		  {
+		    assert(path.size());
+		    path.pop_back();
+		  }
+		continue;
+	      }
+
+	    // We must not escape the current SCC.
+	    const state* dest = iter->current_state();
+	    const state* h_dest = scc->has_state(dest);
+	    if (!h_dest)
+	      {
+		delete dest;
+		iter->next();
+		continue;
+	      }
+
+	    bdd acc = iter->current_acceptance_conditions() | todo.top().acc;
+	    path.push_back(state_proposition(h_dest,
+					     iter->current_condition()));
+
+	    // Advance iterator for next step.
+	    iter->next();
+
+	    if (seen.find(h_dest) == seen.end())
+	      {
+		// A new state: continue the DFS.
+		tgba_succ_iterator* di = ecs_->aut->succ_iter(h_dest);
+		di->first();
+		todo.push(triplet(h_dest, di, acc));
+		seen.insert(h_dest);
+		continue;
+	      }
+
+	    // We have completed a full cycle.
+
+	    // If we already have a best path, let see if the current
+	    // one is better.
+	    if (best_path.size())
+	      {
+		// When comparing the merits of two paths, only the
+		// acceptance conditions we are trying the traverse
+		// are important.
+		bdd acc_restrict = acc & acc_to_traverse;
+		bdd best_acc_restrict = best_acc & acc_to_traverse;
+
+		// If the best path and the current one traverse the
+		// same acceptance conditions, we keep the shorter
+		// path.  Otherwise, we keep the path which has the
+		// more acceptance conditions.
+		if (best_acc_restrict == acc_restrict)
+		  {
+		    if (best_path.size() <= path.size())
+		      goto backtrack_path;
+		  }
+		else
+		  {
+		    // `best_acc_restrict >> acc_restrict' is true
+		    // when the set of acceptance conditions of
+		    // best_acc_restrict is included in the set of
+		    // acceptance conditions of acc_restrict.
+		    //
+		    // FIXME: It would be better to count the number
+		    // of acceptance conditions.
+		    if (bddtrue != (best_acc_restrict >> acc_restrict))
+		      goto backtrack_path;
+		  }
+	      }
+
+	    // The current path the best one.
+	    best_path = path;
+	    best_acc = acc;
+
+	  backtrack_path:
+	    // Continue exploration from parent to find better paths.
+	    // (Do not pop PATH if ITER is done, because that will be
+	    // done at the top of the loop, among other things.)
+	    if (!iter->done())
+	      path.pop_back();
+	  }
+
+	// Append our best path to the period.
+	for (cycle_path::iterator it = best_path.begin();
+	     it != best_path.end(); ++it)
+	  {
+	    period.push_back(*it);
+	    ce::state_ce ce(it->first->clone(), it->second);
+	    counter_->cycle.push_back(ce);
+	    //counter_->cycle.push_back(*it);
+	  }
+
+	// Prepare to find another path for the remaining acceptance
+	// conditions.
+	acc_to_traverse -= best_acc;
+	start = period.back().first;
+      }
+
+    // Complete the path so that it goes back to its beginning,
+    // forming a cycle.
+    complete_cycle(scc, start, suffix.back());
+  }
+
+  /////////////
+
   std::ostream&
   counter_example::print_result(std::ostream& os, const tgba* restrict) const
   {
@@ -444,4 +632,10 @@ namespace spot
     os << period.size() << " states in period" << std::endl;
   }
 
+  ce::counter_example*
+  counter_example::get_counter_example() const
+  {
+    return counter_;
+  }
+
 }

src/tgbaalgos/gtec/ce.hh

@@ -25,6 +25,8 @@
 #include "status.hh"
 #include "explscc.hh"
 
+#include "tgbaalgos/minimalce.hh"
+
 namespace spot
 {
   /// Compute a counter example from a spot::emptiness_check_status
@@ -51,6 +53,8 @@ namespace spot
     /// Output statistics about this object.
     void print_stats(std::ostream& os) const;
 
+    ce::counter_example* get_counter_example() const;
+
   protected:
     /// Called by counter_example to find a path which traverses all
     /// acceptance conditions in the accepted SCC.
@@ -64,6 +68,7 @@ namespace spot
 
   private:
     const emptiness_check_status* ecs_;
+    ce::counter_example* counter_;
   };
 }
 

src/tgbaalgos/minimalce.cc

@@ -0,0 +1,539 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "tgbaalgos/minimalce.hh"
+#include "tgba/tgbaexplicit.hh"
+
+namespace spot
+{
+
+  ///////////////////////////////////////////////////////////////////////////
+  // Class counter example.
+
+  namespace ce
+  {
+
+    counter_example::counter_example(const tgba* a)
+      : automata_(a)
+    {
+    }
+
+    counter_example::~counter_example()
+    {
+      for (l_state_ce::const_iterator i = prefix.begin();
+	   i != prefix.end(); ++i)
+	{
+	  delete i->first;
+	}
+      for (l_state_ce::const_iterator i = cycle.begin();
+	   i != cycle.end(); ++i)
+	{
+	  delete i->first;
+	}
+    }
+
+    void
+    counter_example::build_cycle(const state* x)
+    {
+      if (!x)
+	return;
+      bool in_cycle = false;
+      for (l_state_ce::iterator i = prefix.begin();
+	   i != prefix.end();)
+	{
+	  if (i->first->compare(x) == 0)
+	    in_cycle = true;
+	  if (in_cycle)
+	    {
+	      cycle.push_back(*i);
+	      i = prefix.erase(i);
+	    }
+	  else
+	    ++i;
+	}
+    }
+
+    int
+    counter_example::size()
+    {
+      return prefix.size() + cycle.size();
+    }
+
+    std::ostream&
+    counter_example::print(std::ostream& os) const
+    {
+      os << "Prefix:" << std::endl;
+      const bdd_dict* d = automata_->get_dict();
+      for (l_state_ce::const_iterator i = prefix.begin();
+	   i != prefix.end(); ++i)
+	{
+	  os << "  " << automata_->format_state(i->first) << std::endl;
+	  os << "    | " << bdd_format_set(d, i->second) << std::endl;
+	}
+      os <<"Cycle:" <<std::endl;
+      for (l_state_ce::const_iterator i = cycle.begin();
+	   i != cycle.end(); ++i)
+	{
+	  os << "  " << automata_->format_state(i->first) << std::endl;
+	  os << "    | " << bdd_format_set(d, i->second) << std::endl;
+	}
+      return os;
+    }
+
+    bdd_dict*
+    counter_example::get_dict() const
+    {
+      return automata_->get_dict();
+    }
+
+    void
+    counter_example::project_ce(const tgba* aut, std::ostream& os)
+    {
+      os << "prefix :" << std::endl;
+      for (ce::l_state_ce::const_iterator i = prefix.begin();
+	   i != prefix.end(); ++i)
+	{
+	  const state* s = aut->project_state(i->first, aut);
+	  assert(s);
+	  os << aut->format_state(s) << std::endl;
+	  delete s;
+	}
+
+      os << "cycle :" << std::endl;
+      for (ce::l_state_ce::const_iterator i = cycle.begin();
+	   i != cycle.end(); ++i)
+	{
+	  const state* s = aut->project_state(i->first, aut);
+	  assert(s);
+	  os << aut->format_state(s) << std::endl;
+	  delete s;
+	}
+
+    }
+
+    tgba*
+    counter_example::ce2tgba()
+    {
+
+      tgba_explicit* aut = new tgba_explicit(automata_->get_dict());
+
+      std::string strs, strd;
+      tgba_explicit::transition* t;
+      ce::l_state_ce::const_iterator is = prefix.begin();
+      ce::l_state_ce::const_iterator id = is;
+      //ce::l_state_ce::const_iterator is_c;
+      //ce::l_state_ce::const_iterator id_c;
+      if (is != prefix.end())
+	{
+	  strs = automata_->format_state(is->first);
+	  aut->set_init_state(strs);
+	  ++id;
+
+	  for (; id != prefix.end(); ++is, ++id)
+	    {
+	      strs = automata_->format_state(is->first);
+	      strd = automata_->format_state(id->first);
+	      t = aut->create_transition(strs, strd);
+	      aut->add_conditions(t, is->second);
+	    }
+
+	  id = cycle.begin();
+	}
+      else
+	{
+	  id = cycle.begin();
+	  is = id;
+	  ++id;
+	}
+
+      for (; id != cycle.end();)
+	{
+	  strs = automata_->format_state(is->first);
+	  strd = automata_->format_state(id->first);
+	  t = aut->create_transition(strs, strd);
+	  aut->add_conditions(t, is->second);
+	  is = id;
+	  ++id;
+	}
+
+      assert(cycle.size() != 0);
+      is = cycle.end();
+      is--;
+      id = cycle.begin();
+      strs = automata_->format_state(is->first);
+      strd = automata_->format_state(id->first);
+      t = aut->create_transition(strs, strd);
+      aut->add_conditions(t, is->second);
+
+      aut->merge_transitions();
+
+      return aut;
+    }
+
+  }
+
+  /////////////////////////////////////////////////////////////////////////////
+  // The base interface for build a emptyness search algorithm
+  emptyness_search::emptyness_search()
+  {
+  }
+
+  emptyness_search::~emptyness_search()
+  {
+  }
+
+  /*
+  std::ostream&
+  nesteddfs_search::print_stat(std::ostream& os) const
+  {
+    int ce_size = 0;
+    if (counter_)
+      ce_size = counter_->size();
+    os << "Size of Counter Example : " << ce_size << std::endl
+    os << "States explored : " << size_ << std::endl
+       << "Computed time : " << tps_ << " microseconds" << std::endl;
+    return os;
+  }
+  */
+
+  std::ostream&
+  emptyness_search::print_stat(std::ostream& os) const
+  {
+    return os;
+  }
+
+  /////////////////////////////////////////////////////////////////////////////
+  // minimal_search
+
+  minimalce_search::minimalce_search(const tgba_tba_proxy *a)
+    : a(a), min_ce(0)
+  {
+  }
+
+  minimalce_search::~minimalce_search()
+  {
+
+    hash_type::const_iterator s = h_lenght.begin();
+    while (s != h_lenght.end())
+      {
+	// Advance the iterator before deleting the "key" pointer.
+	const state* ptr = s->first;
+	++s;
+	delete ptr;
+      }
+
+    for (std::list<ce::counter_example*>::iterator i = l_ce.begin();
+	 i != l_ce.end();)
+      {
+	//std::cout << "delete a counter" << std::endl;
+	if (*i == min_ce)
+	  {
+	    ++i;
+	    continue;
+	  }
+	ce::counter_example* ce = *i;
+	++i;
+	delete ce;
+      }
+
+    //std::cout << "END ~minimalce_search()" << std::endl;
+  }
+
+  ce::counter_example*
+  minimalce_search::check()
+  {
+    clock();
+    nb_found = 0;
+    min_ce = new ce::counter_example(a);
+    std::ostringstream os;
+    const state* s = a->get_init_state();
+    recurse_find(s, os);
+    std::cout << "nb_found : " << nb_found << std::endl;
+
+    if (min_ce->size() == 0)
+      {
+	delete min_ce;
+	min_ce = 0;
+      }
+
+    tps_ = clock();
+    return min_ce;
+  }
+
+  ce::counter_example*
+  minimalce_search::check(ce::counter_example*)
+  {
+    min_ce = new ce::counter_example(a);
+
+    /*
+    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;
+    recurse_find(s, os);
+    //if (recurse_find(s))
+    //return min_ce;
+    //else
+    return min_ce;
+  }
+
+  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())
+      {
+	delete s;
+	s = i->first;
+	if (((int)stack.size() + 1) < i->second)
+	  i->second = stack.size() + 1;
+      }
+    else
+      h_lenght[s] = stack.size();
+
+    stack.push_front(state_pair(s, bddfalse));
+    //stack.push_front(s);
+
+    tgba_succ_iterator* iter = a->succ_iter(s);
+    iter->first();
+    while (!iter->done())
+      {
+	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()))
+	  {
+	    int depth = in_stack(succ, os);
+	    if (depth != -1)
+	      {
+		if (closes_accepting(succ, depth, os))
+		  {
+		    // New counter example is found !!
+		    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;
+		      }
+
+		  }
+		else
+		  delete succ;
+	      }
+	    else if ((mode == careful) ||
+		     a->state_is_accepting(succ))
+	      {
+		//std::cout << "recurse 1 : " << stack.size() << " ";
+		mode = careful;
+		os << "  ";
+		recurse_find(succ, os, mode);
+	      }
+	    else if (h_lenght.find(succ) == h_lenght.end())
+	      {
+		//std::cout << "recurse 2 : " << stack.size() << " ";
+		os << "  ";
+		recurse_find(succ, os, mode);
+	      }
+	    else if ((h_lenght[succ] > (int)stack.size() + 1) &&
+		     (min_ce->size() != 0))
+	      {
+		//std::cout << "recurse 3 : " << stack.size() << " ";
+		mode = careful;
+		os << "  ";
+		recurse_find(succ, os, mode);
+	      }
+	    else
+	      delete succ;
+	  }
+	else //if (h_lenght.find(succ) == h_lenght.end())
+	  delete succ;
+
+	iter->next();
+      }
+
+    delete iter;
+
+    //std::cout << os.str() << "stack.pop_front()" << std::endl;
+    stack.pop_front();
+
+  }
+
+  bool
+  minimalce_search::closes_accepting(const state*,
+				     int depth,
+				     std::ostringstream&) const
+  {
+    //std::cout << os.str() << "close accepting : " << a->format_state(s);
+
+    int last_depth = -1;
+    int depth_cp = stack.size();
+
+    for (stack_type::const_iterator i = stack.begin();
+	 i != stack.end(); ++i, --depth_cp)
+      if (a->state_is_accepting(i->first))
+	//if (a->state_is_accepting(*i))
+	{
+	  last_depth = depth_cp - 1;
+	  //last_depth = h_lenght[*i];
+	  break;
+	}
+
+    /*
+    if (depth <= last_depth)
+      std::cout << " : true => depth : "
+		<< depth << ", last_depth"
+		<< last_depth << std::endl;
+    else
+      std::cout << " : false => depth : "
+		<< depth << ", last_depth : "
+		<< last_depth << std::endl;
+    */
+
+    return depth <= last_depth; // May be '<='
+  }
+
+  int
+  minimalce_search::in_stack(const state* s, std::ostringstream&) const
+  {
+    //std::cout << os.str() << "in stack : " << a->format_state(s);
+
+    int depth = stack.size();
+
+    bool return_value = false;
+    for (stack_type::const_iterator i = stack.begin();
+	 i != stack.end() && !return_value; ++i, --depth)
+      {
+	if (s->compare(i->first) == 0)
+	  //if (s->compare(*i) == 0)
+	  return_value = true;
+      }
+
+    if (!return_value)
+      depth = -1;
+
+    /*
+    if (return_value)
+      std::cout << " : true" << std::endl;
+    else
+      {
+	depth = -1;
+	std::cout << " : false" << std::endl;
+      }
+    */
+
+    return depth;
+  }
+
+  void
+  minimalce_search::save_counter(const state* s, std::ostringstream&)
+  {
+    //std::cout << os.str() << "save counter" << std::endl;
+
+    nb_found++;
+    if (min_ce->size())
+      l_ce.push_front(min_ce);
+    else
+      delete min_ce;
+
+    min_ce = new ce::counter_example(a);
+    ce::state_ce ce;
+    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);
+	min_ce->prefix.push_front(ce);
+      }
+
+    stack_type::iterator i = stack.begin();
+    if (i == stack.end()) // empty counter example.
+      return;
+
+    //const state* s = *i;
+    min_ce->build_cycle(s);
+  }
+
+  std::ostream&
+  minimalce_search::print_stat(std::ostream& os) const
+  {
+    int ce_size = 0;
+    if (min_ce)
+      ce_size = min_ce->size();
+    os << "Size of Counter Example : " << ce_size << std::endl
+       << "States explored : " << h_lenght.size() << std::endl
+       << "Computed time : " << tps_ << " microseconds" << std::endl;
+    return os;
+  }
+
+  ce::counter_example*
+  minimalce_search::get_minimal_cyle() const
+  {
+    ce::counter_example* min_cycle = min_ce;
+    for (std::list<ce::counter_example*>::const_iterator i = l_ce.begin();
+	 i != l_ce.end();)
+      if ((*i)->cycle.size() < min_cycle->cycle.size())
+	min_cycle = *i;
+    return min_cycle;
+  }
+
+  ce::counter_example*
+  minimalce_search::get_minimal_prefix() const
+  {
+    ce::counter_example* min_prefix = min_ce;
+    for (std::list<ce::counter_example*>::const_iterator i = l_ce.begin();
+	 i != l_ce.end();)
+      if ((*i)->prefix.size() < min_prefix->prefix.size())
+	min_prefix = *i;
+    return min_prefix;
+  }
+
+}

src/tgbaalgos/minimalce.hh

@@ -0,0 +1,150 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_MINIMALCE_HH
+# define SPOT_TGBAALGOS_MINIMALCE_HH
+
+#include "misc/hash.hh"
+#include <list>
+#include <utility>
+#include <ostream>
+#include <sstream>
+#include "tgba/tgbatba.hh"
+#include "tgba/bddprint.hh"
+//#include "tgbaalgos/gtec/ce.hh"
+
+#include <time.h>
+
+namespace spot
+{
+
+  namespace ce
+  {
+
+    typedef std::pair<const state*, bdd> state_ce;
+    typedef std::list<state_ce> l_state_ce;
+
+    ///////////////////////////////////////////////////////////////////////////
+    // Class counter example.
+
+    class counter_example
+    {
+    public :
+      counter_example(const tgba* a);
+      ~counter_example();
+
+      void build_cycle(const state* x);
+      int size();
+      std::ostream& print(std::ostream& os) const;
+      bdd_dict* get_dict() const;
+
+      /// \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.
+      tgba* ce2tgba();
+
+      l_state_ce prefix;
+      l_state_ce cycle;
+      const tgba* automata_;
+
+    };
+
+  }
+
+  /////////////////////////////////////////////////////////////////////////////
+  // The base interface for build a emptyness search algorithm
+  class emptyness_search
+  {
+  protected:
+    emptyness_search();
+
+  public:
+    virtual ~emptyness_search();
+    virtual ce::counter_example* check() = 0;
+    /// \brief Print Stat.
+    virtual std::ostream& print_stat(std::ostream& os) const;
+  };
+
+  /////////////////////////////////////////////////////////////////////////////
+  // Perform a minimal search
+
+  class minimalce_search: public emptyness_search
+  {
+  public:
+    minimalce_search(const tgba_tba_proxy *a);
+
+    virtual ~minimalce_search();
+
+    /// \brief Find the shortest counter example.
+    virtual ce::counter_example* check();
+
+    /// \brief Find a counter example shorter than \a min_ce.
+    ce::counter_example* check(ce::counter_example* min_ce);
+
+    /// \brief Print Stat.
+    std::ostream& print_stat(std::ostream& os) const;
+
+    ce::counter_example* get_minimal_cyle() const;
+    ce::counter_example* get_minimal_prefix() const;
+
+  private:
+
+    enum search_mode
+      {
+	normal = 0,
+	careful = 1
+      };
+    //int mode;
+
+    //typedef std::pair<int, tgba_succ_iterator*> state_iter_pair;
+    typedef Sgi::hash_map<const state*, int,
+			  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::list<state_pair> stack_type;
+    //typedef std::list<const state*> stack_type;
+    stack_type stack;		///< Stack of visited states on the path.
+
+    const tgba_tba_proxy* a;	///< The automata to check.
+    /// The state for which we are currently seeking an SCC.
+    //const state* x;
+    ce::counter_example* min_ce;
+    std::list<ce::counter_example*> l_ce;
+    int nb_found;
+    clock_t tps_;
+
+    void recurse_find(const state* it,
+		      std::ostringstream& os,
+		      int mode = normal);
+    bool closes_accepting(const state* s,
+			  int detph,
+			  std::ostringstream& os) const;
+    int in_stack(const state* s, std::ostringstream& os) const;
+
+    /// Save the current path in stack as a counter example.
+    /// this counter example is the minimal that we have found yet.
+    void save_counter(const state* s, std::ostringstream& os);
+  };
+
+}
+
+#endif // SPOT_TGBAALGOS_MINIMALCE_HH

src/tgbaalgos/nesteddfs.cc

@@ -0,0 +1,355 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <iterator>
+#include <cassert>
+#include "nesteddfs.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+  nesteddfs_search::nesteddfs_search(const tgba_tba_proxy* a,
+				     int opt)
+    : a(a), x(0),
+      x_bis(0),
+      accepted_path_(false)
+  {
+    nested_ = my_nested_ = false;
+    if (opt == nested)
+      nested_ = true;
+    if (opt == my_nested)
+      my_nested_ = true;
+  }
+
+  nesteddfs_search::~nesteddfs_search()
+  {
+    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;
+    // Release all iterators on the stack.
+    while (!stack.empty())
+      {
+	delete stack.front().second;
+	stack.pop_front();
+      }
+  }
+
+  bool
+  nesteddfs_search::push(const state* s, bool m)
+  {
+    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 };
+	h[s] = d;
+      }
+    else
+      {
+	hi->second.seen_without |= !m;
+	hi->second.seen_with |= m;
+	hi->second.seen_path = true; // for nested search
+	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;
+  }
+
+  bool
+  nesteddfs_search::has(const state* s, bool m) const
+  {
+    hash_type::const_iterator i = h.find(s);
+    if (i == h.end())
+      return false;
+    if (!m && i->second.seen_without)
+      return true;
+    if (m && i->second.seen_with)
+      return true;
+    return false;
+  }
+
+  bool
+  nesteddfs_search::exist_path(const state* s) const
+  {
+    hash_type::const_iterator hi = h.find(s);
+    if (hi == h.end())
+      return false;
+    if (hi->second.seen_with)
+      return false;
+    return hi->second.seen_path && hi->second.seen_without;
+  }
+
+  int
+  nesteddfs_search::depth_path(const state* s) const
+  {
+    int depth = 0;
+    stack_type::const_reverse_iterator i;
+    for (i = stack.rbegin(); i != stack.rend(); ++i, ++depth)
+      if (s->compare(i->first.s) == 0)
+	break;
+
+    if (i != stack.rend())
+      return depth;
+    else
+      return stack.size() + 1;
+  }
+
+  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;
+	accepted_depth_ = 0;
+      }
+
+    if (stack.empty())
+      // It's a new search.
+      push(a->get_init_state(), false);
+    else
+      // Remove the transition to the cycle root.
+      tstack.pop_front();
+
+    assert(stack.size() == 1 + tstack.size());
+
+    while (!stack.empty())
+      {
+      recurse:
+	//std::cout << "recurse : "<< stack.size() << std::endl;
+	nesteddfs_search::state_iter_pair& p = stack.front();
+	tgba_succ_iterator* i = p.second;
+	const bool magic = p.first.m;
+
+	while (!i->done())
+	  {
+	    const state* s_prime = i->current_state();
+	    //std::cout << a->format_state(s_prime) << std::endl;
+	    bdd c = i->current_condition();
+	    i->next();
+
+	    if ((magic && 0 == s_prime->compare(x)) ||
+		(magic && (nested_ || my_nested_) && exist_path(s_prime)) ||
+		(!magic && my_nested_ && accepted_path_ &&
+		 exist_path(s_prime) && depth_path(s_prime) <= accepted_path_))
+	      {
+		if (nested_ || my_nested)
+		  {
+		    if (x)
+		      delete x;
+		    x = s_prime->clone();
+		  }
+		delete s_prime;
+		tstack.push_front(c);
+		assert(stack.size() == tstack.size());
+
+		build_counter();
+		//counter_->build_cycle(x);
+		tps_ = clock();
+		return counter_;
+	      }
+	    if (!has(s_prime, magic))
+	      {
+		if (my_nested_ && a->state_is_accepting(s_prime))
+		  {
+		    accepted_path_ = true;
+		    accepted_depth_ = stack.size();
+		  }
+		push(s_prime, magic);
+		tstack.push_front(c);
+		goto recurse;
+	      }
+	    delete s_prime;
+	  }
+
+	const state* s = p.first.s;
+	delete i;
+	if (nested_ || my_nested_)
+	  {
+	    hash_type::iterator hi = h.find(((stack.front()).first).s);
+	    assert (hi != h.end());
+	    hi->second.seen_path = false;
+	  }
+	stack.pop_front();
+	/*
+	  delete (counter_->prefix.back()).first;
+	  counter_->prefix.pop_back();
+	*/
+
+	if (!magic && a->state_is_accepting(s))
+	  {
+	    if (!has(s, true))
+	      {
+		if (x)
+		  delete x;
+		x = s->clone();
+		push(s, true);
+		continue;
+	      }
+	  }
+	if (!stack.empty())
+	  tstack.pop_front();
+      }
+
+    std::cout << "END CHECK" << std::endl;
+
+    assert(tstack.empty());
+    //delete counter_;
+
+    tps_ = clock();
+
+    return 0;
+  }
+
+  std::ostream&
+  nesteddfs_search::print_result(std::ostream& os, const tgba* restrict) const
+  {
+    stack_type::const_reverse_iterator i;
+    tstack_type::const_reverse_iterator ti;
+    os << "Prefix:" << std::endl;
+    const bdd_dict* d = a->get_dict();
+    for (i = stack.rbegin(), ti = tstack.rbegin();
+	 i != stack.rend(); ++i, ++ti)
+      {
+	if (i->first.s->compare(x) == 0)
+	  os <<"Cycle:" <<std::endl;
+
+	const state* s = i->first.s;
+	if (restrict)
+	  {
+	    s = a->project_state(s, restrict);
+	    assert(s);
+	    os << "  " << restrict->format_state(s) << std::endl;
+	    delete s;
+	  }
+	else
+	  {
+	    os << "  " << a->format_state(s) << std::endl;
+	  }
+	os << "    | " << bdd_format_set(d, *ti) << std::endl;
+      }
+
+    if (restrict)
+      {
+	const state* s = a->project_state(x, restrict);
+	assert(s);
+	os << "  " << restrict->format_state(s) << std::endl;
+	delete s;
+
+      }
+    else
+      {
+	os << "  " << a->format_state(x) << std::endl;
+      }
+    return os;
+  }
+
+  std::ostream&
+  nesteddfs_search::print_stat(std::ostream& os) const
+  {
+    int ce_size = 0;
+    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;
+    return os;
+  }
+
+  void
+  nesteddfs_search::build_counter()
+  {
+    assert(stack.size() == tstack.size());
+    counter_ = new ce::counter_example(a);
+    stack_type::reverse_iterator i;
+    tstack_type::reverse_iterator ti;
+    for (i = stack.rbegin(), ti = tstack.rbegin();
+	 i != stack.rend(); ++i, ++ti)
+      {
+	if (i->first.s->compare(x) == 0)
+	  break;
+	ce::state_ce ce;
+	ce = ce::state_ce(i->first.s->clone(), *ti);
+	counter_->prefix.push_back(ce);
+      }
+    for (; i != stack.rend(); ++i, ++ti)
+      {
+	ce::state_ce ce;
+	ce = ce::state_ce(i->first.s->clone(), *ti);
+	counter_->cycle.push_back(ce);
+      }
+    //counter_->build_cycle(x);
+  }
+
+}

src/tgbaalgos/nesteddfs.hh

@@ -0,0 +1,138 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_NESTEDDFS_HH
+# define SPOT_TGBAALGOS_NESTEDDFS_HH
+
+#include "misc/hash.hh"
+#include <list>
+#include <utility>
+#include <ostream>
+#include "tgba/tgbatba.hh"
+#include "tgbaalgos/minimalce.hh"
+
+namespace spot
+{
+
+  enum search_opt
+    {
+      magic     = 0,
+      nested    = 1,
+      my_nested = 2
+    };
+
+  class nesteddfs_search: public emptyness_search
+  {
+
+  public:
+
+    /// Initialize the Nesteddfs Search algorithm on the automaton \a a.
+    nesteddfs_search(const tgba_tba_proxy *a, int opt = my_nested);
+
+    virtual ~nesteddfs_search();
+
+    /// \brief Perform a Nested DFS Search.
+    ///
+    /// \return true iff the algorithm has found a new accepting
+    ///    path.
+    ///
+    /// check() can be called several times until it return false,
+    /// to enumerate all accepting paths.
+    virtual ce::counter_example* check();
+
+    /// \brief Print the last accepting path found.
+    ///
+    /// Restrict printed states to \a the state space of restrict if
+    /// supplied.
+    std::ostream& print_result(std::ostream& os,
+			       const tgba* restrict = 0) const;
+
+    /// \brief Print Stat.
+    std::ostream& print_stat(std::ostream& os) const;
+
+  private:
+
+    // The names "stack", "h", and "x", are those used in the paper.
+
+    /// \brief  Records whether a state has be seen with the magic bit
+    /// on or off.
+    struct magic
+    {
+      bool seen_without : 1;
+      bool seen_with    : 1;
+      bool seen_path    : 1;
+    };
+
+    /// \brief A state for the spot::magic_search algorithm.
+    struct magic_state
+    {
+      const state* s;
+      bool m;			///< The state of the magic demon.
+      // int depth;
+    };
+
+    typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
+    typedef std::list<state_iter_pair> stack_type;
+    stack_type stack;		///< Stack of visited states on the path.
+
+    typedef std::list<bdd> tstack_type;
+    /// \brief Stack of transitions.
+    ///
+    /// This is an addition to the data from the paper.
+    tstack_type tstack;
+
+    typedef Sgi::hash_map<const state*, magic,
+			  state_ptr_hash, state_ptr_equal> hash_type;
+    hash_type h;		///< Map of visited states.
+
+    /// Append a new state to the current path.
+    bool push(const state* s, bool m);
+    /// Check whether we already visited \a s with the Magic bit set to \a m.
+    bool has(const state* s, bool m) const;
+    /// Check if \a s is in the path.
+    bool exist_path(const state* s) const;
+    /// Return the depth of the state \a s in stack.
+    int depth_path(const state* s) const;
+
+    void build_counter();
+
+    const tgba_tba_proxy* a;	///< The automata to check.
+    /// The state for which we are currently seeking an SCC.
+    const state* x;
+    /// \brief Active the nested search which produce a
+    /// smaller counter example.
+    bool nested_;
+    /// \brief Active the nested bis search which produce a
+    /// smaller counter example.
+    const state* x_bis;
+    bool my_nested_;
+    bool accepted_path_;
+    int accepted_depth_;
+
+    ce::counter_example* counter_;
+    clock_t tps_;
+
+  };
+
+
+}
+
+#endif // SPOT_TGBAALGOS_NESTEDDFS_HH

src/tgbaalgos/reductgba_sim_del.cc

@@ -58,8 +58,6 @@ namespace spot
     lead_2_acc_all_ = false;
 
     seen_ = false;
-    //seen_ = new bool(false);
-    //bool_v[nb_node++] = seen_;
   }
 
   spoiler_node_delayed::~spoiler_node_delayed()
@@ -74,8 +72,6 @@ namespace spot
     // We take the max of the progress measure of the successor node
     // because we are on a spoiler.
 
-    //std::cout << "spoiler_node_delayed::set_win" << std::endl;
-
     if (lnode_succ->size() == 0)
       progress_measure_ = nb_spoiler_loose_ + 1;
 
@@ -125,7 +121,6 @@ namespace spot
   bool
   spoiler_node_delayed::compare(spoiler_node* n)
   {
-    //std::cout << "spoiler_node_delayed::compare" << std::endl;
     return (this->spoiler_node::compare(n) &&
 	    (acceptance_condition_visited_ ==
 	     dynamic_cast<spoiler_node_delayed*>(n)->
@@ -183,7 +178,6 @@ namespace spot
   bool
   spoiler_node_delayed::get_lead_2_acc_all()
   {
-    //std::cout << "spoiler_node_delayed::get_lead_2_acc_all" << std::endl;
     return lead_2_acc_all_;
   }
 
@@ -191,7 +185,6 @@ namespace spot
   bool
   spoiler_node_delayed::set_lead_2_acc_all(bdd acc)
   {
-    //std::cout << "spoiler_node_delayed::set_lead_2_acc_all" << std::endl;
     if (!seen_)
       {
 	seen_ = true;
@@ -201,7 +194,6 @@ namespace spot
       }
     else
       {
-	//seen_ = true;
 	if (acc == all_acc_cond)
 	  lead_2_acc_all_ = true;
       }
@@ -225,9 +217,6 @@ namespace spot
     lead_2_acc_all_ = false;
 
     seen_ = false;
-    //seen_ = new bool(false);
-    //bool_v[nb_node++] = seen_;
-
   }
 
   duplicator_node_delayed::~duplicator_node_delayed()
@@ -240,8 +229,6 @@ namespace spot
     // We take the min of the progress measure of the successor node
     // because we are on a duplicator.
 
-    //std::cout << "duplicator_node_delayed::set_win" << std::endl;
-
     if (lnode_succ->size() == 0)
       progress_measure_ = nb_spoiler_loose_ + 1;
 
@@ -251,11 +238,14 @@ namespace spot
     bool change;
     int tmpmin = 0;
     int tmp = 0;
+    int tmpminwin = -1;
     sn_v::iterator i = lnode_succ->begin();
     if (i != lnode_succ->end())
       {
 	tmpmin =
 	  dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
+	if (dynamic_cast<spoiler_node_delayed*>(*i)->get_lead_2_acc_all())
+	  tmpminwin = tmpmin;
 	++i;
       }
     for (; i != lnode_succ->end(); ++i)
@@ -263,7 +253,12 @@ namespace spot
 	tmp = dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
 	if (tmp < tmpmin)
 	  tmpmin = tmp;
+	if (dynamic_cast<spoiler_node_delayed*>(*i)->get_lead_2_acc_all() &&
+	    (tmp > tmpminwin))
+	  tmpminwin = tmp;
       }
+    if (tmpminwin != -1)
+      tmpmin = tmpminwin;
 
     change = (progress_measure_ < tmpmin);
     progress_measure_ = tmpmin;
@@ -280,7 +275,14 @@ namespace spot
        << " [shape=box, label=\"("
        << a->format_state(sc_->first)
        << ", "
-       << a->format_state(sc_->second);
+       << a->format_state(sc_->second)
+       << ", ";
+    if (label_ == bddfalse)
+      os << "0";
+    else if (label_ == bddtrue)
+      os << "1";
+    else
+      bdd_print_acc(os, a->get_dict(), label_);
     //<< ", ";
     //bdd_print_acc(os, a->get_dict(), acc_);
     os << ")"
@@ -315,14 +317,12 @@ namespace spot
   bool
   duplicator_node_delayed::get_lead_2_acc_all()
   {
-    //std::cout << "duplicator_node_delayed::get_lead_2_acc_all" << std::endl;
     return lead_2_acc_all_;
   }
 
   bool
   duplicator_node_delayed::set_lead_2_acc_all(bdd acc)
   {
-    //std::cout << "duplicator_node_delayed::set_lead_2_acc_all" << std::endl;
     acc |= acc_;
     if (!seen_)
       {
@@ -397,20 +397,14 @@ namespace spot
   build_recurse_successor_spoiler(spoiler_node* sn,
 				  std::ostringstream& os)
   {
-    //std::cout << os.str() << "build_recurse_successor_spoiler : begin"
-    //<< std::endl;
-
     // FIXME
     if (sn == 0)
       return;
 
     tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());
 
-    //int i = 0;
     for (si->first(); !si->done(); si->next())
       {
-	//std::cout << "transition " << i++ << std::endl;
-
 	bdd btmp = si->current_acceptance_conditions() |
 	  dynamic_cast<spoiler_node_delayed*>(sn)->
 	  get_acceptance_condition_visited();
@@ -445,9 +439,6 @@ namespace spot
       }
 
     delete si;
-
-    //std::cout << os.str() << "build_recurse_successor_spoiler : end"
-    //<< std::endl;
   }
 
   void
@@ -456,43 +447,15 @@ namespace spot
 				     spoiler_node* ,
 				     std::ostringstream& os)
   {
-    /*
-    std::cout << os.str() << "build_recurse_successor_duplicator : begin"
-	      << std::endl;
-    */
-
     tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node());
 
     for (si->first(); !si->done(); si->next())
       {
 
-	/*
-	  std::cout << automata_->format_state(dn->get_spoiler_node())
-	  << std::endl;
-	  std::cout << automata_->format_state(dn->get_duplicator_node())
-	  << std::endl;
-	*/
-
-	/*
-	bdd_print_acc(std::cout,
-		      automata_->get_dict(),
-		      si->current_condition());
-	std::cout << " // ";
-	bdd_print_acc(std::cout,
-		      automata_->get_dict(),
-		      dn->get_label());
-	std::cout << " // ";
-	bdd_print_acc(std::cout,
-		      automata_->get_dict(),
-		      si->current_condition() | !dn->get_label());
-	std::cout << std::endl;
-	*/
-
 	// if si->current_condition() doesn't implies dn->get_label()
 	// then duplicator can't play.
 	if ((si->current_condition() | !dn->get_label()) != bddtrue)
 	  {
-	    //std::cout << "doesn't implies" << std::endl;
 	    continue;
 	  }
 
@@ -528,11 +491,6 @@ namespace spot
       }
 
     delete si;
-
-    /*
-    std::cout << os.str() << "build_recurse_successor_duplicator : end"
-	      << std::endl;
-    */
   }
 
   duplicator_node_delayed*
@@ -600,41 +558,45 @@ namespace spot
   void
   parity_game_graph_delayed::lift()
   {
-    // TEST of the hash_map of node
-    /*
-    for (Sgi::vector<duplicator_node*>::iterator i
-	   = duplicator_vertice_.begin();
-	 i != duplicator_vertice_.end(); ++i)
-      seen_node_[*i] = 1;
-
-    for (Sgi::vector<spoiler_node*>::iterator i
-	   = spoiler_vertice_.begin();
-	 i != spoiler_vertice_.end(); ++i)
-      seen_node_[*i] = 1;
-    */
-    //
-
-
     // Before the lift we compute each vertices
     // to know if he belong to a all accepting cycle
     // of the graph.
-    /* FIXME
+
     if (this->nb_set_acc_cond() > 1)
-      for (Sgi::vector<duplicator_node*>::iterator i
+      {
-	     = duplicator_vertice_.begin();
+	for (Sgi::vector<duplicator_node*>::iterator i
-	   i != duplicator_vertice_.end(); ++i)
+	       = duplicator_vertice_.begin();
-	{
+	     i != duplicator_vertice_.end(); ++i)
-	  for (Sgi::vector<duplicator_node*>::iterator i2
+	  {
-		 = duplicator_vertice_.begin();
+	    /*
-	       i2 != duplicator_vertice_.end(); ++i2)
+	    for (Sgi::vector<duplicator_node*>::iterator i2
-	    dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
+		   = duplicator_vertice_.begin();
-	  for (Sgi::vector<spoiler_node*>::iterator i3
+		 i2 != duplicator_vertice_.end(); ++i2)
-		 = spoiler_vertice_.begin();
+	      dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
-	       i3 != spoiler_vertice_.end(); ++i3)
+	    for (Sgi::vector<spoiler_node*>::iterator i3
-	    dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
+		   = spoiler_vertice_.begin();
-	  dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all();
+		 i3 != spoiler_vertice_.end(); ++i3)
-	}
+	      dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
-    */
+	    */
+	    dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all();
+	  }
+	for (Sgi::vector<spoiler_node*>::iterator i
+	       = spoiler_vertice_.begin();
+	     i != spoiler_vertice_.end(); ++i)
+	  {
+	    /*
+	    for (Sgi::vector<duplicator_node*>::iterator i2
+		   = duplicator_vertice_.begin();
+		 i2 != duplicator_vertice_.end(); ++i2)
+	      dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
+	    for (Sgi::vector<spoiler_node*>::iterator i3
+		   = spoiler_vertice_.begin();
+		 i3 != spoiler_vertice_.end(); ++i3)
+	      dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
+	    */
+	    dynamic_cast<spoiler_node_delayed*>(*i)->set_lead_2_acc_all();
+	  }
+      }
 
     // Jurdzinski's algorithm
     //int iter = 0;
@@ -667,12 +629,17 @@ namespace spot
     state_couple* p = 0;
     seen_map::iterator j;
 
+    if (this->nb_set_acc_cond() > 1)
+      return rel;
+
     for (Sgi::vector<spoiler_node*>::iterator i
 	   = spoiler_vertice_.begin();
 	 i != spoiler_vertice_.end(); ++i)
       {
-	if (dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure()
+	if ((dynamic_cast<spoiler_node_delayed*>(*i)->get_progress_measure()
-	     < nb_spoiler_loose_ + 1)
+	     < nb_spoiler_loose_ + 1) &&
+	    (dynamic_cast<spoiler_node_delayed*>(*i)
+	     ->get_acceptance_condition_visited() == bddfalse))
 	  {
 	    p = new state_couple((*i)->get_spoiler_node(),
 				 (*i)->get_duplicator_node());
@@ -702,18 +669,8 @@ namespace spot
     : parity_game_graph(a)
   {
     nb_spoiler_loose_ = 0;
-
-    /* FIXME
-       if (this->nb_set_acc_cond() > 1)
-       return;
-    */
-
-    //std::cout << "build couple" << std::endl;
     this->build_graph();
-    //std::cout << "lift begin : " << nb_spoiler_loose_ << std::endl;
     this->lift();
-    //std::cout << "lift end : " << nb_spoiler_loose_ << std::endl;
-    //std::cout << "END" << std::endl;
   }
 
   ///////////////////////////////////////////

src/tgbaalgos/tarjan_on_fly.cc

@@ -0,0 +1,258 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "tgbaalgos/tarjan_on_fly.hh"
+
+
+namespace spot
+{
+
+  tarjan_on_fly::tarjan_on_fly(const tgba_tba_proxy *a)
+    : a(a), x(0)
+  {
+  }
+
+  tarjan_on_fly::~tarjan_on_fly()
+  {
+    for (stack_type::iterator i = stack.begin();
+	 i != stack.end(); ++i)
+      {
+	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();
+
+    top = dftop = -1;
+    violation = false;
+
+    const state* s = a->get_init_state();
+    push(s);
+
+    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;
+	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;
+	if (!iter->done())
+	  {
+	    succ = iter->current_state();
+	    if (h.find(succ) == h.end())
+	      push(succ);
+	    else
+	      {
+		int pos = in_stack(succ);
+		delete succ;
+		if (pos != -1) // succ is in stack
+		  lowlinkupdate(dftop, pos);
+	      }
+	  }
+	else
+	  pop();
+      }
+
+    tps_ = clock();
+    if (violation)
+      return build_counter();
+
+    //std::cout << "NO COUNTER EXAMPLE FOUND" << std::endl;
+
+    return 0;
+  }
+
+  void
+  tarjan_on_fly::push(const state* s)
+  {
+    std::cout << "tarjan_on_fly::push() : "
+	      << a->format_state(s) << " : " << std::endl;
+
+    h[s] = 1;
+    top++;
+
+    struct_state ss = { s, 0, top, dftop, 0, 0 };
+
+    if (a->state_is_accepting(s))
+      {
+	ss.acc = top;
+	x = s; // FIXME
+      }
+    else if (dftop >= 0)
+      ss.acc = stack[dftop].acc;
+    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;
+	*/
+
+      }
+    else
+      {
+	std::cout << "INS" << std::endl;
+	stack.push_back(ss);
+      }
+
+    dftop = top;
+  }
+
+  void
+  tarjan_on_fly::pop()
+  {
+    std::cout << "tarjan_on_fly::pop()" << std::endl;
+
+    int p = stack[dftop].pre;
+
+    if (p >= 0)
+      lowlinkupdate(p, dftop);
+
+    if (stack[dftop].lowlink == dftop)
+      top = dftop - 1;
+
+    dftop = p;
+  }
+
+  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;
+      }
+  }
+
+  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)
+      if (s->compare((*i).s) == 0)
+	break;
+
+    if (i == stack.end())
+      return -1;
+
+    return n;
+  }
+
+  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;
+    for (i = stack.begin(); i != stack.end(); ++i)
+      {
+	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()));
+      }
+
+    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()));
+      }
+
+    return ce;
+  }
+
+  std::ostream&
+  tarjan_on_fly::print_stat(std::ostream& os) const
+  {
+    int ce_size = 0;
+    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;
+    return os;
+  }
+
+}

src/tgbaalgos/tarjan_on_fly.hh

@@ -0,0 +1,94 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_TARJAN_ON_FLY_HH
+# define SPOT_TGBAALGOS_TARJAN_ON_FLY_HH
+
+#include "misc/hash.hh"
+#include <list>
+#include <utility>
+#include <ostream>
+#include "tgba/tgbatba.hh"
+//#include "tgba/bddprint.hh"
+#include "tgbaalgos/minimalce.hh"
+
+namespace spot
+{
+
+  class tarjan_on_fly: public emptyness_search
+  {
+
+  public:
+
+    tarjan_on_fly(const tgba_tba_proxy *a);
+    virtual ~tarjan_on_fly();
+
+    /// \brief Find a counter example.
+    virtual ce::counter_example* check();
+
+    /// \brief Print Stat.
+    std::ostream& print_stat(std::ostream& os) const;
+
+  private:
+
+    struct struct_state
+    {
+      const state* s;
+      tgba_succ_iterator* lasttr;
+      int lowlink;
+      int pre;
+      int acc;
+
+      int pos;
+    };
+
+    //typedef std::pair<int, tgba_succ_iterator*> state_iter_pair;
+    typedef Sgi::hash_map<const state*, int,
+			  state_ptr_hash, state_ptr_equal> hash_type;
+    hash_type h;		///< Map of visited states.
+
+
+    //typedef std::pair<const state*, struct_state> pair_type;
+    typedef std::vector<struct_state> stack_type;
+    stack_type stack;		///< Stack of visited states on the path.
+
+    const tgba_tba_proxy* a;	///< The automata to check.
+
+    int top;
+    int dftop;
+    bool violation;
+
+    const state* x;
+    ce::counter_example* ce;
+
+    void push(const state* s);
+    void pop();
+    void lowlinkupdate(int f, int t);
+    int in_stack(const state* s) const;
+
+    ce::counter_example* build_counter();
+    clock_t tps_;
+
+  };
+
+}
+
+#endif // SPOT_TGBAALGOS_MINIMALCE_HH

src/tgbatest/emptchk.test

@@ -27,6 +27,13 @@ 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 -e "$1"
   run 0 ./ltl2tgba -e -D "$1"
   run 0 ./ltl2tgba -e -f "$1"
@@ -35,12 +42,19 @@ expect_ce()
   run 0 ./ltl2tgba -e2 -D "$1"
   run 0 ./ltl2tgba -e2 -f "$1"
   run 0 ./ltl2tgba -e2 -f -D "$1"
-  run 0 ./ltl2tgba -m "$1"
+  run 0 ./ltl2tgba -mold "$1"
-  run 0 ./ltl2tgba -m -f "$1"
+  run 0 ./ltl2tgba -mold -f "$1"
 }
 
 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 -E "$1"
   run 0 ./ltl2tgba -E -D "$1"
   run 0 ./ltl2tgba -E -f "$1"
@@ -53,6 +67,9 @@ 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 'a'
 expect_ce 'a U b'
 expect_ce 'X a'

src/tgbatest/ltl2tgba.cc

@@ -35,6 +35,10 @@
 #include "tgbaalgos/lbtt.hh"
 #include "tgba/tgbatba.hh"
 #include "tgbaalgos/magic.hh"
+#include "tgbaalgos/nesteddfs.hh"
+#include "tgbaalgos/colordfs.hh"
+#include "tgbaalgos/tarjan_on_fly.hh"
+//#include "tgbaalgos/minimalce.hh"
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/gtec/ce.hh"
 #include "tgbaparse/public.hh"
@@ -51,67 +55,95 @@ syntax(char* prog)
             << "       "<< prog << " -X [OPTIONS...] file" << std::endl
 	    << std::endl
 	    << "Options:" << std::endl
-	    << "  -a   display the acceptance_conditions BDD, not the "
+	    << "  -a    display the acceptance_conditions BDD, not the "
 	    << "reachability graph"
 	    << std::endl
-	    << "  -A   same as -a, but as a set" << std::endl
+	    << "  -A    same as -a, but as a set" << std::endl
-	    << "  -d   turn on traces during parsing" << std::endl
+	    << "  -c    color-search (implies -D), expect a counter-example"
-	    << "  -D   degeneralize the automaton" << std::endl
-	    << "  -e   emptiness-check (Couvreur), expect and compute "
-	    << "a counter-example" << std::endl
-	    << "  -e2  emptiness-check (Couvreur variant), expect and compute "
-	    << "a counter-example" << std::endl
-	    << "  -E   emptiness-check (Couvreur), expect no counter-example "
 	    << std::endl
-	    << "  -E2  emptiness-check (Couvreur variant), expect no "
+	    << "  -C    color-search (implies -D), expect no counter-example"
+	    << std::endl
+	    << "  -d    turn on traces during parsing" << std::endl
+	    << "  -D    degeneralize the automaton" << std::endl
+	    << "  -e    emptiness-check (Couvreur), expect and compute "
+	    << "a counter-example" << std::endl
+	    << "  -e2   emptiness-check (Couvreur variant), expect and compute "
+	    << "a counter-example" << std::endl
+	    << "  -E    emptiness-check (Couvreur), expect no counter-example "
+	    << std::endl
+	    << "  -E2   emptiness-check (Couvreur variant), expect no "
 	    << "counter-example " << std::endl
-            << "  -f   use Couvreur's FM algorithm for translation"
+            << "  -f    use Couvreur's FM algorithm for translation"
 	    << std::endl
-            << "  -F   read the formula from the file" << std::endl
+            << "  -F    read the formula from the file" << std::endl
-            << "  -L   fair-loop approximation (implies -f)" << std::endl
+            << "  -L    fair-loop approximation (implies -f)" << std::endl
-	    << "  -m   magic-search (implies -D), expect a counter-example"
+	    << "  -m    magic-search (implies -D), expect a counter-example"
 	    << std::endl
-	    << "  -M   magic-search (implies -D), expect no counter-example"
+	    << "  -ms   minmimal-search (implies -D), expect a counter-example"
 	    << std::endl
-	    << "  -n   same as -m, but display more counter-examples"
+	    << "  -mold magic-search (implies -D), expect a counter-example"
 	    << std::endl
-	    << "  -N   display the never clain for Spin "
+	    << "  -M    magic-search (implies -D), expect no counter-example"
+	    << std::endl
+	    << "  -Mold magic-search (implies -D), expect no counter-example"
+	    << std::endl
+	    << "  -ndfs nesteddfs-search (implies -D), expect a "
+	    << "counter-example"
+	    << std::endl
+	    << "  -Ndfs nesteddfs-search (implies -D), expect no "
+	    << "counter-example"
+	    << std::endl
+	    << "  -ndfs2 modify-nesteddfs-search (implies -D), "
+	    << "expect a counter-example"
+	    << std::endl
+	    << "  -Ndfs2 modify-nesteddfs-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
-            << "  -p   branching postponement (implies -f)" << std::endl
+            << "  -p    branching postponement (implies -f)" << std::endl
-	    << "  -r   display the relation BDD, not the reachability graph"
+	    << "  -r    display the relation BDD, not the reachability graph"
 	    << std::endl
-	    << "  -r1  reduce formula using basic rewriting" << std::endl
+	    << "  -r1   reduce formula using basic rewriting" << std::endl
-	    << "  -r2  reduce formula using class of eventuality and "
+	    << "  -r2   reduce formula using class of eventuality and "
 	    << "and universality" << std::endl
-	    << "  -r3  reduce formula using implication between "
+	    << "  -r3   reduce formula using implication between "
 	    << "sub-formulae" << std::endl
-	    << "  -r4  reduce formula using all rules" << std::endl
+	    << "  -r4   reduce formula using all rules" << std::endl
-	    << "  -rd  display the reduce formula" << std::endl
+	    << "  -rd   display the reduce formula" << std::endl
-	    << "  -R   same as -r, but as a set" << std::endl
+	    << "  -R    same as -r, but as a set" << std::endl
-	    << "  -R1  use direct simulation to reduce the automata "
+	    << "  -R1   use direct simulation to reduce the automata "
 	    << "(use -L for more reduction)"
 	    << std::endl
-	    << "  -R2  use delayed simulation to reduce the automata "
+	    << "  -R2   use delayed simulation to reduce the automata "
 	    << "(use -L for more reduction)"
 	    << std::endl
-	    << "  -R3  use SCC to reduce the automata"
+	    << "  -R3   use SCC to reduce the automata"
 	    << std::endl
-	    << "  -Rd  display the simulation relation"
+	    << "  -Rd   display the simulation relation"
 	    << std::endl
-	    << "  -RD  display the parity game (dot format)"
+	    << "  -RD   display the parity game (dot format)"
 	    << std::endl
-	    << "  -s   convert to explicit automata, and number states "
+	    << "  -s    convert to explicit automata, and number states "
 	    << "in DFS order" << std::endl
-	    << "  -S   convert to explicit automata, and number states "
+	    << "  -S    convert to explicit automata, and number states "
 	    << "in BFS order" << std::endl
-	    << "  -t   display reachable states in LBTT's format" << std::endl
+	    << "  -t    display reachable states in LBTT's format" << std::endl
-	    << "  -v   display the BDD variables used by the automaton"
+	    << "  -T    display reachable states in LBTT's format w/o "
+	    << "acceptance conditions" << std::endl
+	    << "  -tj   tarjan-on-fly (implies -D), expect a counter-example"
 	    << std::endl
-            << "  -x   try to produce a more deterministic automaton "
+	    << "  -TJ   tarjan-on-fly (implies -D), expect no counter-example"
+	    << std::endl
+	    << "  -v    display the BDD variables used by the automaton"
+	    << std::endl
+            << "  -x    try to produce a more deterministic automata "
 	    << "(implies -f)" << std::endl
-	    << "  -X   do not compute an automaton, read it from a file"
+	    << "  -X    do not compute an automaton, read it from a file"
 	    << std::endl
-	    << "  -y   do not merge states with same symbolic representation "
+	    << "  -y    do not merge states with same symbolic representation "
 	    << "(implies -f)" << std::endl;
   exit(2);
 }
@@ -129,7 +161,12 @@ main(int argc, char** argv)
   bool file_opt = false;
   int output = 0;
   int formula_index = 0;
-  enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
+  enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld,
+	 NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
+	 TarjanOnFly, MinimalSearch} 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;
   bool expect_counter_example = false;
@@ -157,6 +194,22 @@ main(int argc, char** argv)
 	{
 	  output = 4;
 	}
+      else if (!strcmp(argv[formula_index], "-c"))
+	{
+	  echeck = ColorDFSSearch;
+	  //opt_search = 0;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	  magic_many = false;
+	}
+      else if (!strcmp(argv[formula_index], "-C"))
+	{
+	  echeck = ColorDFSSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
       else if (!strcmp(argv[formula_index], "-d"))
 	{
 	  debug_opt = true;
@@ -202,23 +255,92 @@ main(int argc, char** argv)
 	  fair_loop_approx = true;
 	  fm_opt = true;
 	}
-      else if (!strcmp(argv[formula_index], "-m"))
+      else if (!strcmp(argv[formula_index], "-mold"))
 	{
-	  echeck = MagicSearch;
+	  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;
+	}
       else if (!strcmp(argv[formula_index], "-M"))
 	{
+	  opt_nested_search = spot::magic;
 	  echeck = MagicSearch;
 	  degeneralize_opt = true;
 	  expect_counter_example = false;
 	  output = -1;
 	}
+      else if (!strcmp(argv[formula_index], "-Ms"))
+	{
+	  echeck = MinimalSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  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 = 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;
+	  output = -1;
+	}
       else if (!strcmp(argv[formula_index], "-n"))
 	{
-	  echeck = MagicSearch;
+	  echeck = MagicSearchOld;
 	  degeneralize_opt = true;
 	  expect_counter_example = true;
 	  output = -1;
@@ -260,10 +382,12 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[formula_index], "-R1"))
 	{
+	  //degeneralize_opt = true; // FIXME
 	  reduc_aut |= spot::Reduce_Dir_Sim;
 	}
       else if (!strcmp(argv[formula_index], "-R2"))
 	{
+	  //degeneralize_opt = true; // FIXME
 	  reduc_aut |= spot::Reduce_Del_Sim;
 	}
       else if (!strcmp(argv[formula_index], "-R3"))
@@ -294,6 +418,20 @@ main(int argc, char** argv)
 	{
 	  output = 6;
 	}
+      else if (!strcmp(argv[formula_index], "-tj"))
+	{
+	  echeck = TarjanOnFly;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-TJ"))
+	{
+	  echeck = TarjanOnFly;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
       else if (!strcmp(argv[formula_index], "-v"))
 	{
 	  output = 5;
@@ -497,6 +635,7 @@ main(int argc, char** argv)
 	{
 	case None:
 	  break;
+
 	case Couvreur:
 	case Couvreur2:
 	  {
@@ -505,9 +644,7 @@ main(int argc, char** argv)
 	      ec = new spot::emptiness_check(a);
 	    else
 	      ec = new spot::emptiness_check_shy(a);
-
 	    bool res = ec->check();
-
 	    if (expect_counter_example)
 	      {
 		if (res)
@@ -517,7 +654,12 @@ main(int argc, char** argv)
 		    break;
 		  }
 		spot::counter_example ce(ec->result());
-		ce.print_result(std::cout);
+		//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;
 	      }
 	    else
 	      {
@@ -526,7 +668,8 @@ main(int argc, char** argv)
 	    delete ec;
 	  }
 	  break;
-	case MagicSearch:
+
+	case MagicSearchOld:
 	  {
 	    spot::magic_search ms(degeneralized);
 	    bool res = ms.check();
@@ -547,8 +690,68 @@ main(int argc, char** argv)
 	      }
 	  }
 	  break;
+
+	case ColorDFSSearch:
+	  es = new spot::colordfs_search(degeneralized);
+	  break;
+
+	case TarjanOnFly:
+	  es = new spot::tarjan_on_fly(degeneralized);
+	  break;
+
+	case MinimalSearch:
+	  es = new spot::minimalce_search(degeneralized);
+	  break;
+
+	case MagicSearch:
+	case NestedDFSSearch:
+	case NestedDFSSearchModify:
+	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
+	  break;
+
 	}
 
+      if (es)
+	{
+	  spot::ce::counter_example* res = es->check();
+	  if (expect_counter_example)
+	    {
+	      do
+		{
+		  if (!res)
+		    {
+		      exit_code = 1;
+		      break;
+		    }
+		  std::cout << "CE : " << std::endl
+			    << "     size : " << res->size()
+			    << std::endl;
+		  spot::tgba* aut = res->ce2tgba();
+		  //spot::dotty_reachable(std::cout, aut);
+		  res->print(std::cout);
+		  es->print_stat(std::cout);
+		  delete aut;
+		  delete res;
+		  res = 0;
+		}
+	      while (magic_many && (res = es->check()));
+	    }
+	  else if (res)
+	    {
+	      exit_code = res->size();
+	      std::cout << "res->size ?? : " << exit_code << std::endl;
+	    }
+	  else
+	    {
+	      exit_code = (res != 0);
+	      std::cout << "res != 0 ?? : " << exit_code << std::endl;
+	    }
+	  if (res)
+	    delete res;
+	}
+
+      if (es)
+	delete es;
       if (f)
         spot::ltl::destroy(f);
       if (expl)