From 6ebbb930240e5411c43ec5a0665d52d80235def9 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Thu, 7 Jul 2022 16:40:41 +0200
Subject: [PATCH] twaalgos: filter accepting sinks in oe combiner

---
 spot/twaalgos/alternation.cc | 21 ++++++++++++++++++---
 spot/twaalgos/alternation.hh |  3 ++-
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc
index c7b2a17d5..d5d59a961 100644
--- a/spot/twaalgos/alternation.cc
+++ b/spot/twaalgos/alternation.cc
@@ -28,8 +28,8 @@
 
 namespace spot
 {
-  outedge_combiner::outedge_combiner(const twa_graph_ptr& aut)
-    : aut_(aut), vars_(bddtrue)
+  outedge_combiner::outedge_combiner(const twa_graph_ptr& aut, unsigned sink)
+    : aut_(aut), vars_(bddtrue), acc_sink_(sink)
   {
   }
 
@@ -50,6 +50,9 @@ namespace spot
             bdd out = bddtrue;
             for (unsigned d: aut_->univ_dests(e.dst))
               {
+                if (d == acc_sink_)
+                  continue;
+
                 auto p = state_to_var.emplace(d, 0);
                 if (p.second)
                   {
@@ -78,7 +81,17 @@ namespace spot
       {
         bdd cond = bdd_exist(cube, vars_);
         bdd dest = bdd_existcomp(cube, vars_);
-        while (dest != bddtrue)
+
+        if (dest == bddtrue)
+          {
+            // if dest is bddtrue then the accepting sink is the only
+            // destination for this edge, in that case don't filter it out
+            assert(acc_sink_ != -1u);
+            aut_->new_edge(st, acc_sink_, cond);
+            continue;
+          }
+
+        do
           {
             assert(bdd_low(dest) == bddfalse);
             auto it = var_to_state.find(bdd_var(dest));
@@ -86,6 +99,8 @@ namespace spot
             univ_dest.push_back(it->second);
             dest = bdd_high(dest);
           }
+        while  (dest != bddtrue);
+
         std::sort(univ_dest.begin(), univ_dest.end());
         aut_->new_univ_edge(st, univ_dest.begin(), univ_dest.end(), cond);
         univ_dest.clear();
diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh
index a03ddc121..9490272a1 100644
--- a/spot/twaalgos/alternation.hh
+++ b/spot/twaalgos/alternation.hh
@@ -49,8 +49,9 @@ namespace spot
     std::map<unsigned, int> state_to_var;
     std::map<int, unsigned> var_to_state;
     bdd vars_;
+    unsigned acc_sink_;
   public:
-    outedge_combiner(const twa_graph_ptr& aut);
+    outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u);
     ~outedge_combiner();
     bdd operator()(unsigned st);
     void new_dests(unsigned st, bdd out) const;