diff --git a/NEWS b/NEWS index 5873a3e16..6e448a110 100644 --- a/NEWS +++ b/NEWS @@ -31,6 +31,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 b2b8dcc09..971a32637 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 bdbe18195..821f9eb61 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