dualize: improve performance on small automata with large |AP|

For issue #566.

* spot/twaalgos/dualize.cc (dualizer::copy_edges): Implement another
loop to be used when the number of outgoing edges of a state is
smaller than the number of AP.
* tests/core/566.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the improvement.
This commit is contained in:
Alexandre Duret-Lutz 2024-03-17 21:27:04 +01:00
parent 75e552fdac
commit 1e512d422b
4 changed files with 205 additions and 16 deletions

4
NEWS
View file

@ -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 should raise an exception of return nullptr if it requires more
acceptance sets than supported. 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 - [Potential backward incompatibility] spot::dualize() does not call
cleanup_acceptance() anymore. This change ensures that the dual cleanup_acceptance() anymore. This change ensures that the dual
of a Büchi automaton will always be a co-Büchi automaton. of a Büchi automaton will always be a co-Büchi automaton.

View file

@ -146,29 +146,74 @@ namespace spot
{ {
std::vector<unsigned> st; std::vector<unsigned> st;
unsigned n = aut_->num_states(); unsigned n = aut_->num_states();
unsigned n_ap = res->ap().size();
std::vector<bdd> labels;
for (unsigned i = 0; i < n; ++i) 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 ap = bdd_exist(bdd_support(delta), all_vars_);
bdd letters = bdd_exist(delta, all_vars_); bdd letters = bdd_exist(delta, all_vars_);
for (bdd oneletter: minterms_of(letters, ap)) // Create edges with label LABEL, and destinations states
{ // encoded in the Boolean function RESTRICTED_DELTA.
minato_isop isop(bdd_restrict(delta, oneletter)); auto create_edges = [&](bdd label, bdd restricted_delta) {
bdd dest; 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(); // make sure we don't realloc during the loop
acc_cond::mark_t m = bdd_to_state(dest, st); labels.reserve(labels.size() * 2);
if (st.empty()) // Do not use a range-based or iterator-based for
{ // loop here, as push_back invalidates the end
st.push_back(true_state_); // iterator.
if (aut_->prop_state_acc()) for (unsigned cur = 0, sz = labels.size(); cur < sz; ++cur)
m = aut_->state_acc_sets(i); if (bdd common = labels[cur] & e.cond; common != bddfalse)
} {
res->new_univ_edge(i, st.begin(), st.end(), oneletter, m); 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. // 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) if (state_to_var_[state_id] == bddtrue)
return bddfalse; return bddfalse;
bdd res = bddtrue; bdd res = bddtrue;
for (auto& e : aut_->out(state_id)) for (auto& e : aut_->out(state_id))
{ {
++n_succ;
bdd dest = bddfalse; bdd dest = bddfalse;
for (unsigned d : aut_->univ_dests(e)) for (unsigned d : aut_->univ_dests(e))
dest |= state_to_var_[d]; dest |= state_to_var_[d];

View file

@ -220,6 +220,7 @@ TESTS_twa = \
core/385.test \ core/385.test \
core/521.test \ core/521.test \
core/522.test \ core/522.test \
core/566.test \
core/acc.test \ core/acc.test \
core/acc2.test \ core/acc2.test \
core/bdddict.test \ core/bdddict.test \

137
tests/core/566.test Executable file
View file

@ -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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
cat >21.hoa <<EOF
HOA: v1 States: 5 Start: 0 AP: 21 "__ap6" "__ap10" "__ap57" "__ap61"
"__ap63" "__ap67" "__ap97" "__ap94" "__ap96" "__ap111" "__ap114" "__ap117"
"__ap120" "__ap121" "__ap124" "__ap125" "__ap128" "__ap129" "__ap132"
"__ap133" "__ap135" acc-name: Buchi Acceptance: 1 Inf(0) properties:
trans-labels explicit-labels state-acc very-weak --BODY-- State: 0
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&20
|
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
1
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&17&!18&!19&!20
|
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
2
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&20
|
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
3
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&17&!18&!19&!20
|
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&!8&9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&!7&8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&!6&7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&!5&6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&!4&5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&!3&4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&!2&3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&!1&2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
!0&1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20 |
0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
4 State: 1
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
1
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
2 State: 2 {0}
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
2 State: 3
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
1
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
2
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
3
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
4 State: 4
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
2
[!0&!1&!2&!3&!4&!5&!6&!7&!8&!9&!10&!11&!12&!13&!14&!15&!16&!17&!18&!19&!20]
4 --END--
EOF
# The real test would be to check that this result is instantaneous,
# but it is difficult to test so in the test suite.
res=`autfilt --dualize 21.hoa --stats='%S %E %T %s %e %t'`
test "$res" = "5 13 85 6 13 12582912"