diff --git a/NEWS b/NEWS index 694d5bf6f..b875bfd6e 100644 --- a/NEWS +++ b/NEWS @@ -148,6 +148,10 @@ New in spot 2.11.6.dev (not yet released) should raise an exception of return nullptr if it requires more acceptance sets than supported. + - spot::dualize() learned a trick to be faster on states that have + less outgoing edges than atomic proposition declared on the + automaton. (Issue #566.) + - [Potential backward incompatibility] spot::dualize() does not call cleanup_acceptance() anymore. This change ensures that the dual of a Büchi automaton will always be a co-Büchi automaton. diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index fc60d78af..cbef6d451 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -146,29 +146,74 @@ namespace spot { std::vector st; unsigned n = aut_->num_states(); + unsigned n_ap = res->ap().size(); + std::vector labels; + for (unsigned i = 0; i < n; ++i) { - bdd delta = dualized_transition_function(i); + unsigned n_succs; + bdd delta = dualized_transition_function(i, n_succs); + if (delta == bddfalse) + continue; bdd ap = bdd_exist(bdd_support(delta), all_vars_); bdd letters = bdd_exist(delta, all_vars_); - for (bdd oneletter: minterms_of(letters, ap)) - { - minato_isop isop(bdd_restrict(delta, oneletter)); - bdd dest; + // Create edges with label LABEL, and destinations states + // encoded in the Boolean function RESTRICTED_DELTA. + auto create_edges = [&](bdd label, bdd restricted_delta) { + minato_isop isop(restricted_delta); + bdd dest; + while ((dest = isop.next()) != bddfalse) + { + st.clear(); + acc_cond::mark_t m = bdd_to_state(dest, st); + if (st.empty()) + { + st.push_back(true_state_); + if (aut_->prop_state_acc()) + m = aut_->state_acc_sets(i); + } + res->new_univ_edge(i, st.begin(), st.end(), label, m); + } + }; - while ((dest = isop.next()) != bddfalse) + // Iterating over all mineterms can be very slow when |AP| + // is large (see issue #566) . The else branch implements + // another approach that should be exponential in the + // number of successors instead of in the number of atomic + // propositions. + if (n_succs > n_ap) + { + for (bdd oneletter: minterms_of(letters, ap)) + create_edges(oneletter, bdd_restrict(delta, oneletter)); + } + else + { + // gather all labels in the successors of state, + // and split those labels so they are all disjoint. + // + // LABELS may have 2^{n_succ} elements after this + // loop, but since n_succ <= n_ap, we expect this + // approach to be faster. + labels.clear(); + labels.reserve(n_succs); + labels.push_back(bddtrue); + for (auto& e: aut_->out(i)) { - st.clear(); - acc_cond::mark_t m = bdd_to_state(dest, st); - if (st.empty()) - { - st.push_back(true_state_); - if (aut_->prop_state_acc()) - m = aut_->state_acc_sets(i); - } - res->new_univ_edge(i, st.begin(), st.end(), oneletter, m); + // make sure we don't realloc during the loop + labels.reserve(labels.size() * 2); + // Do not use a range-based or iterator-based for + // loop here, as push_back invalidates the end + // iterator. + for (unsigned cur = 0, sz = labels.size(); cur < sz; ++cur) + if (bdd common = labels[cur] & e.cond; common != bddfalse) + { + labels[cur] -= e.cond; + labels.push_back(common); + } } + for (auto& cur: labels) + create_edges(cur, bdd_relprod(cur, delta, res->ap_vars())); } } } @@ -223,14 +268,16 @@ namespace spot } // Returns the dualized transition function of any input state as a bdd. - bdd dualized_transition_function(unsigned state_id) + bdd dualized_transition_function(unsigned state_id, unsigned& n_succ) { + n_succ = 0; if (state_to_var_[state_id] == bddtrue) return bddfalse; bdd res = bddtrue; for (auto& e : aut_->out(state_id)) { + ++n_succ; bdd dest = bddfalse; for (unsigned d : aut_->univ_dests(e)) dest |= state_to_var_[d]; diff --git a/tests/Makefile.am b/tests/Makefile.am index 67e5bb4d6..4a36a725b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -220,6 +220,7 @@ TESTS_twa = \ core/385.test \ core/521.test \ core/522.test \ + core/566.test \ core/acc.test \ core/acc2.test \ core/bdddict.test \ diff --git a/tests/core/566.test b/tests/core/566.test new file mode 100755 index 000000000..3adcc3bc6 --- /dev/null +++ b/tests/core/566.test @@ -0,0 +1,137 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs + +set -e + +cat >21.hoa <