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());
+ }
}
}