Commit 457e130e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: completely fix #420

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.
parent 1a0c8a44
......@@ -45,6 +45,10 @@ New in spot 2.9.2.dev (not yet released)
file. With this refactoring, we can retrieve both a kripke or a
kripkecube from a PINS file.
Bugs fixed:
- Completely fix the ltlcross issue mentionned in previous release.
New in spot 2.9.2 (2020-07-21)
Bugs fixed:
......
......@@ -1531,6 +1531,7 @@ namespace
<< " ed.\n";
sm = new
spot::scc_info(p, spot::scc_info_options::TRACK_STATES);
sm->determine_unknown_acceptance();
}
catch (const std::bad_alloc&)
{
......
......@@ -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
......
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