merge_states: fix segfault reported by Philipp
* spot/twa/twagraph.cc: Here. * tests/python/mergedge.py: Add test case.
This commit is contained in:
Alexandre Duret-Lutz
parent
634dd28379
commit
edfcd5b0d8
2 changed files with 112 additions and 1 deletions
|
|
@ -331,7 +331,35 @@ namespace spot
|
||||||
|| (a.dst == a.src && b.dst == b.src))
|
|| (a.dst == a.src && b.dst == b.src))
|
||||||
&& a.data() == b.data()); }))
|
&& a.data() == b.data()); }))
|
||||||
{
|
{
|
||||||
remap[i] = j;
|
remap[i] = (remap[j] != -1U) ? remap[j] : j;
|
||||||
|
|
||||||
|
// Because of the special self-loop tests we use above,
|
||||||
|
// it's possible that i can be mapped to remap[j] even
|
||||||
|
// if j was last compatible states found. Consider the
|
||||||
|
// following cases, taken from an actual test case:
|
||||||
|
// 18 is equal to 5, 35 is equal to 18, but 35 is not
|
||||||
|
// equal to 5.
|
||||||
|
//
|
||||||
|
// State: 5
|
||||||
|
// [0&1&2] 8 {3}
|
||||||
|
// [!0&1&2] 10 {1}
|
||||||
|
// [!0&!1&!2] 18 {1}
|
||||||
|
// [!0&!1&2] 19 {1}
|
||||||
|
// [!0&1&!2] 20 {1}
|
||||||
|
//
|
||||||
|
// State: 18
|
||||||
|
// [0&1&2] 8 {3}
|
||||||
|
// [!0&1&2] 10 {1}
|
||||||
|
// [!0&!1&!2] 18 {1} // self-loop
|
||||||
|
// [!0&!1&2] 19 {1}
|
||||||
|
// [!0&1&!2] 20 {1}
|
||||||
|
//
|
||||||
|
// State: 35
|
||||||
|
// [0&1&2] 8 {3}
|
||||||
|
// [!0&1&2] 10 {1}
|
||||||
|
// [!0&!1&!2] 35 {1} // self-loop
|
||||||
|
// [!0&!1&2] 19 {1}
|
||||||
|
// [!0&1&!2] 20 {1}
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -83,3 +83,86 @@ assert aut.num_edges() == 4
|
||||||
assert aut.num_states() == 2
|
assert aut.num_states() == 2
|
||||||
assert spot.is_deterministic(aut)
|
assert spot.is_deterministic(aut)
|
||||||
assert aut.prop_complete()
|
assert aut.prop_complete()
|
||||||
|
|
||||||
|
|
||||||
|
aa = spot.automaton("""
|
||||||
|
HOA: v1 States: 41 Start: 0 AP: 3 "allfinished" "finished_0"
|
||||||
|
"finished_1" acc-name: parity max odd 4 Acceptance: 4 Inf(3) | (Fin(2)
|
||||||
|
& (Inf(1) | Fin(0))) properties: trans-labels explicit-labels
|
||||||
|
trans-acc colored properties: deterministic --BODY-- State: 0
|
||||||
|
[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [!0&1&!2] 3 {1} [!0&1&2] 4 {1}
|
||||||
|
[0&!1&!2] 5 {1} [0&!1&2] 6 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} State: 1
|
||||||
|
[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1}
|
||||||
|
[!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} [0&!1&2] 12 {1}
|
||||||
|
State: 2 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1}
|
||||||
|
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1}
|
||||||
|
State: 3 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1}
|
||||||
|
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1}
|
||||||
|
State: 4 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1}
|
||||||
|
[0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 {1}
|
||||||
|
State: 5 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19
|
||||||
|
{1} [!0&1&!2] 20 {1} State: 6 [0&1&2] 8 {1} [!0&1&2] 10 {1} [!0&!1&2]
|
||||||
|
19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 21 {1} State: 7 [0&1&2] 8 {3}
|
||||||
|
[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 22 {1}
|
||||||
|
State: 8 [!0&!1&!2] 5 {1} [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19
|
||||||
|
{1} [!0&1&!2] 20 {1} State: 9 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] 8
|
||||||
|
{1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 {1}
|
||||||
|
[!0&!1&2] 24 {1} State: 10 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8
|
||||||
|
{3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {1}
|
||||||
|
[!0&!1&!2] 25 {1} State: 11 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19
|
||||||
|
{1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 12 [0&1&2] 8 {3}
|
||||||
|
[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 27 {1} [!0&!1&!2] 28 {1}
|
||||||
|
State: 13 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1}
|
||||||
|
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1}
|
||||||
|
State: 14 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2}
|
||||||
|
[0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1}
|
||||||
|
State: 15 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1}
|
||||||
|
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1}
|
||||||
|
State: 16 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11
|
||||||
|
{1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17
|
||||||
|
{1} State: 17 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2]
|
||||||
|
11 {1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17
|
||||||
|
{1} State: 18 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1}
|
||||||
|
[!0&!1&2] 19 {1} [!0&1&!2] 20 {1} State: 19 [0&1&!2] 7 {3} [0&1&2] 8
|
||||||
|
{3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} [!0&1&2] 32
|
||||||
|
{1} State: 20 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 {1} [!0&1&2]
|
||||||
|
32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 21 [0&1&2] 8 {1}
|
||||||
|
[!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1}
|
||||||
|
State: 22 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20
|
||||||
|
{1} [!0&!1&!2] 35 {1} State: 23 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2]
|
||||||
|
8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23
|
||||||
|
{1} [!0&!1&2] 24 {1} State: 24 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2]
|
||||||
|
8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24
|
||||||
|
{1} [!0&!1&!2] 25 {1} State: 25 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2]
|
||||||
|
8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24
|
||||||
|
{1} [!0&!1&!2] 25 {1} State: 26 [0&1&2] 8 {3} [!0&1&2] 10 {1}
|
||||||
|
[!0&!1&2] 19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 27 [0&1&2]
|
||||||
|
8 {3} [0&!1&2] 12 {3} [!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36
|
||||||
|
{1} [!0&!1&2] 37 {1} State: 28 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2]
|
||||||
|
19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 29 [0&!1&!2] 5 {3}
|
||||||
|
[0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2]
|
||||||
|
14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} State: 30 [0&1&!2] 7 {3}
|
||||||
|
[0&1&2] 8 {3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1}
|
||||||
|
[!0&1&2] 32 {1} State: 31 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3}
|
||||||
|
[0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2}
|
||||||
|
[!0&!1&!2] 38 {1} State: 32 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8
|
||||||
|
{3} [0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {1}
|
||||||
|
[!0&!1&!2] 39 {1} State: 33 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20
|
||||||
|
{1} [!0&1&2] 32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 34
|
||||||
|
[0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 {1}
|
||||||
|
[!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 {1}
|
||||||
|
State: 35 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20
|
||||||
|
{1} [!0&!1&!2] 35 {1} State: 36 [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||||
|
[!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 {1} [!0&!1&2] 37 {1}
|
||||||
|
State: 37 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||||
|
[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1}
|
||||||
|
State: 38 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||||
|
[!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} [!0&!1&!2] 38 {1}
|
||||||
|
State: 39 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||||
|
[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1}
|
||||||
|
State: 40 [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12
|
||||||
|
{1} [!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40
|
||||||
|
{1} --END--""")
|
||||||
|
aa.merge_states()
|
||||||
|
# This used to cause a segfault reported by Philipp.
|
||||||
|
print(aa.to_str())
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue