diff --git a/ChangeLog b/ChangeLog
index d71bcd938..ec2b2546d 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,42 @@
 2003-06-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* doc/Doxyfile.in (HAVE_DOT): Set to YES to output
+	collaboration diagrams.
+	* doc/mainpage.dox: Typo.
+
+	* src/tgba/state.hh (state::as_bdd): Delete.
+	* src/tgba/tgbaproduct.hh (state_bdd_product): Inherit from state,
+	not state_bdd.
+	(state_bdd_product::state_bdd_product): Adjust.
+	* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):
+	Adjust.
+	
+	* src/tgba/succiter.hh (tgba_bdd_succ_iterator::done):
+	Mark as const.
+	* src/tgba/succiterconcrete.cc 
+	(tgba_succ_iterator_concrete::done): Likewise.
+	* src/tgba/succiterconcrete.hh
+	(tgba_succ_iterator_concrete::done): Likewise.
+	* src/tgba/tgbaexplicit.cc 
+	(tgba_explicit_succ_iterator::done): Likewise.
+	* src/tgba/tgbaexplicit.hh
+	(tgba_explicit_succ_iterator::done): Likewise.
+	* src/tgba/tgbaproduct.cc
+	(tgba_product_succ_iterator::done): Likewise.
+	* src/tgba/tgbaproduct.hh
+	(tgba_product_succ_iterator::done): Likewise.
+	* src/tgba/tgbatranslateproxy.hh
+	(tgba_translate_proxy_succ_iterator::done): Likewise.
+	* src/tgba/tgbatranslateproxy.cc
+	(tgba_translate_proxy_succ_iterator::done): Likewise.
+	
+	* src/tgba/succiterconcrete.cc
+	(tgba_succ_iterator_concrete::next): Call bdd_satoneset
+	on data_.varandnext_set.  The previous implementation
+	was wrong for GFa.
+	* src/tgba/tgbabddcoredata.hh: Declare varandnext_set.
+	* src/tgba/tgbabddcoredata.cc: Handle varandnext_set.	
+
 	* doc/Doxygen.in: Enable LaTeX output.
 	* doc/Makefile.am (spotref.pdf): New rule.
 	(EXTRA_DIST): Add spotref.pdf.
diff --git a/doc/Doxyfile.in b/doc/Doxyfile.in
index e709ad7b5..5dd950e71 100644
--- a/doc/Doxyfile.in
+++ b/doc/Doxyfile.in
@@ -180,7 +180,7 @@ PERL_PATH              = /usr/bin/perl
 #---------------------------------------------------------------------------
 CLASS_DIAGRAMS         = YES
 HIDE_UNDOC_RELATIONS   = YES
-HAVE_DOT               = NO
+HAVE_DOT               = YES
 CLASS_GRAPH            = YES
 COLLABORATION_GRAPH    = YES
 TEMPLATE_RELATIONS     = YES
diff --git a/doc/mainpage.dox b/doc/mainpage.dox
index b82c70ad2..a7398711e 100644
--- a/doc/mainpage.dox
+++ b/doc/mainpage.dox
@@ -9,7 +9,7 @@
 ///                         spot::ltl::formula.
 /// \li spot::tgba          Base class for Transition-based
 ///                         Generalized Büchi Automaton.
-/// \li spot::ltl_to_tgba   Convert an spot::ltl:formula into a
+/// \li spot::ltl_to_tgba   Convert an spot::ltl::formula into a
 ///                         spot::tgba.
 
 
diff --git a/src/tgba/state.hh b/src/tgba/state.hh
index 75fcbc0e2..fea4dba84 100644
--- a/src/tgba/state.hh
+++ b/src/tgba/state.hh
@@ -37,13 +37,6 @@ namespace spot
     /// Duplicate a state.
     virtual state* clone() const = 0;
 
-    /// Return the BDD part of the state.
-    virtual bdd
-    as_bdd() const
-    {
-      return bddtrue;
-    }
-
     virtual ~state()
     {
     }
diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh
index 7a382db15..4c278c7ad 100644
--- a/src/tgba/succiter.hh
+++ b/src/tgba/succiter.hh
@@ -51,7 +51,7 @@ namespace spot
     ///    for (s->first(); !s->done(); s->next())
     ///      ...
     /// \endcode
