acc: fix detection of generalized-Rabin

Fixes #99.

* src/tests/parseaut.test: New test case.
* src/twa/acc.cc (is_generalized_rabin): Fix detection
of Fin(0)|Fin(1)|Fin(2)&Inf(3).
* NEWS: Mention it.

NEWS

@@ -1,6 +1,8 @@
-New in spot 1.99.2a (no yet released)
+New in spot 1.99.2a (not yet released)
 
-  Nothing yet.
+  * Bugs fixed
+    - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
+      where not detected as generalized-Rabin.
 
 New in spot 1.99.2 (2015-07-18)
 

src/tests/parseaut.test

@@ -2182,3 +2182,55 @@ State: 0
 [0&1] 0
 --END--
 EOF
+
+cat >input <<EOF
+HOA: v1
+tool: "ltl3dra" "0.2.2"
+name: "TGDRA for p0 || XG(p1 && F!p0)"
+States: 4
+Start: 2
+acc-name: generalized-Rabin 3 0 0 1
+Acceptance: 4 (Fin(0)) | (Fin(1)) | (Fin(2)&Inf(3))
+AP: 2 "p0" "p1"
+properties: deterministic trans-labels explicit-labels trans-acc no-univ-branch
+--BODY--
+State: 0 "[]"
+  [t] 0 {0 1 2}
+State: 1 "[{}]"
+  [t] 1 {1 2}
+State: 2 "[{1}, {9}]"
+  [(0)] 1 {1 2}
+  [(!0 & !1)] 3 {0 1 2}
+  [(!0 & 1)] 3 {0 3}
+State: 3 "[{8}]"
+  [(0 & 1)] 3 {0 1}
+  [(!0 & 1)] 3 {0 3}
+  [(!1)] 0 {0 1 2}
+--END--
+EOF
+
+expectok input <<EOF
+HOA: v1
+name: "TGDRA for p0 || XG(p1 && F!p0)"
+States: 4
+Start: 2
+AP: 2 "p0" "p1"
+acc-name: generalized-Rabin 3 0 0 1
+Acceptance: 4 (Fin(0)|Fin(1)) | (Fin(2) & Inf(3))
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0 "[]"
+[t] 0 {0 1 2}
+State: 1 "[{}]"
+[t] 1 {1 2}
+State: 2 "[{1}, {9}]"
+[0] 1 {1 2}
+[!0&!1] 3 {0 1 2}
+[!0&1] 3 {0 3}
+State: 3 "[{8}]"
+[0&1] 3 {0 1}
+[!0&1] 3 {0 3}
+[!1] 0 {0 1 2}
+--END--
+EOF

src/twa/acc.cc

@@ -496,12 +496,11 @@ namespace spot
 	else if (code_[s].op == acc_op::Fin)
 	  {
 	    auto m1 = code_[--s].mark;
-	    if (m1.count() != 1)
+	    for (auto s: m1.sets())
-	      return false;
+	      // If we have seen this pair already, it must have the
-	    // If we have seen this pair already, it must have the
+	      // same size.
-	    // same size.
+	      if (p.emplace(s, 0U).first->second != 0U)
-	    if (p.emplace(m1.max_set(), 0U).first->second != 0U)
+		return false;
-	      return false;
 	    seen_fin |= m1;
 	  }
 	else