diff --git a/src/tests/hoaparse.test b/src/tests/hoaparse.test index 307f6a02e..483f7cce9 100755 --- a/src/tests/hoaparse.test +++ b/src/tests/hoaparse.test @@ -1821,7 +1821,7 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Inf(0)|Fin(1)&Inf(2) /* min even 4 */ +Acceptance: 4 Inf(0)|Fin(1)&(Inf(2)|Fin(3)) /* min even 4 */ --BODY-- State: 0 [!0&!1] 0 {0 1} @@ -1833,7 +1833,7 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Inf(3)|Fin(2)&Inf(1) /* max odd 4 */ +Acceptance: 4 Inf(3)|Fin(2)&(Inf(1)|Fin(0)) /* max odd 4 */ --BODY-- State: 0 [!0&!1] 0 {0 1} @@ -1857,7 +1857,7 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Inf(0) | (Fin(1) & Inf(2)) /* min even 4 (reorderd) */ +Acceptance: 4 Inf(0) | (Fin(3)|Inf(2))&Fin(1) /* min even 4 (reordered) */ --BODY-- State: 0 [!0&!1] 0 {0 1} @@ -1964,7 +1964,7 @@ States: 1 Start: 0 AP: 2 "a" "b" acc-name: parity min even 4 -Acceptance: 4 Inf(0) | (Fin(1) & Inf(2)) +Acceptance: 4 Inf(0) | (Fin(1) & (Inf(2) | Fin(3))) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- @@ -1979,7 +1979,7 @@ States: 1 Start: 0 AP: 2 "a" "b" acc-name: parity max odd 4 -Acceptance: 4 Inf(3) | (Fin(2) & Inf(1)) +Acceptance: 4 Inf(3) | (Fin(2) & (Inf(1) | Fin(0))) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- @@ -2008,8 +2008,7 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -acc-name: parity min even 4 -Acceptance: 4 Inf(0) | (Fin(1) & Inf(2)) +Acceptance: 4 Inf(0) | ((Fin(3) | Inf(2)) & Fin(1)) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- @@ -2115,7 +2114,8 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Fin(0) & (Inf(1) | Fin(2)) +acc-name: parity min odd 4 +Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- @@ -2129,7 +2129,8 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Fin(3) & (Inf(2) | Fin(1)) +acc-name: parity max even 4 +Acceptance: 4 Fin(3) & (Inf(2) | (Fin(1) & Inf(0))) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- @@ -2143,6 +2144,7 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" +acc-name: parity max odd 4 Acceptance: 4 Inf(3) | (Fin(2) & (Inf(1) | Fin(0))) properties: trans-labels explicit-labels trans-acc complete properties: deterministic @@ -2157,7 +2159,7 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Fin(0) & (Inf(1) | Fin(2)) +Acceptance: 4 Fin(0) & ((Fin(2) & Inf(3)) | Inf(1)) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- diff --git a/src/twa/acc.cc b/src/twa/acc.cc index 9499d7a88..32f7dfbf6 100644 --- a/src/twa/acc.cc +++ b/src/twa/acc.cc @@ -517,8 +517,16 @@ namespace spot acc_cond::acc_code acc_cond::acc_code::parity(bool max, bool odd, unsigned sets) { + acc_cond::acc_code res; + + if (max) + res = odd ? t() : f(); + else + res = (sets & 1) == odd ? t() : f(); + if (sets == 0) - return f(); + return res; + // When you look at something like // acc-name: parity min even 5 // Acceptance: 5 Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4)))) @@ -526,10 +534,6 @@ namespace spot int start = max ? 0 : sets - 1; int inc = max ? 1 : -1; int end = max ? sets : -1; - // Do not start with a Fin term, the right-most term is always Inf. - if ((start & 1) != odd) - start += inc; - acc_cond::acc_code res = f(); for (int i = start; i != end; i += inc) { if ((i & 1) == odd) @@ -623,12 +627,10 @@ namespace spot unsigned sets = num_; if (sets == 0) { - max = false; - odd = false; - return is_false(); + max = true; + odd = is_true(); + return true; } - if (is_true()) - return false; acc_cond::mark_t u_inf; acc_cond::mark_t u_fin; std::tie(u_inf, u_fin) = code_.used_inf_fin_sets(); diff --git a/wrap/python/tests/accparse.ipynb b/wrap/python/tests/accparse.ipynb index 61f39cf0e..031d02090 100644 --- a/wrap/python/tests/accparse.ipynb +++ b/wrap/python/tests/accparse.ipynb @@ -17,8 +17,7 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "", - "signature": "sha256:b0fe4d13694abcf6bcdfe7bb8dca49a0b48757f0a09464300a214f1d30e72edb" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -136,24 +135,24 @@ "Streett 0: t\n", "generalized-Rabin 3 1 2 3: (Fin(0) & Inf(1)) | (Fin(2) & (Inf(3)&Inf(4))) | (Fin(5) & (Inf(6)&Inf(7)&Inf(8)))\n", "generalized-Rabin 0: f\n", - "parity min even 6: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))\n", - "parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & Inf(1))))\n", + "parity min even 6: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & (Inf(4) | Fin(5)))))\n", + "parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))\n", "parity max even 6: Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))))\n", "parity min odd 6: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | (Fin(4) & Inf(5)))))\n", "parity min even 5: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))\n", - "parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & Inf(1)))\n", + "parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))\n", "parity max even 5: Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))\n", - "parity min odd 5: Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))\n", - "parity min even 2: Inf(0)\n", - "parity max odd 2: Inf(1)\n", + "parity min odd 5: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))\n", + "parity min even 2: Inf(0) | Fin(1)\n", + "parity max odd 2: Inf(1) | Fin(0)\n", "parity max even 2: Fin(1) & Inf(0)\n", "parity min odd 2: Fin(0) & Inf(1)\n", "parity min even 1: Inf(0)\n", - "parity max odd 1: f\n", + "parity max odd 1: Fin(0)\n", "parity max even 1: Inf(0)\n", - "parity min odd 1: f\n", - "parity min even 0: f\n", - "parity max odd 0: f\n", + "parity min odd 1: Fin(0)\n", + "parity min even 0: t\n", + "parity max odd 0: t\n", "parity max even 0: f\n", "parity min odd 0: f\n" ] diff --git a/wrap/python/tests/accparse2.py b/wrap/python/tests/accparse2.py index 4c844ad5e..38efae552 100644 --- a/wrap/python/tests/accparse2.py +++ b/wrap/python/tests/accparse2.py @@ -36,9 +36,11 @@ a = spot.acc_cond(0) a.set_acceptance(spot.parse_acc_code('all')) assert(a.is_rabin() == -1) assert(a.is_streett() == 0) +assert(a.is_parity() == [True, True, True]) a.set_acceptance(spot.parse_acc_code('none')) assert(a.is_rabin() == 0) assert(a.is_streett() == -1) +assert(a.is_parity() == [True, True, False]) a = spot.acc_cond(2) a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))'))