* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,

couvreur99_check_result::complete_cycle,
couvreur99_check_result::accepting_path): Record conditions and
acceptance conditions in the accepting run.  Simplify the
todo BFS stack for accepting_run and complete_cycle.
* src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run
now everything works.
* src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose
when an outgoing transition is not found.

ChangeLog

@@ -1,3 +1,15 @@
+2004-10-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
+	couvreur99_check_result::complete_cycle,
+	couvreur99_check_result::accepting_path): Record conditions and
+	acceptance conditions in the accepting run.  Simplify the
+	todo BFS stack for accepting_run and complete_cycle.
+	* src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run
+	now everything works.
+	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose
+	when an outgoing transition is not found.
+
 2004-10-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search):

src/tgbaalgos/gtec/ce.cc

@@ -25,12 +25,6 @@
 
 namespace spot
 {
-  namespace
-  {
-    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
-    typedef std::pair<const state*, bdd> state_proposition;
-  }
-
   couvreur99_check_result::couvreur99_check_result
   (const couvreur99_check_status* ecs,
    const explicit_connected_component_factory* eccf)
@@ -89,30 +83,27 @@ namespace spot
     // first SCC, the starting state is the initial state of the
     // automaton.  The destination state is the closest state
     // from the next SCC.  This destination state becomes the
-    // starting state when building a path though the next SCC.
+    // starting state when building a path through the next SCC.
     for (int k = 0; k < comp_size - 1; ++k)
       {
 	// FIFO for the breadth-first search.
 	// (we are looking for the closest state in the next SCC.)
-	std::deque<pair_state_iter> todo;
+	std::deque<const state*> todo;
 
 	// Record the father of each state, while performing the BFS.
-	typedef std::map<const state*, const state*,
+	typedef std::map<const state*, tgba_run::step,
 	                 state_ptr_less_than> father_map;
 	father_map father;
 
 	// Initial state of the BFS.
 	const state* start = run_->prefix.back().s;
-	{
+	todo.push_back(start);
-	  tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
-	  todo.push_back(pair_state_iter(start, i));
-	}
 
 	while (!todo.empty())
 	  {
-	    const state* src = todo.front().first;
+	    const state* src = todo.front();
-	    tgba_succ_iterator* i = todo.front().second;
 	    todo.pop_front();
+	    tgba_succ_iterator* i = ecs_->aut->succ_iter(src);
 
 	    for (i->first(); !i->done(); i->next())
 	      {
@@ -129,26 +120,31 @@ namespace spot
 		      {
 			tgba_run::steps seq;
 
-			/// FIXME: Should compute label and acceptance
+			// The condition and acceptance conditions
-			/// condition.
+			// for the transition leaving H_DEST will
+			// be overwritten later when we know them.
+
 			tgba_run::step s = { h_dest, bddtrue, bddfalse };
 			seq.push_front(s);
-			while (src->compare(start))
+
+			// Now unwind our track until we reach START.
+			tgba_run::step t =
+			  { src,
+			    i->current_condition(),
+			    i->current_acceptance_conditions() };
+			while (t.s->compare(start))
 			  {
-			    /// FIXME: Should compute label and acceptance
+			    seq.push_front(t);
-			    /// condition.
+			    t = father[t.s];
-			    tgba_run::step s = { h_dest, bddtrue, bddfalse };
-			    seq.push_front(s);
-			    src = father[src];
 			  }
+			assert(!run_->prefix.empty());
+			run_->prefix.back() = t;
+
 			// Append SEQ to RUN_->PREFIX.
 			run_->prefix.splice(run_->prefix.end(), seq);
+
 			// Exit this BFS for this SCC.
-			while (!todo.empty())
+			todo.clear();
-			  {
-			    delete todo.front().second;
-			    todo.pop_front();
-			  }
 			break;
 		      }
 		    // Restrict the BFS to state inside the SCC.
@@ -158,9 +154,11 @@ namespace spot
 
 		if (father.find(h_dest) == father.end())
 		  {
-		    todo.push_back
+		    todo.push_back(h_dest);
-		      (pair_state_iter(h_dest, ecs_->aut->succ_iter(h_dest)));
+		    tgba_run::step s = { src,
-		    father[h_dest] = src;
+					 i->current_condition(),
+					 i->current_acceptance_conditions() };
+		    father[h_dest] = s;
 		  }
 	      }
 	    delete i;
@@ -202,22 +200,19 @@ namespace spot
 
     // Records backlinks to parent state during the BFS.
     // (This also stores the propositions of this link.)
-    std::map<const state*, state_proposition, state_ptr_less_than> father;
+    std::map<const state*, tgba_run::step, state_ptr_less_than> father;
 
     // BFS queue.
-    std::deque<pair_state_iter> todo;
+    std::deque<const state*> todo;
 
     // Initial state.
-    {
+    todo.push_back(from);
-      tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
-      todo.push_back(pair_state_iter(from, i));
-    }
 
     while (!todo.empty())
       {
-	const state* src = todo.front().first;
+	const state* src = todo.front();
-	tgba_succ_iterator* i = todo.front().second;
 	todo.pop_front();
+	tgba_succ_iterator* i = ecs_->aut->succ_iter(src);
 	for (i->first(); !i->done(); i->next())
 	  {
 	    const state* dest = i->current_state();
@@ -233,38 +228,31 @@ namespace spot
 	      continue;
 
 	    bdd cond = i->current_condition();
+	    bdd acc = i->current_acceptance_conditions();
+	    tgba_run::step s = { src, cond, acc };
 
 	    // If we have reached our destination, unwind the path
 	    // and populate RUN_->CYCLE.
 	    if (h_dest == to)
 	      {
 		tgba_run::steps p;
-		// FIXME: should compute acceptance condition.
+
-		tgba_run::step s = { h_dest, cond, bddfalse };
+		while (s.s != from)
-		p.push_front(s);
-		while (src != from)
 		  {
-		    const state_proposition& psi = father[src];
-		    // FIXME: should compute acceptance condition.
-		    tgba_run::step s = { src, psi.second, bddfalse };
 		    p.push_front(s);
-		    src = psi.first;
+		    s = father[s.s];
 		  }
+		p.push_front(s);
 		run_->cycle.splice(run_->cycle.end(), p);
 
 		// Exit the BFS, but release all iterators first.
-		while (!todo.empty())
+		todo.clear();
-		  {
-		    delete todo.front().second;
-		    todo.pop_front();
-		  }
 		break;
 	      }
 
 	    // Common case: record backlinks and continue BFS.
-	    todo.push_back(pair_state_iter(h_dest,
+	    todo.push_back(h_dest);
-					   ecs_->aut->succ_iter(h_dest)));
+	    father[h_dest] = s;
-	    father[h_dest] = state_proposition(src, cond);
 	  }
 	delete i;
       }
@@ -315,6 +303,8 @@ namespace spot
 	tgba_run::steps path;
 	// The best path seen so far.
 	tgba_run::steps best_path;
+	// The end state of the base path.
+	const state* best_end;
 	// The acceptance conditions traversed by BEST_PATH.
 	bdd best_acc = bddfalse;
 
@@ -348,8 +338,8 @@ namespace spot
 	      }
 
 	    bdd acc = iter->current_acceptance_conditions() | todo.top().acc;
-	    tgba_run::step st = { h_dest, iter->current_condition(),
+	    tgba_run::step st = { s, iter->current_condition(),
-				 iter->current_acceptance_conditions() };
+				  iter->current_acceptance_conditions() };
 	    path.push_back(st);
 
 	    // Advance iterator for next step.
@@ -403,6 +393,7 @@ namespace spot
 	    // The current path the best one.
 	    best_path = path;
 	    best_acc = acc;
+	    best_end = h_dest;
 
 	  backtrack_path:
 	    // Continue exploration from parent to find better paths.
@@ -420,7 +411,7 @@ namespace spot
 	// Prepare to find another path for the remaining acceptance
 	// conditions.
 	acc_to_traverse -= best_acc;
-	start = run_->cycle.back().s;
+	start = best_end;
       }
 
     // Complete the path so that it goes back to its beginning,

src/tgbaalgos/replayrun.cc

@@ -111,9 +111,22 @@ namespace spot
 	       << bdd_format_formula(a->get_dict(), label)
 	       << " and acc=" << bdd_format_accset(a->get_dict(), acc)
 	       << " leaving state " << serial
-	       << " and going to state "
+	       << " for state " << a->format_state(next)
-	       << a->format_state(next)
+	       << std::endl
-	       << std::endl;
+	       << "The following transitions leave state " << serial
+	       << ":" << std::endl;
+	    for (j->first(); !j->done(); j->next())
+	      {
+		const state* s2 = j->current_state();
+		os << "  * "
+		   << "label=" << bdd_format_formula(a->get_dict(),
+						     j->current_condition())
+		   << " and acc="
+		   << bdd_format_accset(a->get_dict(),
+					j->current_acceptance_conditions())
+		   << " going to " << a->format_state(s2) << std::endl;
+		delete s2;
+	      }
 	    delete j;
 	    return false;
 	  }

src/tgbatest/ltl2tgba.cc

@@ -581,8 +581,8 @@ main(int argc, char** argv)
 		  else
 		    {
 		      spot::print_tgba_run(std::cout, run, ec_a);
-		      // if (!spot::replay_tgba_run(std::cout, ec_a, run))
+		      if (!spot::replay_tgba_run(std::cout, ec_a, run))
-		      //   exit_code = 1;
+			exit_code = 1;
 		      delete run;
 		    }
 		}