-    virtual bool done() = 0;
+    virtual bool done() const = 0;
 
     //@}
 
diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc
index 2304e0599..2e5c9e270 100644
--- a/src/tgba/succiterconcrete.cc
+++ b/src/tgba/succiterconcrete.cc
@@ -47,8 +47,7 @@ namespace spot
     //     d * !Next[a] * Next[b]
     // (We don't really care about the Now variables here.)
     //
-    // Note: on this example we would not exactly get the six transitions
-    // mentionned, but maybe something like
+    // Note: on this example it's ok to get something like
     //     c * Next[a] * Next[b]
     //     c * Next[a] * !Next[b]
     //     c * !Next[a] * Next[b]
@@ -56,7 +55,10 @@ namespace spot
     //     d * !c * Next[a] * !Next[b]
     //     d * !c * !Next[a] * Next[b]
     // depending on the BDD order.  It doesn't really matter.  The important
-    // point is that we don't list all four possible 'c' and 'd' combinations.
+    // point is that we don't want to list all four possible 'c' and 'd' 
+    // combinations.
+    // FIXME: This is not what we do now: we list all possible combinations
+    // of atomic propositions.
 
     // FIXME: Iterating on the successors this way (calling
     // bdd_satone/bdd_fullsetone and NANDing out the result from a
@@ -67,8 +69,8 @@ namespace spot
 	succ_set_left_ &= !current_;
 	if (succ_set_left_ == bddfalse) // No more successors?
 	  return;
-	current_ = bdd_satoneset(succ_set_left_, data_.next_set, bddfalse);
-
+	current_ = bdd_satoneset(succ_set_left_,
+				 data_.varandnext_set, bddfalse);
 	// The destination state, computed here, should be
 	// compatible with the transition relation.  Otherwise
 	// it won't have any successor (a dead node).
@@ -79,7 +81,7 @@ namespace spot
   }
 
   bool
-  tgba_succ_iterator_concrete::done()
+  tgba_succ_iterator_concrete::done() const
   {
     return succ_set_left_ == bddfalse;
   }
diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh
index 9d0058281..2e9d2837a 100644
--- a/src/tgba/succiterconcrete.hh
+++ b/src/tgba/succiterconcrete.hh
@@ -27,7 +27,7 @@ namespace spot
     // iteration
     void first();
     void next();
-    bool done();
+    bool done() const;
 
     // inspection
     state_bdd* current_state();
diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc
index 4df8a2ea2..eec363fa7 100644
--- a/src/tgba/tgbabddcoredata.cc
+++ b/src/tgba/tgbabddcoredata.cc
@@ -12,6 +12,7 @@ namespace spot
       notnext_set(bddtrue),
       var_set(bddtrue),
       notvar_set(bddtrue),
+      varandnext_set(bddtrue),
       notacc_set(bddtrue),
       negacc_set(bddtrue),
       next_to_now(bdd_newpair())
@@ -28,6 +29,7 @@ namespace spot
       notnext_set(copy.notnext_set),
       var_set(copy.var_set),
       notvar_set(copy.notvar_set),
+      varandnext_set(copy.varandnext_set),
       notacc_set(copy.notacc_set),
       negacc_set(copy.negacc_set),
       next_to_now(bdd_copypair(copy.next_to_now))
@@ -47,6 +49,7 @@ namespace spot
       notnext_set(left.notnext_set & right.notnext_set),
       var_set(left.var_set & right.var_set),
       notvar_set(left.notvar_set & right.notvar_set),
+      varandnext_set(left.varandnext_set & right.varandnext_set),
       notacc_set(left.notacc_set & right.notacc_set),
       negacc_set(left.negacc_set & right.negacc_set),
       next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now))
@@ -80,6 +83,7 @@ namespace spot
     bdd both = now & next;
     notvar_set &= both;
     notacc_set &= both;
+    varandnext_set &= next;
   }
 
   void
@@ -89,6 +93,7 @@ namespace spot
     notnext_set &= var;
     notacc_set &= var;
     var_set &= var;
+    varandnext_set &= var;
   }
 
   void
diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh
index 68b21f65a..8fda345b5 100644
--- a/src/tgba/tgbabddcoredata.hh
+++ b/src/tgba/tgbabddcoredata.hh
@@ -79,6 +79,9 @@ namespace spot
     /// \brief The (positive) conjunction of all variables which are
     /// not atomic propositions.
     bdd notvar_set;
+    /// \brief The (positive) conjunction of all Next variables 
+    /// and atomic propositions.
+    bdd varandnext_set;
     /// \brief The (positive) conjunction of all variables which are not
     /// accepting conditions.
     bdd notacc_set;
diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc
index 75d3f2c18..3a7a8175b 100644
--- a/src/tgba/tgbaexplicit.cc
+++ b/src/tgba/tgbaexplicit.cc
@@ -29,7 +29,7 @@ namespace spot
   }
 
   bool
-  tgba_explicit_succ_iterator::done()
+  tgba_explicit_succ_iterator::done() const
   {
     return i_ == s_->end();
   }
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index 17f308c00..672fd89bc 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -91,7 +91,7 @@ namespace spot
 
 
   /// Successor iterators used by spot::tgba_explicit.
-  class tgba_explicit_succ_iterator : public tgba_succ_iterator
+  class tgba_explicit_succ_iterator: public tgba_succ_iterator
   {
   public:
     tgba_explicit_succ_iterator(const tgba_explicit::state* s, bdd all_acc);
@@ -103,7 +103,7 @@ namespace spot
 
     virtual void first();
     virtual void next();
-    virtual bool done();
+    virtual bool done() const;
 
     virtual state_explicit* current_state();
     virtual bdd current_condition();
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index c1e56ca09..7e3f2a757 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -11,7 +11,7 @@ namespace spot
   // state_bdd_product
 
   state_bdd_product::state_bdd_product(const state_bdd_product& o)
-    : state_bdd(o.as_bdd()),
+    : state(),
       left_(o.left()->clone()),
       right_(o.right()->clone())
   {
@@ -116,7 +116,7 @@ namespace spot
   }
 
   bool
-  tgba_product_succ_iterator::done()
+  tgba_product_succ_iterator::done() const
   {
     return !right_ || right_->done();
   }
diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh
index eada93268..fae6c5d71 100644
--- a/src/tgba/tgbaproduct.hh
+++ b/src/tgba/tgbaproduct.hh
@@ -11,7 +11,7 @@ namespace spot
   ///
   /// This state is in fact a pair of state: the state from the left
   /// automaton and that of the right.
-  class state_bdd_product : public state_bdd
+  class state_bdd_product : public state
   {
   public:
     /// \brief Constructor
@@ -20,8 +20,7 @@ namespace spot
     /// These state are acquired by spot::state_bdd_product, and will
     /// be deleted on destruction.
     state_bdd_product(state* left, state* right)
-      : state_bdd(left->as_bdd() & right->as_bdd()),
-	left_(left),
+      :	left_(left),
 	right_(right)
     {
     }
@@ -65,7 +64,7 @@ namespace spot
     // iteration
     void first();
     void next();
-    bool done();
+    bool done() const;
 
     // inspection
     state_bdd_product* current_state();
diff --git a/src/tgba/tgbatranslateproxy.cc b/src/tgba/tgbatranslateproxy.cc
index 1bcb7e6a5..df07f2943 100644
--- a/src/tgba/tgbatranslateproxy.cc
+++ b/src/tgba/tgbatranslateproxy.cc
@@ -33,7 +33,7 @@ namespace spot
   }
 
   bool
-  tgba_translate_proxy_succ_iterator::done()
+  tgba_translate_proxy_succ_iterator::done() const
   {
     return iter_->done();
   }
diff --git a/src/tgba/tgbatranslateproxy.hh b/src/tgba/tgbatranslateproxy.hh
index 66f1416e9..2943444c0 100644
--- a/src/tgba/tgbatranslateproxy.hh
+++ b/src/tgba/tgbatranslateproxy.hh
@@ -17,7 +17,7 @@ namespace spot
     // iteration
     void first();
     void next();
-    bool done();
+    bool done() const;
 
     // inspection
     state* current_state();