diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index cbbe5eabf..7f2660b54 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -915,8 +915,6 @@ namespace spot // auto* names = new std::vector; // res->set_named_prop("state-names", names); - auto old_orig_states = - a->get_named_prop>("original-states"); auto orig_states = new std::vector(); auto levels = new std::vector(); unsigned ns = a->num_states(); @@ -972,8 +970,6 @@ namespace spot // names->push_back(os.str()); unsigned orig = ds.first; - if (old_orig_states) - orig = (*old_orig_states)[orig]; assert(ns == orig_states->size()); orig_states->emplace_back(orig); levels->emplace_back(ds.second); @@ -1071,6 +1067,14 @@ namespace spot force_purge = true; } } + // compose original-states with the any previously existing one. + // We do that now, because the above loop uses orig_states to + // find the local source, but for the bottommost copy below, it's better + // if we compose everything. + if (auto old_orig_states = + a->get_named_prop>("original-states")) + for (auto& s: *orig_states) + s = (*old_orig_states)[s]; //orders.print(); res->merge_edges(); keep_bottommost_copies(res, si_orig, orig_states, force_purge); diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index dedcc5a19..72cc8f6e4 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -391,3 +391,25 @@ State: 1 aut13g = spot.partial_degeneralize(aut13) assert aut13g.equivalent_to(aut13) assert aut13g.num_states() == 3 + + +aut14 = spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 5 (Inf(0)&Inf(1)) | ((Fin(2)|Fin(3)) & Fin(4)) +--BODY-- +State: 0 +[!0 & 1] 0 {2 3} +[!0 & !1] 0 {3} +[0] 1 +State: 1 +[0&1] 1 {1 2 4} +[0&!1] 1 {4} +[!0&1] 1 {0 1 2 3} +[!0&!1] 1 {0 3} +--END-- +""") +aut14g = spot.partial_degeneralize(aut14) +assert aut14g.equivalent_to(aut14) +assert aut14g.num_states() == 3