From 55575a11e31c687f3ad7596e75ecbb7d8fb8fbd6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 23 Nov 2023 20:27:05 +0100
Subject: [PATCH] twagraph: fix highlight-edges in defrag_states
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #555 reported by Dávid Smolka.

* spot/twa/twagraph.cc (defrag_states): Update highlight-edge.
* spot/graph/graph.hh (defrag_states): Just point to
twa_graph::defrag_states in a comment, because the latter relies
on the implementation detail of graph::defrag_state.
* tests/python/parsetgba.py: Add test case.
* NEWS: Mention the bug.
---
 NEWS                      |  4 ++++
 spot/graph/graph.hh       |  5 +++++
 spot/twa/twagraph.cc      | 25 +++++++++++++++++++++++++
 tests/python/parsetgba.py | 32 ++++++++++++++++++++++++++++++++
 4 files changed, 66 insertions(+)

diff --git a/NEWS b/NEWS
index fb8177c7a..a9cb0a830 100644
--- a/NEWS
+++ b/NEWS
@@ -187,6 +187,10 @@ New in spot 2.11.6.dev  (not yet released)
     completely obsolete.  This third argument has been marked as
     depreated.  (Issue #553)
 
+  - twa::defrag_states(), which is called for instance by
+    purge_dead_state(), did not update the highlight-edges property.
+    (Issue #555.)
+
 New in spot 2.11.6  (2023-08-01)
 
   Bug fixes:
diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh
index dc3c221c1..4f62f3dcd 100644
--- a/spot/graph/graph.hh
+++ b/spot/graph/graph.hh
@@ -1485,6 +1485,11 @@ namespace spot
       // Shift all edges in edges_.  The algorithm is
       // similar to remove_if, but it also keeps the correspondence
       // between the old and new index as newidx[old] = new.
+      //
+      // If you change anything to this logic, you might want to
+      // double check twa_graph::defrag_states where we need to
+      // predict the new edges indices in order to update
+      // highlight-edges.
       unsigned tend = edges_.size();
       std::vector<edge> newidx(tend);
       unsigned dest = 1;
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index 1b9e2f484..2bcce5fed 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -1283,6 +1283,31 @@ namespace spot
           }
         std::swap(*hs, hs2);
       }
+    if (auto he = get_named_prop<std::map<unsigned, unsigned>>
+        ("highlight-edges"))
+      {
+        // Unfortunately, the underlying graph, who might remove some
+        // edges, know nothing about named properties.  So we have to
+        // predict the indices of the edges after
+        // graph::defrag_states() will run.  This might break if
+        // graph::defrag_states() is changed.
+        auto& ev = edge_vector();
+        unsigned es = ev.size();
+        std::vector<unsigned> newedges(es, -1U);
+        unsigned edgeidx = 1;
+        for (unsigned e = 1; e < es; ++e)
+          {
+            if (is_dead_edge(e) || newst[ev[e].dst] == -1U)
+              newedges[e] = -1U;
+            else
+              newedges[e] = edgeidx++;
+          }
+        std::map<unsigned, unsigned> he2;
+        for (auto [e, c]: *he)
+          if (newedges[e] != -1U)
+            he2.emplace(newedges[e], c);
+        std::swap(*he, he2);
+      }
     for (const char* prop: {"original-classes",
                             "original-states",
                             "degen-levels"})
diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py
index d6f665ae5..ad657dfcc 100755
--- a/tests/python/parsetgba.py
+++ b/tests/python/parsetgba.py
@@ -91,3 +91,35 @@ State: 1
 [f] 0
 [t] 0
 --END--""")
+
+# Issue #555.
+a3 = spot.automaton("""HOA: v1.1 States: 6 Start: 0 AP: 3 "a" "b" "c"
+acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels
+explicit-labels state-acc !complete properties: !deterministic
+exist-branch spot.highlight.edges: 5 3 6 1 7 3 8 2 --BODY-- State: 0 [0] 1 [0] 2
+State: 1 [0] 3 State: 2 [0] 5 State: 3 {0} [0] 3 State: 4 {0} [0] 4
+[1] 4 State: 5 {0} [1] 5 [2] 5 --END--""")
+a3.purge_dead_states()
+tc.assertEqual(a3.to_str("hoa", "1.1"), """HOA: v1.1
+States: 5
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: !deterministic exist-branch
+spot.highlight.edges: 5 3 6 2
+--BODY--
+State: 0
+[0] 1
+[0] 2
+State: 1
+[0] 3
+State: 2
+[0] 4
+State: 3 {0}
+[0] 3
+State: 4 {0}
+[1] 4
+[2] 4
+--END--""")