Improve documentation here and there.

* doc/Doxyfile.in: Update to Doxygen 1.8.4
* doc/footer.html: Point to the mailing list.
* doc/mainpage.dox: Point to spot::translator,
and spot::kripke.
* src/ta/tgta.hh: Do not use \emph.
* src/tgba/succiter.hh: Fix rendering of example.
* src/tgba/tgba.hh: Correct documentation.
* src/tgbaalgos/cycles.hh: Improve rendering of
documentation.
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/minimize.hh:
Document missing arguments.

doc/footer.html

@@ -1,6 +1,5 @@
 <hr size="1">
-Please <b>comment</b> this page and <b>report errors</b> about it on
+Please direct any <b>question</b>, <b>comment</b>, or <b>bug report</b> to the Spot mailing list at <a href="mailto:spot@lrde.epita.fr">spot@lrde.epita.fr</a>.
-<a href="http://spot.lip6.fr/wiki/RefDocComments">the RefDocComments page</a>.
 <br><address style="align: right;"><small>
 Generated on $datetime for $projectname by <a href="http://www.doxygen.org/index.html"><img src="doxygen.png" alt="doxygen" align="middle" border=0></a> $doxygenversion</small></address>
 </body>

doc/mainpage.dox

@@ -19,13 +19,14 @@
 ///
 /// \section pointers Handy starting points
 ///
-/// \li spot::ltl::formula  Base class for an LTL formulae.
+/// \li spot::ltl::formula    Base class for an LTL or PSL formula.
-/// \li spot::ltl::parse    Parsing a text string into a
+/// \li spot::ltl::parse      Parsing a text string into a
-///                         spot::ltl::formula.
+///                           spot::ltl::formula.
-/// \li spot::tgba          Base class for Transition-based
+/// \li spot::tgba            Base class for Transition-based
-///                         Generalized Büchi Automaton.
+///                           Generalized Büchi Automaton.
-/// \li spot::ltl_to_tgba_fm  Convert a spot::ltl::formula into a
+/// \li spot::translator      Convert a spot::ltl::formula into a
 ///                           spot::tgba.
+/// \li spot::kripke          Base class for Kripke structures.
 /// \li spot::tgba_product    On-the-fly product of two spot::tgba.
 /// \li spot::emptiness_check Base class for all emptiness-check algorithms
 ///                           (see also module \ref emptiness_check)

src/ta/tgta.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -27,20 +27,22 @@ namespace spot
   /// \ingroup ta_essentials
   /// \brief A Transition-based Generalized Testing Automaton (TGTA).
   ///
-  ///  Transition-based Generalized Testing Automaton (TGTA) is a new kind of
+  /// Transition-based Generalized Testing Automaton (TGTA) is a new
-  /// automaton that combines features from both TA and TGBA.
+  /// kind of automaton that combines features from both TA and TGBA.
-  /// From TA, we take the idea of labeling transitions with changesets,
+  /// From TA, we take the idea of labeling transitions with
-  /// however we remove the use of livelock-acceptance (because it may require
+  /// changesets, however we remove the use of livelock-acceptance
-  /// a two-pass emptiness check), and the implicit stuttering.  From TGBA, we
+  /// (because it may require a two-pass emptiness check), and the
-  /// inherit the use of transition-based generalized acceptance conditions.
+  /// implicit stuttering.  From TGBA, we inherit the use of
-  ///  The resulting Chimera, which we call \emph{Transition-based
+  /// transition-based generalized acceptance conditions.  The
-  ///  Generalized Testing Automaton} (TGTA), accepts only
+  /// resulting Chimera, which we call "Transition-based Generalized
-  ///  stuttering-insensitive languages like TA, and inherits advantages from
+  /// Testing Automaton" (TGTA), accepts only stuttering-insensitive
-  ///  both TA and TGBA: it has a simple one-pass emptiness-check procedure
+  /// languages like TA, and inherits advantages from both TA and
-  /// (the same as algorithm the one for TGBA), and can benefit from reductions
+  /// TGBA: it has a simple one-pass emptiness-check procedure (the
-  ///  based on the stuttering of the properties pretty much like a TA.
+  /// same as algorithm the one for TGBA), and can benefit from
-  ///  Livelock acceptance states, which are no longer supported are emulated
+  /// reductions based on the stuttering of the properties pretty much
-  ///using states with a Büchi accepting self-loop labeled by empty changeset.
+  /// like a TA.  Livelock acceptance states, which are no longer
+  /// supported are emulated using states with a Büchi accepting
+  /// self-loop labeled by empty changeset.
   ///
   /// Browsing such automaton can be achieved using two functions:
   /// \c get_initial_state and \c

