From 36f7c648b63d3212da8ae7fe1443af4a01774405 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 30 Mar 2011 19:47:18 +0200 Subject: [PATCH] Make state_explicit instances persistent objects. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge state_explicit and tgba_explicit::state. In the past, state_explicit was a small object encapsulating a pointer to the persistent tgba_explicit::state; and we used to clone() and destroy() a lot of state_explicit instance. Now state_explicit is persistent, and clone() and destroy() have no effects. * src/tgba/tgbareduce.cc: Adjust, since this inherits from tgbaexplicit and uses the internals of state_explicit. * src/tgbatest/reductgba.cc: Fix deletion order for automata. * src/tgba/tgba.hh (last_support_conditions_input_, last_support_variables_input_): Make these protected, so they can be zeroed by tgba_explicit. --- ChangeLog | 17 +++++ src/tgba/tgba.hh | 5 +- src/tgba/tgbaexplicit.cc | 85 +++++++++------------ src/tgba/tgbaexplicit.hh | 155 ++++++++++++++++++++++---------------- src/tgba/tgbareduc.cc | 78 ++++++++++--------- src/tgbatest/reductgba.cc | 4 +- 6 files changed, 188 insertions(+), 156 deletions(-) diff --git a/ChangeLog b/ChangeLog index bf1099ba4..0848d410c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2011-03-31 Alexandre Duret-Lutz + + Make state_explicit instances persistent objects. + + * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge + state_explicit and tgba_explicit::state. In the past, + state_explicit was a small object encapsulating a pointer to the + persistent tgba_explicit::state; and we used to clone() and + destroy() a lot of state_explicit instance. Now state_explicit is + persistent, and clone() and destroy() have no effects. + * src/tgba/tgbareduce.cc: Adjust, since this inherits from + tgbaexplicit and uses the internals of state_explicit. + * src/tgbatest/reductgba.cc: Fix deletion order for automata. + * src/tgba/tgba.hh (last_support_conditions_input_, + last_support_variables_input_): Make these protected, so + they can be zeroed by tgba_explicit. + 2011-03-30 Alexandre Duret-Lutz Remove tgba_reduc::format_state(). diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index c434d7649..2aba2eaef 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -209,10 +209,11 @@ namespace spot virtual bdd compute_support_conditions(const state* state) const = 0; /// Do the actual computation of tgba::support_variables(). virtual bdd compute_support_variables(const state* state) const = 0; - private: + protected: mutable const state* last_support_conditions_input_; - mutable bdd last_support_conditions_output_; mutable const state* last_support_variables_input_; + private: + mutable bdd last_support_conditions_output_; mutable bdd last_support_variables_output_; mutable int num_acc_; }; diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 613aba1e7..c074caada 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -37,7 +37,7 @@ namespace spot // tgba_explicit_succ_iterator tgba_explicit_succ_iterator::tgba_explicit_succ_iterator - (const tgba_explicit::state* s, bdd all_acc) + (const state_explicit::transitions_t* s, bdd all_acc) : s_(s), all_acceptance_conditions_(all_acc) { } @@ -64,53 +64,47 @@ namespace spot tgba_explicit_succ_iterator::current_state() const { assert(!done()); - return new state_explicit((*i_)->dest); + return const_cast(i_->dest); } bdd tgba_explicit_succ_iterator::current_condition() const { assert(!done()); - return (*i_)->condition; + return i_->condition; } bdd tgba_explicit_succ_iterator::current_acceptance_conditions() const { assert(!done()); - return (*i_)->acceptance_conditions & all_acceptance_conditions_; + return i_->acceptance_conditions & all_acceptance_conditions_; } //////////////////////////////////////// // state_explicit - const tgba_explicit::state* - state_explicit::get_state() const - { - return state_; - } - int state_explicit::compare(const spot::state* other) const { const state_explicit* o = dynamic_cast(other); assert(o); - return o->get_state() - get_state(); + // 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; } size_t state_explicit::hash() const { return - reinterpret_cast(get_state()) - static_cast(0); + reinterpret_cast(this) - static_cast(0); } - state_explicit* - state_explicit::clone() const - { - return new state_explicit(*this); - } //////////////////////////////////////// // tgba_explicit @@ -131,12 +125,13 @@ namespace spot tgba_explicit::transition* tgba_explicit::create_transition(state* source, const state* dest) { - transition* t = new transition; - t->dest = dest; - t->condition = bddtrue; - t->acceptance_conditions = bddfalse; - source->push_back(t); - return t; + transition t; + t.dest = dest; + t.condition = bddtrue; + t.acceptance_conditions = bddfalse; + state_explicit::transitions_t::iterator i = + source->successors.insert(source->successors.end(), t); + return &*i; } void tgba_explicit::add_condition(transition* t, const ltl::formula* f) @@ -219,7 +214,7 @@ namespace spot // Fix empty automata by adding a lone initial state. if (!init_) const_cast(this)->add_default_init(); - return new state_explicit(init_); + return init_; } tgba_succ_iterator* @@ -231,7 +226,7 @@ namespace spot assert(s); (void) global_state; (void) global_automaton; - return new tgba_explicit_succ_iterator(s->get_state(), + return new tgba_explicit_succ_iterator(&s->successors, all_acceptance_conditions()); } @@ -240,12 +235,12 @@ namespace spot { const state_explicit* s = dynamic_cast(in); assert(s); - const state* st = s->get_state(); + const state_explicit::transitions_t& st = s->successors; bdd res = bddfalse; - tgba_explicit::state::const_iterator i; - for (i = st->begin(); i != st->end(); ++i) - res |= (*i)->condition; + state_explicit::transitions_t::const_iterator i; + for (i = st.begin(); i != st.end(); ++i) + res |= i->condition; return res; } @@ -254,12 +249,12 @@ namespace spot { const state_explicit* s = dynamic_cast(in); assert(s); - const state* st = s->get_state(); + const state_explicit::transitions_t& st = s->successors; bdd res = bddtrue; - tgba_explicit::state::const_iterator i; - for (i = st->begin(); i != st->end(); ++i) - res &= bdd_support((*i)->condition); + state_explicit::transitions_t::const_iterator i; + for (i = st.begin(); i != st.end(); ++i) + res &= bdd_support(i->condition); return res; } @@ -295,9 +290,6 @@ namespace spot // Do not erase the same state twice. (Because of possible aliases.) if (state_name_map_.erase(i->second)) { - tgba_explicit::state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) - delete *i2; delete i->second; } } @@ -314,7 +306,7 @@ namespace spot { const state_explicit* se = dynamic_cast(s); assert(se); - sn_map::const_iterator i = state_name_map_.find(se->get_state()); + sn_map::const_iterator i = state_name_map_.find(se); assert(i != state_name_map_.end()); return i->second; } @@ -324,9 +316,6 @@ namespace spot ns_map::iterator i = name_state_map_.begin(); while (i != name_state_map_.end()) { - tgba_explicit::state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) - delete *i2; // Advance the iterator before deleting the formula. const ltl::formula* s = i->first; delete i->second; @@ -345,7 +334,7 @@ namespace spot { const state_explicit* se = dynamic_cast(s); assert(se); - sn_map::const_iterator i = state_name_map_.find(se->get_state()); + sn_map::const_iterator i = state_name_map_.find(se); assert(i != state_name_map_.end()); return ltl::to_string(i->second); } @@ -354,14 +343,10 @@ namespace spot { ns_map::iterator i = name_state_map_.begin(); while (i != name_state_map_.end()) - { - tgba_explicit::state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) - delete *i2; - // Advance the iterator before deleting the state. - delete i->second; - ++i; - } + { + delete i->second; + ++i; + } } tgba_explicit::state* tgba_explicit_number::add_default_init() @@ -374,7 +359,7 @@ namespace spot { const state_explicit* se = dynamic_cast(s); assert(se); - sn_map::const_iterator i = state_name_map_.find(se->get_state()); + sn_map::const_iterator i = state_name_map_.find(se); assert(i != state_name_map_.end()); std::stringstream ss; ss << i->second; diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index f9f08cbfa..9ab757beb 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -37,24 +37,66 @@ namespace spot class tgba_explicit_succ_iterator; class tgba_explicit; + /// States used by spot::tgba_explicit. + /// \ingroup tgba_representation + class state_explicit: public spot::state + { + public: + state_explicit() + { + } + + virtual int compare(const spot::state* other) const; + virtual size_t hash() const; + + virtual state_explicit* clone() const + { + return const_cast(this); + } + + bool empty() const + { + return successors.empty(); + } + + virtual + void destroy() const + { + } + + /// Explicit transitions. + struct transition + { + bdd condition; + bdd acceptance_conditions; + const state_explicit* dest; + }; + + typedef std::list transitions_t; + transitions_t successors; + private: + state_explicit(const state_explicit& other); + state_explicit& operator=(const state_explicit& other); + + virtual ~state_explicit() + { + } + friend class tgba_explicit_string; + friend class tgba_explicit_formula; + friend class tgba_explicit_number; + }; + + /// Explicit representation of a spot::tgba. /// \ingroup tgba_representation class tgba_explicit: public tgba { public: + typedef state_explicit state; + typedef state_explicit::transition transition; + tgba_explicit(bdd_dict* dict); - struct transition; - typedef std::list state; - - /// Explicit transitions (used by spot::tgba_explicit). - struct transition - { - bdd condition; - bdd acceptance_conditions; - const state* dest; - }; - /// Add a default initial state. virtual state* add_default_init() = 0; @@ -100,7 +142,7 @@ namespace spot bdd get_acceptance_condition(const ltl::formula* f); bdd_dict* dict_; - tgba_explicit::state* init_; + state_explicit* init_; mutable bdd all_acceptance_conditions_; bdd neg_acceptance_conditions_; mutable bool all_acceptance_conditions_computed_; @@ -113,36 +155,13 @@ namespace spot - /// States used by spot::tgba_explicit. - /// \ingroup tgba_representation - class state_explicit : public spot::state - { - public: - state_explicit(const tgba_explicit::state* s) - : state_(s) - { - } - - virtual int compare(const spot::state* other) const; - virtual size_t hash() const; - virtual state_explicit* clone() const; - - virtual ~state_explicit() - { - } - - const tgba_explicit::state* get_state() const; - private: - const tgba_explicit::state* state_; - }; - - /// Successor iterators used by spot::tgba_explicit. /// \ingroup tgba_representation class tgba_explicit_succ_iterator: public tgba_succ_iterator { public: - tgba_explicit_succ_iterator(const tgba_explicit::state* s, bdd all_acc); + tgba_explicit_succ_iterator(const state_explicit::transitions_t* s, + bdd all_acc); virtual void first(); virtual void next(); @@ -153,8 +172,8 @@ namespace spot virtual bdd current_acceptance_conditions() const; private: - const tgba_explicit::state* s_; - tgba_explicit::state::const_iterator i_; + const state_explicit::transitions_t* s_; + state_explicit::transitions_t::const_iterator i_; bdd all_acceptance_conditions_; }; @@ -164,10 +183,10 @@ namespace spot { protected: typedef label label_t; - typedef Sgi::hash_map ns_map; - typedef Sgi::hash_map > sn_map; + typedef Sgi::hash_map > sn_map; ns_map name_state_map_; sn_map state_name_map_; public: @@ -178,7 +197,7 @@ namespace spot return name_state_map_.find(name) != name_state_map_.end(); } - const label& get_label(const tgba_explicit::state* s) const + const label& get_label(const state_explicit* s) const { typename sn_map::const_iterator i = state_name_map_.find(s); assert(i != state_name_map_.end()); @@ -189,17 +208,17 @@ namespace spot { const state_explicit* se = dynamic_cast(s); assert(se); - return get_label(se->get_state()); + return get_label(se); } - /// Return the tgba_explicit::state for \a name, creating the state if + /// Return the state_explicit for \a name, creating the state if /// it does not exist. state* add_state(const label& name) { typename ns_map::iterator i = name_state_map_.find(name); if (i == name_state_map_.end()) { - tgba_explicit::state* s = new tgba_explicit::state; + state_explicit* s = new state_explicit; name_state_map_[name] = s; state_name_map_[s] = name; @@ -216,7 +235,7 @@ namespace spot state* set_init_state(const label& state) { - tgba_explicit::state* s = add_state(state); + state_explicit* s = add_state(state); init_ = s; return s; } @@ -245,10 +264,11 @@ namespace spot typename ns_map::iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - tgba_explicit::state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + state_explicit::transitions_t::iterator i2; + for (i2 = i->second->successors.begin(); + i2 != i->second->successors.end(); ++i2) { - (*i2)->acceptance_conditions = all - (*i2)->acceptance_conditions; + i2->acceptance_conditions = all - i2->acceptance_conditions; } } } @@ -265,9 +285,10 @@ namespace spot typename ns_map::iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - tgba_explicit::state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) - (*i2)->acceptance_conditions &= neg; + state_explicit::transitions_t::iterator i2; + for (i2 = i->second->successors.begin(); + i2 != i->second->successors.end(); ++i2) + i2->acceptance_conditions &= neg; } all_acceptance_conditions_computed_ = false; @@ -280,25 +301,25 @@ namespace spot typename ns_map::iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - state::iterator t1; - for (t1 = i->second->begin(); t1 != i->second->end(); ++t1) + state_explicit::transitions_t::iterator t1; + for (t1 = i->second->successors.begin(); + t1 != i->second->successors.end(); ++t1) { - bdd acc = (*t1)->acceptance_conditions; - const state* dest = (*t1)->dest; + bdd acc = t1->acceptance_conditions; + const state* dest = t1->dest; // Find another transition with the same destination and // acceptance conditions. - state::iterator t2 = t1; + state_explicit::transitions_t::iterator t2 = t1; ++t2; - while (t2 != i->second->end()) + while (t2 != i->second->successors.end()) { - state::iterator t2copy = t2++; - if ((*t2copy)->acceptance_conditions == acc - && (*t2copy)->dest == dest) + state_explicit::transitions_t::iterator t2copy = t2++; + if (t2copy->acceptance_conditions == acc + && t2copy->dest == dest) { - (*t1)->condition |= (*t2copy)->condition; - delete *t2copy; - i->second->erase(t2copy); + t1->condition |= t2copy->condition; + i->second->successors.erase(t2copy); } } } @@ -309,6 +330,10 @@ namespace spot virtual ~tgba_explicit_labelled() { + // These have already been destroyed by subclasses. + // Prevent destroying by tgba::~tgba. + last_support_conditions_input_ = 0; + last_support_variables_input_ = 0; } }; diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index 838e11072..31ccb9ef3 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -173,8 +173,8 @@ namespace spot tgba_explicit::state* s = tgba_explicit_string::add_state(ss); tgba_explicit::state* d = tgba_explicit_string::add_state(sd); - transition* t = new transition(); - t->dest = d; + transition t; + t.dest = d; sp_map::iterator i = state_predecessor_map_.find(d); if (i == state_predecessor_map_.end()) @@ -188,11 +188,11 @@ namespace spot (i->second)->push_back(s); } - t->condition = bddtrue; - t->acceptance_conditions = bddfalse; - s->push_back(t); - - return t; + t.condition = bddtrue; + t.acceptance_conditions = bddfalse; + state_explicit::transitions_t::iterator is + = s->successors.insert(s->successors.end(), t); + return &*is; } /////////////////////////////////////////////////// @@ -218,16 +218,16 @@ namespace spot for (std::list::iterator p = (i->second)->begin(); p != (i->second)->end(); ++p) { - // We check if simul belong to the successor of p, // as s belong too. - for (tgba_explicit::state::iterator j = (*p)->begin(); - j != (*p)->end(); ++j) - if ((*j)->dest == s2) // simul belong to the successor of p. + for (state_explicit::transitions_t::iterator + j = (*p)->successors.begin(); + j != (*p)->successors.end(); ++j) + if (j->dest == s2) // simul belong to the successor of p. { belong = true; - cond_simul = (*j)->condition; - acc_simul = (*j)->acceptance_conditions; + cond_simul = j->condition; + acc_simul = j->acceptance_conditions; break; } @@ -236,18 +236,19 @@ namespace spot continue; // for all successor of p, a predecessor of s and simul. - for (tgba_explicit::state::iterator j = (*p)->begin(); - j != (*p)->end(); ++j) + for (state_explicit::transitions_t::iterator + j = (*p)->successors.begin(); + j != (*p)->successors.end(); ++j) { // if the transition lead to s. - if (((*j)->dest == s1) && + if ((j->dest == s1) && // if the label of the transition whose lead to s implies // this leading to simul. - (((!(*j)->condition | cond_simul) == bddtrue) && - ((!(*j)->acceptance_conditions) | acc_simul) == bddtrue)) + (((!j->condition | cond_simul) == bddtrue) && + ((!j->acceptance_conditions) | acc_simul) == bddtrue)) { // We can redirect transition leading to s on simul. - (*j)->dest = const_cast(s2); + j->dest = const_cast(s2); // We memorize that we have to remove p // of the predecessor of s. @@ -297,8 +298,9 @@ namespace spot // for all successor q of s, we remove s of the predecessor of q. // Note that the initial node can't be removed. - for (state::iterator j = st->begin(); j != st->end(); ++j) - this->remove_predecessor_state((*j)->dest, st); + for (state_explicit::transitions_t::iterator j = + st->successors.begin(); j != st->successors.end(); ++j) + this->remove_predecessor_state(j->dest, st); sp_map::iterator i = state_predecessor_map_.find(st); @@ -310,14 +312,14 @@ namespace spot p != (i->second)->end(); ++p) { // for all transition of p, a predecessor of s. - for (state::iterator j = (*p)->begin(); - j != (*p)->end();) + for (state_explicit::transitions_t::iterator + j = (*p)->successors.begin(); + j != (*p)->successors.end();) { - if ((*j)->dest == st) + if (j->dest == st) { // Remove the transition - delete *j; - j = (*p)->erase(j); + j = (*p)->successors.erase(j); ++j; } else @@ -367,14 +369,15 @@ namespace spot p != (i->second)->end(); ++p) { // for all successor of p, a predecessor of s1. - for (tgba_explicit::state::iterator j = (*p)->begin(); - j != (*p)->end(); ++j) + for (state_explicit::transitions_t::iterator + j = (*p)->successors.begin(); + j != (*p)->successors.end(); ++j) { // if the successor was s1... - if ((*j)->dest == s1) + if (j->dest == s1) { // ... make it s2. - (*j)->dest = const_cast(s2); + j->dest = const_cast(s2); } } } @@ -385,14 +388,15 @@ namespace spot // leaving s1 (possible when the simulation is delayed). Since s2 // simulates s1, s2 has some labels that imply these of s1, so we // can put the acceptance conditions on its arcs. - for (tgba_explicit::state::const_iterator j = s1->begin(); - j != s1->end(); ++j) + for (state_explicit::transitions_t::const_iterator + j = s1->successors.begin(); + j != s1->successors.end(); ++j) { - transition* t = new transition(); - t->dest = (*j)->dest; - t->condition = (*j)->condition; - t->acceptance_conditions = (*j)->acceptance_conditions; - const_cast(s2)->push_back(t); + transition t; + t.dest = j->dest; + t.condition = j->condition; + t.acceptance_conditions = j->acceptance_conditions; + const_cast(s2)->successors.push_back(t); } // We remove all the predecessor of s1. diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 68d3674bd..608754bd5 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -161,8 +161,8 @@ main(int argc, char** argv) spot::dotty_reachable(std::cout, res); - delete automata; delete res; + delete automata; #ifndef REDUCCMP if (f != 0) f->destroy();