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

fix previous two patches

Browse source 
make sure we don't split a label with a label that subsume it

* spot/twaalgos/alternation.cc, spot/twaalgos/dualize.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2024-03-18 10:37:21 +01:00
parent f26f3243dd
commit ef10be047c
2 changed files with 3 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/alternation.cc
View file

@ -408,14 +408,12 @@ namespace spot
separated_labels.push_back(bddtrue); separated_labels.push_back(bddtrue);
for (auto& lab: all_labels) for (auto& lab: all_labels)
{ {
// make sure don't realloc during the loop
separated_labels.reserve(separated_labels.size() * 2);
// Do not use a range-based or iterator-based for loop // Do not use a range-based or iterator-based for loop
// here, as push_back invalidates the end iterator. // here, as push_back invalidates the end iterator.
for (unsigned cur = 0, sz = separated_labels.size(); for (unsigned cur = 0, sz = separated_labels.size();
cur < sz; ++cur) cur < sz; ++cur)
if (bdd common = separated_labels[cur] & lab; if (bdd common = separated_labels[cur] & lab;
common != bddfalse) common != bddfalse && common != separated_labels[cur])
{ {
separated_labels[cur] -= lab; separated_labels[cur] -= lab;
separated_labels.push_back(common); separated_labels.push_back(common);

5
spot/twaalgos/dualize.cc
View file

@ -200,13 +200,12 @@ namespace spot
labels.push_back(bddtrue); labels.push_back(bddtrue);
for (auto& e: aut_->out(i)) for (auto& e: aut_->out(i))
{ {
// make sure we don't realloc during the loop
labels.reserve(labels.size() * 2);
// Do not use a range-based or iterator-based for // Do not use a range-based or iterator-based for
// loop here, as push_back invalidates the end // loop here, as push_back invalidates the end
// iterator. // iterator.
for (unsigned cur = 0, sz = labels.size(); cur < sz; ++cur) for (unsigned cur = 0, sz = labels.size(); cur < sz; ++cur)
if (bdd common = labels[cur] & e.cond; common != bddfalse) if (bdd common = labels[cur] & e.cond;
common != bddfalse && common != labels[cur])
{ {
labels[cur] -= e.cond; labels[cur] -= e.cond;
labels.push_back(common); labels.push_back(common);