From dd8c00fff02c380e438f50c5b6b7e6d5dbf69c15 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 10 Feb 2020 14:08:05 +0100
Subject: [PATCH] partial_degeneralize: force purge_unreachable in some corner
 case

* spot/twaalgos/degen.cc: If an all-accepting transition has been
redirected, we need to force purge_unreachable_state() to be called,
otherwise we may have unreachable states.
* tests/python/pdegen.py: Add test case.
---
 spot/twaalgos/degen.cc | 22 +++++++++++++++++-----
 tests/python/pdegen.py | 21 +++++++++++++++++++++
 2 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc
index 1d694bc14..af5368786 100644
--- a/spot/twaalgos/degen.cc
+++ b/spot/twaalgos/degen.cc
@@ -266,7 +266,8 @@ namespace spot
       static void
       keep_bottommost_copies(twa_graph_ptr& res,
                              scc_info& si_orig,
-                             std::vector<unsigned>* orig_states)
+                             std::vector<unsigned>* orig_states,
+                             bool force_purge = false)
       {
         unsigned res_ns = res->num_states();
         auto a = si_orig.get_aut();
@@ -276,7 +277,11 @@ namespace spot
         scc_info si_res(res, scc_info_options::TRACK_STATES);
         unsigned res_scc_count = si_res.scc_count();
         if (res_scc_count <= si_orig.scc_count())
-          return;
+          {
+            if (force_purge)
+              res->purge_unreachable_states();
+            return;
+          }
 
         // If we reach this place, we have more SCCs in the output than
         // in the input.  This means that we have created some redundant
@@ -1064,18 +1069,25 @@ namespace spot
           }
       }
     // Raise the destination of the "all-accepting" edges to the
-    // highest existing level.
+    // highest existing level.  If we do such a redirection, we need
+    // to force keep_bottommost_copies to purge unreachable_states.
+    bool force_purge = false;
     auto& ev = res->edge_vector();
     for (unsigned idx: allaccedges)
       {
         unsigned dst = ev[idx].dst;
         unsigned orig_dst = (*orig_states)[dst];
         unsigned hl = highest_level[orig_dst];
-        ev[idx].dst = ds2num[degen_state{orig_dst, hl}];
+        unsigned new_dst = ds2num[degen_state{orig_dst, hl}];
+        if (dst != new_dst)
+          {
+            ev[idx].dst = new_dst;
+            force_purge = true;
+          }
       }
     //orders.print();
     res->merge_edges();
-    keep_bottommost_copies(res, si_orig, orig_states);
+    keep_bottommost_copies(res, si_orig, orig_states, force_purge);
     return res;
   }
 
diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py
index 815fe0b3d..abea21053 100644
--- a/tests/python/pdegen.py
+++ b/tests/python/pdegen.py
@@ -366,3 +366,24 @@ assert dot == """digraph "" {
 
 aut12g = spot.partial_degeneralize(aut12f)
 assert aut12f == aut12g
+
+aut13 = spot.automaton("""HOA: v1
+States: 2
+Start: 0
+AP: 4 "p9" "p14" "p10" "p7"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[!0&!1&2] 0 {0 1 2}
+[!0&!1&!2] 1 {0 1}
+State: 1
+[!0&!1&2&!3] 0 {0 1 2}
+[!0&!1&!2&!3] 1 {0 1}
+[!0&!1&!2&3] 1 {0}
+[!0&!1&2&3] 1 {0 2}
+--END--""")
+aut13g = spot.partial_degeneralize(aut13)
+assert aut13g.equivalent_to(aut13)
+assert aut13g.num_states() == 3