* src/tgba/bddprint.hh (bdd_format_set): New function.

* src/tgba/bddprint.cc (bdd_format_set): Likewise.
* src/tgba/state.hh: Add Doxygen comments.
(state::compare): Take a state*, not a state&.
(state_ptr_less_than): New functor.
* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
state&.
* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
* src/tgba/succiter.hh: Add Doxygen comments.
* src/tgba/tgba.hh: Mention promises.
(tgba::formate_state): New pure virtual method.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
New method.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
Likewise.
* src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
and tgba::formate_state.

ChangeLog

@@ -1,13 +1,28 @@
 2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/bddprint.hh (bdd_format_set): New function.
+	* src/tgba/bddprint.cc (bdd_format_set): Likewise.
+	* src/tgba/state.hh: Add Doxygen comments.
+	(state::compare): Take a state*, not a state&.
+	(state_ptr_less_than): New functor.
+	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a 
+	state&.
+	* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
+	* src/tgba/succiter.hh: Add Doxygen comments.
+	* src/tgba/tgba.hh: Mention promises.
+	(tgba::formate_state): New pure virtual method.
+	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
+	New method.
+	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
+	Likewise.
+	* src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
+	and tgba::formate_state.
+
 	* src/tgba/succiter.hh (tgba_succ_iterator::current_state):
 	Return a state*, not a state_bdd.
 	* src/tgba/succiterconcrete.hh
 	(tgba_succ_iterator_concrete::current_state): Return a state_bdd*,
 	not a state_bdd.
-	* src/tgba/state.hh (state::as_bdd): New abstract method.
-	* src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ...
-	* src/tgba/statebdd.cc (state_bdd::as_bdd): ... here.
 	* src/tgba/tgba.hh: Add Doxygen comments.
 	(tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd.
 	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state):

src/tgba/bddprint.cc

@@ -1,3 +1,4 @@
+#include <sstream>
 #include "bddprint.hh"
 #include "ltlvisit/tostring.hh"
 
@@ -54,6 +55,14 @@ namespace spot
     return os;
   }
 
+  std::string
+  bdd_format_set(const tgba_bdd_dict& d, bdd b)
+  {
+    std::ostringstream os;
+    bdd_print_set(os, d, b);
+    return os.str();
+  }
+
   std::ostream&
   bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
   {

src/tgba/bddprint.hh

@@ -1,6 +1,7 @@
 #ifndef SPOT_TGBA_BDDPRINT_HH
 # define SPOT_TGBA_BDDPRINT_HH
 
+#include <string>
 #include <iostream>
 #include "tgbabdddict.hh"
 #include <bdd.h>
@@ -10,6 +11,7 @@ namespace spot
 
   std::ostream& bdd_print_set(std::ostream& os,
 			      const tgba_bdd_dict& dict, bdd b);
+  std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b);
 
   std::ostream& bdd_print_dot(std::ostream& os,
 			      const tgba_bdd_dict& dict, bdd b);

src/tgba/state.hh

@@ -5,25 +5,48 @@
 
 namespace spot
 {
+
+  /// \brief Abstract class for states.
   class state
   {
   public:
-    // Compares two states (that come from the same automaton).
+    /// \brief Compares two states (that come from the same automaton).
-    //
+    ///
-    // This method returns an integer less than, equal to, or greater
+    /// This method returns an integer less than, equal to, or greater
-    // than zero if THIS is found, respectively, to be less than, equal
+    /// than zero if \a this is found, respectively, to be less than, equal
-    // to, or greater than OTHER according to some implicit total order.
+    /// to, or greater than \a other according to some implicit total order.
-    //
+    ///
-    // This method should not be called to compare state from
+    /// This method should not be called to compare states from
-    // different automata.
+    /// different automata.
-    virtual int compare(const state& other) const = 0;
+    ///
-
+    /// \sa spot::state_ptr_less_than
-    virtual bdd as_bdd() const = 0;
+    virtual int compare(const state* other) const = 0;
 
     virtual ~state()
     {
     }
   };
+
+  /// \brief Strict Weak Ordering for \c state*.
+  ///
+  /// This is meant to be used as a comparison functor for
+  /// STL \c map whose key are of type \c state*.
+  ///
+  /// For instance here is how one could declare
+  /// a map of \c state*.
+  /// \code
+  ///   // Remember how many times each state has been visited.
+  ///   std::map<spot::state*, int, spot::state_ptr_less_than> seen;
+  /// \endcode
+  struct state_ptr_less_than
+  {
+    bool
+    operator()(const state* left, const state *right)
+    {
+      return left->compare(right) < 0;
+    }
+  };
+
 }
 
 #endif // SPOT_TGBA_STATE_HH

