diff --git a/NEWS b/NEWS index b875bfd6e..9da91b234 100644 --- a/NEWS +++ b/NEWS @@ -150,7 +150,10 @@ 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. (Issue #566.) + automaton. spot::remove_alternation() learned a similar trick, + except it isn't applied at the state level but of the entire + alternating use few distinct labels. These two changes speed up + the complementation of very weak automata. (Issue #566.) - [Potential backward incompatibility] spot::dualize() does not call cleanup_acceptance() anymore. This change ensures that the dual diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 1de366b66..dad0f307a 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -22,6 +22,7 @@ #include #include #include +#include namespace spot { @@ -361,7 +362,7 @@ namespace spot (has_reject_more_ + reject_1_count_) > SPOT_MAX_ACCSETS) return nullptr; - // Rejecting SCCs of size 1 can be handled using genralized + // Rejecting SCCs of size 1 can be handled using generalized // Büchi acceptance, using one set per SCC, as in Gastin & // Oddoux CAV'01. See also Boker & et al. ICALP'10. Larger // rejecting SCCs require a more expensive procedure known as @@ -375,6 +376,54 @@ namespace spot // This will raise an exception if we request too many sets. res->set_generalized_buchi(has_reject_more_ + reject_1_count_); + // Before we start, let's decide how we will iterate on the + // BDD that we use to encode the transition function. We have + // two way of doing so: iterating over 2^AP, or precomputing a + // set of "separated labels" that cover all labels. The + // latter is a good idea if that set is much smaller than + // 2^AP, but we cannot always know that before hand. + std::vector separated_labels; + unsigned n_ap = aut_->ap().size(); + // If |AP| is small, don't bother with the computation of + // separated labels. + bool will_use_labels = n_ap > 5; + if (will_use_labels) + { + std::set all_labels; + // Gather all labels, but stop if we see too many. + // The threshold below is arbitrary. + unsigned max_labels = 100 * n_ap; + for (auto& e: aut_->edges()) + { + if (all_labels.insert(e.cond).second) + if (all_labels.size() > max_labels) + { + will_use_labels = false; + break; + } + } + if (will_use_labels) + { + separated_labels.reserve(all_labels.size()); + separated_labels.push_back(bddtrue); + for (auto& lab: all_labels) + { + // make sure don't realloc during the loop + separated_labels.reserve(separated_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 = separated_labels.size(); + cur < sz; ++cur) + if (bdd common = separated_labels[cur] & lab; + common != bddfalse) + { + separated_labels[cur] -= lab; + separated_labels.push_back(common); + } + } + } + } + // We for easier computation of outgoing sets, we will // represent states using BDD variables. allocate_state_vars(); @@ -459,44 +508,53 @@ namespace spot bdd ap = bdd_exist(bdd_support(bs), all_vars_); bdd all_letters = bdd_exist(bs, all_vars_); - // First loop over all possible valuations atomic properties. - for (bdd oneletter: minterms_of(all_letters, ap)) - { - minato_isop isop(bdd_restrict(bs, oneletter)); - bdd dest; - while ((dest = isop.next()) != bddfalse) - { - v.clear(); - acc_cond::mark_t m = bdd_to_state(dest, v); + // Given a label, and BDD expression representing + // the combination of destinations, create the edges. + auto create_edges = [&](bdd label, bdd dest_formula) + { + minato_isop isop(dest_formula); + bdd dest; + while ((dest = isop.next()) != bddfalse) + { + v.clear(); + acc_cond::mark_t m = bdd_to_state(dest, v); - // if there is no promise "f" between a state - // that does not have f, and a state that have - // "f", we can add one. Doing so will help later - // simplifications performed by postprocessor. An - // example where this is needed is the VWAA - // generated by ltl[23]ba for GFa. Without the - // next loop, the final TGBA has 2 states instead - // of 1. - for (unsigned m1: (all_marks - m).sets()) - { - if (has_reject_more_ && m1 == 0) - continue; - auto& sv = s_to_ss[s]; - unsigned ms = mark_to_state_[m1]; - if (std::find(v.begin(), v.end(), ms) != v.end()) - { - unsigned ms = mark_to_state_[m1]; - if (std::find(sv.begin(), sv.end(), ms) == sv.end()) - m.set(m1); - } - } + // if there is no promise "f" between a state + // that does not have f, and a state that have + // "f", we can add one. Doing so will help later + // simplifications performed by postprocessor. An + // example where this is needed is the VWAA + // generated by ltl[23]ba for GFa. Without the + // next loop, the final TGBA has 2 states instead + // of 1. + for (unsigned m1: (all_marks - m).sets()) + { + if (has_reject_more_ && m1 == 0) + continue; + auto& sv = s_to_ss[s]; + unsigned ms = mark_to_state_[m1]; + if (std::find(v.begin(), v.end(), ms) != v.end()) + { + unsigned ms = mark_to_state_[m1]; + if (std::find(sv.begin(), sv.end(), ms) == sv.end()) + m.set(m1); + } + } - unsigned d = new_state(v, has_mark); - if (has_mark) - m.set(0); - res->new_edge(s, d, oneletter, all_marks - m); - } - } + unsigned d = new_state(v, has_mark); + if (has_mark) + m.set(0); + res->new_edge(s, d, label, all_marks - m); + } + }; + + if (!will_use_labels) + // Loop over all possible valuations atomic properties. + for (bdd oneletter: minterms_of(all_letters, ap)) + create_edges(oneletter, bdd_restrict(bs, oneletter)); + else + for (bdd label: separated_labels) + create_edges(label, bdd_relprod(label, bs, res->ap_vars())); } res->merge_edges(); return res; diff --git a/tests/core/566.test b/tests/core/566.test index 3adcc3bc6..2399576c4 100755 --- a/tests/core/566.test +++ b/tests/core/566.test @@ -135,3 +135,6 @@ EOF # 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" + +res=`autfilt --complement 21.hoa --stats='%S %E %T %s %e %t'` +test "$res" = "5 13 85 5 11 10485760"