diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc index cdfd776ba..5ee8027fc 100644 --- a/src/tgbaalgos/cleanacc.cc +++ b/src/tgbaalgos/cleanacc.cc @@ -47,6 +47,10 @@ namespace spot // Remove useless marks from the acceptance condition aut->set_acceptance(useful.count(), c.strip(useless, true)); + + // This may in turn cause even more set to be unused, because of + // some simplifications, so do it again. + return cleanup_acceptance(aut); } } diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 7d9e663d1..a8953036a 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -1371,6 +1371,23 @@ State: 0 [0&!1&!2] 0 {0} [!0&!1&!2] 0 --END-- +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 {2} +[0&!1] 1 +[!0&1] 0 +[0&1] 1 +State: 1 {1 2} +[!0&!1] 1 +[0&!1] 1 +[!0&1] 1 +[0&1] 1 +--END-- EOF expectok input -v --is-empty <