diff --git a/ChangeLog b/ChangeLog index 2da3577dd..de22c2982 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-03-06 Alexandre Duret-Lutz + + Reverse the order of expected acceptance conditions in + degeneralization. + + * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_tba_proxy): Build the + list of acceptance condition in the reverse order. The order is + still arbitrary, but the bdd_satone() call seems to output the + acceptance conditions that are more used first, and this helps the + degeneralization process. + 2010-03-06 Alexandre Duret-Lutz Tweak precedence of "->" and <->. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 69c87e021..7b08d8627 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -263,12 +263,19 @@ namespace spot else { // Build a cycle of expected acceptance conditions. + // + // The order is arbitrary, but it turns out that using + // push_back instead of push_front often gives better results + // because acceptance conditions and the beginning if the + // cycle are more often used in the automaton. (This + // surprising fact is probably related to order in which we + // declare the BDD variables during the translation.) bdd all = a_->all_acceptance_conditions(); while (all != bddfalse) { bdd next = bdd_satone(all); all -= next; - acc_cycle_.push_front(next); + acc_cycle_.push_back(next); } } }