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

@@ -1,3 +1,14 @@
+2010-03-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	Tweak precedence of "->" and <->.

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);
 	  }
       }
   }