From d5f488647b0ab04a7b88f02c22e84720992e13c6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Jul 2020 16:08:03 +0200 Subject: [PATCH] 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. --- NEWS | 4 +++- bin/ltlcross.cc | 1 + tests/core/ltlcross3.test | 3 +++ 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 9b98a5989..f246da955 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 2.9.2.dev (not yet released) - Nothing yet. + Bugs fixed: + + - Completely fix the ltlcross issue mentionned in previous release. New in spot 2.9.2 (2020-07-21) diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 784f06b2f..d36478837 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -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&) { diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 652c9f88b..590d369ae 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -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