diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index e7a47ecc7..05393caef 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -2599,7 +2599,8 @@ namespace spot if (!fin) { auto m = pos[-1].mark & possibles; - if (m.count() == 1 || conj) + if ((!conj && pos[-1].mark.count() == 1) + || (conj && m.count() > 0)) { found_one = true; res |= m; @@ -2611,7 +2612,8 @@ namespace spot if (!found_one || fin) { auto m = pos[-1].mark & possibles; - if (m.count() == 1 || !conj) + if ((conj && pos[-1].mark.count() == 1) + || (!conj && m.count() > 0)) { found_one = true; fin = true; diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 608e8c40f..eb5fe20d1 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -240,6 +240,10 @@ int main() auto cond1 = spot::acc_cond::acc_code( "(Inf(0) & Inf(5)) | Inf(5) | Inf(0)"); std::cout << cond1.unit_propagation() << '\n'; + auto cond2 = spot::acc_cond::acc_code("Fin(1) | Inf(0) | Inf(0)"); + std::cout << cond2.unit_propagation() << '\n'; + auto cond3 = spot::acc_cond::acc_code("Inf(0) & Inf(2) | Fin(2)"); + std::cout << cond3.unit_propagation() << '\n'; return 0; } diff --git a/tests/core/acc.test b/tests/core/acc.test index af1d0ac0a..aac7874ab 100755 --- a/tests/core/acc.test +++ b/tests/core/acc.test @@ -86,6 +86,8 @@ Inf(2) & Fin(2) (Fin(0)|Fin(3)) | (Inf(1) & Fin(2)) (Fin(0)|Fin(3)) | (Inf(1) & Fin(2)) Inf(5) | Inf(0) +Fin(1) | Inf(0) +Inf(0) | Fin(2) EOF run 0 ../acc > stdout diff --git a/tests/core/remfin.test b/tests/core/remfin.test index c8b1eb670..73d7eec28 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -313,25 +313,27 @@ State: 2 {0} [!1] 2 --END-- HOA: v1 -States: 3 +States: 4 Start: 0 AP: 2 "a" "b" -acc-name: Buchi -Acceptance: 1 Inf(0) +Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2)) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {0} -[0] 1 {0} -[!0] 2 {0} +[t] 0 {1 3} +[0] 1 {1 3} +[!0] 2 {1 3} State: 1 -[1] 0 {0} -[0&1] 1 {0} -[!0&1] 2 {0} +[1] 0 {1} +[0&1] 1 {1} +[!0&1] 2 {1 2} State: 2 [!1] 0 -[0&!1] 1 {0} -[!0&!1] 2 {0} +[0&!1] 1 +[!0&!1] 2 +[!0&!1] 3 +State: 3 +[!0&!1] 3 {0} --END-- HOA: v1 States: 3 @@ -913,7 +915,7 @@ State: 2 {0} [!1] 2 --END-- HOA: v1 -States: 3 +States: 4 Start: 0 AP: 2 "a" "b" acc-name: Buchi @@ -925,13 +927,16 @@ State: 0 [0] 1 {0} [!0] 2 {0} State: 1 -[1] 0 {0} -[0&1] 1 {0} +[1] 0 +[0&1] 1 [!0&1] 2 {0} State: 2 [!1] 0 -[0&!1] 1 {0} -[!0&!1] 2 {0} +[0&!1] 1 +[!0&!1] 2 +[!0&!1] 3 +State: 3 +[!0&!1] 3 {0} --END-- HOA: v1 States: 3