From 20df3b4e9886fd1e15eba234557195ab77f6d404 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 21 Jun 2017 16:03:17 +0200
Subject: [PATCH] acc: fix maybe_accepting() on Fin(x)|Fin(y)|Fin(z)

Fixes #271, reported by Henrich Lauko.

* spot/twa/acc.cc (maybe_accepting): Fix handling in case
of disjunction of Fin.
* tests/core/scc.test, tests/python/accparse2.py: Add more
tests.
---
 spot/twa/acc.cc           |  8 ++++----
 tests/core/scc.test       | 32 ++++++++++++++++++++++++++++++++
 tests/python/accparse2.py |  6 ++++++
 3 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index be3837658..9bd502d0a 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -255,12 +255,12 @@ namespace spot
         case acc_cond::acc_op::Inf:
           return (pos[-1].mark & infinitely_often) == pos[-1].mark;
         case acc_cond::acc_op::Fin:
-          if (pos[-1].mark & always_present)
+          if ((pos[-1].mark & always_present) == pos[-1].mark)
             return false;
-          else if (pos[-1].mark & infinitely_often)
-            return trival::maybe();
-          else
+          else if ((pos[-1].mark & infinitely_often) != pos[-1].mark)
             return true;
+          else
+            return trival::maybe();
         case acc_cond::acc_op::FinNeg:
         case acc_cond::acc_op::InfNeg:
           SPOT_UNREACHABLE();
diff --git a/tests/core/scc.test b/tests/core/scc.test
index ec1388787..ba9232f6a 100755
--- a/tests/core/scc.test
+++ b/tests/core/scc.test
@@ -103,3 +103,35 @@ EOF
 run 0 autfilt --decompose-scc=1 -F aut> out
 cat out
 diff out ref
+
+
+# From issue #271, reported by Henrich Lauko.
+cat >in.hoa <<EOF
+HOA: v1
+States: 4
+Start: 2
+AP: 2 "p1" "p0"
+acc-name: generalized-co-Buchi 2
+Acceptance: 2 Fin(0)|Fin(1)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0 {0}
+[1] 0
+[!1] 1
+State: 1 {0 1}
+[1] 0
+[!1] 1
+State: 2
+[0&1] 0
+[0&!1] 1
+[!0&1] 2
+[!0&!1] 3
+State: 3 {1}
+[0&1] 0
+[0&!1] 1
+[!0&1] 2
+[!0&!1] 3
+--END--
+EOF
+test 2 = `autfilt --stats=%[a]c in.hoa`
diff --git a/tests/python/accparse2.py b/tests/python/accparse2.py
index 48c8d66e1..952d19703 100644
--- a/tests/python/accparse2.py
+++ b/tests/python/accparse2.py
@@ -41,6 +41,12 @@ assert a.maybe_accepting([2], []).is_true()
 assert a.maybe_accepting([0, 1], []).is_maybe()
 assert a.maybe_accepting([0, 1], [1]).is_false()
 
+a.set_acceptance('Fin(0)|Fin(1)')
+assert a.maybe_accepting([0, 1], [1]).is_maybe()
+assert a.maybe_accepting([0, 1], [0, 1]).is_false()
+assert a.maybe_accepting([0], []).is_true()
+assert a.maybe_accepting([], [0]).is_true()
+
 a = spot.acc_cond(0)
 a.set_acceptance('all')
 assert(a.is_rabin() == -1)