diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index 9978d925d..0896dd6b5 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -18,9 +18,11 @@ // along with this program. If not, see . #include "config.h" +#include #include #include #include +#include #include #include #include @@ -495,6 +497,22 @@ namespace spot } exp = exp_new; } + + // sort and remove duplicates from expansion to canonicalize it for + // eventual signature use + if (exp.size() >= 2) + { + 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); + }); + exp.erase(std::unique(exp.begin(), exp.end()), exp.end()); + } } } diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc index 012ac11e8..ecd98f5cb 100644 --- a/spot/tl/expansions2.cc +++ b/spot/tl/expansions2.cc @@ -18,9 +18,11 @@ // along with this program. If not, see . #include "config.h" +#include #include #include #include +#include #include #include #include @@ -495,6 +497,21 @@ namespace spot } exp = exp_new; } + + // sort expansion to canonicalize it for eventual signature use + if (exp.size() >= 2) + { + 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); + }); + exp.erase(std::unique(exp.begin(), exp.end()), exp.end()); + } } }