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

@@ -1,3 +1,18 @@
+2010-12-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	* src/ltltest/Makefile.am (genltl_SOURCES): Add missing variable.

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);
+	acc |= aut_->common_acceptance_conditions_of_original_state(dest);
-	for (dest_it->first(); !dest_it->done(); dest_it->next())
-	  common &= dest_it->current_acceptance_conditions();
-	acc |= common;
-	delete dest_it;
 	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*

src/tgba/tgbatba.hh

@@ -27,6 +27,7 @@
 #include <list>
 #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<bdd> 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<const state*, bdd,
+			  state_ptr_hash, state_ptr_equal> accmap_t;
+    mutable accmap_t accmap_;
+
     // Disallow copy.
     tgba_tba_proxy(const tgba_tba_proxy&);
     tgba_tba_proxy& operator=(const tgba_tba_proxy&);