diff --git a/ChangeLog b/ChangeLog index bb598aa5f..0bf6eec35 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2012-01-18 Alexandre Duret-Lutz + + Implement a unicity table for states created by tgba_tba_proxy. + + Suggested by Nikos Gorogiannis. + + * src/tgba/tgbatba.hh (tgba_tba_proxy::create_state): New method. + (tgba_tba_proxy::uniq_map_): New attribute. + * src/tgba/tgbatba.cc (state_tba_proxy): Use the default + copy constructor. Empty the destructor. Implement an empty + destroy() method. Use addresses for comparison. Make clone() + a no-op. + (tgba_tba_proxy): Allocate and deallocate the unicity table. + Implement create_sates(). + (tgba_tba_proxy, tgba_sba_proxy, tgba_tba_proxy_succ_iterator): + Adjust state construction to call create_state(). + 2012-01-17 Alexandre Duret-Lutz Minor speedups in tgba_safra_complement(). diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 37248aa6a..956316e01 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement de // l'Epita. // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -45,18 +45,19 @@ namespace spot { } - /// Copy constructor - state_tba_proxy(const state_tba_proxy& o) - : state(), - s_(o.real_state()->clone()), - acc_(o.acceptance_iterator()) - { - } + // Note: There is a default copy constructor, needed by + // Sgi::hash_set. It does not clone the state "s", because the + // destructor will not destroy it either. Actually, the states + // are all destroyed in the tgba_tba_proxy destructor. virtual ~state_tba_proxy() { - s_->destroy(); + } + + void + destroy() const + { } state* @@ -82,10 +83,12 @@ namespace spot { const state_tba_proxy* o = down_cast(other); assert(o); - int res = s_->compare(o->real_state()); - if (res != 0) - return res; - return acc_->id() - o->acceptance_cond().id(); + // Do not simply return "o - this", it might not fit in an int. + if (o < this) + return -1; + if (o > this) + return 1; + return 0; } virtual size_t @@ -97,7 +100,7 @@ namespace spot virtual state_tba_proxy* clone() const { - return new state_tba_proxy(*this); + return const_cast(this); } private: @@ -105,6 +108,30 @@ namespace spot iterator acc_; }; + struct state_tba_proxy_hash + { + size_t + operator()(const state_tba_proxy& s) const + { + return s.state_tba_proxy::hash(); + } + }; + + struct state_tba_proxy_equal + { + bool + operator()(const state_tba_proxy& left, + const state_tba_proxy& right) const + { + if (left.acceptance_iterator() != right.acceptance_iterator()) + return false; + return left.real_state()->compare(right.real_state()) == 0; + } + }; + + typedef Sgi::hash_set uniq_map_t; typedef std::pair state_ptr_bool_t; @@ -267,7 +294,8 @@ namespace spot while (next != expected && (acc & *next) == *next) ++next; next_is_set: - state_tba_proxy* dest = new state_tba_proxy(odest, next); + state_tba_proxy* dest = + down_cast(aut->create_state(odest, next)); // Is DEST already reachable with the same value of ACCEPTING? state_ptr_bool_t key(dest, accepting); transmap_t::iterator id = transmap_.find(key); @@ -369,7 +397,7 @@ namespace spot } // anonymous tgba_tba_proxy::tgba_tba_proxy(const tgba* a) - : a_(a) + : a_(a), uniq_map_(new uniq_map_t) { // We will use one acceptance condition for this automata. // Let's call it Acc[True]. @@ -421,12 +449,37 @@ namespace spot ++i; s->destroy(); } + + uniq_map_t* m = static_cast(uniq_map_); + uniq_map_t::const_iterator j = m->begin(); + while (j != m->end()) + { + const state* s = j->real_state(); + ++j; + s->destroy(); + } + delete m; } + state* + tgba_tba_proxy::create_state(state* s, cycle_list::const_iterator acc) const + { + uniq_map_t* m = static_cast(uniq_map_); + state_tba_proxy st(s, acc); + + std::pair res = m->insert(st); + if (!res.second) + s->destroy(); + + return const_cast(&(*res.first)); + } + + + state* tgba_tba_proxy::get_init_state() const { - return new state_tba_proxy(a_->get_init_state(), acc_cycle_.begin()); + return create_state(a_->get_init_state(), acc_cycle_.begin()); } tgba_succ_iterator* @@ -596,7 +649,7 @@ namespace spot state* tgba_sba_proxy::get_init_state() const { - return new state_tba_proxy(a_->get_init_state(), cycle_start_); + return create_state(a_->get_init_state(), cycle_start_); } bool diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index 46eb06f01..300b280dc 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita. // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -97,12 +97,19 @@ namespace spot /// then cached. bdd union_acceptance_conditions_of_original_state(const state* s) const; + /// \brief Create a degeneralized state using the unicity table. + /// + /// This is an internal function. \a s should be a fresh state + /// from the source automaton. + state* create_state(state* s, cycle_list::const_iterator acc) const; + protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; cycle_list acc_cycle_; const tgba* a_; + private: bdd the_acceptance_cond_; typedef Sgi::hash_map