Better documentation for print_tgba_run.

* src/tgbaalgos/emptiness.hh (print_tgba_run): Reword the
documentation after a report from Nikos Gorogiannis.

ChangeLog

@@ -1,3 +1,10 @@
+2011-10-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Better documentation for print_tgba_run.
+
+	* src/tgbaalgos/emptiness.hh (print_tgba_run): Reword the
+	documentation after a report from Nikos Gorogiannis.
+
 2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* iface/dve2/finite.test: Swap -e and -E after change from 2011-07-26.

THANKS

@@ -7,6 +7,7 @@ Jean-Michel Ilié
 Kristin Y. Rozier
 Martin Dieguez Lodeiro
 Michael Weber
+Nikos Gorogiannis
 Rüdiger Ehlers
 Silien Hong
 Tomáš Babiak

src/tgbaalgos/emptiness.hh

@@ -1,4 +1,6 @@
-// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
+// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -273,19 +275,18 @@ namespace spot
 
   /// \brief Display a tgba_run.
   ///
-  /// Output the prefix and cycle of the tgba_run \a run, even if it
+  /// Output the prefix and cycle parts of the tgba_run \a run on \a os.
-  /// does not corresponds to an actual run of the automaton \a a.
-  /// This is unlike replay_tgba_run(), which will ensure the run
-  /// actually exist in the automaton (and will display any transition
-  /// annotation).
   ///
-  /// (\a a is used here only to format states and transitions.)
+  /// The automaton \a a is used only to format the states, and
+  /// to know how to print the BDDs describing the conditions and
+  /// acceptance conditions of the run; it is <b>not</b> used to
+  /// replay the run.  In other words this function will work even if
+  /// the tgba_run you are trying to print appears to connect states
+  /// of \a a that are not connected.
   ///
-  /// Output the prefix and cycle of the tgba_run \a run, even if it
-  /// does not corresponds to an actual run of the automaton \a a.
   /// This is unlike replay_tgba_run(), which will ensure the run
-  /// actually exist in the automaton (and will display any transition
+  /// actually exists in the automaton (and will also display any
-  /// annotation).
+  /// transition annotation).
   std::ostream& print_tgba_run(std::ostream& os,
                                const tgba* a,
                                const tgba_run* run);