diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 7d87ae2ab..a5e16e03d 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -30,6 +30,7 @@ #include #include #include "misc/casts.hh" +#include "misc/hash.hh" namespace spot { @@ -171,6 +172,11 @@ namespace spot } }; + typedef Sgi::hash_set state_set; + + // Functions related to shared_ptr. ////////////////////////////////////////////////// @@ -259,6 +265,10 @@ namespace spot } }; + typedef Sgi::hash_set shared_state_set; + } #endif // SPOT_TGBA_STATE_HH diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index 0f1ef39c1..1e60bca84 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE) +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -61,7 +61,7 @@ namespace spot taa_tgba::get_init_state() const { assert(init_); - return new spot::state_set(init_); + return new spot::set_state(init_); } tgba_succ_iterator* @@ -69,7 +69,7 @@ namespace spot const spot::state* global_state, const tgba* global_automaton) const { - const spot::state_set* s = down_cast(state); + const spot::set_state* s = down_cast(state); assert(s); (void) global_state; (void) global_automaton; @@ -103,7 +103,7 @@ namespace spot bdd taa_tgba::compute_support_conditions(const spot::state* s) const { - const spot::state_set* se = down_cast(s); + const spot::set_state* se = down_cast(s); assert(se); const state_set* ss = se->get_state(); @@ -119,7 +119,7 @@ namespace spot bdd taa_tgba::compute_support_variables(const spot::state* s) const { - const spot::state_set* se = down_cast(s); + const spot::set_state* se = down_cast(s); assert(se); const state_set* ss = se->get_state(); @@ -137,15 +137,15 @@ namespace spot `----------*/ const taa_tgba::state_set* - state_set::get_state() const + set_state::get_state() const { return s_; } int - state_set::compare(const spot::state* other) const + set_state::compare(const spot::state* other) const { - const state_set* o = down_cast(other); + const set_state* o = down_cast(other); assert(o); const taa_tgba::state_set* s1 = get_state(); @@ -166,7 +166,7 @@ namespace spot } size_t - state_set::hash() const + set_state::hash() const { size_t res = 0; taa_tgba::state_set::const_iterator it = s_->begin(); @@ -178,13 +178,13 @@ namespace spot return res; } - state_set* - state_set::clone() const + set_state* + set_state::clone() const { if (delete_me_ && s_) - return new spot::state_set(new taa_tgba::state_set(*s_), true); + return new spot::set_state(new taa_tgba::state_set(*s_), true); else - return new spot::state_set(s_, false); + return new spot::set_state(s_, false); } /*--------------. @@ -241,7 +241,7 @@ namespace spot assert(p > 0); t->dst = ss; // Boxing to be able to insert ss in the map directly. - spot::state_set* b = new spot::state_set(ss); + spot::set_state* b = new spot::set_state(ss); // If no contradiction, then look for another transition to // merge with the new one. @@ -304,7 +304,7 @@ namespace spot for (seen_map::iterator i = seen_.begin(); i != seen_.end();) { // Advance the iterator before deleting the state set. - const spot::state_set* s = i->first; + const spot::set_state* s = i->first; ++i; delete s; } @@ -333,11 +333,11 @@ namespace spot return i_ == succ_.end(); } - spot::state_set* + spot::set_state* taa_succ_iterator::current_state() const { assert(!done()); - return new spot::state_set(new taa_tgba::state_set(*(*i_)->dst), true); + return new spot::set_state(new taa_tgba::state_set(*(*i_)->dst), true); } bdd diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 59ee73991..20b649599 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -83,19 +83,19 @@ namespace spot }; /// Set of states deriving from spot::state. - class SPOT_API state_set : public spot::state + class SPOT_API set_state : public spot::state { public: - state_set(const taa_tgba::state_set* s, bool delete_me = false) + set_state(const taa_tgba::state_set* s, bool delete_me = false) : s_(s), delete_me_(delete_me) { } virtual int compare(const spot::state*) const; virtual size_t hash() const; - virtual state_set* clone() const; + virtual set_state* clone() const; - virtual ~state_set() + virtual ~set_state() { if (delete_me_) delete s_; @@ -117,7 +117,7 @@ namespace spot virtual void next(); virtual bool done() const; - virtual state_set* current_state() const; + virtual set_state* current_state() const; virtual bdd current_condition() const; virtual bdd current_acceptance_conditions() const; @@ -128,7 +128,7 @@ namespace spot typedef std::pair iterator_pair; typedef std::vector bounds_t; typedef Sgi::hash_map< - const spot::state_set*, std::vector, + const spot::set_state*, std::vector, state_ptr_hash, state_ptr_equal> seen_map; struct distance_sort : @@ -218,15 +218,15 @@ namespace spot /// \brief Format the state as a string for printing. /// - /// If state is a spot::state_set of only one element, then the + /// If state is a spot::set_state of only one element, then the /// string corresponding to state->get_state() is returned. /// /// Otherwise a string composed of each string corresponding to - /// each state->get_state() in the spot::state_set is returned, + /// each state->get_state() in the spot::set_state is returned, /// e.g. like {string_1,...,string_n}. virtual std::string format_state(const spot::state* s) const { - const spot::state_set* se = down_cast(s); + const spot::set_state* se = down_cast(s); assert(se); const state_set* ss = se->get_state(); return format_state_set(ss); diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index 07e930a16..3e13e55bc 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -91,9 +91,6 @@ namespace spot typedef Sgi::hash_map state_rank_map; - typedef Sgi::hash_set state_set; //////////////////////////////////////// // state_kv_complement @@ -106,7 +103,8 @@ namespace spot { public: state_kv_complement(); - state_kv_complement(state_rank_map state_map, state_set state_filter); + state_kv_complement(state_rank_map state_map, + shared_state_set state_filter); virtual ~state_kv_complement() {} virtual int compare(const state* other) const; @@ -115,11 +113,11 @@ namespace spot void add(shared_state state, const rank_t& rank); const state_rank_map& get_state_map() const; - const state_set& get_filter_set() const; + const shared_state_set& get_filter_set() const; bool accepting() const; private: state_rank_map state_map_; - state_set state_filter_; + shared_state_set state_filter_; }; state_kv_complement::state_kv_complement() @@ -127,7 +125,7 @@ namespace spot } state_kv_complement::state_kv_complement(state_rank_map state_map, - state_set state_filter) + shared_state_set state_filter) : state_map_(state_map), state_filter_(state_filter) { } @@ -169,8 +167,8 @@ namespace spot } { - state_set::const_iterator i = state_filter_.begin(); - state_set::const_iterator j = other->state_filter_.begin(); + shared_state_set::const_iterator i = state_filter_.begin(); + shared_state_set::const_iterator j = other->state_filter_.begin(); while (i != state_filter_.end() && j != other->state_filter_.end()) { int result = (*i)->compare(j->get()); @@ -200,7 +198,7 @@ namespace spot } { - state_set::const_iterator i = state_filter_.begin(); + shared_state_set::const_iterator i = state_filter_.begin(); while (i != state_filter_.end()) { hash ^= (*i)->hash(); @@ -230,7 +228,7 @@ namespace spot return state_map_; } - const state_set& + const shared_state_set& state_kv_complement::get_filter_set() const { return state_filter_; @@ -283,7 +281,7 @@ namespace spot bdd_list_t::const_iterator current_condition_; state_rank_map highest_current_ranks_; state_rank_map current_ranks_; - state_set highest_state_set_; + shared_state_set highest_state_set_; }; tgba_kv_complement_succ_iterator:: @@ -455,10 +453,10 @@ namespace spot } // Highest $O$ set of the algorithm. - state_set s_set = origin_->get_filter_set(); + shared_state_set s_set = origin_->get_filter_set(); highest_state_set_.clear(); - for (state_set::const_iterator i = s_set.begin(); + for (shared_state_set::const_iterator i = s_set.begin(); i != s_set.end(); ++i) { @@ -523,7 +521,7 @@ namespace spot // If the filter set is empty, all the states of the map // that are associated to an even rank create the new filter set. - state_set filter; + shared_state_set filter; if (origin_->get_filter_set().empty()) { for (state_rank_map::const_iterator i = current_ranks_.begin(); @@ -536,7 +534,7 @@ namespace spot { // It the filter set is non-empty, we delete from this set states // that are now associated to an odd rank. - for (state_set::const_iterator i = highest_state_set_.begin(); + for (shared_state_set::const_iterator i = highest_state_set_.begin(); i != highest_state_set_.end(); ++i) { @@ -651,7 +649,7 @@ namespace spot ss << "{ set: {" << std::endl; const state_rank_map& state_map = s->get_state_map(); - const state_set& state_filter = s->get_filter_set(); + const shared_state_set& state_filter = s->get_filter_set(); for (state_rank_map::const_iterator i = state_map.begin(); i != state_map.end(); @@ -662,7 +660,7 @@ namespace spot } ss << "} odd-less: {"; - for (state_set::const_iterator i = state_filter.begin(); + for (shared_state_set::const_iterator i = state_filter.begin(); i != state_filter.end(); ++i) ss << " " << automaton_->format_state(i->get()) << std::endl; diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 5f37f80e5..5bd4c76cb 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -81,7 +81,7 @@ namespace spot } // Find all states of an automaton. - void state_set(const tgba* a, hash_set* seen) + void build_state_set(const tgba* a, hash_set* seen) { std::queue tovisit; // Perform breadth-first traversal. @@ -515,7 +515,7 @@ namespace spot // non_final contain all states. // final is empty: there is no acceptance condition - state_set(det_a, non_final); + build_state_set(det_a, non_final); return minimize_dfa(det_a, final, non_final); }