A tgba can now annotate a transition (i.e., the position of a

tgba_succ_iterator) with some string.  This comes handy to
associate that transition to its high-level name.
* src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation):
New method.
* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product::transition_annotation): Implement it.
* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
(tgba_tba_proxy::transition_annotation): Likewise.
* src/tgbaalgos/replayrun.cc (print_annotation): New function.
(replay_tgba_run): Use it.

ChangeLog

@@ -1,5 +1,17 @@
 2004-10-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	A tgba can now annotate a transition (i.e., the position of a
+	tgba_succ_iterator) with some string.  This comes handy to
+	associate that transition to its high-level name.
+	* src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation):
+	New method.
+	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
+	(tgba_product::transition_annotation): Implement it.
+	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
+	(tgba_tba_proxy::transition_annotation): Likewise.
+	* src/tgbaalgos/replayrun.cc (print_annotation): New function.
+	(replay_tgba_run): Use it.
+
 	* src/tgbaalgos/gtec/gtec.cc,
 	src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
 	* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.

src/tgba/tgba.cc

@@ -69,4 +69,10 @@ namespace spot
     return 0;
   }
 
+  std::string
+  tgba::transition_annotation(const tgba_succ_iterator*) const
+  {
+    return "";
+  }
+
 }

src/tgba/tgba.hh

@@ -138,6 +138,16 @@ namespace spot
     /// who owns the state.
     virtual std::string format_state(const state* state) const = 0;
 
+    /// \brief Return a possible annotation for the transition
+    /// pointed to by the iterator.
+    ///
+    /// Implementing this function is optional; the default annotation
+    /// it the empty string.
+    ///
+    /// \param t a non-done tgba_succ_iterator for this automata
+    virtual std::string
+    transition_annotation(const tgba_succ_iterator* t) const;
+
     /// \brief Project a state on an automata.
     ///
     /// This converts \a s, into that corresponding spot::state for \a

src/tgba/tgbaproduct.cc

@@ -289,4 +289,19 @@ namespace spot
     return neg_acceptance_conditions_;
   }
 
+  std::string
+  tgba_product::transition_annotation(const tgba_succ_iterator* t) const
+  {
+    const tgba_succ_iterator_product* i =
+      dynamic_cast<const tgba_succ_iterator_product*>(t);
+    assert(i);
+    std::string left = left_->transition_annotation(i->left_);
+    std::string right = right_->transition_annotation(i->right_);
+    if (left == "")
+      return right;
+    if (right == "")
+      return left;
+    return "<" + left + ", " + right + ">";
+  }
+
 }

src/tgba/tgbaproduct.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -106,6 +106,7 @@ namespace spot
     bdd current_cond_;
     bdd left_neg_;
     bdd right_neg_;
+    friend class tgba_product;
   };
 
   /// \brief A lazy product.  (States are computed on the fly.)
@@ -131,6 +132,9 @@ namespace spot
 
     virtual std::string format_state(const state* state) const;
 
+    virtual std::string
+    transition_annotation(const tgba_succ_iterator* t) const;
+
     virtual state* project_state(const state* s, const tgba* t) const;
 
     virtual bdd all_acceptance_conditions() const;

src/tgba/tgbatba.cc

@@ -191,6 +191,7 @@ namespace spot
       const iterator expected_;
       const iterator end_;
       const bdd the_acceptance_cond_;
+      friend class tgba_tba_proxy;
     };
 
   } // anonymous
@@ -317,4 +318,13 @@ namespace spot
     return a_->support_variables(s->real_state());
   }
 
+  std::string
+  tgba_tba_proxy::transition_annotation(const tgba_succ_iterator* t) const
+  {
+    const tgba_tba_proxy_succ_iterator* i =
+      dynamic_cast<const tgba_tba_proxy_succ_iterator*>(t);
+    assert(i);
+    return a_->transition_annotation(i->it_);
+  }
+
 }

src/tgba/tgbatba.hh

@@ -65,6 +65,9 @@ namespace spot
 
     virtual state* project_state(const state* s, const tgba* t) const;
 
+    virtual std::string
+    transition_annotation(const tgba_succ_iterator* t) const;
+
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
 

src/tgbaalgos/replayrun.cc

@@ -27,6 +27,19 @@
 
 namespace spot
 {
+  namespace
+  {
+    void
+    print_annotation(std::ostream& os, const tgba* a,
+		     const tgba_succ_iterator* i)
+    {
+      std::string s = a->transition_annotation(i);
+      if (s == "")
+	return;
+      os << " " << s;
+    }
+  }
+
   bool
   replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run)
   {
@@ -66,6 +79,8 @@ namespace spot
 
     for (; i != l->end(); ++serial)
       {
+	// Keep track of the serial associated to each state so we
+	// can note duplicate states and make the replay easier to read.
 	state_map::iterator o = seen.find(s);
 	std::ostringstream msg;
 	if (o != seen.end())
@@ -140,8 +155,9 @@ namespace spot
 	    for (j->first(); !j->done(); j->next())
 	      {
 		const state* s2 = j->current_state();
-		os << "  * "
+		os << "  *";
-		   << "label=" << bdd_format_formula(a->get_dict(),
+		print_annotation(os, a, j);
+		os << " label=" << bdd_format_formula(a->get_dict(),
 						     j->current_condition())
 		   << " and acc="
 		   << bdd_format_accset(a->get_dict(),
@@ -152,7 +168,9 @@ namespace spot
 	    delete j;
 	    return false;
 	  }
-	os << "transition with label="
+	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;