From abe3da54fb798d27f2a50ce0cad6529c1983b72d Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Thu, 7 Jul 2022 16:38:33 +0200
Subject: [PATCH] graph: filter accepting sinks in univ_dest_mapper

---
 spot/graph/graph.hh | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh
index 04c21fec9..e6afda738 100644
--- a/spot/graph/graph.hh
+++ b/spot/graph/graph.hh
@@ -557,10 +557,11 @@ namespace spot
     {
       std::map<std::vector<unsigned>, unsigned> uniq_;
       G& g_;
+      unsigned acc_sink_;
     public:
 
-      univ_dest_mapper(G& graph)
-        : g_(graph)
+      univ_dest_mapper(G& graph, unsigned sink = -1u)
+        : g_(graph), acc_sink_(sink)
       {
       }
 
@@ -570,6 +571,9 @@ namespace spot
         std::vector<unsigned> tmp(begin, end);
         std::sort(tmp.begin(), tmp.end());
         tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
+        if (acc_sink_ != -1u && tmp.size() > 1)
+          tmp.erase(std::remove(tmp.begin(), tmp.end(), acc_sink_),
+                    tmp.end());
         auto p = uniq_.emplace(tmp, 0);
         if (p.second)
           p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());