From 76d4fe236cdded1338a38b2b8686e91fc80b211c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 16 Mar 2018 14:00:27 +0100
Subject: [PATCH] autfilt --acceptance-is=Fin-less should reject "f"

* bin/autfilt.cc: Fix detection of Fin-less acceptance.
* tests/core/remfin.test: Add some tests.
* NEWS: Mention the bug.
---
 NEWS                   | 3 +++
 bin/autfilt.cc         | 2 +-
 tests/core/remfin.test | 7 +++++++
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index 0d7f2f287..e64801692 100644
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,9 @@ New in spot 2.5.1.dev (not yet released)
   - remove_fin(), streett_to_generalized_buchi() should never
     return automata with "f" acceptance.
 
+  - "autfilt --acceptance-is=Fin-less" no longer accept automata
+    with "f" acceptance.
+
 New in spot 2.5.1 (2018-02-20)
 
   Library:
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index 32418adb9..c586d1ed6 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -1191,7 +1191,7 @@ namespace
             }
         }
       case ACC_FinLess:
-        return !acc.uses_fin_acceptance();
+        return !acc.uses_fin_acceptance() && !acc.is_f();
       }
     SPOT_UNREACHABLE();
   }
diff --git a/tests/core/remfin.test b/tests/core/remfin.test
index 4479835b5..bdd535099 100755
--- a/tests/core/remfin.test
+++ b/tests/core/remfin.test
@@ -1541,3 +1541,10 @@ SPOT_STREETT_CONV_MIN=0 \
 autcross --language-preserved -Ftest1 \
   'SPOT_STREETT_CONV_MIN=1 autfilt --remove-fin %H>%O' \
   'SPOT_STREETT_CONV_MIN=1 autfilt --tgba %H>%O'
+
+ltl2tgba true > h1
+autfilt -F h1 --acceptance-is=Fin-less
+autfilt --complement -F h1 > h2
+autfilt -F h2 --acceptance-is=f
+autfilt -F h2 --acceptance-is=Fin-less && exit 1
+autfilt --remove-fin -F h2 | autfilt --acceptance-is=Fin-less