src/tgba/succiter.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
 // l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -68,10 +68,9 @@ namespace spot
     /// 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())
+    ///     for (s->first(); !s->done(); s->next())
-    ///      ...
+    ///       ...
-    /// \endcode
     virtual bool done() const = 0;
 
     //@}

src/tgba/tgba.hh

@@ -1,5 +1,5 @@
-// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 // 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.
@@ -139,11 +139,11 @@ namespace spot
 
     /// \brief Get the dictionary associated to the automaton.
     ///
-    /// State are represented as BDDs.  The dictionary allows
+    /// Atomic propositions and acceptance conditions are represented
-    /// to map BDD variables back to formulae, and vice versa.
+    /// as BDDs.  The dictionary allows to map BDD variables back to
-    /// This is useful when dealing with several automata (which
+    /// formulae, and vice versa.  This is useful when dealing with
-    /// may use the same BDD variable for different formula),
+    /// several automata (which may use the same BDD variable for
-    /// or simply when printing.
+    /// different formula), or simply when printing.
     virtual bdd_dict* get_dict() const = 0;
 
     /// \brief Format the state as a string for printing.

src/tgbaalgos/cycles.hh

@@ -63,11 +63,12 @@ namespace spot
   /// cycle.
   ///
   /// The class constructor takes an scc_map that should already have
-  /// been built for its automaton.  Calling run(n) will enumerate all
+  /// been built for its automaton.  Calling <code>run(n)</code> will
-  /// elementary cycles in SCC #n.  Each time an SCC is found, the
+  /// enumerate all elementary cycles in SCC <code>n</code>.  Each
-  /// method cycle_found(s) is called with the initial state s of the
+  /// time an SCC is found, the method cycle_found(s) is called with
-  /// cycle: the cycle is constituted from all the states that are on
+  /// the initial state s of the cycle: the cycle is constituted from
-  /// the dfs_ stack after s (including s).
+  /// all the states that are on the \c dfs_ stack after \c s
+  /// (including \c s).
   ///
   /// You should inherit from this class and redefine the
   /// cycle_found() method to perform any work you would like to do on

src/tgbaalgos/lbtt.hh

@@ -44,6 +44,8 @@ namespace spot
   ///
   /// \param is The stream on which the automaton should be input.
   /// \param error A string in which to write any error message.
+  /// \param dict The dictionary that should register the BDD variables
+  /// used by the automaton built.
   /// \param env The environment of atomic proposition into which parsing
   ///        should take place.
   /// \param envacc The environment of acceptance conditions into which parsing

src/tgbaalgos/minimize.hh

@@ -127,6 +127,8 @@ namespace spot
   /// \param aut_f the automaton to minimize
   /// \param f the LTL formula represented by the automaton \a aut_f
   /// \param aut_neg_f an automaton representing the negation of \a aut_f
+  /// \param reject_bigger Whether the minimal WDBA should be discarded if
+  /// it has more states than the input.
   /// \return a new tgba if the automaton could be minimized, \a aut_f if
   /// the automaton cannot be minimized, 0 if we do not know if the
   /// minimization is correct because neither \a f nor \a aut_neg_f