Commit 9cebcdc1 authored by Damien Lefortier's avatar Damien Lefortier
Browse files

* 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.
parent be78c82e
2010-01-18 Damien Lefortier <dam@lrde.epita.fr>
* 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 <sadegh@lrde.epita.fr> 2010-01-16 Guillaume Sadegh <sadegh@lrde.epita.fr>
* src/saba/sabacomplementtgba.cc: Fix a bug. * src/saba/sabacomplementtgba.cc: Fix a bug.
......
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
#include <iostream> #include <iostream>
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh"
#include "misc/bddop.hh" #include "misc/bddop.hh"
#include "taatgba.hh" #include "taatgba.hh"
...@@ -350,7 +351,13 @@ namespace spot ...@@ -350,7 +351,13 @@ namespace spot
`----------------*/ `----------------*/
std::string 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; return label;
} }
...@@ -359,9 +366,22 @@ namespace spot ...@@ -359,9 +366,22 @@ namespace spot
| taa_tgba_formula | | 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 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); return ltl::to_string(label);
} }
ltl::formula*
taa_tgba_formula::clone_if(const label_t& label) const
{
return label->clone();
}
} }
...@@ -264,6 +264,8 @@ namespace spot ...@@ -264,6 +264,8 @@ namespace spot
} }
protected: protected:
typedef label label_t;
typedef Sgi::hash_map< typedef Sgi::hash_map<
const label, taa_tgba::state*, label_hash const label, taa_tgba::state*, label_hash
> ns_map; > ns_map;
...@@ -275,7 +277,11 @@ namespace spot ...@@ -275,7 +277,11 @@ namespace spot
sn_map state_name_map_; sn_map state_name_map_;
/// \brief Return a label as a string. /// \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: private:
/// \brief Return the taa_tgba::state for \a name, creating it /// \brief Return the taa_tgba::state for \a name, creating it
...@@ -285,9 +291,10 @@ namespace spot ...@@ -285,9 +291,10 @@ namespace spot
typename ns_map::iterator i = name_state_map_.find(name); typename ns_map::iterator i = name_state_map_.find(name);
if (i == name_state_map_.end()) if (i == name_state_map_.end())
{ {
const label& name_ = clone_if(name);
taa_tgba::state* s = new taa_tgba::state; taa_tgba::state* s = new taa_tgba::state;
name_state_map_[name] = s; name_state_map_[name_] = s;
state_name_map_[s] = name; state_name_map_[s] = name_;
return s; return s;
} }
return i->second; return i->second;
...@@ -338,17 +345,21 @@ namespace spot ...@@ -338,17 +345,21 @@ namespace spot
taa_tgba_string(bdd_dict* dict) : taa_tgba_string(bdd_dict* dict) :
taa_tgba_labelled<std::string, string_hash>(dict) {}; taa_tgba_labelled<std::string, string_hash>(dict) {};
protected: 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 : class taa_tgba_formula :
public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash> public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
{ {
public: public:
taa_tgba_formula(bdd_dict* dict): taa_tgba_formula(bdd_dict* dict) :
taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {}; taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {};
// Labels are pointers here and must be destroyed eventually.
~taa_tgba_formula();
protected: 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;
}; };
} }
......
...@@ -95,10 +95,10 @@ namespace spot ...@@ -95,10 +95,10 @@ namespace spot
// A little hack to define a sink // A little hack to define a sink
dst.push_back(unop::instance(unop::Finish, dst.push_back(unop::instance(unop::Finish,
constant::true_instance())); constant::true_instance()));
to_free_.push_back(dst[0]);
res_->create_transition(init_, dst); res_->create_transition(init_, dst);
succ_state ss = { dst, node, a }; succ_state ss = { dst, node, a };
succ_.push_back(ss); succ_.push_back(ss);
to_free_.push_back(dst[0]);
return; return;
} }
case constant::False: case constant::False:
...@@ -169,7 +169,7 @@ namespace spot ...@@ -169,7 +169,7 @@ namespace spot
(remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end()); (remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end());
i1->Q.push_back(init_); // Add the initial state 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); t = res_->create_transition(init_, i1->Q);
res_->add_condition(t, i1->condition->clone()); res_->add_condition(t, i1->condition->clone());
res_->add_acceptance_condition(t, node->second()->clone()); res_->add_acceptance_condition(t, node->second()->clone());
...@@ -231,14 +231,9 @@ namespace spot ...@@ -231,14 +231,9 @@ namespace spot
void void
visit(const multop* node) visit(const multop* node)
{ {
bool ok = true;
std::vector<ltl2taa_visitor> vs; std::vector<ltl2taa_visitor> vs;
for (unsigned n = 0; n < node->size(); ++n) for (unsigned n = 0; n < node->size(); ++n)
{
vs.push_back(recurse(node->nth(n))); vs.push_back(recurse(node->nth(n)));
if (vs[n].succ_.empty()) // Handle 0
ok = false;
}
init_ = node; init_ = node;
std::vector<succ_state>::iterator i; std::vector<succ_state>::iterator i;
...@@ -248,7 +243,7 @@ namespace spot ...@@ -248,7 +243,7 @@ namespace spot
case multop::And: case multop::And:
{ {
std::vector<succ_state> p = all_n_tuples(vs); std::vector<succ_state> p = all_n_tuples(vs);
for (unsigned n = 0; n < p.size() && ok; ++n) for (unsigned n = 0; n < p.size(); ++n)
{ {
if (refined_) if (refined_)
{ {
...@@ -274,7 +269,7 @@ namespace spot ...@@ -274,7 +269,7 @@ namespace spot
for (unsigned i = 0; i < p[n].acc.size(); ++i) for (unsigned i = 0; i < p[n].acc.size(); ++i)
res_->add_acceptance_condition(t, p[n].acc[i]->clone()); res_->add_acceptance_condition(t, p[n].acc[i]->clone());
succ_.push_back(p[n]); succ_.push_back(p[n]);
return; continue;
} }
} }
t = res_->create_transition(init_, p[n].Q); t = res_->create_transition(init_, p[n].Q);
...@@ -342,9 +337,9 @@ namespace spot ...@@ -342,9 +337,9 @@ namespace spot
{ {
std::vector<succ_state> product; std::vector<succ_state> product;
std::vector<int> pos; std::vector<int> pos(vs.size());
for (unsigned i = 0; i < vs.size(); ++i) 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) while (pos[0] != 0)
{ {
......
...@@ -777,6 +777,15 @@ main(int argc, char** argv) ...@@ -777,6 +777,15 @@ main(int argc, char** argv)
a = state_labeled = new spot::tgba_sgba_proxy(a); 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<spot::tgba_bdd_concrete*>(a))
bc->delete_unaccepting_scc();
tm.stop("reducing A_f w/ SCC on BDD");
}
spot::tgba_reduc* aut_red = 0; spot::tgba_reduc* aut_red = 0;
spot::tgba* aut_scc = 0; spot::tgba* aut_scc = 0;
if (reduc_aut != spot::Reduce_None) if (reduc_aut != spot::Reduce_None)
...@@ -789,15 +798,6 @@ main(int argc, char** argv) ...@@ -789,15 +798,6 @@ main(int argc, char** argv)
tm.stop("reducing A_f w/ SCC"); 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<spot::tgba_bdd_concrete*>(a))
bc->delete_unaccepting_scc();
tm.stop("reducing A_f w/ SCC on BDD");
}
if (reduc_aut & ~spot::Reduce_Scc) if (reduc_aut & ~spot::Reduce_Scc)
{ {
tm.start("reducing A_f w/ sim."); tm.start("reducing A_f w/ sim.");
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment