diff --git a/NEWS b/NEWS index d89e92050..7ea126243 100644 --- a/NEWS +++ b/NEWS @@ -156,6 +156,16 @@ New in spot 2.11.6.dev (not yet released) could fail to equate two "t" condition, because we have two ways to represent "t": the empty condition, or the empty "Inf({})". + - Functions complement() and change_parity() could incorrectly read + or write the unused edge #0. In the case of complement(), writing + that edge was usually harmless. However in some scenario, + complement could need to stick a ⓪ acceptance mark on edge #0, + then the acceptance condition could be simplified to "t", and + finally change_parity could be confused to find such an accepting + mark in an automaton that declares no colors, and perform some + computation on that color that caused it to crash with a "Too many + acceptance sets used" message. (issue #552) + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 8de9d9fab..328977f2b 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -2556,7 +2556,7 @@ static void fix_acceptance(result_& r) auto onlyneg = r.neg_acc_sets - r.pos_acc_sets; if (onlyneg) { - for (auto& t: r.h->aut->edge_vector()) + for (auto& t: r.h->aut->edges()) t.acc ^= onlyneg; } @@ -2570,7 +2570,7 @@ static void fix_acceptance(result_& r) if (both) { base = acc.add_sets(both.count()); - for (auto& t: r.h->aut->edge_vector()) + for (auto& t: r.h->aut->edges()) { unsigned i = 0; if ((t.acc & both) != both) diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 803b3f440..b6ace400e 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -144,7 +144,7 @@ namespace spot if (need_acc_fix) { auto a = aut->set_buchi(); - for (auto& t: aut->edge_vector()) + for (auto& t: aut->edges()) t.acc = a; if (aut->num_edges()) acc = a; diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 98ac010fe..4da129bfb 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -50,7 +50,7 @@ namespace spot change_acc(twa_graph_ptr& aut, unsigned num_sets, bool change_kind, bool change_style, bool output_max, bool input_max) { - for (auto& e: aut->edge_vector()) + for (auto& e: aut->edges()) if (e.acc) { unsigned msb = (input_max ? e.acc.max_set() : e.acc.min_set()) - 1; diff --git a/tests/core/ltlcross.test b/tests/core/ltlcross.test index 381cf7a66..885269685 100755 --- a/tests/core/ltlcross.test +++ b/tests/core/ltlcross.test @@ -69,7 +69,12 @@ ltlcross --verbose ltl2tgba ltl2tgba \ # Issue #524. ltlcross ltl2tgba -f '!(X(v3 | G!v5) | ((Xv5 & !(v5 & !X!v3)) U !v5))' -# Issue #546. -ltlcross 'ltl2tgba --medium -p' 'ltl2tgba -p' 'ltl2tgba --medium -D -p' \ +# Issue #546, Issue #552. +ltlcross 'ltl2tgba --medium -p' \ + 'ltl2tgba -p' \ + 'ltl2tgba --medium -D -p' \ + 'ltl2tgba --medium --colored-parity="min even" -C -D' \ + 'ltl2tgba --colored-parity="min even" -C -D' \ -f 'a | FGa | GF(!b | Gb)' \ - -f '(~ v1 U ~ v5) | G(F v9 & F G v1) | G F(~ v7 | G v7 | G v3)' + -f '(~ v1 U ~ v5) | G(F v9 & F G v1) | G F(~ v7 | G v7 | G v3)' \ + -f 'FG((a | Fb | FG!b) & !G(c & d))' diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 064079f37..372bbeba2 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -298,6 +298,11 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do $GREP 'catch *([^.]' $tmp | $GREP -v 'const.*&' && diag 'Always capture exceptions by const reference.' + # iterating over edge_vector() is suspicious, because the + # first edge should not be used. + $GREP 'for (.*:.*edge_vector()' $tmp && + diag 'Did you mean to iterate over edges()?' + case $file in *.hh | *.hxx) if $GREP -E '(<<|>>)' $tmp >/dev/null; then