From 457e130e24485ddf9833536d90ff2aeb87cfd694 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, 8 insertions(+) diff --git a/NEWS b/NEWS index 5e3640af0..bf0e4fcef 100644 --- a/NEWS +++ b/NEWS @@ -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: 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