src/tgba/statebdd.cc

@@ -1,23 +1,17 @@
 #include "statebdd.hh"
+#include "bddprint.hh"
 #include <cassert>
 
 namespace spot
 {
   int
-  state_bdd::compare(const state& other) const
+  state_bdd::compare(const state* other) const
   {
     // This method should not be called to compare states from different
     // automata, and all states from the same automaton will use the same
     // state class.
-    const state_bdd* o = dynamic_cast<const state_bdd*>(&other);
+    const state_bdd* o = dynamic_cast<const state_bdd*>(other);
     assert(o);
     return o->as_bdd().id() - state_.id();
   }
-
-  bdd
-  state_bdd::as_bdd() const
-  {
-    return state_;
-  }
-
 }

src/tgba/statebdd.hh

@@ -14,8 +14,13 @@ namespace spot
     {
     }
 
-    virtual bdd as_bdd() const;
+    bdd 
-    virtual int compare(const state& other) const;
+    as_bdd() const
+    {
+      return state_;
+    }
+    
+    virtual int compare(const state* other) const;
 
   protected:
     bdd state_;

src/tgba/succiter.hh

@@ -6,6 +6,13 @@
 namespace spot
 {
 
+  /// \brief Iterate over the successors of a state.
+  ///
+  /// This class provides the basic functionalities required to
+  /// iterate over the successors of a state, as well as querying
+  /// transition labels.  Because transitions are never explicitely
+  /// encoded, labels (conditions and promises) can only be queried
+  /// while iterating over the successors.
   class tgba_succ_iterator
   {
   public:
@@ -14,15 +21,57 @@ namespace spot
     {
     }
 
-    // iteration
+    /// \name Iteration
+    //@{
+
+    /// \brief Position the iterator on the first successor (if any).
+    ///
+    /// This method can be called several times to make multiple
+    /// passes over successors.  
+    ///
+    /// \warning One should always call \c done() to
+    /// ensure there is a successor, even after \c first().  A
+    /// common trap is to assume that there is at least one
+    /// successor: this is wrong.
     virtual void first() = 0;
+
+    /// \brief Jump to the next successor (if any).
+    ///
+    /// \warning Again, one should always call \c done() to ensure
+    /// there is a successor.
     virtual void next() = 0;
+
+    /// \brief Check whether the iteration is finished.
+    ///
+    /// This function should be called after any call to \c first()
+    /// or \c next() and before any enquiry about the current state.
+    ///
+    /// The usual way to do this is with a \c for loop.
+    /// \code
+    ///    for (s->first(); !s->done(); s->next())
+    ///      ...
+    /// \endcode
     virtual bool done() = 0;
 
-    // inspection
+    //@}
+
+    /// \name Inspection
+    //@{
+
+    /// \brief Get the state of the current successor.
+    ///
+    /// Note that the same state may occur at different points
+    /// in the iteration.  These actually correspond to the same
+    /// destination.  It just means there were several transitions,
+    /// with different conditions or promises, leading to the
+    /// same state.
     virtual state* current_state() = 0;
+    /// \brief Get the condition on the transition leading to this successor.
     virtual bdd current_condition() = 0;
+    /// \brief Get the promise on the transition leading to this successor.
     virtual bdd current_promise() = 0;
+
+    //@}
   };
 
 }

