diff --git a/NEWS b/NEWS index debc196c7..af4287184 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,13 @@ New in spot 2.9.1.dev (not yet released) - Nothing yet. + Bugs fixed: + + - ltlcross --csv=... --product=N with N>0 could output spurious + diagnosics claiming that words were rejected when evaluating + the automaton on state-space. + + - spot::scc_info::determine_unknown_acceptance() now also update the + result of spot::scc_info::one_accepting_scc(). New in spot 2.9.1 (2020-07-15) diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index fd8deb228..784f06b2f 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1568,6 +1568,7 @@ namespace sm = new spot::scc_info(p, spot::scc_info_options::TRACK_STATES); + sm->determine_unknown_acceptance(); } catch (const std::bad_alloc&) { diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 024051bcb..74498c49f 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -472,9 +472,15 @@ namespace spot "does not support alternating automata"); auto& node = node_[s]; if (check_scc_emptiness(s)) - node.rejecting_ = true; + { + node.rejecting_ = true; + } else - node.accepting_ = true; + { + node.accepting_ = true; + if (one_acc_scc_ < 0) + one_acc_scc_ = s; + } changed = true; } } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index a76ca3612..0b70b29d5 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -535,7 +535,14 @@ namespace spot return node_.size(); } - /// Return the number of one accepting SCC if any, -1 otherwise. + /// \brief Return the number of one accepting SCC if any, -1 otherwise. + /// + /// If an accepting SCC has been found, return its number. + /// Otherwise return -1. Note that when the acceptance condition + /// contains Fin, -1 does not implies that all SCCs are rejecting: + /// it just means that no accepting SCC is known currently. In + /// that case, you might want to call + /// determine_unknown_acceptance() first. int one_accepting_scc() const { return one_acc_scc_; diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 430107239..652c9f88b 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -327,6 +327,11 @@ diff foo expected # This command used to crash. Report from FrantiĊĦek Blahoudek. run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba' +# In spot 2.9 and 2.9.1 the following command used to report a bug +# 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))))))))' + # The CSV file should not talk about product if --products=0 ltlcross --color --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv grep product out.csv && exit 1