From 754d7064ae4b89ffa76f7352c23398f9a79a75a2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 29 Oct 2004 16:45:49 +0000 Subject: [PATCH] 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 | 12 ++++++++++++ src/tgba/tgba.cc | 6 ++++++ src/tgba/tgba.hh | 10 ++++++++++ src/tgba/tgbaproduct.cc | 15 +++++++++++++++ src/tgba/tgbaproduct.hh | 6 +++++- src/tgba/tgbatba.cc | 10 ++++++++++ src/tgba/tgbatba.hh | 3 +++ src/tgbaalgos/replayrun.cc | 24 +++++++++++++++++++++--- 8 files changed, 82 insertions(+), 4 deletions(-) diff --git a/ChangeLog b/ChangeLog index 8fd2b761e..502386768 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,17 @@ 2004-10-29 Alexandre Duret-Lutz + 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. diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 237b0ef9d..62663d951 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -69,4 +69,10 @@ namespace spot return 0; } + std::string + tgba::transition_annotation(const tgba_succ_iterator*) const + { + return ""; + } + } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 2d4009cfe..f9c613a83 100644 --- a/src/tgba/tgba.hh +++ b/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 diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 87f91d752..d6f3ce0df 100644 --- a/src/tgba/tgbaproduct.cc +++ b/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(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 + ">"; + } + } diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index ef809f4aa..a24c3b2d6 100644 --- a/src/tgba/tgbaproduct.hh +++ b/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; diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 7d92fa93c..394043533 100644 --- a/src/tgba/tgbatba.cc +++ b/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(t); + assert(i); + return a_->transition_annotation(i->it_); + } + } diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index b19b59234..4353d29d7 100644 --- a/src/tgba/tgbatba.hh +++ b/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; diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index f43a73be0..ff8235caa 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/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 << " * " - << "label=" << bdd_format_formula(a->get_dict(), + os << " *"; + 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;