From 3e7debe53e834f17823542118949c7a88e247ef4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 Dec 2010 19:37:01 +0100 Subject: [PATCH] Use a cache to speed up tgba_tba_proxy. tgba_tba_proxy used to spend a lot of time (re)computing the acceptance condition common to all outgoing transition of a state. * src/tgba/tgbatba.hh (accmap_): New cache. (common_acceptance_conditions_of_original_state): New method. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~sync) Call common_acceptance_conditions_of_original_state() instead of computing the result. (~tgba_tba_proxy): Cleanup the cache. (common_acceptance_conditions_of_original_state): Implement it. --- ChangeLog | 15 +++++++++++++++ src/tgba/tgbatba.cc | 42 +++++++++++++++++++++++++++++++++--------- src/tgba/tgbatba.hh | 18 ++++++++++++++++++ 3 files changed, 66 insertions(+), 9 deletions(-) diff --git a/ChangeLog b/ChangeLog index 8907c2769..e2bcde5ad 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2010-12-09 Alexandre Duret-Lutz + + Use a cache to speed up tgba_tba_proxy. + + tgba_tba_proxy used to spend a lot of time (re)computing the + acceptance condition common to all outgoing transition of a state. + + * src/tgba/tgbatba.hh (accmap_): New cache. + (common_acceptance_conditions_of_original_state): New method. + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~sync) + Call common_acceptance_conditions_of_original_state() instead of + computing the result. + (~tgba_tba_proxy): Cleanup the cache. + (common_acceptance_conditions_of_original_state): Implement it. + 2010-12-07 Alexandre Duret-Lutz * src/ltltest/Makefile.am (genltl_SOURCES): Add missing variable. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 0623b3ebf..cf2b11479 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -117,7 +117,7 @@ namespace spot iterator expected, const list& cycle, bdd the_acceptance_cond, - const tgba* aut) + const tgba_tba_proxy* aut) : it_(it), expected_(expected), cycle_(cycle), the_acceptance_cond_(the_acceptance_cond), aut_(aut) { @@ -185,13 +185,8 @@ namespace spot // conditions common to all outgoing transitions of the // destination state, and pretend they are already present // on this transition. - bdd common = aut_->all_acceptance_conditions(); state* dest = it_->current_state(); - tgba_succ_iterator* dest_it = aut_->succ_iter(dest); - for (dest_it->first(); !dest_it->done(); dest_it->next()) - common &= dest_it->current_acceptance_conditions(); - acc |= common; - delete dest_it; + acc |= aut_->common_acceptance_conditions_of_original_state(dest); delete dest; // bddtrue is a special condition used for tgba_sba_proxy @@ -241,7 +236,7 @@ namespace spot bool accepting_; const list& cycle_; const bdd the_acceptance_cond_; - const tgba* aut_; + const tgba_tba_proxy* aut_; friend class ::spot::tgba_tba_proxy; }; @@ -283,6 +278,15 @@ namespace spot tgba_tba_proxy::~tgba_tba_proxy() { get_dict()->unregister_all_my_variables(this); + + accmap_t::const_iterator i = accmap_.begin(); + while (i != accmap_.end()) + { + // Advance the iterator before deleting the key. + const state* s = i->first; + ++i; + delete s; + } } state* @@ -305,7 +309,27 @@ namespace spot return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(), acc_cycle_, the_acceptance_cond_, - a_); + this); + } + + bdd + tgba_tba_proxy::common_acceptance_conditions_of_original_state(const state* s) + const + { + // Lookup cache + accmap_t::const_iterator i = accmap_.find(s); + if (i != accmap_.end()) + return i->second; + + bdd common = a_->all_acceptance_conditions(); + tgba_succ_iterator* it = a_->succ_iter(s); + for (it->first(); !it->done() && common != bddfalse; it->next()) + common &= it->current_acceptance_conditions(); + delete it; + + // Populate cache + accmap_[s->clone()] = common; + return common; } bdd_dict* diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index eb45384dc..bbfe804a2 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -27,6 +27,7 @@ #include #include "tgba.hh" #include "misc/bddlt.hh" +#include "misc/hash.hh" namespace spot { @@ -76,6 +77,19 @@ namespace spot virtual bdd neg_acceptance_conditions() const; typedef std::list cycle_list; + + + /// \brief Return the acceptance conditions common to all outgoing + /// transitions of state \a ostate in the original automaton. + /// + /// This internal function is only meant to be used to implement + /// the iterator returned by succ_iter. + /// + /// The result of this function is computed the first time, and + /// then cached. + bdd common_acceptance_conditions_of_original_state(const state* + ostate) const; + protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; @@ -84,6 +98,10 @@ namespace spot const tgba* a_; private: bdd the_acceptance_cond_; + typedef Sgi::hash_map accmap_t; + mutable accmap_t accmap_; + // Disallow copy. tgba_tba_proxy(const tgba_tba_proxy&); tgba_tba_proxy& operator=(const tgba_tba_proxy&);