diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc index c368cf939..bca717cbb 100644 --- a/spot/twaalgos/toweak.cc +++ b/spot/twaalgos/toweak.cc @@ -121,10 +121,11 @@ namespace spot int curr = static_cast(rank); // We must always be able to go to the previous even rank int lower = less_ ? ((curr - 1) & ~1) : 0; - for (int i = curr; i >= lower; --i) + for (int i = curr, start_set = st.mark.min_set() - 1; + i >= lower; --i, start_set = 0) { if (i % 2) - for (unsigned m = 0; m < numsets_; ++m) + for (unsigned m = start_set; m < numsets_; ++m) levels |= state_to_var_[new_state(d, i, {m})]; else levels |= state_to_var_[new_state(d, i, 0U)]; diff --git a/tests/python/toweak.py b/tests/python/toweak.py index 120d23e00..c1b3ade93 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -53,3 +53,51 @@ def test_phi(phi): for p in phi1: test_phi(p) + + +phi2 = spot.formula("(G((F a) U b)) W a") +a2 = spot.automaton(""" +HOA: v1 +States: 7 +Start: 1 +AP: 2 "a" "b" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc complete univ-branch +--BODY-- +State: 0 +[t] 0 {0 1} +State: 1 +[0] 0 {0 1} +[1] 1&2 {0 1} +[0&!1] 1&3 {0 1} +[!0&!1] 1&4 {0 1} +State: 2 +[1] 2 {0 1} +[0&!1] 3 {0 1} +[!0&!1] 4 {0 1} +State: 3 +[1] 2 {0 1} +[0&!1] 3 {1} +[!0&!1] 4 {1} +State: 4 +[0&1] 2 {0 1} +[0&!1] 3 {1} +[!0&!1] 4 {1} +[!0&1] 5 {0 1} +State: 5 +[0&1] 2 {0 1} +[0&!1] 3 {0 1} +[!0&1] 5 {0} +[!0&!1] 6 {0} +State: 6 +[0&1] 2 {0 1} +[0&!1] 3 {1} +[!0&1] 5 {0} +[!0&!1] 6 +--END-- +""") +a2 = spot.to_weak_alternating(a2) +assert equivalent(a2, phi2) + +