Optimize tgba_tba_proxy and tgba_sba_proxy for states that share

an acceptance condition on all outgoing transitions.

This was motivated by experiments from R�diger Ehlers, showing
that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
U (b U c)'".  With this change and the previous one, it is no
longer the case.

* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store
a pointer to the source automaton and...
(tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra
optimization step to gather the acceptance conditions common
to all outgoing transitions of the destination state, and pretend
they are on the current (ingoing) transition.
(tgba_tba_proxy::succ_iter): Pass the
source automaton to the constructed iterator.
* src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7.
* src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'.

ChangeLog

@@ -1,3 +1,24 @@
+2010-03-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Optimize tgba_tba_proxy and tgba_sba_proxy for states that share
+	an acceptance condition on all outgoing transitions.
+
+	This was motivated by experiments from Rüdiger Ehlers, showing
+	that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
+	U (b U c)'".  With this change and the previous one, it is no
+	longer the case.
+
+	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store
+	a pointer to the source automaton and...
+	(tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra
+	optimization step to gather the acceptance conditions common
+	to all outgoing transitions of the destination state, and pretend
+	they are on the current (ingoing) transition.
+	(tgba_tba_proxy::succ_iter): Pass the
+	source automaton to the constructed iterator.
+	* src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7.
+	* src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'.
+
 2010-03-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	ltl2tgba: apply -R3 before -D or -DS.

src/tgba/tgbatba.cc

@@ -1,6 +1,8 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// l'Epita.
-// et Marie Curie.
+// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -114,9 +116,10 @@ namespace spot
       tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
 				   iterator expected,
 				   const list& cycle,
-				   bdd the_acceptance_cond)
+				   bdd the_acceptance_cond,
+				   const tgba* aut)
 	: it_(it), expected_(expected), cycle_(cycle),
-	  the_acceptance_cond_(the_acceptance_cond)
+	  the_acceptance_cond_(the_acceptance_cond), aut_(aut)
       {
       }
 
@@ -203,6 +206,20 @@ namespace spot
 	    //   month	= {December}
 	    // }
 
+
+	    // As an extra optimization step, gather the acceptance
+	    // conditions common to all outgoing transitions of the
+	    // destination state, and pretend they are already present
+	    // on this transition.
+	    bdd common = aut_->all_acceptance_conditions();
+	    state* dest = it_->current_state();
+	    tgba_succ_iterator* dest_it = aut_->succ_iter(dest);
+	    for (dest_it->first(); !dest_it->done(); dest_it->next())
+	      common &= dest_it->current_acceptance_conditions();
+	    acc |= common;
+	    delete dest_it;
+	    delete dest;
+
 	    next_ = expected_;
 	    while (next_ != cycle_.end() && (acc & *next_) == *next_)
 	      ++next_;
@@ -226,6 +243,7 @@ namespace spot
       bool accepting_;
       const list& cycle_;
       const bdd the_acceptance_cond_;
+      const tgba* aut_;
       friend class ::spot::tgba_tba_proxy;
     };
 
@@ -281,7 +299,8 @@ namespace spot
 					   global_state, global_automaton);
 
     return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(),
-					    acc_cycle_, the_acceptance_cond_);
+					    acc_cycle_, the_acceptance_cond_,
+					    a_);
   }
 
   bdd_dict*

src/tgbatest/ltl2tgba.test

@@ -50,3 +50,12 @@ check 'a R (b R c)'
 check '(a U b) U (c U d)'
 
 check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
+
+
+# Make sure 'a U (b U c)' has 3 states and 6 transitions,
+# before and after degeneralization.
+for opt in '' -D -DS; do
+  ../ltl2tgba -k -f -R3 $opt 'a U (b U c)' > stdout
+  grep 'transitions: 6$' stdout
+  grep 'states: 3$' stdout
+done

src/tgbatest/spotlbtt.test

@@ -270,6 +270,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), pre + post reduction, via never claim"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spin '../ltl2tgba -F -f -N -R3 -r7'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Tauriainen -- TAA)"