diff --git a/NEWS b/NEWS index 251f5feb3..d2c5ce5cb 100644 --- a/NEWS +++ b/NEWS @@ -60,6 +60,14 @@ New in spot 2.11.6.dev (not yet released) 36 seconds; it now produce an AIG circuit with 53 nodes in only 0.1 second. + Bugs fixed: + + - tgba_determinize()'s use_simulation option would cause it to + segfault on automata with more than 2^16 SCCs, due to overflows in + computations of indices in the reachability matrix for SCCs. + (Issue #541.) This has been fixed by disabled the use_simulation + optimization in this case. + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/THANKS b/THANKS index 7986c3875..25fac900b 100644 --- a/THANKS +++ b/THANKS @@ -10,6 +10,7 @@ Caroline Lemieux Christian Dax Christopher Ziegler Clément Tamines +David Dokoupil David Müller Dávid Smolka Edmond Irani Liu diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index d2d35a824..2bc84cd6a 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2022 Laboratoire de Recherche et +// Copyright (C) 2015-2023 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -820,30 +820,44 @@ namespace spot return nodes_ == other.nodes_ && braces_ == other.braces_; } - // res[i + scccount*j] = 1 iff SCC i is reachable from SCC j - std::vector - find_scc_paths(const scc_info& scc) + namespace { - unsigned scccount = scc.scc_count(); - std::vector res(scccount * scccount, 0); - for (unsigned i = 0; i != scccount; ++i) - res[i + scccount * i] = 1; - for (unsigned i = 0; i != scccount; ++i) + class reachability_matrix final + { + // Store a lower triangular matrix. + // (j can reach i) <=> (i<=j and m[j*(j+1)/2 + i]==1) + std::vector m; + public: + reachability_matrix(const scc_info& scc) { - unsigned ibase = i * scccount; - for (unsigned d: scc.succ(i)) + unsigned scccount = scc.scc_count(); + m.resize(scccount * (scccount + 1) / 2, 0); + for (unsigned i = 0; i < scccount; ++i) + m[(i * (i + 1) / 2) + i] = 1; + for (unsigned i = 1; i < scccount; ++i) { - // we necessarily have d < i because of the way SCCs are - // numbered, so we can build the transitive closure by - // just ORing any SCC reachable from d. - unsigned dbase = d * scccount; - for (unsigned j = 0; j != scccount; ++j) - res[ibase + j] |= res[dbase + j]; + unsigned ibase = i * (i + 1) / 2; + for (unsigned d: scc.succ(i)) + { + // we necessarily have d < i because of the way SCCs are + // numbered, so we can build the transitive closure by + // just ORing any SCC reachable from d. + unsigned dbase = d * (d + 1) / 2; + for (unsigned j = 0; j <= d; ++j) + m[ibase + j] |= m[dbase + j]; + } } } - return res; + + bool operator()(unsigned j, unsigned i) const + { + return i <= j && m[(j * (j + 1) / 2) + i]; + } + }; + } + twa_graph_ptr tgba_determinize(const const_twa_graph_ptr& a, bool pretty_print, bool use_scc, @@ -882,49 +896,56 @@ namespace spot scc_opt = scc_info_options::TRACK_SUCCS | scc_info_options::TRACK_STATES; scc_info scc = scc_info(aut, scc_opt); + // If we have too many SCCs, disable simulation-based checks, as + // computations to index the matrix would overflow. (Issue #541.) + if (scc.scc_count() >= (1 << 16)) + { + use_simulation = false; + implications.clear(); + } + // If use_simulation is false, implications is empty, so nothing is built std::vector> implies( implications.size(), std::vector(implications.size(), 0)); - { - std::vector is_connected = find_scc_paths(scc); - unsigned sccs = scc.scc_count(); - bool something_implies_something = false; - for (unsigned i = 0; i != implications.size(); ++i) - { - // NB spot::simulation() does not remove unreachable states, as it - // would invalidate the contents of 'implications'. - // so we need to explicitly test for unreachable states - // FIXME: based on the scc_info, we could remove the unreachable - // states, both in the input automaton and in 'implications' - // to reduce the size of 'implies'. - if (!scc.reachable_state(i)) - continue; - unsigned scc_of_i = scc.scc_of(i); - bool i_implies_something = false; - for (unsigned j = 0; j != implications.size(); ++j) - { - if (!scc.reachable_state(j)) - continue; - - bool i_implies_j = !is_connected[sccs * scc.scc_of(j) + scc_of_i] - && bdd_implies(implications[i], implications[j]); - implies[i][j] = i_implies_j; - i_implies_something |= i_implies_j; - } - // Clear useless lines. - if (!i_implies_something) - implies[i].clear(); - else - something_implies_something = true; - } - if (!something_implies_something) - { - implies.clear(); - use_simulation = false; - } - } + if (use_simulation) + { + reachability_matrix scc_can_reach(scc); + bool something_implies_something = false; + for (unsigned i = 0; i != implications.size(); ++i) + { + // NB spot::simulation() does not remove unreachable states, as it + // would invalidate the contents of 'implications'. + // so we need to explicitly test for unreachable states + // FIXME: based on the scc_info, we could remove the unreachable + // states, both in the input automaton and in 'implications' + // to reduce the size of 'implies'. + if (!scc.reachable_state(i)) + continue; + unsigned scc_of_i = scc.scc_of(i); + bool i_implies_something = false; + for (unsigned j = 0; j != implications.size(); ++j) + { + if (!scc.reachable_state(j)) + continue; + bool i_implies_j = !scc_can_reach(scc.scc_of(j), scc_of_i) + && bdd_implies(implications[i], implications[j]); + implies[i][j] = i_implies_j; + i_implies_something |= i_implies_j; + } + // Clear useless lines. + if (!i_implies_something) + implies[i].clear(); + else + something_implies_something = true; + } + if (!something_implies_something) + { + implies.clear(); + use_simulation = false; + } + } // Compute the support of each state std::vector support(aut->num_states()); diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh index b047e8234..aa8196eaa 100644 --- a/spot/twaalgos/determinize.hh +++ b/spot/twaalgos/determinize.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2016, 2019-2021 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2015-2016, 2019-2021, 2023 Laboratoire de Recherche +// et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -64,7 +64,9 @@ namespace spot /// /// \param use_simulation whether to simplify the construction based /// on simulation relations between states in - /// the original automaton. + /// the original automaton. This optimization + /// is automatically disabled on automata with + /// more than 2^16 SCCs. /// /// \param use_stutter whether to simplify the construction when the /// input automaton is known to be