From 36aadba74027a0c2cd17a5caba634ae272ac825e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Nov 2004 16:23:40 +0000 Subject: [PATCH] * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/public.hh, src/ltlvisit/apcollect.hh, src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen groups for LTL algorithms and types. * doc/Makefile.am (fast-doc): New target. --- ChangeLog | 14 ++++++++++++++ doc/Makefile.am | 7 ++++++- src/ltlast/atomic_prop.hh | 3 ++- src/ltlast/binop.hh | 3 ++- src/ltlast/constant.hh | 3 ++- src/ltlast/formula.hh | 31 +++++++++++++++++++++++++++++++ src/ltlast/multop.hh | 1 + src/ltlast/refformula.hh | 1 + src/ltlast/unop.hh | 3 ++- src/ltlast/visitor.hh | 1 + src/ltlenv/declenv.hh | 1 + src/ltlenv/defaultenv.hh | 3 ++- src/ltlenv/environment.hh | 6 +++--- src/ltlparse/public.hh | 5 +++++ src/ltlvisit/apcollect.hh | 5 +++++ src/ltlvisit/basicreduce.hh | 9 ++++++--- src/ltlvisit/clone.hh | 4 +++- src/ltlvisit/destroy.hh | 3 ++- src/ltlvisit/dotty.hh | 1 + src/ltlvisit/dump.hh | 1 + src/ltlvisit/length.hh | 1 + src/ltlvisit/lunabbrev.hh | 4 +++- src/ltlvisit/nenoform.hh | 3 ++- src/ltlvisit/postfix.hh | 3 ++- src/ltlvisit/reduce.hh | 6 ++++++ src/ltlvisit/simpfg.hh | 2 ++ src/ltlvisit/syntimpl.hh | 9 +++++++-- src/ltlvisit/tostring.hh | 5 +++++ src/ltlvisit/tunabbrev.hh | 3 ++- 29 files changed, 121 insertions(+), 20 deletions(-) diff --git a/ChangeLog b/ChangeLog index 0c6213808..78395aa98 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,19 @@ 2004-11-17 Alexandre Duret-Lutz + * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, + src/ltlast/constant.hh, src/ltlast/formula.hh, + src/ltlast/multop.hh, src/ltlast/refformula.hh, + src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh, + src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, + src/ltlparse/public.hh, src/ltlvisit/apcollect.hh, + src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh, + src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, + src/ltlvisit/dump.hh, src/ltlvisit/length.hh, + src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen + groups for LTL algorithms and types. + * doc/Makefile.am (fast-doc): New target. + + * src/misc/hashfunc.hh: Include cstddef to define size_t, and guard the file for multiple inclusions. diff --git a/doc/Makefile.am b/doc/Makefile.am index a8224ab36..71dc22661 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -21,7 +21,7 @@ DOXYGEN = doxygen -.PHONY: doc spot +.PHONY: doc fast-doc all-local: $(srcdir)/stamp @@ -29,6 +29,11 @@ doc: rm -f $(srcdir)/stamp $(MAKE) $(srcdir)/stamp +fast-doc: + $(MAKE) Doxyfile + $(DOXYGEN) + touch $(srcdir)/stamp + $(srcdir)/stamp: $(srcdir)/Doxyfile.in $(top_srcdir)/configure.ac $(MAKE) Doxyfile rm -rf spot.html spot.latex diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 5cc945353..984c37619 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -35,7 +35,8 @@ namespace spot namespace ltl { - /// Atomic propositions. + /// \brief Atomic propositions. + /// \ingroup ltl_ast class atomic_prop : public ref_formula { public: diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 0197a28d4..6bf9fec5d 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -35,7 +35,8 @@ namespace spot namespace ltl { - /// Binary operator. + /// \brief Binary operator. + /// \ingroup ltl_ast class binop : public ref_formula { public: diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 4eee4cd5c..46b15e698 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -31,7 +31,8 @@ namespace spot namespace ltl { - /// A constant (True or False) + /// \brief A constant (True or False) + /// \ingroup ltl_ast class constant : public formula { public: diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 40a6ef221..f043cc6b1 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -30,8 +30,39 @@ namespace spot { namespace ltl { + /// \defgroup ltl LTL formulae + /// + /// This module gathers types and definitions related to LTL formulae. + + /// \addtogroup ltl_essential Essential LTL types + /// \ingroup ltl + + /// \addtogroup ltl_ast LTL Abstract Syntax Tree + /// \ingroup ltl + + /// \addtogroup ltl_environment LTL environments + /// \ingroup ltl + /// LTL environment implementations. + + /// \addtogroup ltl_algorithm Algorithms for LTL formulae + /// \ingroup ltl + + /// \addtogroup ltl_io Input/Output of LTL formulae + /// \ingroup ltl_algorithm + + /// \addtogroup ltl_visitor Derivable visitors + /// \ingroup ltl_algorithm + + /// \addtogroup ltl_rewriting Rewriting LTL formulae + /// \ingroup ltl_algorithm + + /// \addtogroup ltl_misc Miscellaneous algorithms for LTL formulae + /// \ingroup ltl_algorithm + /// \brief An LTL formula. + /// \ingroup ltl_essential + /// \ingroup ltl_ast /// /// The only way you can work with a formula is to /// build a spot::ltl::visitor or spot::ltl::const_visitor. diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 60179fdf4..7157b503b 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -34,6 +34,7 @@ namespace spot { /// \brief Multi-operand operators. + /// \ingroup ltl_ast /// /// These operators are considered commutative and associative. class multop : public ref_formula diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh index e6b99baa6..f93a91549 100644 --- a/src/ltlast/refformula.hh +++ b/src/ltlast/refformula.hh @@ -32,6 +32,7 @@ namespace spot { /// \brief A reference-counted LTL formula. + /// \ingroup ltl_ast class ref_formula : public formula { protected: diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 27ad95c19..487ecf034 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -32,7 +32,8 @@ namespace spot namespace ltl { - /// Unary operator. + /// \brief Unary operators. + /// \ingroup ltl_ast class unop : public ref_formula { public: diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index 5d7e77eb2..0cbf6d45d 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -31,6 +31,7 @@ namespace spot namespace ltl { /// \brief Formula visitor that can modify the formula. + /// \ingroup ltl_essential /// /// Writing visitors is the prefered way /// to traverse a formula, since it doesn't diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh index 58971348a..27ff98e01 100644 --- a/src/ltlenv/declenv.hh +++ b/src/ltlenv/declenv.hh @@ -34,6 +34,7 @@ namespace spot { /// \brief A declarative environment. + /// \ingroup ltl_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 863d81f45..064c3cc2e 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -30,6 +30,7 @@ namespace spot { /// \brief A laxist environment. + /// \ingroup ltl_environment /// /// This environment recognizes all atomic propositions. /// diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index 77e52cae9..ba19cde51 100644 --- a/src/ltlenv/environment.hh +++ b/src/ltlenv/environment.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -29,8 +29,8 @@ namespace spot { namespace ltl { - - /// An environment that describes atomic propositions. + /// \brief An environment that describes atomic propositions. + /// \ingroup ltl_essential class environment { public: diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 5186bf0f1..33b37f7b5 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -34,6 +34,9 @@ namespace spot { namespace ltl { + /// \addtogroup ltl_io + /// @{ + /// \brief A parse diagnostic with its location. typedef std::pair parse_error; /// \brief A list of parser diagnostics, as filled by parse. @@ -69,6 +72,8 @@ namespace spot bool format_parse_errors(std::ostream& os, const std::string& ltl_string, parse_error_list& error_list); + + /// @} } } diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 8897cce07..0c2b037d3 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -29,6 +29,9 @@ namespace spot { namespace ltl { + /// \addtogroup ltl_misc + /// @{ + /// Set of atomic propositions. typedef std::set atomic_prop_set; @@ -42,6 +45,8 @@ namespace spot /// set containing all these atomic propositions if \c s is 0. atomic_prop_set* atomic_prop_collect(const formula* f, atomic_prop_set* s = 0); + + /// @} } } #endif diff --git a/src/ltlvisit/basicreduce.hh b/src/ltlvisit/basicreduce.hh index f7bd51f31..5f64dbda2 100644 --- a/src/ltlvisit/basicreduce.hh +++ b/src/ltlvisit/basicreduce.hh @@ -28,12 +28,15 @@ namespace spot { namespace ltl { - /// Basic rewritings. + /// \brief Basic rewritings. + /// \ingroup ltl_rewriting formula* basic_reduce(const formula* f); - /// Whether a formula starts with GF. + /// \brief Whether a formula starts with GF. + /// \ingroup ltl_misc bool is_GF(const formula* f); - /// Whether a formula starts with FG. + /// \brief Whether a formula starts with FG. + /// \ingroup ltl_misc bool is_FG(const formula* f); } } diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 81155c65c..604f8bf13 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -30,6 +30,7 @@ namespace spot namespace ltl { /// \brief Clone a formula. + /// \ingroup ltl_visitor /// /// This visitor is public, because it's convenient /// to derive from it and override part of its methods. @@ -56,6 +57,7 @@ namespace spot }; /// \brief Clone a formula. + /// \ingroup ltl_essential formula* clone(const formula* f); } } diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh index 2d4444f74..7b076fc01 100644 --- a/src/ltlvisit/destroy.hh +++ b/src/ltlvisit/destroy.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -29,6 +29,7 @@ namespace spot namespace ltl { /// \brief Destroys a formula + /// \ingroup ltl_essential void destroy(const formula *f); } } diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh index 693269d05..420a4f7f8 100644 --- a/src/ltlvisit/dotty.hh +++ b/src/ltlvisit/dotty.hh @@ -30,6 +30,7 @@ namespace spot namespace ltl { /// \brief Write a formula tree using dot's syntax. + /// \ingroup ltl_io /// \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 11b2aba8e..9420ad349 100644 --- a/src/ltlvisit/dump.hh +++ b/src/ltlvisit/dump.hh @@ -30,6 +30,7 @@ namespace spot namespace ltl { /// \brief Dump a formula tree. + /// \ingroup ltl_io /// \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 a1afd7a1b..7aacf9ebe 100644 --- a/src/ltlvisit/length.hh +++ b/src/ltlvisit/length.hh @@ -29,6 +29,7 @@ namespace spot namespace ltl { /// \brief Compute the length of a formula. + /// \ingroup ltl_misc /// /// The length of a formula is the number of atomic properties, /// constants, and operators (logical and temporal) occurring in diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 882fa6d81..3d192863f 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -30,6 +30,7 @@ namespace spot { /// \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,6 +55,7 @@ namespace spot /// \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/nenoform.hh b/src/ltlvisit/nenoform.hh index 9cbc215e0..3569c1359 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -30,6 +30,7 @@ namespace spot namespace ltl { /// \brief Build the negative normal form of \a f. + /// \ingroup ltl_rewriting /// /// 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 1a40d7d27..4d341f59b 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -31,6 +31,7 @@ namespace spot { /// \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/reduce.hh b/src/ltlvisit/reduce.hh index 365a10f22..f4e7eccc0 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -30,6 +30,9 @@ namespace spot namespace ltl { + /// \addtogroup ltl_rewriting + /// @{ + /// Options for spot::ltl::reduce. enum reduce_options { @@ -52,8 +55,10 @@ namespace spot /// which optimizations to apply. /// \return the reduced formula formula* reduce(const formula* f, int opt = Reduce_All); + /// @} /// \brief Check whether a formula is a pure eventuality. + /// \ingroup ltl_misc /// /// Pure eventuality formulae are defined in /// \verbatim @@ -76,6 +81,7 @@ namespace spot bool is_eventual(const formula* f); /// \brief Check whether a formula is purely universal. + /// \ingroup ltl_misc /// /// Purely universal formulae are defined in /// \verbatim diff --git a/src/ltlvisit/simpfg.hh b/src/ltlvisit/simpfg.hh index 8f01350cd..2cd7eadec 100644 --- a/src/ltlvisit/simpfg.hh +++ b/src/ltlvisit/simpfg.hh @@ -30,6 +30,7 @@ namespace spot { /// \brief Replace true U f and false R g by /// F f and G g. + /// \ingroup ltl_visitor class simplify_f_g_visitor : public clone_visitor { typedef clone_visitor super; @@ -45,6 +46,7 @@ namespace spot /// \brief Replace true U f and false R g by /// F f and G g. + /// \ingroup ltl_rewriting formula* simplify_f_g(const formula* f); } } diff --git a/src/ltlvisit/syntimpl.hh b/src/ltlvisit/syntimpl.hh index 8ce307900..12addefe2 100644 --- a/src/ltlvisit/syntimpl.hh +++ b/src/ltlvisit/syntimpl.hh @@ -28,6 +28,10 @@ namespace spot { namespace ltl { + + /// \brief Syntactic implication. + /// \ingroup ltl_misc + /// /// This comes from /// \verbatim /// @InProceedings{ somenzi.00.cav, @@ -42,14 +46,15 @@ namespace spot /// publisher = {Springer-Verlag} /// } /// \endverbatim - - /// \brief Syntactic implication. bool syntactic_implication(const formula* f1, const formula* f2); /// \brief Syntactic implication. + /// \ingroup ltl_misc /// /// If right==false, true if !f1 < f2, false otherwise. /// If right==true, true if f1 < !f2, false otherwise. + /// + /// \see syntactic_implication bool syntactic_implication_neg(const formula* f1, const formula* f2, bool right); } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 8f6ff8e89..8b03e05c7 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -29,6 +29,9 @@ namespace spot { namespace ltl { + /// \addtogroup ltl_io + /// @{ + /// \brief Output a formula as a (parsable) string. /// \param f The formula to translate. /// \param os The stream where it should be output. @@ -46,6 +49,8 @@ namespace spot /// \brief Convert a formula into a (parsable by Spin) string. /// \param f The formula to translate. std::string to_spin_string(const formula* f); + + /// @} } } diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh index e382b2037..875d8c478 100644 --- a/src/ltlvisit/tunabbrev.hh +++ b/src/ltlvisit/tunabbrev.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -31,6 +31,7 @@ namespace spot { /// \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.