* src/tgbaalgos/replayrun.hh,

src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
option to decide whether the output should look like that of
print_tgba_run() or a complete debug trace.
* src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with
debug=true.

ChangeLog

@@ -1,5 +1,12 @@
 2004-11-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/replayrun.hh,
+	src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
+	option to decide whether the output should look like that of
+	print_tgba_run() or a complete debug trace.
+	* src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with
+	debug=true.
+
 	* iface/gspn/ltlgspn.cc (main): Adjust to recent changes to
 	src/tgbaalgos/magic.cc, call explicit_magic_search() instead of
 	building a spot::magic_search.

src/tgbaalgos/replayrun.cc

@@ -41,7 +41,8 @@ namespace spot
   }
 
   bool
-  replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run)
+  replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run,
+		  bool debug)
   {
     const state* s = a->get_init_state();
     int serial = 1;
@@ -58,17 +59,22 @@ namespace spot
       {
 	l = &run->cycle;
 	in = "cycle";
+	if (!debug)
+	  os << "No prefix.\nCycle:" << std::endl;
       }
     else
       {
 	l = &run->prefix;
 	in = "prefix";
+	if (!debug)
+	  os << "Prefix:" << std::endl;
       }
 
     tgba_run::steps::const_iterator i = l->begin();
 
     if (s->compare(i->s))
       {
+	if (debug)
 	  os << "ERROR: First state of run (in " << in << "): "
 	     << a->format_state(i->s) << std::endl
 	     << "does not match initial state of automata: "
@@ -78,6 +84,8 @@ namespace spot
       }
 
     for (; i != l->end(); ++serial)
+      {
+	if (debug)
 	  {
 	    // Keep track of the serial associated to each state so we
 	    // can note duplicate states and make the replay easier to read.
@@ -96,9 +104,13 @@ namespace spot
 	      {
 		seen[s].insert(serial);
 	      }
-
+	    os << "state " << serial << " in " << in << msg.str() << ": ";
-	os << "state " << serial << " in " << in << msg.str() << ": "
+	  }
-	   << a->format_state(s) << std::endl;
+	else
+	  {
+	    os << "  ";
+	  }
+	os << a->format_state(s) << std::endl;
 
 	// expected outgoing transition
 	bdd label = i->label;
@@ -118,6 +130,8 @@ namespace spot
 		l = &run->cycle;
 		in = "cycle";
 		i = l->begin();
+		if (!debug)
+		  std::cout << "Cycle:" << std::endl;
 	      }
 	    next = l->begin()->s;
 	  }
@@ -143,6 +157,8 @@ namespace spot
 	      }
 	  }
 	if (j->done())
+	  {
+	    if (debug)
 	      {
 		os << "ERROR: no transition with label="
 		   << bdd_format_formula(a->get_dict(), label)
@@ -157,7 +173,8 @@ namespace spot
 		    const state* s2 = j->current_state();
 		    os << "  *";
 		    print_annotation(os, a, j);
-		os << " label=" << bdd_format_formula(a->get_dict(),
+		    os << " label="
+		       << bdd_format_formula(a->get_dict(),
 					     j->current_condition())
 		       << " and acc="
 		       << bdd_format_accset(a->get_dict(),
@@ -165,16 +182,29 @@ namespace spot
 		       << " going to " << a->format_state(s2) << std::endl;
 		    delete s2;
 		  }
+	      }
 	    delete j;
 	    delete s;
 	    return false;
 	  }
+	if (debug)
+	  {
 	    os << "transition";
 	    print_annotation(os, a, j);
 	    os << " with label="
 	       << bdd_format_formula(a->get_dict(), label)
 	       << " and acc=" << bdd_format_accset(a->get_dict(), acc)
 	       << std::endl;
+	  }
+	else
+	  {
+	    os << "  |  ";
+	    print_annotation(os, a, j);
+	    bdd_print_formula(os, a->get_dict(), label);
+	    os << "\t";
+	    bdd_print_accset(os, a->get_dict(), acc);
+	    os << std::endl;
+	  }
 	delete j;
 
 	// Sum acceptance conditions.
@@ -184,6 +214,7 @@ namespace spot
 	    if (!all_acc_seen && all_acc == expected_all_acc)
 	      {
 		all_acc_seen = true;
+		if (debug)
 		  os << "all acceptance conditions ("
 		     << bdd_format_accset(a->get_dict(), all_acc)
 		     << ") have been seen"
@@ -194,6 +225,7 @@ namespace spot
     delete s;
     if (all_acc != expected_all_acc)
       {
+	if (debug)
 	  os << "ERROR: The cycle's acceptance conditions ("
 	     << bdd_format_accset(a->get_dict(), all_acc) << ") do not"
 	     << std::endl

src/tgbaalgos/replayrun.hh

@@ -31,11 +31,20 @@ namespace spot
 
   /// \brief Replay a tgba_run on a tgba.
   ///
+  /// This is similar to print_tgba_run(), except that the run is
+  /// actually replayed on the automaton while it is printed.  Doing
+  /// so makes it possible to display transition annotations (returned
+  /// by spot::tgba::transition_annotation()).  The output will stop
+  /// if the run cannot be completed.
+  ///
   /// \param run the run to replay
   /// \param a the automata on which to replay that run
   /// \param os the stream on which the replay should be traced
+  /// \param debug if set the output will be more verbose and extra
+  ///              debugging informations will be output on failure
   /// \return true iff the run could be completed
-  bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run);
+  bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run,
+		       bool debug = false);
 }
 
 #endif // SPOT_TGBAALGOS_REPLAYRUN_HH

src/tgbatest/ltl2tgba.cc

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