diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 51854dad9..1d694bc14 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -1082,8 +1082,28 @@ namespace spot twa_graph_ptr partial_degeneralize(twa_graph_ptr a) { + bool composeorig = false; while (acc_cond::mark_t m = is_partially_degeneralizable(a)) - a = partial_degeneralize(a, m); + { + twa_graph_ptr b = partial_degeneralize(a, m); + // After the first partial degeneralization, we need to compose + // the original-states, so that original-states still appear + // to reference the original automaton. + if (composeorig) + { + auto origa = + a->get_named_prop>("original-states"); + auto origb = + b->get_named_prop>("original-states"); + for (auto& s: *origb) + s = (*origa)[s]; + } + else + { + composeorig = true; + } + a = b; + } return a; } diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 4eeb989fa..815fe0b3d 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -324,5 +324,45 @@ aut12f = spot.partial_degeneralize(aut12) assert aut12f.equivalent_to(aut12) assert aut12f.num_states() == 9 +# Check handling of original-states +dot = aut12f.to_str('dot', 'd') +assert dot == """digraph "" { + rankdir=LR + label="Inf(2) | (Inf(1) & Fin(0))\\n[Rabin-like 2]" + labelloc="t" + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0 (0)"] + 0 -> 1 [label="p0"] + 1 [label="1 (1)"] + 1 -> 2 [label="!p0"] + 1 -> 2 [label="p0\\n{0}"] + 2 [label="2 (2)"] + 2 -> 0 [label="p0"] + 2 -> 3 [label="!p0"] + 2 -> 4 [label="p0\\n{1}"] + 3 [label="3 (1)"] + 3 -> 8 [label="!p0"] + 3 -> 8 [label="p0\\n{0}"] + 4 [label="4 (2)"] + 4 -> 0 [label="p0"] + 4 -> 4 [label="p0"] + 4 -> 5 [label="!p0"] + 5 [label="5 (1)"] + 5 -> 6 [label="!p0"] + 5 -> 6 [label="p0\\n{0}"] + 6 [label="6 (2)"] + 6 -> 5 [label="!p0"] + 6 -> 6 [label="p0"] + 6 -> 7 [label="p0"] + 7 [label="7 (0)"] + 7 -> 3 [label="p0"] + 8 [label="8 (2)"] + 8 -> 3 [label="!p0"] + 8 -> 4 [label="p0\\n{1,2}"] + 8 -> 7 [label="p0"] +} +""" + aut12g = spot.partial_degeneralize(aut12f) assert aut12f == aut12g