* 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.

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.

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

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.
 
 

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()
     {
     }

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;
 
     //@}
 

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
+    // Note: on this example it's ok to get something like
-    // mentionned, but maybe 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;
   }

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

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

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;

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

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

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

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

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

src/tgba/tgbatranslateproxy.hh

@@ -17,7 +17,7 @@ namespace spot
     // iteration
     void first();
     void next();
-    bool done();
+    bool done() const;
 
     // inspection
     state* current_state();