diff --git a/NEWS b/NEWS index 1d8494ae0..e7b9b10b2 100644 --- a/NEWS +++ b/NEWS @@ -165,12 +165,12 @@ New in spot 2.11.6.dev (not yet released) - spot::dualize() learned a trick to be faster on states that have less outgoing edges than atomic proposition declared on the - automaton. spot::remove_alternation(), spot::tgba_powerset(), and - simulation-based reductions learned a similar trick, except it - isn't applied at the state level but if the entire automaton use - few distinct labels. These changes may speed up the processing of - automata with many atomic propositions but few distinct labels. - (Issue #566 and issue #568.) + automaton. spot::remove_alternation(), spot::tgba_powerset(), + simulation-based reductions, and spot::tgba_determinize() learned + a similar trick, except it isn't applied at the state level but if + the entire automaton use few distinct labels. These changes may + speed up the processing of automata with many atomic propositions + but few distinct labels. (Issue #566 and issue #568.) - [Potential backward incompatibility] spot::dualize() does not call cleanup_acceptance() anymore. This change ensures that the dual diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index a364ffa48..8f135298a 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -23,6 +23,8 @@ #include #include #include +#include +#include #include #include #include @@ -31,6 +33,7 @@ #include #include #include +#include #include namespace spot @@ -586,9 +589,27 @@ namespace spot { const std::vector& state_supports; robin_hood::unordered_flat_map, bdd_hash> cache; - + std::vector basis; + unsigned log_basis_size = 0; public: - safra_support(const std::vector& s): state_supports(s) {} + safra_support(const std::vector& s, + const const_twa_graph_ptr& orig_aut) + : state_supports(s) + { + unsigned nap = orig_aut->ap().size(); + if (nap > 5) + { + edge_separator es; + // Gather all labels, but stop if we see too many. The + // threshold below is arbitrary: adjust if you know better. + if (es.add_to_basis(orig_aut, 256 * nap)) + { + basis = es.basis(); + auto sz = basis.size(); + log_basis_size = CHAR_BIT*sizeof(sz) - clz(sz); + } + } + } const std::vector& get(const safra_state& s) @@ -600,6 +621,21 @@ namespace spot if (i.second) // insertion took place { std::vector& res = i.first->second; + // If we have a basis, we probably want to use it. + // But we should do that only if 2^|supp| is larger. + if (log_basis_size) + { + // Compute the size of the support + bdd s = supp; + unsigned sz = log_basis_size; + while (sz && s != bddtrue) + { + --sz; + s = bdd_high(s); + } + if (s != bddtrue) + return res = basis; + } for (bdd one: minterms_of(bddtrue, supp)) res.emplace_back(one); } @@ -971,7 +1007,7 @@ namespace spot } } - safra_support safra2letters(support); + safra_support safra2letters(support, aut); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); diff --git a/tests/core/568.test b/tests/core/568.test index 2fb4b8df2..b538bfb7d 100755 --- a/tests/core/568.test +++ b/tests/core/568.test @@ -75,3 +75,29 @@ cat >expected < 80 EOF diff expected out + +genaut --cycle-onehot=7..12 | + autfilt --parity -D --stats="%S -> %s" > out +cat >expected < 13 +64 -> 15 +81 -> 17 +100 -> 19 +121 -> 4360 +144 -> 9481 +EOF + +genaut --cycle-onehot=7..12 | + autfilt -x simul-max=10000 --parity -D --stats="%S -> %s" > out +cat >expected < 13 +64 -> 15 +81 -> 17 +100 -> 19 +121 -> 21 +144 -> 23 +EOF + +# Using autcross will also test tgba_determinize +genaut --cycle-onehot-nba=11..12 --cycle-log-nba=11..12 | + autcross --language-preserved 'autfilt --small' --verbose