src/tgba/tgba.hh

@@ -20,6 +20,12 @@ namespace spot
   /// transitions), and a path can be accepted only if it traverse
   /// at least one transition of each set infinitely often.
   ///
+  /// Actually we do not really encode accepting sets but their
+  /// complement: promise sets.  Formulae such as 'a U b' and
+  /// 'F b' make the promise to fulfil 'b' enventually.  A path can
+  /// be accepted if for each promise it traverse infinitely often
+  /// a transition that does not make this promise.
+  ///
   /// Browsing such automaton can be achieved using two functions.
   /// \c get_init_state, and \c succ_iter.  The former returns
   /// the initial state while the latter allows to explore the
@@ -65,6 +71,12 @@ namespace spot
     /// may use the same BDD variable for different formula),
     /// or simply when printing.
     virtual const tgba_bdd_dict& get_dict() const = 0;
+
+    /// \brief Format the state as a string for printing.
+    ///
+    /// This formating is the responsability of the automata
+    /// who owns the state.
+    virtual std::string format_state(const state* state) const = 0;
   }; 
 
 }

src/tgba/tgbabddconcrete.cc

@@ -1,4 +1,5 @@
 #include "tgbabddconcrete.hh"
+#include "bddprint.hh"
 
 namespace spot
 {
@@ -45,6 +46,14 @@ namespace spot
     return new tgba_succ_iterator_concrete(data_, succ_set);
   }
 
+  std::string
+  tgba_bdd_concrete::format_state(const state* state) const
+  {
+    const state_bdd* s = dynamic_cast<const state_bdd*>(state);
+    assert(s);
+    return bdd_format_set(dict_, s->as_bdd());
+  }
+
   const tgba_bdd_dict&
   tgba_bdd_concrete::get_dict() const
   {

src/tgba/tgbabddconcrete.hh

@@ -21,6 +21,8 @@ namespace spot
 
     tgba_succ_iterator_concrete* succ_iter(const state* state) const;
 
+    std::string format_state(const state* state) const;
+
     const tgba_bdd_dict& get_dict() const;
     const tgba_bdd_core_data& get_core_data() const;
 

src/tgbaalgos/dotty.cc

@@ -5,14 +5,13 @@
 
 namespace spot
 {
-  typedef std::map<int, int> seen_map;
+  typedef std::map<state*, int, state_ptr_less_than> seen_map;
 
   static bool
   dotty_state(std::ostream& os,
 	      const tgba& g, state* st, seen_map& m, int& node)
   {
-    bdd s = st->as_bdd();
+    seen_map::iterator i = m.find(st);
-    seen_map::iterator i = m.find(s.id());
 
     // Already drawn?
     if (i != m.end())
@@ -22,10 +21,10 @@ namespace spot
       }
 
     node = m.size() + 1;
-    m[s.id()] = node;
+    m[st] = node;
 
-    std::cout << "  " << node << " [label=\"";
+    os << "  " << node << " [label=\"" 
-    bdd_print_set(os, g.get_dict(), s) << "\"]" << std::endl;
+       << g.format_state(st) << "\"]" << std::endl;
     return true;
   }
 
@@ -44,9 +43,15 @@ namespace spot
 	bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]"
 							       << std::endl;
 	if (recurse)
+	  {
 	    dotty_rec(os, g, s, m, node);
+	    // Do not delete S, it is used as key in M.
+	  }
+	else
+	  {
 	    delete s;
 	  }
+      }
     delete si;
   }
 
@@ -63,7 +68,11 @@ namespace spot
     os << "  0 -> " << init << std::endl;
     dotty_rec(os, g, state, m, init);
     os << "}" << std::endl;
-    delete state;
+
+    // Finally delete all states used as keys in m:
+    for (seen_map::iterator i = m.begin(); i != m.end(); ++i)
+      delete i->first;
+
     return os;
   }