alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/ltl2taa.cc: Fix the previous patch.

Browse source
This commit is contained in:
Damien Lefortier 2010-01-19 10:43:43 +01:00
parent 9cebcdc124
commit 9fb8701667
2 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2010-01-18 Damien Lefortier <dam@lrde.epita.fr>
* src/tgbaalgos/ltl2taa.cc: Fix the previous patch.
2010-01-18 Damien Lefortier <dam@lrde.epita.fr> 2010-01-18 Damien Lefortier <dam@lrde.epita.fr>
* src/tgba/taatgba.cc, src/tgba/taatgba.hh: Fix memory issues * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Fix memory issues

11
src/tgbaalgos/ltl2taa.cc
View file

@ -231,9 +231,14 @@ 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;
@ -242,6 +247,8 @@ namespace spot
{ {
case multop::And: case multop::And:
{ {
if (!ok)
return;
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(); ++n) for (unsigned n = 0; n < p.size(); ++n)
{ {
@ -397,9 +404,9 @@ namespace spot
new language_containment_checker(&b, false, false, false, false); new language_containment_checker(&b, false, false, false, false);
ltl2taa_visitor v(res, lcc, refined_rules); ltl2taa_visitor v(res, lcc, refined_rules);
f2->accept(v); f2->accept(v);
taa_tgba* taa = v.result(); // Careful: before the destroy!
f2->destroy(); f2->destroy();
delete lcc; delete lcc;
return taa;
return v.result();
} }
} }