From 2e2a3b4544f533faf36157dd621f55edbdedcbb1 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Fri, 16 Sep 2022 15:48:07 +0200
Subject: [PATCH] ltl2aa: finalize UConcat

---
 spot/twaalgos/alternation.cc  |  6 +++++-
 spot/twaalgos/alternation.hh  |  3 ++-
 spot/twaalgos/translate_aa.cc | 11 +++++++----
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc
index 03b8d5c2a..205979f92 100644
--- a/spot/twaalgos/alternation.cc
+++ b/spot/twaalgos/alternation.cc
@@ -38,7 +38,8 @@ namespace spot
     aut_->get_dict()->unregister_all_my_variables(this);
   }
 
-  bdd outedge_combiner::operator()(unsigned st, const std::vector<unsigned>& dst_filter)
+  bdd outedge_combiner::operator()(unsigned st, const std::vector<unsigned>& dst_filter,
+                                   bool remove_original_edges)
   {
     const auto& dict = aut_->get_dict();
     bdd res = bddtrue;
@@ -79,6 +80,9 @@ namespace spot
                 out &= bdd_ithvar(p.first->second);
               }
             res2 |= e.cond & out;
+
+            if (remove_original_edges)
+              e.cond = bddfalse;
           }
 
         if (res2 != bddfalse)
diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh
index 4949006f2..8d1027e8b 100644
--- a/spot/twaalgos/alternation.hh
+++ b/spot/twaalgos/alternation.hh
@@ -53,7 +53,8 @@ namespace spot
   public:
     outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u);
     ~outedge_combiner();
-    bdd operator()(unsigned st, const std::vector<unsigned>& dst_filter = std::vector<unsigned>());
+    bdd operator()(unsigned st, const std::vector<unsigned>& dst_filter = std::vector<unsigned>(),
+                   bool remove_original_edges = false);
     void new_dests(unsigned st, bdd out) const;
   };
 
diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc
index 11b783691..bd1a1d3de 100644
--- a/spot/twaalgos/translate_aa.cc
+++ b/spot/twaalgos/translate_aa.cc
@@ -355,15 +355,18 @@ namespace spot
                 unsigned new_st = it->second;
 
                 bdd comb = bddtrue;
-                comb &= oe_(new_st, acc_states);
-                comb &= oe_(rhs_init);
-                oe_.new_dests(new_st, comb);
+                comb &= oe_(new_st, acc_states, true);
+                if (comb != bddtrue)
+                  {
+                    comb &= oe_(rhs_init);
+                    oe_.new_dests(new_st, comb);
+                  }
               }
 
             auto it = old_to_new.find(sere_aut->get_init_state_number());
             assert(it != old_to_new.end());
 
-            //aut_->merge_edges();
+            aut_->merge_edges();
             return it->second;
           }