From 37b814c75092b34580154769a32c409bbc93fb48 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Tue, 4 Mar 2025 19:20:50 +0100
Subject: [PATCH] expansions: make signature canonical

Linear forms are now sorted and duplicates are removed
---
 spot/tl/expansions.cc  | 18 ++++++++++++++++++
 spot/tl/expansions2.cc | 17 +++++++++++++++++
 2 files changed, 35 insertions(+)

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 <http://www.gnu.org/licenses/>.
 
 #include "config.h"
+#include <algorithm>
 #include <spot/misc/minato.hh>
 #include <spot/priv/robin_hood.hh>
 #include <spot/tl/expansions.hh>
+#include <spot/tl/formula.hh>
 #include <spot/twa/bdddict.hh>
 #include <spot/twa/formula2bdd.hh>
 #include <spot/twaalgos/remprop.hh>
@@ -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 <http://www.gnu.org/licenses/>.
 
 #include "config.h"
+#include <algorithm>
 #include <spot/misc/minato.hh>
 #include <spot/priv/robin_hood.hh>
 #include <spot/tl/expansions2.hh>
+#include <spot/tl/formula.hh>
 #include <spot/twa/bdddict.hh>
 #include <spot/twa/formula2bdd.hh>
 #include <spot/twaalgos/remprop.hh>
@@ -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());
+        }
     }
   }