alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: fix issue #555 better

Browse source 
Reported by Dávid Smolka.

* spot/twa/twagraph.cc (defrag_states): Also ignore edges with erased
source when updating highlight-edges.
* tests/python/parsetgba.py: Add Dávid's test case.
This commit is contained in:
Alexandre Duret-Lutz 2023-12-03 22:26:12 +01:00
parent 3d05ecb4ac
commit 444d4f773d
2 changed files with 47 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/twa/twagraph.cc
View file

@ -1287,7 +1287,7 @@ namespace spot
("highlight-edges")) ("highlight-edges"))
{ {
// Unfortunately, the underlying graph, who might remove some // 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 // predict the indices of the edges after
// graph::defrag_states() will run. This might break if // graph::defrag_states() will run. This might break if
// graph::defrag_states() is changed. // graph::defrag_states() is changed.
@ -1297,7 +1297,9 @@ namespace spot
unsigned edgeidx = 1; unsigned edgeidx = 1;
for (unsigned e = 1; e < es; ++e) 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; newedges[e] = -1U;
else else
newedges[e] = edgeidx++; newedges[e] = edgeidx++;

43
tests/python/parsetgba.py
View file

@ -146,3 +146,46 @@ State: 4 {0}
[1] 4 [1] 4
[2] 4 [2] 4
--END--""") --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--""")