diff --git a/ChangeLog b/ChangeLog
index c88b473c2..873685583 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Display transition annotations in dotty output.
+
+	* src/tgbaalgos/dotty.cc (process_link): Call
+	transition_annotation().  Reported by Nikos Gorogiannis.
+	* src/tgba/tgba.hh (transition_annotation): More documentation.
+	* NEWS: Mention this change.
+
 2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* NEWS: Add an entry for the previous fix.
diff --git a/NEWS b/NEWS
index 059590511..c9875ba4a 100644
--- a/NEWS
+++ b/NEWS
@@ -16,6 +16,9 @@ New in spot 0.7.1a:
       In that case, acceptance states are displayed with a double
       circle. ltl2tgba (both command line and on-line) Use it to display
       degeneralized automata.
+    - The dotty_reachable() function will also display transition
+      annotations (as returned by the tgba::transitition_annotation()).
+      This can be useful when displaying (small) state spaces.
     - Identifiers used to name atomic proposition can contain dots.
       E.g.: X.Y is now an atomic proposition, while it was understood
       as X&Y in previous versions.
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index 2aba2eaef..361aada38 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -157,10 +157,19 @@ namespace spot
     /// \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.
+    /// You may decide to use annotations when building a tgba class
+    /// that represents the state space of a model, for instance to
+    /// indicate how the tgba transitions relate to the original model
+    /// (e.g. the annotation could be the name of a PetriNet
+    /// transition, or the line number of some textual formalism).
     ///
-    /// \param t a non-done tgba_succ_iterator for this automata
+    /// Implementing this method is optional; the default annotation
+    /// is the empty string.
+    ///
+    /// This method is used for instance in dotty_reachable(),
+    /// and replay_tgba_run().
+    ///
+    /// \param t a non-done tgba_succ_iterator for this automaton
     virtual std::string
     transition_annotation(const tgba_succ_iterator* t) const;
 
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index 76a9363ab..919665a0a 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -100,6 +100,14 @@ namespace spot
 	  + bdd_format_accset(automata_->get_dict(),
 			      si->current_acceptance_conditions());
 
+	std::string s = automata_->transition_annotation(si);
+	if (!s.empty())
+	  {
+	    if (*label.rbegin() != '\n')
+	      label += '\n';
+	    label += s;
+	  }
+
 	os_ << "  " << in << " -> " << out << " "
 	    << dd_->link_decl(automata_, in_s, in, out_s, out, si,
 			      escape_str(label))