acc: Adjust generalition of parity acceptance

According to https://github.com/adl/hoaf/issues/46

* src/twa/acc.cc (parity): Adjust generation.
* src/tests/hoaparse.test, wrap/python/tests/accparse.ipynb:
Adjust existing test cases.
* wrap/python/tests/accparse2.py: New test cases.

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(3) | Inf(2)) & Fin(1))
-Acceptance: 4 Inf(0) | (Fin(1) & Inf(2))
 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--

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;
+	max = true;
-	odd = false;
+	odd = is_true();
-	return is_false();
+	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();

wrap/python/tests/accparse.ipynb

@@ -17,8 +17,7 @@
    "pygments_lexer": "ipython3",
    "version": "3.4.3+"
   },
-  "name": "",
+  "name": ""
-  "signature": "sha256:b0fe4d13694abcf6bcdfe7bb8dca49a0b48757f0a09464300a214f1d30e72edb"
  },
  "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 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))))\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 odd 5: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))\n",
-        "parity min even 2: Inf(0)\n",
+        "parity min even 2: Inf(0) | Fin(1)\n",
-        "parity max odd 2: Inf(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 odd 1: Fin(0)\n",
-        "parity min even 0: f\n",
+        "parity min even 0: t\n",
-        "parity max odd 0: f\n",
+        "parity max odd 0: t\n",
         "parity max even 0: f\n",
         "parity min odd 0: f\n"
        ]

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))'))