twagraph: fix highlight-edges in defrag_states

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

@@ -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:

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;

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"})

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--""")