From 05e6e088590fc9303dd948f1c238a0ea7c3ea7f0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 24 Jul 2020 16:24:28 +0200
Subject: [PATCH] tra_to_tba: remove more useless edges

* spot/twaalgos/remfin.cc (tra_to_tba): Implement the same
optimization has in the generic remove_fin transformation.
* tests/python/tra2tba.py: Adjust.
---
 NEWS                    |  3 ++-
 spot/twaalgos/remfin.cc | 17 ++++++++++++++---
 tests/python/tra2tba.py | 11 ++---------
 3 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/NEWS b/NEWS
index d54f1b670..ad79561b7 100644
--- a/NEWS
+++ b/NEWS
@@ -49,7 +49,8 @@ New in spot 2.9.3.dev  (not yet released)
     used to take ages are now instantaneous.  (See issue #412.)
 
   - remove_fin() learned to remove more unnecessary edges by using
-    propagate_marks_vector().
+    propagate_marks_vector(), both in the general case and in the
+    Rabin-like case.
 
   Bugs fixed:
 
diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index e812fdd05..646db08e5 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -210,9 +210,13 @@ namespace spot
       std::vector<bool> scc_is_tba_type(si.scc_count(), false);
       std::vector<bool> final(aut->edge_vector().size(), false);
 
+      bool tba_type = true;
       for (unsigned scc = 0; scc < si.scc_count(); ++scc)
-        scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc,
-                                               aut_pairs, final);
+        {
+          bool res = is_scc_tba_type(aut, si, scc, aut_pairs, final);
+          scc_is_tba_type[scc] = res;
+          tba_type &= res;
+        }
 
       auto res = make_twa_graph(aut->get_dict());
       res->copy_ap_of(aut);
@@ -223,6 +227,11 @@ namespace spot
       trival deterministic = aut->prop_universal();
       trival complete = aut->prop_complete();
 
+      std::vector<bool> accedge(aut->edge_vector().size(), false);
+      std::vector<acc_cond::mark_t> propmarks;
+      if (!tba_type)
+        propmarks = propagate_marks_vector(aut, &si);
+
       std::vector<unsigned> state_map(aut->num_states());
       for (unsigned scc = 0; scc < si.scc_count(); ++scc)
         {
@@ -250,6 +259,8 @@ namespace spot
                 {
                   bool acc = !!(e.acc & scc_infs_alone);
                   res->new_acc_edge(e.src, e.dst, e.cond, acc);
+                  if (acc)
+                    accedge[aut->edge_number(e)] = true;
                 }
 
               auto fins_alone = aut_pairs.fins_alone();
@@ -262,7 +273,7 @@ namespace spot
                       state_map[s] = base++;
                   for (const auto& e: si.inner_edges_of(scc))
                     {
-                      if (e.acc.has(r))
+                      if (e.acc.has(r) || accedge[aut->edge_number(e)])
                         continue;
                       auto src = state_map[e.src];
                       auto dst = state_map[e.dst];
diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py
index e96a4a5fc..2cb1bfb5c 100644
--- a/tests/python/tra2tba.py
+++ b/tests/python/tra2tba.py
@@ -232,7 +232,7 @@ State: 0 "F(Gp3|GFp2)"
 """)
 
 exp = """HOA: v1
-States: 4
+States: 3
 Start: 0
 AP: 2 "p3" "p2"
 acc-name: Buchi
@@ -246,14 +246,8 @@ State: 0
 State: 1 {0}
 [!1] 0
 [1] 1
-[0&!1] 2
-[0&1] 3
 State: 2 {0}
 [0&!1] 2
-[0&1] 3
-State: 3 {0}
-[0&!1] 2
-[0&1] 3
 --END--"""
 
 res = spot.remove_fin(aut)
@@ -648,9 +642,8 @@ State: 0
 [!0] 0
 [0] 0 {0}
 [!0&!1] 1
-[0&!1] 1 {0}
 State: 1
-[!1] 1 {0}
+[!0&!1] 1 {0}
 --END--"""
 
 res = spot.remove_fin(aut)