From f00aa49dc3b7d930c1d898a918a83153c3a4f797 Mon Sep 17 00:00:00 2001 From: Guillaume Sadegh Date: Fri, 27 Nov 2009 23:17:38 +0100 Subject: [PATCH] Rename the class taa as taa_tgba. * src/tgba/taa.cc, src/tgba/taa.hh: Rename as ... * src/tgba/taatgba.cc, src/tgba/taatgba.hh: ... these, and rename the class taa as taa_tgba. * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/Makefile.am: Adjust. * src/tgbatest/ltl2tgba.cc, src/tgbatest/Makefile.am: Adjust. * src/tgbatest/taa.test: Rename as ... * src/tgbatest/taatgba.test ... this. * src/tgbatest/taa.cc: Rename as ... * src/tgbatest/taatgba.cc ... this, and adjust. --- ChangeLog | 15 ++++ src/tgba/Makefile.am | 4 +- src/tgba/{taa.cc => taatgba.cc} | 109 ++++++++++++------------ src/tgba/{taa.hh => taatgba.hh} | 50 +++++------ src/tgbaalgos/ltl2taa.cc | 16 ++-- src/tgbaalgos/ltl2taa.hh | 6 +- src/tgbatest/Makefile.am | 6 +- src/tgbatest/{taa.cc => taatgba.cc} | 10 +-- src/tgbatest/{taa.test => taatgba.test} | 2 +- 9 files changed, 117 insertions(+), 101 deletions(-) rename src/tgba/{taa.cc => taatgba.cc} (79%) rename src/tgba/{taa.hh => taatgba.hh} (80%) rename src/tgbatest/{taa.cc => taatgba.cc} (90%) rename src/tgbatest/{taa.test => taatgba.test} (59%) diff --git a/ChangeLog b/ChangeLog index a4a8e4b50..6e9799bdb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2009-11-27 Guillaume Sadegh + + Rename the class taa as taa_tgba. + + * src/tgba/taa.cc, src/tgba/taa.hh: Rename as ... + * src/tgba/taatgba.cc, src/tgba/taatgba.hh: ... these, and + rename the class taa as taa_tgba. + * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh, + src/tgbaalgos/Makefile.am: Adjust. + * src/tgbatest/ltl2tgba.cc, src/tgbatest/Makefile.am: Adjust. + * src/tgbatest/taa.test: Rename as ... + * src/tgbatest/taatgba.test ... this. + * src/tgbatest/taa.cc: Rename as ... + * src/tgbatest/taatgba.cc ... this, and adjust. + 2009-11-26 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (main): Fix typo to re-enable diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index aee3b13dd..8168ac52c 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -34,7 +34,7 @@ tgba_HEADERS = \ statebdd.hh \ succiter.hh \ succiterconcrete.hh \ - taa.hh \ + taatgba.hh \ tgba.hh \ tgbabddconcrete.hh \ tgbabddconcretefactory.hh \ @@ -60,7 +60,7 @@ libtgba_la_SOURCES = \ futurecondcol.cc \ succiterconcrete.cc \ statebdd.cc \ - taa.cc \ + taatgba.cc \ tgba.cc \ tgbabddconcrete.cc \ tgbabddconcretefactory.cc \ diff --git a/src/tgba/taa.cc b/src/tgba/taatgba.cc similarity index 79% rename from src/tgba/taa.cc rename to src/tgba/taatgba.cc index d4197b07a..65b14ba4c 100644 --- a/src/tgba/taa.cc +++ b/src/tgba/taatgba.cc @@ -25,15 +25,15 @@ #include #include "tgba/formula2bdd.hh" #include "misc/bddop.hh" -#include "taa.hh" +#include "taatgba.hh" namespace spot { - /*----. - | taa | - `----*/ + /*--------. + | taa_tgba | + `--------*/ - taa::taa(bdd_dict* dict) + taa_tgba::taa_tgba(bdd_dict* dict) : name_state_map_(), state_name_map_(), dict_(dict), all_acceptance_conditions_(bddfalse), all_acceptance_conditions_computed_(false), @@ -42,12 +42,12 @@ namespace spot { } - taa::~taa() + taa_tgba::~taa_tgba() { ns_map::iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - taa::state::iterator i2; + taa_tgba::state::iterator i2; for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) delete *i2; delete i->second; @@ -59,7 +59,7 @@ namespace spot } void - taa::set_init_state(const std::string& s) + taa_tgba::set_init_state(const std::string& s) { std::vector v(1); v[0] = s; @@ -67,14 +67,14 @@ namespace spot } void - taa::set_init_state(const std::vector& s) + taa_tgba::set_init_state(const std::vector& s) { init_ = add_state_set(s); } - taa::transition* - taa::create_transition(const std::string& s, - const std::vector& d) + taa_tgba::transition* + taa_tgba::create_transition(const std::string& s, + const std::vector& d) { state* src = add_state(s); state_set* dst = add_state_set(d); @@ -86,8 +86,8 @@ namespace spot return t; } - taa::transition* - taa::create_transition(const std::string& s, const std::string& d) + taa_tgba::transition* + taa_tgba::create_transition(const std::string& s, const std::string& d) { std::vector vec; vec.push_back(d); @@ -95,14 +95,14 @@ namespace spot } void - taa::add_condition(transition* t, const ltl::formula* f) + taa_tgba::add_condition(transition* t, const ltl::formula* f) { t->condition &= formula_to_bdd(f, dict_, this); f->destroy(); } void - taa::add_acceptance_condition(transition* t, const ltl::formula* f) + taa_tgba::add_acceptance_condition(transition* t, const ltl::formula* f) { if (dict_->acc_map.find(f) == dict_->acc_map.end()) { @@ -114,7 +114,7 @@ namespace spot ns_map::iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - taa::state::iterator i2; + taa_tgba::state::iterator i2; for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) (*i2)->acceptance_conditions &= neg; } @@ -130,12 +130,12 @@ namespace spot } void - taa::output(std::ostream& os) const + taa_tgba::output(std::ostream& os) const { ns_map::const_iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - taa::state::const_iterator i2; + taa_tgba::state::const_iterator i2; os << "State: " << i->first << std::endl; for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) { @@ -147,16 +147,16 @@ namespace spot } state* - taa::get_init_state() const + taa_tgba::get_init_state() const { assert(init_); return new spot::state_set(init_); } tgba_succ_iterator* - taa::succ_iter(const spot::state* state, - const spot::state* global_state, - const tgba* global_automaton) const + taa_tgba::succ_iter(const spot::state* state, + const spot::state* global_state, + const tgba* global_automaton) const { const spot::state_set* s = dynamic_cast(state); assert(s); @@ -166,13 +166,13 @@ namespace spot } bdd_dict* - taa::get_dict() const + taa_tgba::get_dict() const { return dict_; } std::string - taa::format_state(const spot::state* s) const + taa_tgba::format_state(const spot::state* s) const { const spot::state_set* se = dynamic_cast(s); assert(se); @@ -181,7 +181,7 @@ namespace spot } bdd - taa::all_acceptance_conditions() const + taa_tgba::all_acceptance_conditions() const { if (!all_acceptance_conditions_computed_) { @@ -193,21 +193,21 @@ namespace spot } bdd - taa::neg_acceptance_conditions() const + taa_tgba::neg_acceptance_conditions() const { return neg_acceptance_conditions_; } bdd - taa::compute_support_conditions(const spot::state* s) const + taa_tgba::compute_support_conditions(const spot::state* s) const { const spot::state_set* se = dynamic_cast(s); assert(se); const state_set* ss = se->get_state(); bdd res = bddtrue; - taa::state_set::const_iterator i; - taa::state::const_iterator j; + taa_tgba::state_set::const_iterator i; + taa_tgba::state::const_iterator j; for (i = ss->begin(); i != ss->end(); ++i) for (j = (*i)->begin(); j != (*i)->end(); ++j) res |= (*j)->condition; @@ -215,28 +215,28 @@ namespace spot } bdd - taa::compute_support_variables(const spot::state* s) const + taa_tgba::compute_support_variables(const spot::state* s) const { const spot::state_set* se = dynamic_cast(s); assert(se); const state_set* ss = se->get_state(); bdd res = bddtrue; - taa::state_set::const_iterator i; - taa::state::const_iterator j; + taa_tgba::state_set::const_iterator i; + taa_tgba::state::const_iterator j; for (i = ss->begin(); i != ss->end(); ++i) for (j = (*i)->begin(); j != (*i)->end(); ++j) res &= bdd_support((*j)->condition); return res; } - taa::state* - taa::add_state(const std::string& name) + taa_tgba::state* + taa_tgba::add_state(const std::string& name) { ns_map::iterator i = name_state_map_.find(name); if (i == name_state_map_.end()) { - taa::state* s = new taa::state; + taa_tgba::state* s = new taa_tgba::state; name_state_map_[name] = s; state_name_map_[s] = name; return s; @@ -244,8 +244,8 @@ namespace spot return i->second; } - taa::state_set* - taa::add_state_set(const std::vector& names) + taa_tgba::state_set* + taa_tgba::add_state_set(const std::vector& names) { state_set* ss = new state_set; for (unsigned i = 0; i < names.size(); ++i) @@ -255,7 +255,7 @@ namespace spot } std::string - taa::format_state_set(const taa::state_set* ss) const + taa_tgba::format_state_set(const taa_tgba::state_set* ss) const { state_set::const_iterator i1 = ss->begin(); sn_map::const_iterator i2; @@ -286,7 +286,7 @@ namespace spot | state_set | `----------*/ - const taa::state_set* + const taa_tgba::state_set* state_set::get_state() const { return s_; @@ -298,14 +298,14 @@ namespace spot const state_set* o = dynamic_cast(other); assert(o); - const taa::state_set* s1 = get_state(); - const taa::state_set* s2 = o->get_state(); + const taa_tgba::state_set* s1 = get_state(); + const taa_tgba::state_set* s2 = o->get_state(); if (s1->size() != s2->size()) return s1->size() - s2->size(); - taa::state_set::const_iterator it1 = s1->begin(); - taa::state_set::const_iterator it2 = s2->begin(); + taa_tgba::state_set::const_iterator it1 = s1->begin(); + taa_tgba::state_set::const_iterator it2 = s2->begin(); while (it2 != s2->end()) { int i = *it1++ - *it2++; @@ -319,7 +319,7 @@ namespace spot state_set::hash() const { size_t res = 0; - taa::state_set::const_iterator it = s_->begin(); + taa_tgba::state_set::const_iterator it = s_->begin(); while (it != s_->end()) { res ^= reinterpret_cast(*it++) - static_cast(0); @@ -332,7 +332,7 @@ namespace spot state_set::clone() const { if (delete_me_ && s_) - return new spot::state_set(new taa::state_set(*s_), true); + return new spot::state_set(new taa_tgba::state_set(*s_), true); else return new spot::state_set(s_, false); } @@ -341,21 +341,22 @@ namespace spot | taa_succ_iter | `--------------*/ - taa_succ_iterator::taa_succ_iterator(const taa::state_set* s, bdd all_acc) + taa_succ_iterator::taa_succ_iterator(const taa_tgba::state_set* s, + bdd all_acc) : all_acceptance_conditions_(all_acc), seen_() { if (s->empty()) { - taa::transition* t = new taa::transition; + taa_tgba::transition* t = new taa_tgba::transition; t->condition = bddtrue; t->acceptance_conditions = bddfalse; - t->dst = new taa::state_set; + t->dst = new taa_tgba::state_set; succ_.push_back(t); return; } bounds_t bounds; - for (taa::state_set::const_iterator i = s->begin(); i != s->end(); ++i) + for (taa_tgba::state_set::const_iterator i = s->begin(); i != s->end(); ++i) bounds.push_back(std::make_pair((*i)->begin(), (*i)->end())); /// Sorting might make the cartesian product faster by not @@ -369,15 +370,15 @@ namespace spot while (pos[0] != bounds[0].second) { - taa::transition* t = new taa::transition; + taa_tgba::transition* t = new taa_tgba::transition; t->condition = bddtrue; t->acceptance_conditions = bddfalse; - taa::state_set* ss = new taa::state_set; + taa_tgba::state_set* ss = new taa_tgba::state_set; unsigned p; for (p = 0; p < pos.size() && t->condition != bddfalse; ++p) { - taa::state_set::const_iterator j; + taa_tgba::state_set::const_iterator j; for (j = (*pos[p])->dst->begin(); j != (*pos[p])->dst->end(); ++j) if ((*j)->size() > 0) // Remove sink states. ss->insert(*j); @@ -475,7 +476,7 @@ namespace spot taa_succ_iterator::current_state() const { assert(!done()); - return new spot::state_set(new taa::state_set(*(*i_)->dst), true); + return new spot::state_set(new taa_tgba::state_set(*(*i_)->dst), true); } bdd diff --git a/src/tgba/taa.hh b/src/tgba/taatgba.hh similarity index 80% rename from src/tgba/taa.hh rename to src/tgba/taatgba.hh index ad3ae9bbe..9ec0fd416 100644 --- a/src/tgba/taa.hh +++ b/src/tgba/taatgba.hh @@ -19,8 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TGBA_TAA_HH -# define SPOT_TGBA_TAA_HH +#ifndef SPOT_TGBA_TAATGBA_HH +# define SPOT_TGBA_TAATGBA_HH #include #include @@ -33,10 +33,10 @@ namespace spot { /// \brief A Transition-based Alternating Automaton (TAA). - class taa : public tgba + class taa_tgba : public tgba { public: - taa(bdd_dict* dict); + taa_tgba(bdd_dict* dict); struct transition; typedef std::list state; @@ -66,7 +66,7 @@ namespace spot void output(std::ostream& os) const; /// TGBA interface. - virtual ~taa(); + virtual ~taa_tgba(); virtual spot::state* get_init_state() const; virtual tgba_succ_iterator* succ_iter(const spot::state* local_state, @@ -92,14 +92,14 @@ namespace spot virtual bdd compute_support_variables(const spot::state* state) const; typedef Sgi::hash_map< - const std::string, taa::state*, string_hash + const std::string, taa_tgba::state*, string_hash > ns_map; typedef Sgi::hash_map< - const taa::state*, std::string, ptr_hash + const taa_tgba::state*, std::string, ptr_hash > sn_map; - typedef std::vector ss_vec; + typedef std::vector ss_vec; ns_map name_state_map_; sn_map state_name_map_; @@ -107,31 +107,31 @@ namespace spot mutable bdd all_acceptance_conditions_; mutable bool all_acceptance_conditions_computed_; bdd neg_acceptance_conditions_; - taa::state_set* init_; + taa_tgba::state_set* init_; ss_vec state_set_vec_; private: // Disallow copy. - taa(const taa& other); - taa& operator=(const taa& other); + taa_tgba(const taa_tgba& other); + taa_tgba& operator=(const taa_tgba& other); - /// \brief Return the taa::state for \a name, creating it if it + /// \brief Return the taa_tgba::state for \a name, creating it if it /// does not exist. The first state added is the initial state /// which can be overridden with set_init_state. - taa::state* add_state(const std::string& name); + taa_tgba::state* add_state(const std::string& name); /// \brief Return the taa::state_set for \a names. - taa::state_set* add_state_set(const std::vector& names); + taa_tgba::state_set* add_state_set(const std::vector& names); /// \brief Format a taa::state_set as a string for printing. - std::string format_state_set(const taa::state_set* ss) const; + std::string format_state_set(const taa_tgba::state_set* ss) const; }; /// Set of states deriving from spot::state. class state_set : public spot::state { public: - state_set(const taa::state_set* s, bool delete_me = false) + state_set(const taa_tgba::state_set* s, bool delete_me = false) : s_(s), delete_me_(delete_me) { } @@ -146,16 +146,16 @@ namespace spot delete s_; } - const taa::state_set* get_state() const; + const taa_tgba::state_set* get_state() const; private: - const taa::state_set* s_; + const taa_tgba::state_set* s_; bool delete_me_; }; class taa_succ_iterator : public tgba_succ_iterator { public: - taa_succ_iterator(const taa::state_set* s, bdd all_acc); + taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc); virtual ~taa_succ_iterator(); virtual void first(); @@ -169,12 +169,12 @@ namespace spot private: /// Those typedefs are used to generate all possible successors in /// the constructor using a cartesian product. - typedef taa::state::const_iterator iterator; + typedef taa_tgba::state::const_iterator iterator; typedef std::pair iterator_pair; typedef std::vector bounds_t; typedef Sgi::hash_multimap< - const spot::state_set*, taa::transition*, state_ptr_hash, state_ptr_equal - > seen_map; + const spot::state_set*, taa_tgba::transition*, state_ptr_hash, + state_ptr_equal> seen_map; struct distance_sort : public std::binary_function::const_iterator i_; - std::vector succ_; + std::vector::const_iterator i_; + std::vector succ_; bdd all_acceptance_conditions_; seen_map seen_; }; } -#endif // SPOT_TGBA_TAA_HH +#endif // SPOT_TGBA_TAATGBA_HH diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index eedff07c1..65c0083f6 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -39,7 +39,7 @@ namespace spot class ltl2taa_visitor : public const_visitor { public: - ltl2taa_visitor(taa* res, language_containment_checker* lcc, + ltl2taa_visitor(taa_tgba* res, language_containment_checker* lcc, bool refined = false, bool negated = false) : res_(res), refined_(refined), negated_(negated), lcc_(lcc), init_(), succ_(), to_free_() @@ -51,7 +51,7 @@ namespace spot { } - taa* + taa_tgba* result() { for (unsigned i = 0; i < to_free_.size(); ++i) @@ -73,7 +73,7 @@ namespace spot std::vector dst; dst.push_back(std::string("sink")); - taa::transition* t = res_->create_transition(init_, dst); + taa_tgba::transition* t = res_->create_transition(init_, dst); res_->add_condition(t, f->clone()); succ_state ss = { dst, f, constant::true_instance() }; succ_.push_back(ss); @@ -146,7 +146,7 @@ namespace spot init_ = to_string(node); std::vector::iterator i1; std::vector::iterator i2; - taa::transition* t = 0; + taa_tgba::transition* t = 0; bool contained = false; switch (node->op()) { @@ -232,7 +232,7 @@ namespace spot init_ = to_string(node); std::vector::iterator i; - taa::transition* t = 0; + taa_tgba::transition* t = 0; switch (node->op()) { case multop::And: @@ -305,7 +305,7 @@ namespace spot } private: - taa* res_; + taa_tgba* res_; bool refined_; bool negated_; language_containment_checker* lcc_; @@ -373,7 +373,7 @@ namespace spot }; } // anonymous - taa* + taa_tgba* ltl_to_taa(const ltl::formula* f, bdd_dict* dict, bool refined_rules) { // TODO: s/unabbreviate_ltl/unabbreviate_logic/ @@ -381,7 +381,7 @@ namespace spot const ltl::formula* f2 = ltl::negative_normal_form(f1); f1->destroy(); - spot::taa* res = new spot::taa(dict); + spot::taa_tgba* res = new spot::taa_tgba(dict); bdd_dict b; language_containment_checker* lcc = new language_containment_checker(&b, false, false, false, false); diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh index 3b81a60bf..77fe723d6 100644 --- a/src/tgbaalgos/ltl2taa.hh +++ b/src/tgbaalgos/ltl2taa.hh @@ -23,7 +23,7 @@ # define SPOT_TGBAALGOS_LTL2TAA_HH #include "ltlast/formula.hh" -#include "tgba/taa.hh" +#include "tgba/taatgba.hh" namespace spot { @@ -49,8 +49,8 @@ namespace spot /// \param dict The spot::bdd_dict the constructed automata should use. /// \param refined_rules If this parameter is set, refined rules are used. /// \return A spot::taa that recognizes the language of \a f. - taa* ltl_to_taa(const ltl::formula* f, bdd_dict* dict, - bool refined_rules = false); + taa_tgba* ltl_to_taa(const ltl::formula* f, bdd_dict* dict, + bool refined_rules = false); } #endif // SPOT_TGBAALGOS_LTL2TAA_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index bba1e257d..913c9a7a9 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -41,7 +41,7 @@ check_PROGRAMS = \ readsave \ reductgba \ reduccmp \ - taa \ + taatgba \ tgbaread \ tripprod @@ -63,7 +63,7 @@ readsave_SOURCES = readsave.cc reductgba_SOURCES = reductgba.cc reduccmp_SOURCES = reductgba.cc reduccmp_CXXFLAGS = -DREDUCCMP -taa_SOURCES = taa.cc +taatgba_SOURCES = taatgba.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc @@ -72,7 +72,7 @@ tripprod_SOURCES = tripprod.cc TESTS = \ eltl2tgba.test \ explicit.test \ - taa.test \ + taatgba.test \ tgbaread.test \ readsave.test \ ltl2tgba.test \ diff --git a/src/tgbatest/taa.cc b/src/tgbatest/taatgba.cc similarity index 90% rename from src/tgbatest/taa.cc rename to src/tgbatest/taatgba.cc index 2c5922580..48be22c6b 100644 --- a/src/tgbatest/taa.cc +++ b/src/tgbatest/taatgba.cc @@ -25,7 +25,7 @@ #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" #include "tgbaalgos/dotty.hh" -#include "tgba/taa.hh" +#include "tgba/taatgba.hh" int main() @@ -34,11 +34,11 @@ main() spot::ltl::default_environment& e = spot::ltl::default_environment::instance(); - spot::taa* a = new spot::taa(dict); + spot::taa_tgba* a = new spot::taa_tgba(dict); - typedef spot::taa::transition trans; - typedef spot::taa::state state; - typedef spot::taa::state_set state_set; + typedef spot::taa_tgba::transition trans; + typedef spot::taa_tgba::state state; + typedef spot::taa_tgba::state_set state_set; std::string ss1_values[] = { "state 2", "state 3" }; std::vector ss1_vector(ss1_values, ss1_values + 2); diff --git a/src/tgbatest/taa.test b/src/tgbatest/taatgba.test similarity index 59% rename from src/tgbatest/taa.test rename to src/tgbatest/taatgba.test index d7e39d256..5dc1ecbd8 100755 --- a/src/tgbatest/taa.test +++ b/src/tgbatest/taatgba.test @@ -3,4 +3,4 @@ . ./defs || exit -1 set -e -run 0 ../taa || exit 1 +run 0 ../taatgba || exit 1