From 57792ca541bcb3040be9567b763cd18219cf757c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 Nov 2004 14:09:37 +0000 Subject: [PATCH] * src/tgbaalgos/emptiness.hh (print_tgba_run): Document it. --- ChangeLog | 2 ++ src/tgbaalgos/emptiness.hh | 10 ++++++++++ 2 files changed, 12 insertions(+) diff --git a/ChangeLog b/ChangeLog index b332d59d1..2cd7d5c63 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,7 @@ 2004-11-10 Alexandre Duret-Lutz + * src/tgbaalgos/emptiness.hh (print_tgba_run): Document it. + * 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 diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 933000023..7dcdd4bd8 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -53,6 +53,16 @@ namespace spot }; class tgba; + + /// \brief Display a tgba_run. + /// + /// 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 + /// annotation). + /// + /// (\a a is used here only to format states and transitions.) std::ostream& print_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run);