From fb5ff901d0d1033df867530a62712c6d1bbf90c6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 27 May 2003 13:05:22 +0000 Subject: [PATCH] * src/tgba/bddprint.hh (bdd_format_set): New function. * src/tgba/bddprint.cc (bdd_format_set): Likewise. * src/tgba/state.hh: Add Doxygen comments. (state::compare): Take a state*, not a state&. (state_ptr_less_than): New functor. * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a state&. * src/tgba/statebdd.cc (state_bdd::compare): Likewise. * src/tgba/succiter.hh: Add Doxygen comments. * src/tgba/tgba.hh: Mention promises. (tgba::formate_state): New pure virtual method. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state): New method. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state): Likewise. * src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than and tgba::formate_state. --- ChangeLog | 21 ++++++++++++--- src/tgba/bddprint.cc | 21 ++++++++++----- src/tgba/bddprint.hh | 14 +++++----- src/tgba/state.hh | 45 +++++++++++++++++++++++-------- src/tgba/statebdd.cc | 12 +++------ src/tgba/statebdd.hh | 9 +++++-- src/tgba/succiter.hh | 53 +++++++++++++++++++++++++++++++++++-- src/tgba/tgba.hh | 14 +++++++++- src/tgba/tgbabddconcrete.cc | 9 +++++++ src/tgba/tgbabddconcrete.hh | 2 ++ src/tgbaalgos/dotty.cc | 27 ++++++++++++------- 11 files changed, 178 insertions(+), 49 deletions(-) diff --git a/ChangeLog b/ChangeLog index 6fd24a13e..d8b79b898 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,13 +1,28 @@ 2003-05-27 Alexandre Duret-Lutz + * src/tgba/bddprint.hh (bdd_format_set): New function. + * src/tgba/bddprint.cc (bdd_format_set): Likewise. + * src/tgba/state.hh: Add Doxygen comments. + (state::compare): Take a state*, not a state&. + (state_ptr_less_than): New functor. + * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a + state&. + * src/tgba/statebdd.cc (state_bdd::compare): Likewise. + * src/tgba/succiter.hh: Add Doxygen comments. + * src/tgba/tgba.hh: Mention promises. + (tgba::formate_state): New pure virtual method. + * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state): + New method. + * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state): + Likewise. + * src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than + and tgba::formate_state. + * src/tgba/succiter.hh (tgba_succ_iterator::current_state): Return a state*, not a state_bdd. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_state): Return a state_bdd*, not a state_bdd. - * src/tgba/state.hh (state::as_bdd): New abstract method. - * src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ... - * src/tgba/statebdd.cc (state_bdd::as_bdd): ... here. * src/tgba/tgba.hh: Add Doxygen comments. (tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state): diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index e02a2ebae..e8397ded6 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -1,3 +1,4 @@ +#include #include "bddprint.hh" #include "ltlvisit/tostring.hh" @@ -9,7 +10,7 @@ namespace spot static void print_handler(std::ostream& o, int var) { - tgba_bdd_dict::vf_map::const_iterator isi = + tgba_bdd_dict::vf_map::const_iterator isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) to_string(isi->second, o); @@ -42,9 +43,9 @@ namespace spot } } } - - std::ostream& + + std::ostream& bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b) { dict = &d; @@ -54,7 +55,15 @@ namespace spot return os; } - std::ostream& + std::string + bdd_format_set(const tgba_bdd_dict& d, bdd b) + { + std::ostringstream os; + bdd_print_set(os, d, b); + return os.str(); + } + + std::ostream& bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b) { dict = &d; @@ -63,8 +72,8 @@ namespace spot bdd_strm_hook(0); return os; } - - std::ostream& + + std::ostream& bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b) { dict = &d; diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index 42cfef456..5d4f1c1d0 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -1,20 +1,22 @@ #ifndef SPOT_TGBA_BDDPRINT_HH # define SPOT_TGBA_BDDPRINT_HH +#include #include #include "tgbabdddict.hh" #include namespace spot { - - std::ostream& bdd_print_set(std::ostream& os, + + std::ostream& bdd_print_set(std::ostream& os, + const tgba_bdd_dict& dict, bdd b); + std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b); + + std::ostream& bdd_print_dot(std::ostream& os, const tgba_bdd_dict& dict, bdd b); - std::ostream& bdd_print_dot(std::ostream& os, - const tgba_bdd_dict& dict, bdd b); - - std::ostream& bdd_print_table(std::ostream& os, + std::ostream& bdd_print_table(std::ostream& os, const tgba_bdd_dict& dict, bdd b); } diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 3d5d2ba44..608e6fb0c 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -5,25 +5,48 @@ namespace spot { + + /// \brief Abstract class for states. class state { public: - // Compares two states (that come from the same automaton). - // - // This method returns an integer less than, equal to, or greater - // than zero if THIS is found, respectively, to be less than, equal - // to, or greater than OTHER according to some implicit total order. - // - // This method should not be called to compare state from - // different automata. - virtual int compare(const state& other) const = 0; - - virtual bdd as_bdd() const = 0; + /// \brief Compares two states (that come from the same automaton). + /// + /// This method returns an integer less than, equal to, or greater + /// than zero if \a this is found, respectively, to be less than, equal + /// to, or greater than \a other according to some implicit total order. + /// + /// This method should not be called to compare states from + /// different automata. + /// + /// \sa spot::state_ptr_less_than + virtual int compare(const state* other) const = 0; virtual ~state() { } }; + + /// \brief Strict Weak Ordering for \c state*. + /// + /// This is meant to be used as a comparison functor for + /// STL \c map whose key are of type \c state*. + /// + /// For instance here is how one could declare + /// a map of \c state*. + /// \code + /// // Remember how many times each state has been visited. + /// std::map seen; + /// \endcode + struct state_ptr_less_than + { + bool + operator()(const state* left, const state *right) + { + return left->compare(right) < 0; + } + }; + } #endif // SPOT_TGBA_STATE_HH diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc index 4a6688eda..028eabb58 100644 --- a/src/tgba/statebdd.cc +++ b/src/tgba/statebdd.cc @@ -1,23 +1,17 @@ #include "statebdd.hh" +#include "bddprint.hh" #include namespace spot { int - state_bdd::compare(const state& other) const + state_bdd::compare(const state* other) const { // This method should not be called to compare states from different // automata, and all states from the same automaton will use the same // state class. - const state_bdd* o = dynamic_cast(&other); + const state_bdd* o = dynamic_cast(other); assert(o); return o->as_bdd().id() - state_.id(); } - - bdd - state_bdd::as_bdd() const - { - return state_; - } - } diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh index c721497f6..fdc84b0b6 100644 --- a/src/tgba/statebdd.hh +++ b/src/tgba/statebdd.hh @@ -14,8 +14,13 @@ namespace spot { } - virtual bdd as_bdd() const; - virtual int compare(const state& other) const; + bdd + as_bdd() const + { + return state_; + } + + virtual int compare(const state* other) const; protected: bdd state_; diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 0ff7e7e77..6d8643d76 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.hh @@ -6,6 +6,13 @@ namespace spot { + /// \brief Iterate over the successors of a state. + /// + /// This class provides the basic functionalities required to + /// iterate over the successors of a state, as well as querying + /// transition labels. Because transitions are never explicitely + /// encoded, labels (conditions and promises) can only be queried + /// while iterating over the successors. class tgba_succ_iterator { public: @@ -14,15 +21,57 @@ namespace spot { } - // iteration + /// \name Iteration + //@{ + + /// \brief Position the iterator on the first successor (if any). + /// + /// This method can be called several times to make multiple + /// passes over successors. + /// + /// \warning One should always call \c done() to + /// ensure there is a successor, even after \c first(). A + /// common trap is to assume that there is at least one + /// successor: this is wrong. virtual void first() = 0; + + /// \brief Jump to the next successor (if any). + /// + /// \warning Again, one should always call \c done() to ensure + /// there is a successor. virtual void next() = 0; + + /// \brief Check whether the iteration is finished. + /// + /// This function should be called after any call to \c first() + /// or \c next() and before any enquiry about the current state. + /// + /// The usual way to do this is with a \c for loop. + /// \code + /// for (s->first(); !s->done(); s->next()) + /// ... + /// \endcode virtual bool done() = 0; - // inspection + //@} + + /// \name Inspection + //@{ + + /// \brief Get the state of the current successor. + /// + /// Note that the same state may occur at different points + /// in the iteration. These actually correspond to the same + /// destination. It just means there were several transitions, + /// with different conditions or promises, leading to the + /// same state. virtual state* current_state() = 0; + /// \brief Get the condition on the transition leading to this successor. virtual bdd current_condition() = 0; + /// \brief Get the promise on the transition leading to this successor. virtual bdd current_promise() = 0; + + //@} }; } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 206912548..18013f446 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -20,6 +20,12 @@ namespace spot /// transitions), and a path can be accepted only if it traverse /// at least one transition of each set infinitely often. /// + /// Actually we do not really encode accepting sets but their + /// complement: promise sets. Formulae such as 'a U b' and + /// 'F b' make the promise to fulfil 'b' enventually. A path can + /// be accepted if for each promise it traverse infinitely often + /// a transition that does not make this promise. + /// /// Browsing such automaton can be achieved using two functions. /// \c get_init_state, and \c succ_iter. The former returns /// the initial state while the latter allows to explore the @@ -65,7 +71,13 @@ namespace spot /// may use the same BDD variable for different formula), /// or simply when printing. virtual const tgba_bdd_dict& get_dict() const = 0; - }; + + /// \brief Format the state as a string for printing. + /// + /// This formating is the responsability of the automata + /// who owns the state. + virtual std::string format_state(const state* state) const = 0; + }; } diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index a65b72d20..d2e38c9d5 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -1,4 +1,5 @@ #include "tgbabddconcrete.hh" +#include "bddprint.hh" namespace spot { @@ -45,6 +46,14 @@ namespace spot return new tgba_succ_iterator_concrete(data_, succ_set); } + std::string + tgba_bdd_concrete::format_state(const state* state) const + { + const state_bdd* s = dynamic_cast(state); + assert(s); + return bdd_format_set(dict_, s->as_bdd()); + } + const tgba_bdd_dict& tgba_bdd_concrete::get_dict() const { diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 97d5e6a07..312a10dae 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -21,6 +21,8 @@ namespace spot tgba_succ_iterator_concrete* succ_iter(const state* state) const; + std::string format_state(const state* state) const; + const tgba_bdd_dict& get_dict() const; const tgba_bdd_core_data& get_core_data() const; diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index c61b3d528..9db0d06b2 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -5,14 +5,13 @@ namespace spot { - typedef std::map seen_map; + typedef std::map seen_map; static bool dotty_state(std::ostream& os, const tgba& g, state* st, seen_map& m, int& node) { - bdd s = st->as_bdd(); - seen_map::iterator i = m.find(s.id()); + seen_map::iterator i = m.find(st); // Already drawn? if (i != m.end()) @@ -22,10 +21,10 @@ namespace spot } node = m.size() + 1; - m[s.id()] = node; + m[st] = node; - std::cout << " " << node << " [label=\""; - bdd_print_set(os, g.get_dict(), s) << "\"]" << std::endl; + os << " " << node << " [label=\"" + << g.format_state(st) << "\"]" << std::endl; return true; } @@ -44,8 +43,14 @@ namespace spot bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]" << std::endl; if (recurse) - dotty_rec(os, g, s, m, node); - delete s; + { + dotty_rec(os, g, s, m, node); + // Do not delete S, it is used as key in M. + } + else + { + delete s; + } } delete si; } @@ -63,7 +68,11 @@ namespace spot os << " 0 -> " << init << std::endl; dotty_rec(os, g, state, m, init); os << "}" << std::endl; - delete state; + + // Finally delete all states used as keys in m: + for (seen_map::iterator i = m.begin(); i != m.end(); ++i) + delete i->first; + return os; }