alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/emptiness.hh (print_tgba_run): Document it.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-11-10 14:09:37 +00:00
parent 21e0e9bc18
commit 57792ca541
2 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
ChangeLog
View file

@ -1,5 +1,7 @@
2004-11-10 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptiness.hh (print_tgba_run): Document it.
* src/tgbaalgos/replayrun.hh, * src/tgbaalgos/replayrun.hh,
src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug' src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
option to decide whether the output should look like that of option to decide whether the output should look like that of

10
src/tgbaalgos/emptiness.hh
View file

@ -53,6 +53,16 @@ namespace spot
}; };
class tgba; 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, std::ostream& print_tgba_run(std::ostream& os,
const tgba* a, const tgba* a,
const tgba_run* run); const tgba_run* run);