diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh
index aca7b6174..22e3656e4 100644
--- a/src/kripke/fairkripke.hh
+++ b/src/kripke/fairkripke.hh
@@ -28,8 +28,8 @@ namespace spot
{
class fair_kripke;
- /// \brief Iterator code for a Fair Kripke structure.
/// \ingroup kripke
+ /// \brief Iterator code for a Fair Kripke structure.
///
/// This iterator can be used to simplify the writing
/// of an iterator on a Fair Kripke structure (or lookalike).
@@ -62,8 +62,8 @@ namespace spot
bdd acc_cond_;
};
- /// \brief Interface for a Fair Kripke structure.
/// \ingroup kripke
+ /// \brief Interface for a Fair Kripke structure.
///
/// A Kripke structure is a graph in which each node (=state) is
/// labeled by a conjunction of atomic proposition, and a set of
diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh
index f5964a7b6..b9c08f752 100644
--- a/src/kripke/kripke.hh
+++ b/src/kripke/kripke.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief Iterator code for Kripke structure
/// \ingroup kripke
+ /// \brief Iterator code for Kripke structure
///
/// This iterator can be used to simplify the writing
/// of an iterator on a Kripke structure (or lookalike).
@@ -55,8 +55,8 @@ namespace spot
bdd cond_;
};
- /// \brief Interface for a Kripke structure
/// \ingroup kripke
+ /// \brief Interface for a Kripke structure
///
/// A Kripke structure is a graph in which each node (=state) is
/// labeled by a conjunction of atomic proposition.
diff --git a/src/kripke/kripkeprint.hh b/src/kripke/kripkeprint.hh
index 2d63d62d5..d232a4a77 100644
--- a/src/kripke/kripkeprint.hh
+++ b/src/kripke/kripkeprint.hh
@@ -26,6 +26,7 @@ namespace spot
class kripke;
+ /// \ingroup tgba_io
/// \brief Save the reachable part of Kripke structure in text format.
///
/// The states will be named with the value returned by the
@@ -34,9 +35,9 @@ namespace spot
/// function only for debugging. Use
/// kripke_save_reachable_renumbered() for large output.
///
- /// \ingroup tgba_io
std::ostream& kripke_save_reachable(std::ostream& os, const kripke* k);
+ /// \ingroup tgba_io
/// \brief Save the reachable part of Kripke structure in text format.
///
/// States will be renumbered with sequential number. This is much
@@ -44,7 +45,6 @@ namespace spot
/// state names. The drawback is that any information carried by
/// the state name is lost.
///
- /// \ingroup tgba_io
std::ostream& kripke_save_reachable_renumbered(std::ostream& os,
const kripke* k);
diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh
index a9362828c..f9be37f43 100644
--- a/src/ltlast/atomic_prop.hh
+++ b/src/ltlast/atomic_prop.hh
@@ -36,8 +36,8 @@ namespace spot
namespace ltl
{
- /// \brief Atomic propositions.
/// \ingroup ltl_ast
+ /// \brief Atomic propositions.
class atomic_prop : public ref_formula
{
public:
diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh
index addfb2451..203d743c7 100644
--- a/src/ltlast/automatop.hh
+++ b/src/ltlast/automatop.hh
@@ -32,8 +32,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Automaton operators.
/// \ingroup eltl_ast
+ /// \brief Automaton operators.
///
class automatop : public ref_formula
{
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index 11375291e..c53759383 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -37,8 +37,8 @@ namespace spot
namespace ltl
{
- /// \brief Binary operator.
/// \ingroup ltl_ast
+ /// \brief Binary operator.
class binop : public ref_formula
{
public:
diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh
index d645a719f..b4a1de7bf 100644
--- a/src/ltlast/bunop.hh
+++ b/src/ltlast/bunop.hh
@@ -31,8 +31,8 @@ namespace spot
namespace ltl
{
- /// \brief Bounded unary operator.
/// \ingroup ltl_ast
+ /// \brief Bounded unary operator.
class bunop : public ref_formula
{
public:
diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh
index 55386ba3c..2ebe83675 100644
--- a/src/ltlast/constant.hh
+++ b/src/ltlast/constant.hh
@@ -29,8 +29,8 @@ namespace spot
namespace ltl
{
- /// \brief A constant (True or False)
/// \ingroup ltl_ast
+ /// \brief A constant (True or False)
class constant : public formula
{
public:
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index 0949b6df0..d12b62583 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -62,9 +62,9 @@ namespace spot
/// \ingroup ltl_algorithm
- /// \brief An LTL formula.
/// \ingroup ltl_essential
/// \ingroup ltl_ast
+ /// \brief An LTL formula.
///
/// The only way you can work with a formula is to
/// build a spot::ltl::visitor or spot::ltl::const_visitor.
@@ -353,8 +353,8 @@ namespace spot
opkind kind_;
};
- /// \brief Strict Weak Ordering for const formula*.
/// \ingroup ltl_essentials
+ /// \brief Strict Weak Ordering for const formula*.
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type const formula*.
@@ -394,9 +394,9 @@ namespace spot
}
};
- /// \brief Hash Function for const formula*.
/// \ingroup ltl_essentials
/// \ingroup hash_funcs
+ /// \brief Hash Function for const formula*.
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type const formula*.
diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index b11fa6e5a..b2ddf779c 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -34,8 +34,8 @@ namespace spot
namespace ltl
{
- /// \brief Multi-operand operators.
/// \ingroup ltl_ast
+ /// \brief Multi-operand operators.
class multop : public ref_formula
{
public:
diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh
index eedc8a5f3..c7eed062c 100644
--- a/src/ltlast/refformula.hh
+++ b/src/ltlast/refformula.hh
@@ -32,8 +32,8 @@ namespace spot
namespace ltl
{
- /// \brief A reference-counted LTL formula.
/// \ingroup ltl_ast
+ /// \brief A reference-counted LTL formula.
class ref_formula : public formula
{
protected:
diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh
index 77b90a663..2eff2dbe3 100644
--- a/src/ltlast/unop.hh
+++ b/src/ltlast/unop.hh
@@ -34,8 +34,8 @@ namespace spot
namespace ltl
{
- /// \brief Unary operators.
/// \ingroup ltl_ast
+ /// \brief Unary operators.
class unop : public ref_formula
{
public:
diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh
index 5bbb40ecd..ed8bf1d53 100644
--- a/src/ltlast/visitor.hh
+++ b/src/ltlast/visitor.hh
@@ -30,8 +30,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Formula visitor
/// \ingroup ltl_essential
+ /// \brief Formula visitor
///
/// Implementing visitors is the prefered way
/// to traverse a formula, since it does not
diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh
index 2a73bf29f..45076e8fe 100644
--- a/src/ltlenv/declenv.hh
+++ b/src/ltlenv/declenv.hh
@@ -33,8 +33,8 @@ namespace spot
namespace ltl
{
- /// \brief A declarative environment.
/// \ingroup ltl_environment
+ /// \brief A declarative environment.
///
/// This environment recognizes all atomic propositions
/// that have been previously declared. It will reject other.
diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh
index 64ac68cbf..c73594a08 100644
--- a/src/ltlenv/defaultenv.hh
+++ b/src/ltlenv/defaultenv.hh
@@ -30,8 +30,8 @@ namespace spot
namespace ltl
{
- /// \brief A laxist environment.
/// \ingroup ltl_environment
+ /// \brief A laxist environment.
///
/// This environment recognizes all atomic propositions.
///
diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh
index 5a2d5c153..fb5b2fee3 100644
--- a/src/ltlenv/environment.hh
+++ b/src/ltlenv/environment.hh
@@ -29,8 +29,8 @@ namespace spot
{
namespace ltl
{
- /// \brief An environment that describes atomic propositions.
/// \ingroup ltl_essential
+ /// \brief An environment that describes atomic propositions.
class environment
{
public:
diff --git a/src/ltlparse/ltlfile.hh b/src/ltlparse/ltlfile.hh
index b0035d734..8e4572574 100644
--- a/src/ltlparse/ltlfile.hh
+++ b/src/ltlparse/ltlfile.hh
@@ -27,8 +27,8 @@ namespace spot
namespace ltl
{
- /// \brief Read LTL formulae from a file, one by one
/// \ingroup ltl_io
+ /// \brief Read LTL formulae from a file, one by one
class ltl_file
{
public:
diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh
index 8a65b5524..cab13d08a 100644
--- a/src/ltlvisit/clone.hh
+++ b/src/ltlvisit/clone.hh
@@ -30,8 +30,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Clone a formula.
/// \ingroup ltl_visitor
+ /// \brief Clone a formula.
///
/// This visitor is public, because it's convenient
/// to derive from it and override part of its methods.
@@ -60,13 +60,13 @@ namespace spot
};
#if __GNUC__
- /// \brief Clone a formula.
/// \ingroup ltl_essential
+ /// \brief Clone a formula.
/// \deprecated Use f->clone() instead.
const formula* clone(const formula* f) __attribute__ ((deprecated));
#else
- /// \brief Clone a formula.
/// \ingroup ltl_essential
+ /// \brief Clone a formula.
/// \deprecated Use f->clone() instead.
const formula* clone(const formula* f);
#endif
diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh
index 2d1015567..81218f612 100644
--- a/src/ltlvisit/destroy.hh
+++ b/src/ltlvisit/destroy.hh
@@ -29,13 +29,13 @@ namespace spot
namespace ltl
{
#if __GNUC__
- /// \brief Destroys a formula
/// \ingroup ltl_essential
+ /// \brief Destroys a formula
/// \deprecated Use f->destroy() instead.
void destroy(const formula *f) __attribute__ ((deprecated));
#else
- /// \brief Destroys a formula
/// \ingroup ltl_essential
+ /// \brief Destroys a formula
/// \deprecated Use f->destroy() instead.
void destroy(const formula *f);
#endif
diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh
index fde60f1bc..b88950d3c 100644
--- a/src/ltlvisit/dotty.hh
+++ b/src/ltlvisit/dotty.hh
@@ -27,8 +27,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Write a formula tree using dot's syntax.
/// \ingroup ltl_io
+ /// \brief Write a formula tree using dot's syntax.
/// \param os The stream where it should be output.
/// \param f The formula to translate.
///
diff --git a/src/ltlvisit/dump.hh b/src/ltlvisit/dump.hh
index c1c75c822..483d8ba47 100644
--- a/src/ltlvisit/dump.hh
+++ b/src/ltlvisit/dump.hh
@@ -27,8 +27,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Dump a formula tree.
/// \ingroup ltl_io
+ /// \brief Dump a formula tree.
/// \param os The stream where it should be output.
/// \param f The formula to dump.
///
diff --git a/src/ltlvisit/length.hh b/src/ltlvisit/length.hh
index 48a54238e..5ab222e35 100644
--- a/src/ltlvisit/length.hh
+++ b/src/ltlvisit/length.hh
@@ -28,8 +28,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Compute the length of a formula.
/// \ingroup ltl_misc
+ /// \brief Compute the length of a formula.
///
/// The length of a formula is the number of atomic propositions,
/// constants, and operators (logical and temporal) occurring in
@@ -42,8 +42,8 @@ namespace spot
/// to have length one.
int length(const formula* f);
- /// \brief Compute the length of a formula, squashing Boolean formulae
/// \ingroup ltl_misc
+ /// \brief Compute the length of a formula, squashing Boolean formulae
///
/// This is similar to spot::ltl::length(), except all Boolean
/// formulae are assumed to have length one.
diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh
index 3bff9949a..9f41bf476 100644
--- a/src/ltlvisit/lunabbrev.hh
+++ b/src/ltlvisit/lunabbrev.hh
@@ -29,9 +29,9 @@ namespace spot
{
namespace ltl
{
+ /// \ingroup ltl_visitor
/// \brief Clone and rewrite a formula to remove most of the
/// abbreviated logical operators.
- /// \ingroup ltl_visitor
///
/// This will rewrite binary operators such as binop::Implies,
/// binop::Equals, and binop::Xor, using only unop::Not, multop::Or,
@@ -54,9 +54,9 @@ namespace spot
virtual const formula* recurse(const formula* f);
};
+ /// \ingroup ltl_rewriting
/// \brief Clone and rewrite a formula to remove most of the abbreviated
/// logical operators.
- /// \ingroup ltl_rewriting
///
/// This will rewrite binary operators such as binop::Implies,
/// binop::Equals, and binop::Xor, using only unop::Not, multop::Or,
diff --git a/src/ltlvisit/mark.hh b/src/ltlvisit/mark.hh
index 75f45d0d9..c1521542b 100644
--- a/src/ltlvisit/mark.hh
+++ b/src/ltlvisit/mark.hh
@@ -30,8 +30,8 @@ namespace spot
class mark_tools
{
public:
- /// \brief Mark operators NegClosure and EConcat.
/// \ingroup ltl_rewriting
+ /// \brief Mark operators NegClosure and EConcat.
///
/// \param f The formula to rewrite.
const formula* mark_concat_ops(const formula* f);
diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh
index 879f5f8b5..b49801a41 100644
--- a/src/ltlvisit/nenoform.hh
+++ b/src/ltlvisit/nenoform.hh
@@ -29,8 +29,8 @@ namespace spot
{
namespace ltl
{
- /// \brief Build the negative normal form of \a f.
/// \ingroup ltl_rewriting
+ /// \brief Build the negative normal form of \a f.
///
/// All negations of the formula are pushed in front of the
/// atomic propositions.
diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh
index 80b719b72..c0141f8fb 100644
--- a/src/ltlvisit/postfix.hh
+++ b/src/ltlvisit/postfix.hh
@@ -29,9 +29,9 @@ namespace spot
{
namespace ltl
{
+ /// \ingroup ltl_visitor
/// \brief Apply an algorithm on each node of an AST,
/// during a postfix traversal.
- /// \ingroup ltl_visitor
///
/// Override one or more of the postifix_visitor::doit methods
/// with the algorithm to apply.
diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh
index c2bafb523..e19055922 100644
--- a/src/ltlvisit/randomltl.hh
+++ b/src/ltlvisit/randomltl.hh
@@ -31,8 +31,8 @@ namespace spot
namespace ltl
{
- /// \brief Base class for random formula generators
/// \ingroup ltl_io
+ /// \brief Base class for random formula generators
class random_formula
{
public:
@@ -98,8 +98,8 @@ namespace spot
};
- /// \brief Generate random LTL formulae.
/// \ingroup ltl_io
+ /// \brief Generate random LTL formulae.
///
/// This class recursively constructs LTL formulae of a given
/// size. The formulae will use the use atomic propositions from
@@ -151,8 +151,8 @@ namespace spot
random_ltl(int size, const atomic_prop_set* ap);
};
- /// \brief Generate random Boolean formulae.
/// \ingroup ltl_io
+ /// \brief Generate random Boolean formulae.
///
/// This class recursively constructs Boolean formulae of a given size.
/// The formulae will use the use atomic propositions from the
@@ -191,8 +191,8 @@ namespace spot
random_boolean(const atomic_prop_set* ap);
};
- /// \brief Generate random SERE.
/// \ingroup ltl_io
+ /// \brief Generate random SERE.
///
/// This class recursively constructs SERE of a given size.
/// The formulae will use the use atomic propositions from the
@@ -234,8 +234,8 @@ namespace spot
random_boolean rb;
};
- /// \brief Generate random PSL formulae.
/// \ingroup ltl_io
+ /// \brief Generate random PSL formulae.
///
/// This class recursively constructs PSL formulae of a given size.
/// The formulae will use the use atomic propositions from the
diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh
index b89eb76fa..7e9df7cf9 100644
--- a/src/ltlvisit/reduce.hh
+++ b/src/ltlvisit/reduce.hh
@@ -76,8 +76,8 @@ namespace spot
#endif
/// @}
- /// \brief Check whether a formula is a pure eventuality.
/// \ingroup ltl_misc
+ /// \brief Check whether a formula is a pure eventuality.
///
/// Pure eventuality formulae are defined in
/// \verbatim
@@ -105,8 +105,8 @@ namespace spot
bool is_eventual(const formula* f);
#endif
- /// \brief Check whether a formula is purely universal.
/// \ingroup ltl_misc
+ /// \brief Check whether a formula is purely universal.
///
/// Purely universal formulae are defined in
/// \verbatim
diff --git a/src/ltlvisit/relabel.hh b/src/ltlvisit/relabel.hh
index 25d46a246..d52df66a2 100644
--- a/src/ltlvisit/relabel.hh
+++ b/src/ltlvisit/relabel.hh
@@ -28,9 +28,9 @@ namespace spot
{
enum relabeling_style { Abc, Pnn };
+ /// \ingroup ltl_rewriting
/// \brief Relabel the atomic proposition in a formula.
///
- /// \ingroup ltl_rewriting
const formula* relabel(const formula* f, relabeling_style style);
}
}
diff --git a/src/ltlvisit/simpfg.hh b/src/ltlvisit/simpfg.hh
index ad8a64259..6d6f4bfc8 100644
--- a/src/ltlvisit/simpfg.hh
+++ b/src/ltlvisit/simpfg.hh
@@ -29,6 +29,7 @@ namespace spot
{
namespace ltl
{
+ /// \ingroup ltl_visitor
/// \brief Replace true U f and false R g by
/// F f and G g.
///
@@ -39,7 +40,6 @@ namespace spot
/// - false R a = G a
/// - a W false = G a
///
- /// \ingroup ltl_visitor
class simplify_f_g_visitor : public clone_visitor
{
typedef clone_visitor super;
@@ -53,6 +53,7 @@ namespace spot
virtual const formula* recurse(const formula* f);
};
+ /// \ingroup ltl_rewriting
/// \brief Replace true U f and false R g by
/// F f and G g.
///
@@ -63,7 +64,6 @@ namespace spot
/// - false R a = G a
/// - a W false = G a
///
- /// \ingroup ltl_rewriting
const formula* simplify_f_g(const formula* f);
}
}
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index bed0d0630..42827b670 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -73,8 +73,8 @@ namespace spot
// fwd declaration to hide technical details.
class ltl_simplifier_cache;
- /// \brief Rewrite or simplify \a f in various ways.
/// \ingroup ltl_rewriting
+ /// \brief Rewrite or simplify \a f in various ways.
class ltl_simplifier
{
public:
diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh
index ad296d51e..358df0970 100644
--- a/src/ltlvisit/tunabbrev.hh
+++ b/src/ltlvisit/tunabbrev.hh
@@ -30,9 +30,9 @@ namespace spot
{
namespace ltl
{
+ /// \ingroup ltl_visitor
/// \brief Clone and rewrite a formula to remove most of the
/// abbreviated LTL and logical operators.
- /// \ingroup ltl_visitor
///
/// The rewriting performed on logical operator is
/// the same as the one done by spot::ltl::unabbreviate_logic_visitor.
diff --git a/src/ltlvisit/wmunabbrev.hh b/src/ltlvisit/wmunabbrev.hh
index 160ed7076..710a75556 100644
--- a/src/ltlvisit/wmunabbrev.hh
+++ b/src/ltlvisit/wmunabbrev.hh
@@ -26,6 +26,7 @@ namespace spot
{
class formula;
+ /// \ingroup ltl_rewriting
/// \brief Rewrite a formula to remove the W and M operators.
///
/// This is necessary if you want to use the formula with a tool
@@ -34,7 +35,6 @@ namespace spot
/// a W b is replaced by b R (b | a),
/// and a M b is replaced by b U (b & a).
///
- /// \ingroup ltl_rewriting
const formula* unabbreviate_wm(const formula* f);
}
}
diff --git a/src/misc/bddalloc.hh b/src/misc/bddalloc.hh
index 6c74e8f6a..0ad255f61 100644
--- a/src/misc/bddalloc.hh
+++ b/src/misc/bddalloc.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief Manage ranges of variables.
/// \ingroup misc_tools
+ /// \brief Manage ranges of variables.
class bdd_allocator: private free_list
{
public:
diff --git a/src/misc/bddlt.hh b/src/misc/bddlt.hh
index e3d611acb..ed0057fb0 100644
--- a/src/misc/bddlt.hh
+++ b/src/misc/bddlt.hh
@@ -27,8 +27,8 @@
namespace spot
{
- /// \brief Comparison functor for BDDs.
/// \ingroup misc_tools
+ /// \brief Comparison functor for BDDs.
struct bdd_less_than :
public std::binary_function
{
@@ -39,8 +39,8 @@ namespace spot
}
};
- /// \brief Hash functor for BDDs.
/// \ingroup misc_tools
+ /// \brief Hash functor for BDDs.
struct bdd_hash :
public std::unary_function
{
diff --git a/src/misc/freelist.hh b/src/misc/freelist.hh
index eeadbd186..add213c77 100644
--- a/src/misc/freelist.hh
+++ b/src/misc/freelist.hh
@@ -30,8 +30,8 @@
namespace spot
{
- /// \brief Manage list of free integers.
/// \ingroup misc_tools
+ /// \brief Manage list of free integers.
class free_list
{
public:
diff --git a/src/misc/hash.hh b/src/misc/hash.hh
index 4d1d04273..53dc285d0 100644
--- a/src/misc/hash.hh
+++ b/src/misc/hash.hh
@@ -74,8 +74,8 @@
namespace spot
{
- /// \brief A hash function for pointers.
/// \ingroup hash_funcs
+ /// \brief A hash function for pointers.
template
struct ptr_hash :
public std::unary_function
@@ -87,8 +87,8 @@ namespace spot
}
};
- /// \brief A hash function for strings.
/// \ingroup hash_funcs
+ /// \brief A hash function for strings.
/// @{
#if defined(SPOT_HAVE_UNORDERED_MAP) || defined(SPOT_HAVE_TR1_UNORDERED_MAP)
typedef Sgi::hash string_hash;
@@ -107,8 +107,8 @@ namespace spot
/// @}
#endif
- /// \brief A hash function that returns identity
/// \ingroup hash_funcs
+ /// \brief A hash function that returns identity
template
struct identity_hash:
public std::unary_function
diff --git a/src/misc/ltstr.hh b/src/misc/ltstr.hh
index df4ec1961..d56e4b639 100644
--- a/src/misc/ltstr.hh
+++ b/src/misc/ltstr.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief Strict Weak Ordering for \c char*.
/// \ingroup misc_tools
+ /// \brief Strict Weak Ordering for \c char*.
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type const char*.
diff --git a/src/misc/minato.hh b/src/misc/minato.hh
index 2d034fc1b..28b1de148 100644
--- a/src/misc/minato.hh
+++ b/src/misc/minato.hh
@@ -27,9 +27,9 @@
namespace spot
{
+ /// \ingroup misc_tools
/// \brief Generate an irredundant sum-of-products (ISOP) form of a
/// BDD function.
- /// \ingroup misc_tools
///
/// This algorithm implements a derecursived version the Minato-Morreale
/// algorithm presented in the following paper.
diff --git a/src/misc/modgray.hh b/src/misc/modgray.hh
index e9f98f433..c9327c994 100644
--- a/src/misc/modgray.hh
+++ b/src/misc/modgray.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief Loopless modular mixed radix Gray code iteration.
/// \ingroup misc_tools
+ /// \brief Loopless modular mixed radix Gray code iteration.
///
/// This class is based on the loopless modular mixed radix gray
/// code algorithm described in exercise 77 of "The Art of Computer
diff --git a/src/misc/optionmap.hh b/src/misc/optionmap.hh
index b3f5c8507..884a6f3d3 100644
--- a/src/misc/optionmap.hh
+++ b/src/misc/optionmap.hh
@@ -26,8 +26,9 @@
namespace spot
{
- /// \brief Manage a map of options.
/// \ingroup misc_tools
+ /// \brief Manage a map of options.
+ ///
/// Each option is defined by a string and is associated to an integer value.
class option_map
{
diff --git a/src/misc/version.hh b/src/misc/version.hh
index ba7480479..4bdb97628 100644
--- a/src/misc/version.hh
+++ b/src/misc/version.hh
@@ -22,8 +22,8 @@
namespace spot
{
- /// \brief Return Spot's version.
/// \ingroup misc_tools
+ /// \brief Return Spot's version.
const char* version();
}
diff --git a/src/saba/explicitstateconjunction.hh b/src/saba/explicitstateconjunction.hh
index c1ca963f1..9c22b975c 100644
--- a/src/saba/explicitstateconjunction.hh
+++ b/src/saba/explicitstateconjunction.hh
@@ -25,8 +25,8 @@
namespace spot
{
- /// \brief Basic implementation of saba_state_conjunction.
/// \ingroup saba_essentials
+ /// \brief Basic implementation of saba_state_conjunction.
///
/// This class provides a basic implementation to
/// iterate over a conjunction of states of a saba.
diff --git a/src/saba/saba.hh b/src/saba/saba.hh
index a2c2b2fc3..87ded4016 100644
--- a/src/saba/saba.hh
+++ b/src/saba/saba.hh
@@ -36,8 +36,8 @@ namespace spot
/// \addtogroup saba_essentials Essential SABA types
/// \ingroup saba
- /// \brief A State-based Alternating (Generalized) Büchi Automaton.
/// \ingroup saba_essentials
+ /// \brief A State-based Alternating (Generalized) Büchi Automaton.
///
/// Browsing such automaton can be achieved using two functions:
/// \c get_init_state, and \c succ_iter. The former returns
diff --git a/src/saba/sabacomplementtgba.hh b/src/saba/sabacomplementtgba.hh
index 98af277e1..02f42a3e9 100644
--- a/src/saba/sabacomplementtgba.hh
+++ b/src/saba/sabacomplementtgba.hh
@@ -25,8 +25,8 @@
namespace spot
{
- /// \brief Complement a TGBA and produce a SABA.
/// \ingroup saba
+ /// \brief Complement a TGBA and produce a SABA.
///
/// The original TGBA is transformed into a States-based
/// Büchi Automaton.
diff --git a/src/saba/sabastate.hh b/src/saba/sabastate.hh
index a8ac2fee0..f169677f6 100644
--- a/src/saba/sabastate.hh
+++ b/src/saba/sabastate.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief Abstract class for saba states.
/// \ingroup saba_essentials
+ /// \brief Abstract class for saba states.
class saba_state
{
public:
@@ -78,8 +78,8 @@ namespace spot
}
};
- /// \brief Strict Weak Ordering for \c saba_state*.
/// \ingroup saba_essentials
+ /// \brief Strict Weak Ordering for \c saba_state*.
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c saba_state*.
@@ -101,8 +101,8 @@ namespace spot
}
};
- /// \brief An Equivalence Relation for \c saba_state*.
/// \ingroup saba_essentials
+ /// \brief An Equivalence Relation for \c saba_state*.
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c saba_state*.
@@ -125,9 +125,9 @@ namespace spot
}
};
- /// \brief Hash Function for \c saba_state*.
/// \ingroup saba_essentials
/// \ingroup hash_funcs
+ /// \brief Hash Function for \c saba_state*.
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type \c saba_state*.
@@ -155,9 +155,9 @@ namespace spot
typedef boost::shared_ptr shared_saba_state;
+ /// \ingroup saba_essentials
/// \brief Strict Weak Ordering for \c shared_saba_state
/// (shared_ptr).
- /// \ingroup saba_essentials
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c shared_saba_state.
@@ -182,9 +182,9 @@ namespace spot
}
};
+ /// \ingroup saba_essentials
/// \brief An Equivalence Relation for \c shared_saba_state
/// (shared_ptr).
- /// \ingroup saba_essentials
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c shared_saba_state.
@@ -210,10 +210,10 @@ namespace spot
}
};
- /// \brief Hash Function for \c shared_saba_state
- /// (shared_ptr).
/// \ingroup saba_essentials
/// \ingroup hash_funcs
+ /// \brief Hash Function for \c shared_saba_state
+ /// (shared_ptr).
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type
diff --git a/src/saba/sabasucciter.hh b/src/saba/sabasucciter.hh
index 9949a5447..46e4a8d30 100644
--- a/src/saba/sabasucciter.hh
+++ b/src/saba/sabasucciter.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief Iterate over a conjunction of saba_state.
/// \ingroup saba_essentials
+ /// \brief Iterate over a conjunction of saba_state.
///
/// This class provides the basic functionalities required to
/// iterate over a conjunction of states of a saba.
@@ -87,8 +87,8 @@ namespace spot
};
- /// \brief Iterate over the successors of a saba_state.
/// \ingroup saba_essentials
+ /// \brief Iterate over the successors of a saba_state.
///
/// This class provides the basic functionalities required to
/// iterate over the successors of a state of a saba. Since
diff --git a/src/sabaalgos/sabadotty.hh b/src/sabaalgos/sabadotty.hh
index 54e82afbe..402fcf687 100644
--- a/src/sabaalgos/sabadotty.hh
+++ b/src/sabaalgos/sabadotty.hh
@@ -25,8 +25,8 @@ namespace spot
{
class saba;
- /// \brief Print reachable states in dot format.
/// \ingroup saba_io
+ /// \brief Print reachable states in dot format.
std::ostream&
saba_dotty_reachable(std::ostream& os,
const saba* g);
diff --git a/src/sabaalgos/sabareachiter.hh b/src/sabaalgos/sabareachiter.hh
index 1ae3e51b3..d183f1446 100644
--- a/src/sabaalgos/sabareachiter.hh
+++ b/src/sabaalgos/sabareachiter.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief Iterate over all reachable states of a spot::saba.
/// \ingroup saba_generic
+ /// \brief Iterate over all reachable states of a spot::saba.
class saba_reachable_iterator
{
public:
@@ -112,9 +112,9 @@ namespace spot
seen_map seen; ///< States already seen.
};
+ /// \ingroup saba_generic
/// \brief An implementation of spot::saba_reachable_iterator that browses
/// states depth first.
- /// \ingroup saba_generic
class saba_reachable_iterator_depth_first : public saba_reachable_iterator
{
public:
@@ -127,9 +127,9 @@ namespace spot
std::stack todo; ///< A stack of states yet to explore.
};
+ /// \ingroup saba_generic
/// \brief An implementation of spot::saba_reachable_iterator that browses
/// states breadth first.
- /// \ingroup saba_generic
class saba_reachable_iterator_breadth_first : public saba_reachable_iterator
{
public:
diff --git a/src/sanity/style.test b/src/sanity/style.test
index 12e4f776b..86553b35a 100755
--- a/src/sanity/style.test
+++ b/src/sanity/style.test
@@ -63,6 +63,18 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep Copyright $file >/dev/null ||
diag "missing copyright"
+ # A doxygen comments such as
+ #
+ # | \brief foo
+ # | \ingroup bar
+ # |
+ # | baz
+ #
+ # will be output as "foobaz." But if the first two lines
+ # are reversed, it's output correctly.
+ perl -ne '/(.*\\brief.*\n.*\\ingroup.*)/ && print("$1\n") && exit(1)' \
+ -0777 $file || diag "always put 'ingroup' before 'brief'"
+
# Strip comments and strings.
sed 's,[ ]*//.*,,;s,"[^"]*","",g' < $file > $tmp
diff --git a/src/ta/ta.hh b/src/ta/ta.hh
index 945ac4aaa..3a1066baa 100644
--- a/src/ta/ta.hh
+++ b/src/ta/ta.hh
@@ -44,8 +44,8 @@ namespace spot
/// \addtogroup ta_essentials Essential TA types
/// \ingroup ta
- /// \brief A Testing Automaton.
/// \ingroup ta_essentials
+ /// \brief A Testing Automaton.
///
/// The Testing Automata (TA) were introduced by
/// Henri Hansen, Wojciech Penczek and Antti Valmari
@@ -174,8 +174,8 @@ namespace spot
};
- /// \brief Iterate over the successors of a state.
/// \ingroup ta_essentials
+ /// \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
diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh
index ce26fb25c..b1352a84b 100644
--- a/src/ta/taproduct.hh
+++ b/src/ta/taproduct.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief A state for spot::ta_product.
/// \ingroup ta_emptiness_check
+ /// \brief A state for spot::ta_product.
///
/// This state is in fact a pair of state: the state from the TA
/// automaton and that of Kripke structure.
@@ -132,9 +132,9 @@ namespace spot
};
+ /// \ingroup ta_emptiness_check
/// \brief A lazy product between a Testing automaton and a Kripke structure.
/// (States are computed on the fly.)
- /// \ingroup ta_emptiness_check
class ta_product : public ta
{
public:
diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh
index 24f612ece..314cc1664 100644
--- a/src/ta/tgta.hh
+++ b/src/ta/tgta.hh
@@ -24,8 +24,8 @@
namespace spot
{
- /// \brief A Transition-based Generalized Testing Automaton (TGTA).
/// \ingroup ta_essentials
+ /// \brief A Transition-based Generalized Testing Automaton (TGTA).
///
/// Transition-based Generalized Testing Automaton (TGTA) is a new kind of
/// automaton that combines features from both TA and TGBA.
diff --git a/src/taalgos/reachiter.hh b/src/taalgos/reachiter.hh
index 4e266b2b8..e8d77b486 100644
--- a/src/taalgos/reachiter.hh
+++ b/src/taalgos/reachiter.hh
@@ -27,8 +27,8 @@
namespace spot
{
- /// \brief Iterate over all reachable states of a spot::ta.
/// \ingroup ta_generic
+ /// \brief Iterate over all reachable states of a spot::ta.
class ta_reachable_iterator
{
public:
@@ -94,9 +94,9 @@ namespace spot
seen_map seen; ///< States already seen.
};
+ /// \ingroup ta_generic
/// \brief An implementation of spot::ta_reachable_iterator that browses
/// states depth first.
- /// \ingroup ta_generic
class ta_reachable_iterator_depth_first : public ta_reachable_iterator
{
public:
@@ -111,9 +111,9 @@ namespace spot
std::stack todo; ///< A stack of states yet to explore.
};
+ /// \ingroup ta_generic
/// \brief An implementation of spot::ta_reachable_iterator that browses
/// states breadth first.
- /// \ingroup ta_generic
class ta_reachable_iterator_breadth_first : public ta_reachable_iterator
{
public:
diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh
index b32739a24..b1cd6d72e 100644
--- a/src/taalgos/tgba2ta.hh
+++ b/src/taalgos/tgba2ta.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief Build a spot::ta_explicit* (TA) from an LTL formula.
/// \ingroup tgba_ta
+ /// \brief Build a spot::ta_explicit* (TA) from an LTL formula.
///
/// This is based on the following paper.
/// \verbatim
@@ -85,10 +85,10 @@ namespace spot
bool single_pass_emptiness_check = false,
bool artificial_livelock_state_mode = false);
- /// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula.
/// \ingroup tgba_ta
- /// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton
+ /// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula.
///
+ /// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton
/// \param atomic_propositions_set The set of atomic propositions used in the
/// input TGBA \a tgba_to_convert
///
diff --git a/src/tgba/futurecondcol.hh b/src/tgba/futurecondcol.hh
index 7cae12fde..c66a12aba 100644
--- a/src/tgba/futurecondcol.hh
+++ b/src/tgba/futurecondcol.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief Wrap a tgba to offer information about upcoming conditions.
/// \ingroup tgba
+ /// \brief Wrap a tgba to offer information about upcoming conditions.
///
/// This class is a spot::tgba wrapper that simply add a new method,
/// future_conditions(), to any spot::tgba.
diff --git a/src/tgba/sba.hh b/src/tgba/sba.hh
index e755a06a4..b2166c41c 100644
--- a/src/tgba/sba.hh
+++ b/src/tgba/sba.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief A State-based Generalized Büchi Automaton.
/// \ingroup tgba_essentials
+ /// \brief A State-based Generalized Büchi Automaton.
///
/// An SBA is a TGBA in which the outgoing transitions of
/// a state are either all accepting (in which case the
diff --git a/src/tgba/state.hh b/src/tgba/state.hh
index 528894dd9..ca363be02 100644
--- a/src/tgba/state.hh
+++ b/src/tgba/state.hh
@@ -33,8 +33,8 @@
namespace spot
{
- /// \brief Abstract class for states.
/// \ingroup tgba_essentials
+ /// \brief Abstract class for states.
class state
{
public:
@@ -98,8 +98,8 @@ namespace spot
}
};
- /// \brief Strict Weak Ordering for \c state*.
/// \ingroup tgba_essentials
+ /// \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*.
@@ -121,8 +121,8 @@ namespace spot
}
};
- /// \brief An Equivalence Relation for \c state*.
/// \ingroup tgba_essentials
+ /// \brief An Equivalence Relation for \c state*.
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c state*.
@@ -145,9 +145,9 @@ namespace spot
}
};
- /// \brief Hash Function for \c state*.
/// \ingroup tgba_essentials
/// \ingroup hash_funcs
+ /// \brief Hash Function for \c state*.
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type \c state*.
@@ -177,9 +177,9 @@ namespace spot
inline void shared_state_deleter(state* s) { s->destroy(); }
+ /// \ingroup tgba_essentials
/// \brief Strict Weak Ordering for \c shared_state
/// (shared_ptr).
- /// \ingroup tgba_essentials
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c shared_state.
@@ -203,9 +203,9 @@ namespace spot
}
};
+ /// \ingroup tgba_essentials
/// \brief An Equivalence Relation for \c shared_state
/// (shared_ptr).
- /// \ingroup tgba_essentials
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c shared_state.
@@ -231,9 +231,9 @@ namespace spot
}
};
- /// \brief Hash Function for \c shared_state (shared_ptr).
/// \ingroup tgba_essentials
/// \ingroup hash_funcs
+ /// \brief Hash Function for \c shared_state (shared_ptr).
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type
diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh
index 5a640a0b2..2721975d6 100644
--- a/src/tgba/succiter.hh
+++ b/src/tgba/succiter.hh
@@ -26,8 +26,8 @@
namespace spot
{
- /// \brief Iterate over the successors of a state.
/// \ingroup tgba_essentials
+ /// \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
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index ee1f0799c..ec5cc46d1 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -41,8 +41,8 @@ namespace spot
/// \addtogroup tgba_essentials Essential TGBA types
/// \ingroup tgba
- /// \brief A Transition-based Generalized Büchi Automaton.
/// \ingroup tgba_essentials
+ /// \brief A Transition-based Generalized Büchi Automaton.
///
/// The acronym TGBA (Transition-based Generalized Büchi Automaton)
/// was coined by Dimitra Giannakopoulou and Flavio Lerda
diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh
index 5de0edb21..0962f12df 100644
--- a/src/tgba/tgbabddconcrete.hh
+++ b/src/tgba/tgbabddconcrete.hh
@@ -29,8 +29,8 @@
namespace spot
{
- /// \brief A concrete spot::tgba implemented using BDDs.
/// \ingroup tgba_representation
+ /// \brief A concrete spot::tgba implemented using BDDs.
class tgba_bdd_concrete: public tgba
{
public:
diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh
index b4041e0d4..f6ae5687d 100644
--- a/src/tgba/tgbabddconcreteproduct.hh
+++ b/src/tgba/tgbabddconcreteproduct.hh
@@ -24,8 +24,8 @@
namespace spot
{
- /// \brief Multiplies two spot::tgba_bdd_concrete automata.
/// \ingroup tgba_algorithms
+ /// \brief Multiplies two spot::tgba_bdd_concrete automata.
///
/// This function builds the resulting product as another
/// spot::tgba_bdd_concrete automaton.
diff --git a/src/tgba/tgbakvcomplement.hh b/src/tgba/tgbakvcomplement.hh
index 5cc38614c..07312156e 100644
--- a/src/tgba/tgbakvcomplement.hh
+++ b/src/tgba/tgbakvcomplement.hh
@@ -60,8 +60,8 @@ namespace spot
typedef std::vector acc_list_t;
- /// \brief Build a complemented automaton.
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief Build a complemented automaton.
///
/// The construction comes from:
/// \verbatim
diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh
index 284e9d65a..736f75fe7 100644
--- a/src/tgba/tgbaproduct.hh
+++ b/src/tgba/tgbaproduct.hh
@@ -28,8 +28,8 @@
namespace spot
{
- /// \brief A state for spot::tgba_product.
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief A state for spot::tgba_product.
///
/// This state is in fact a pair of state: the state from the left
/// automaton and that of the right.
diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh
index 299fc3d93..54c083c98 100644
--- a/src/tgba/tgbasafracomplement.hh
+++ b/src/tgba/tgbasafracomplement.hh
@@ -29,8 +29,8 @@
namespace spot
{
- /// \brief Build a complemented automaton.
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief Build a complemented automaton.
///
/// It creates an automaton that recognizes the
/// negated language of \a aut.
diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh
index 2c51a31b8..7c4ffaa07 100644
--- a/src/tgba/tgbascc.hh
+++ b/src/tgba/tgbascc.hh
@@ -24,9 +24,9 @@
namespace spot
{
+ /// \ingroup tgba
/// \brief Wrap a tgba to offer information about strongly connected
/// components.
- /// \ingroup tgba
///
/// This class is a spot::tgba wrapper that simply add a new method
/// scc_of_state() to retrieve the number of a SCC a state belongs to.
diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh
index 292fedbc1..92a2a804c 100644
--- a/src/tgba/tgbasgba.hh
+++ b/src/tgba/tgbasgba.hh
@@ -25,9 +25,9 @@
namespace spot
{
+ /// \ingroup tgba_on_the_fly_algorithms
/// \brief Change the labeling-mode of spot::tgba on the fly, producing a
/// state-based generalized Büchi automaton.
- /// \ingroup tgba_on_the_fly_algorithms
///
/// This class acts as a proxy in front of a spot::tgba, that should
/// label on states on-the-fly. The result is still a spot::tgba,
diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh
index b2794fdfb..2ad68757c 100644
--- a/src/tgba/tgbatba.hh
+++ b/src/tgba/tgbatba.hh
@@ -31,8 +31,8 @@
namespace spot
{
- /// \brief Degeneralize a spot::tgba on the fly, producing a TBA.
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief Degeneralize a spot::tgba on the fly, producing a TBA.
///
/// This class acts as a proxy in front of a spot::tgba, that should
/// be degeneralized on the fly. The result is still a spot::tgba,
@@ -124,8 +124,8 @@ namespace spot
tgba_tba_proxy& operator=(const tgba_tba_proxy&);
};
- /// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
///
/// This class acts as a proxy in front of a spot::tgba, that should
/// be degeneralized on the fly.
diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh
index ac2b3c3df..63229bb22 100644
--- a/src/tgba/tgbaunion.hh
+++ b/src/tgba/tgbaunion.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief A state for spot::tgba_union.
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief A state for spot::tgba_union.
///
/// This state is in fact a pair.
/// If the first member equals 0 and the second is different from 0,
diff --git a/src/tgba/wdbacomp.hh b/src/tgba/wdbacomp.hh
index f227bebff..0006b4987 100644
--- a/src/tgba/wdbacomp.hh
+++ b/src/tgba/wdbacomp.hh
@@ -23,8 +23,8 @@
namespace spot
{
- /// \brief Complement a weak deterministic Büchi automaton
/// \ingroup tgba_on_the_fly_algorithms
+ /// \brief Complement a weak deterministic Büchi automaton
/// \param aut a weak deterministic Büchi automaton to complement
/// \return a new automaton that recognizes the complement language
tgba* wdba_complement(const tgba* aut);
diff --git a/src/tgbaalgos/bfssteps.hh b/src/tgbaalgos/bfssteps.hh
index 375be74d1..7dde4dfa0 100644
--- a/src/tgbaalgos/bfssteps.hh
+++ b/src/tgbaalgos/bfssteps.hh
@@ -28,8 +28,8 @@
namespace spot
{
- /// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps.
/// \ingroup tgba_misc
+ /// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps.
///
/// This class should be used to compute the shortest path
/// between a state of a spot::tgba and the first transition or
diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh
index fba5f7168..4ea3086ba 100644
--- a/src/tgbaalgos/degen.hh
+++ b/src/tgbaalgos/degen.hh
@@ -24,6 +24,7 @@ namespace spot
class sba;
class tgba;
+ /// \ingroup tgba_misc
/// \brief Degeneralize a spot::tgba into an equivalent sba with
/// only one acceptance condition.
///
@@ -46,7 +47,6 @@ namespace spot
/// \a a to be computed prior to its actual degeneralization.
///
/// \see tgba_sba_proxy, tgba_tba_proxy
- /// \ingroup tgba_misc
sba* degeneralize(const tgba* a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
bool use_lvl_cache = true);
diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh
index 6b14d2c8c..685910491 100644
--- a/src/tgbaalgos/dotty.hh
+++ b/src/tgbaalgos/dotty.hh
@@ -30,8 +30,8 @@ namespace spot
class tgba;
class dotty_decorator;
- /// \brief Print reachable states in dot format.
/// \ingroup tgba_io
+ /// \brief Print reachable states in dot format.
///
/// If \a assume_sba is set, this assumes that the automaton
/// is an SBA and use double elipse to mark accepting states.
diff --git a/src/tgbaalgos/dottydec.hh b/src/tgbaalgos/dottydec.hh
index 78688bb13..e2f8b51c2 100644
--- a/src/tgbaalgos/dottydec.hh
+++ b/src/tgbaalgos/dottydec.hh
@@ -31,8 +31,8 @@ namespace spot
/// \addtogroup tgba_dotty Decorating the dot output
/// \ingroup tgba_io
- /// \brief Choose state and link styles for spot::dotty_reachable.
/// \ingroup tgba_dotty
+ /// \brief Choose state and link styles for spot::dotty_reachable.
class dotty_decorator
{
public:
diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh
index 1b15ba033..3d9aff070 100644
--- a/src/tgbaalgos/dupexp.hh
+++ b/src/tgbaalgos/dupexp.hh
@@ -27,25 +27,25 @@
namespace spot
{
+ /// \ingroup tgba_misc
/// \brief Build an explicit automata from all states of \a aut,
/// numbering states in bread first order as they are processed.
- /// \ingroup tgba_misc
tgba_explicit_number* tgba_dupexp_bfs(const tgba* aut);
+ /// \ingroup tgba_misc
/// \brief Build an explicit automata from all states of \a aut,
/// numbering states in depth first order as they are processed.
- /// \ingroup tgba_misc
tgba_explicit_number* tgba_dupexp_dfs(const tgba* aut);
+ /// \ingroup tgba_misc
/// \brief Build an explicit automata from all states of \a aut,
/// numbering states in bread first order as they are processed.
- /// \ingroup tgba_misc
tgba_explicit_number*
tgba_dupexp_bfs(const tgba* aut,
std::map& relation);
+ /// \ingroup tgba_misc
/// \brief Build an explicit automata from all states of \a aut,
/// numbering states in depth first order as they are processed.
- /// \ingroup tgba_misc
tgba_explicit_number*
tgba_dupexp_dfs(const tgba* aut,
std::map0). All states
/// will be connected, and there will be no dead state.
diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh
index 2977c63e9..8ef744501 100644
--- a/src/tgbaalgos/reachiter.hh
+++ b/src/tgbaalgos/reachiter.hh
@@ -29,8 +29,8 @@
namespace spot
{
- /// \brief Iterate over all reachable states of a spot::tgba.
/// \ingroup tgba_generic
+ /// \brief Iterate over all reachable states of a spot::tgba.
class tgba_reachable_iterator
{
public:
@@ -95,9 +95,9 @@ namespace spot
seen_map seen; ///< States already seen.
};
+ /// \ingroup tgba_generic
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// states depth first.
- /// \ingroup tgba_generic
class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator
{
public:
@@ -110,9 +110,9 @@ namespace spot
std::stack todo; ///< A stack of states yet to explore.
};
+ /// \ingroup tgba_generic
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// states breadth first.
- /// \ingroup tgba_generic
class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator
{
public:
diff --git a/src/tgbaalgos/reducerun.hh b/src/tgbaalgos/reducerun.hh
index 2f70fd5c3..9539c8ad8 100644
--- a/src/tgbaalgos/reducerun.hh
+++ b/src/tgbaalgos/reducerun.hh
@@ -27,8 +27,8 @@ namespace spot
class tgba;
struct tgba_run;
- /// \brief Reduce an accepting run.
/// \ingroup tgba_run
+ /// \brief Reduce an accepting run.
///
/// Return a run which is accepting for \a and that is no longer
/// that \a org.
diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh
index 0d19c48c2..e352af4cb 100644
--- a/src/tgbaalgos/replayrun.hh
+++ b/src/tgbaalgos/replayrun.hh
@@ -27,8 +27,8 @@ namespace spot
struct tgba_run;
class tgba;
- /// \brief Replay a tgba_run on a tgba.
/// \ingroup tgba_run
+ /// \brief Replay a tgba_run on a tgba.
///
/// This is similar to print_tgba_run(), except that the run is
/// actually replayed on the automaton while it is printed. Doing
diff --git a/src/tgbaalgos/rundotdec.hh b/src/tgbaalgos/rundotdec.hh
index c6b2770c5..539a91ce8 100644
--- a/src/tgbaalgos/rundotdec.hh
+++ b/src/tgbaalgos/rundotdec.hh
@@ -30,8 +30,8 @@
namespace spot
{
- /// \brief Highlight a spot::tgba_run on a spot::tgba.
/// \ingroup tgba_dotty
+ /// \brief Highlight a spot::tgba_run on a spot::tgba.
///
/// An instance of this class can be passed to spot::dotty_reachable.
class tgba_run_dotty_decorator: public dotty_decorator
diff --git a/src/tgbaalgos/save.hh b/src/tgbaalgos/save.hh
index cc37022af..c61b854ce 100644
--- a/src/tgbaalgos/save.hh
+++ b/src/tgbaalgos/save.hh
@@ -25,8 +25,8 @@
namespace spot
{
- /// \brief Save reachable states in text format.
/// \ingroup tgba_io
+ /// \brief Save reachable states in text format.
std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g);
}
diff --git a/src/tgbaalgos/stripacc.hh b/src/tgbaalgos/stripacc.hh
index 93eccbd55..0557e944c 100644
--- a/src/tgbaalgos/stripacc.hh
+++ b/src/tgbaalgos/stripacc.hh
@@ -24,10 +24,10 @@
namespace spot
{
+ /// \ingroup tgba_misc
/// \brief Duplicate automaton \a a, removing all acceptance sets.
///
/// This is equivalent to marking all states/transitions as accepting.
- /// \ingroup tgba_misc
sba_explicit_number* strip_acceptance(const tgba* a);
}
diff --git a/src/tgbaalgos/translate.hh b/src/tgbaalgos/translate.hh
index b06fc96ec..32dc554d4 100644
--- a/src/tgbaalgos/translate.hh
+++ b/src/tgbaalgos/translate.hh
@@ -25,8 +25,8 @@
namespace spot
{
- /// \brief Translate an LTL formula into an optimized spot::tgba.
/// \ingroup tgba_ltl
+ /// \brief Translate an LTL formula into an optimized spot::tgba.
///
/// This class implements a three-step translation:
/// - syntactic simplification of the formula