From 58b233db6f64f13616ba914b6cb34b4799744d1c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Mar 2010 17:42:48 +0100 Subject: [PATCH] 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. --- ChangeLog | 11 +++++++++++ src/tgba/tgbatba.cc | 9 ++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) 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); } } }