Commit 1c26764b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 1db3472a
Pipeline #1003 passed with stages
in 138 minutes and 15 seconds
......@@ -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:
......
......@@ -1191,7 +1191,7 @@ namespace
}
}
case ACC_FinLess:
return !acc.uses_fin_acceptance();
return !acc.uses_fin_acceptance() && !acc.is_f();
}
SPOT_UNREACHABLE();
}
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment