From ef10be047c6b68c95002cdc54b0b656d1cd67842 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Mar 2024 10:37:21 +0100 Subject: [PATCH] fix previous two patches make sure we don't split a label with a label that subsume it * spot/twaalgos/alternation.cc, spot/twaalgos/dualize.cc: Here. --- spot/twaalgos/alternation.cc | 4 +--- spot/twaalgos/dualize.cc | 5 ++--- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index dad0f307a..b7e44a200 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -408,14 +408,12 @@ namespace spot separated_labels.push_back(bddtrue); 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 // here, as push_back invalidates the end iterator. for (unsigned cur = 0, sz = separated_labels.size(); cur < sz; ++cur) if (bdd common = separated_labels[cur] & lab; - common != bddfalse) + common != bddfalse && common != separated_labels[cur]) { separated_labels[cur] -= lab; separated_labels.push_back(common); diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index cbef6d451..bd0f4767d 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -200,13 +200,12 @@ namespace spot labels.push_back(bddtrue); 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 // loop here, as push_back invalidates the end // iterator. 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.push_back(common);