From b93fb41af2578a342961554c5129f1e1a983df2a Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Fri, 7 Mar 2025 11:24:00 +0100 Subject: [PATCH] expansions: fix sort behavior The previous implementation was wrong and led to segfaults when sorting large expansions --- spot/tl/expansions.cc | 10 +++------- spot/tl/expansions2.cc | 10 +++------- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index 0896dd6b5..402236ea6 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -504,13 +504,9 @@ namespace spot { std::sort(exp.begin(), exp.end(), [](const auto& lhs, const auto& rhs) { - bdd_less_than_stable blt; - // first sort by label, then by suffix - if (blt(lhs.first, rhs.first)) - return true; - formula_ptr_less_than_bool_first flt; - return flt(lhs.second, rhs.second); - }); + return std::make_pair(lhs.first.id(), lhs.second.id()) + < std::make_pair(rhs.first.id(), rhs.second.id()); + }); exp.erase(std::unique(exp.begin(), exp.end()), exp.end()); } } diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc index ecd98f5cb..d80e5ffa3 100644 --- a/spot/tl/expansions2.cc +++ b/spot/tl/expansions2.cc @@ -503,13 +503,9 @@ namespace spot { std::sort(exp.begin(), exp.end(), [](const auto& lhs, const auto& rhs) { - bdd_less_than_stable blt; - // first sort by label, then by suffix - if (blt(lhs.first, rhs.first)) - return true; - formula_ptr_less_than_bool_first flt; - return flt(lhs.second, rhs.second); - }); + return std::make_pair(lhs.first.id(), lhs.second.id()) + < std::make_pair(rhs.first.id(), rhs.second.id()); + }); exp.erase(std::unique(exp.begin(), exp.end()), exp.end()); } }