alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: completely fix #420

Browse source 
Reported by Salomon Sickert.

* bin/ltlcross.cc: Also call determinize_unknown_acceptance() for
positive automata.
* tests/core/ltlcross3.test: Add another test case.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2020-07-21 16:08:03 +02:00
parent d61d6570ac
commit d5f488647b
3 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
tests/core/ltlcross3.test
View file

@ -331,6 +331,9 @@ run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba'
# that did not exist. Issue #420.
ltlcross --csv=/dev/null ltl2tgba 'ltl2tgba -D -G' --states=5 \
-f '(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))'
# And this related one even survived in 2.9.2...
ltlcross --csv=/dev/null ltl2tgba 'ltl2tgba -P -D' --states=45 \
-f 'F(G((X(X(b))) | ((c) U (X(X(d))))))'
# The CSV file should not talk about product if --products=0
ltlcross --color --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv