diff --git a/ChangeLog b/ChangeLog index 4f1db1be2..6daabf8f2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2010-01-18 Damien Lefortier + + * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Fix memory issues + occuring when labels are pointers. + * src/tgbaalgos/ltl2taa.cc: Fix a bug. + * src/tgbatest/ltl2tgba.cc: Fix a bug. + 2010-01-16 Guillaume Sadegh * src/saba/sabacomplementtgba.cc: Fix a bug. diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index d085c14ff..8e5afbdde 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -25,6 +25,7 @@ #include #include "tgba/formula2bdd.hh" #include "ltlvisit/tostring.hh" +#include "ltlvisit/clone.hh" #include "misc/bddop.hh" #include "taatgba.hh" @@ -350,7 +351,13 @@ namespace spot `----------------*/ std::string - taa_tgba_string::label_to_string(const std::string label) const + taa_tgba_string::label_to_string(const label_t& label) const + { + return label; + } + + std::string + taa_tgba_string::clone_if(const label_t& label) const { return label; } @@ -359,9 +366,22 @@ namespace spot | taa_tgba_formula | `-----------------*/ + taa_tgba_formula::~taa_tgba_formula() + { + ns_map::iterator i; + for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) + i->first->destroy(); + } + std::string - taa_tgba_formula::label_to_string(const ltl::formula* label) const + taa_tgba_formula::label_to_string(const label_t& label) const { return ltl::to_string(label); } + + ltl::formula* + taa_tgba_formula::clone_if(const label_t& label) const + { + return label->clone(); + } } diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 8ca8088e6..afd5cc328 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -264,6 +264,8 @@ namespace spot } protected: + typedef label label_t; + typedef Sgi::hash_map< const label, taa_tgba::state*, label_hash > ns_map; @@ -275,7 +277,11 @@ namespace spot sn_map state_name_map_; /// \brief Return a label as a string. - virtual std::string label_to_string(const label lbl) const = 0; + virtual std::string label_to_string(const label_t& lbl) const = 0; + + /// \brief Clone the label if necessary to assure it is owned by + /// this, avoiding memory issues when label is a pointer. + virtual label_t clone_if(const label_t& lbl) const = 0; private: /// \brief Return the taa_tgba::state for \a name, creating it @@ -285,9 +291,10 @@ namespace spot typename ns_map::iterator i = name_state_map_.find(name); if (i == name_state_map_.end()) { + const label& name_ = clone_if(name); taa_tgba::state* s = new taa_tgba::state; - name_state_map_[name] = s; - state_name_map_[s] = name; + name_state_map_[name_] = s; + state_name_map_[s] = name_; return s; } return i->second; @@ -338,17 +345,21 @@ namespace spot taa_tgba_string(bdd_dict* dict) : taa_tgba_labelled(dict) {}; protected: - virtual std::string label_to_string(const std::string label) const; + virtual std::string label_to_string(const std::string& label) const; + virtual std::string clone_if(const std::string& label) const; }; class taa_tgba_formula : public taa_tgba_labelled { public: - taa_tgba_formula(bdd_dict* dict): + taa_tgba_formula(bdd_dict* dict) : taa_tgba_labelled(dict) {}; + // Labels are pointers here and must be destroyed eventually. + ~taa_tgba_formula(); protected: - virtual std::string label_to_string(const ltl::formula* label) const; + virtual std::string label_to_string(const label_t& label) const; + virtual ltl::formula* clone_if(const label_t& label) const; }; } diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 65efa8a10..ea7d74ce2 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -95,10 +95,10 @@ namespace spot // A little hack to define a sink dst.push_back(unop::instance(unop::Finish, constant::true_instance())); - to_free_.push_back(dst[0]); res_->create_transition(init_, dst); succ_state ss = { dst, node, a }; succ_.push_back(ss); + to_free_.push_back(dst[0]); return; } case constant::False: @@ -169,7 +169,7 @@ namespace spot (remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end()); i1->Q.push_back(init_); // Add the initial state - i1->acc.push_back(node); + i1->acc.push_back(node->second()); t = res_->create_transition(init_, i1->Q); res_->add_condition(t, i1->condition->clone()); res_->add_acceptance_condition(t, node->second()->clone()); @@ -231,14 +231,9 @@ namespace spot void visit(const multop* node) { - bool ok = true; std::vector vs; for (unsigned n = 0; n < node->size(); ++n) - { vs.push_back(recurse(node->nth(n))); - if (vs[n].succ_.empty()) // Handle 0 - ok = false; - } init_ = node; std::vector::iterator i; @@ -248,7 +243,7 @@ namespace spot case multop::And: { std::vector p = all_n_tuples(vs); - for (unsigned n = 0; n < p.size() && ok; ++n) + for (unsigned n = 0; n < p.size(); ++n) { if (refined_) { @@ -274,7 +269,7 @@ namespace spot for (unsigned i = 0; i < p[n].acc.size(); ++i) res_->add_acceptance_condition(t, p[n].acc[i]->clone()); succ_.push_back(p[n]); - return; + continue; } } t = res_->create_transition(init_, p[n].Q); @@ -342,9 +337,9 @@ namespace spot { std::vector product; - std::vector pos; + std::vector pos(vs.size()); for (unsigned i = 0; i < vs.size(); ++i) - pos.push_back(vs[i].succ_.size()); + pos[i] = vs[i].succ_.size(); while (pos[0] != 0) { diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 127c9e10f..f840341fc 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -777,6 +777,15 @@ main(int argc, char** argv) a = state_labeled = new spot::tgba_sgba_proxy(a); } + if (delete_unaccepting_scc) + { + tm.start("reducing A_f w/ SCC on BDD"); + if (spot::tgba_bdd_concrete* bc = + dynamic_cast(a)) + bc->delete_unaccepting_scc(); + tm.stop("reducing A_f w/ SCC on BDD"); + } + spot::tgba_reduc* aut_red = 0; spot::tgba* aut_scc = 0; if (reduc_aut != spot::Reduce_None) @@ -789,15 +798,6 @@ main(int argc, char** argv) tm.stop("reducing A_f w/ SCC"); } - if (delete_unaccepting_scc) - { - tm.start("reducing A_f w/ SCC on BDD"); - if (spot::tgba_bdd_concrete* bc = - dynamic_cast(a)) - bc->delete_unaccepting_scc(); - tm.stop("reducing A_f w/ SCC on BDD"); - } - if (reduc_aut & ~spot::Reduce_Scc) { tm.start("reducing A_f w/ sim.");