diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index e1cfed932..913c2f10b 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -124,7 +124,7 @@ namespace spot while (rbegin > rend); if (rbegin <= rend) return res; - // Fin(i) & Inf(i) = f; + // Fin(i) & Inf(i) = f; (also done by unit-fin) if (rbegin[-1].mark & seen_fin) return std::move(falsecode); for (auto m: seen_fin.sets()) @@ -192,6 +192,8 @@ namespace spot return aut; // complement[i] holds sets that appear when set #i does not. + // (This is not a strict complement, i.e., the sets in + // complement[i] are allowed to occur at the same time as i.) unsigned num_sets = acc.num_sets(); std::vector complement(num_sets); @@ -214,12 +216,8 @@ namespace spot { prev_acc = tacc; for (unsigned m: used_in_cond.sets()) - { - if (tacc.has(m)) - complement[m] -= tacc; - else - complement[m] &= tacc; - } + if (!tacc.has(m)) + complement[m] &= tacc; }; if (b != e) { diff --git a/tests/python/toparity.py b/tests/python/toparity.py index f8ce7dc1a..a7b034f21 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -220,6 +220,21 @@ State: 1 [!0&!1] 1 {0 3} --END--"""), [7, 5, 3, 6, 5, 5, 3]) +test(spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 5 ((Fin(1)|Fin(3)|Fin(4)) | Inf(2) | Inf(0)) + & (Inf(0) | Inf(1)) & (Inf(2) | Inf(1)) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[0&1] 0 {1 3} +[!0&1] 1 {0} +State: 1 +[0&1] 1 {2 3 4} +[!0&!1] 0 {1 2} +--END--"""), [9, 3, 2, 3, 3, 3, 2]) for i,f in enumerate(spot.randltl(10, 400)): test(spot.translate(f, "det", "G"), full=(i<100))