diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 9cf0a00ff..b83263931 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1287,7 +1287,7 @@ namespace spot ("highlight-edges")) { // Unfortunately, the underlying graph, who might remove some - // edges, know nothing about named properties. So we have to + // edges, knows 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. @@ -1297,7 +1297,9 @@ namespace spot unsigned edgeidx = 1; for (unsigned e = 1; e < es; ++e) { - if (is_dead_edge(e) || newst[ev[e].dst] == -1U) + if (is_dead_edge(e) + || newst[ev[e].dst] == -1U + || newst[ev[e].src] == -1U) newedges[e] = -1U; else newedges[e] = edgeidx++; diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py index 3964ed28d..feeaad0dd 100755 --- a/tests/python/parsetgba.py +++ b/tests/python/parsetgba.py @@ -146,3 +146,46 @@ State: 4 {0} [1] 4 [2] 4 --END--""") + +# Issue #555 again. +a4 = spot.automaton("""HOA: v1.1 States: 5 Start: 2 AP: 3 "p36" "p38" +"p37" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels +explicit-labels state-acc !complete properties: !deterministic +exist-branch spot.highlight.edges: 1 1 3 1 8 1 12 1 --BODY-- State: 0 +[t] 1 State: 1 {0} [!0] 1 State: 2 [!0 | !1 | 2] 0 [t] 3 State: 3 [2] +1 [!2] 4 [2] 1 [!2] 4 State: 4 [!0&2] 1 [!0&!2] 4 [!0&2] 1 [!0&!2] 4 +--END--""") +oi = a4.out_iteraser(2) +while oi: + n = a4.edge_number(oi.current()) + if n == 3: + oi.erase() + else: + oi.advance() +a4.purge_dead_states() +tc.assertEqual(a4.to_str("hoa", "1.1"), +"""HOA: v1.1 +States: 4 +Start: 1 +AP: 3 "p36" "p38" "p37" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc !complete +properties: !deterministic exist-branch +spot.highlight.edges: 6 1 10 1 +--BODY-- +State: 0 {0} +[!0] 0 +State: 1 +[t] 2 +State: 2 +[2] 0 +[!2] 3 +[2] 0 +[!2] 3 +State: 3 +[!0&2] 0 +[!0&!2] 3 +[!0&2] 0 +[!0&!2] 3 +--END--""")