From 49b76bcf66fe8eb8ffb4e8afabeb1edcea3d2745 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 8 Dec 2017 16:57:47 +0100 Subject: [PATCH] doxygen doc: minor improvements * doc/footer.html: Make the footer XML compatible. * doc/mainpage.dox: Fix references to modules. * spot/tl/formula.hh: Introduce a hierarchy module. * spot/tl/hierarchy.hh: Use it. --- doc/footer.html | 2 +- doc/mainpage.dox | 3 ++- spot/tl/formula.hh | 3 +++ spot/tl/hierarchy.hh | 10 +++++++++- 4 files changed, 15 insertions(+), 3 deletions(-) diff --git a/doc/footer.html b/doc/footer.html index 651057411..f9212b389 100644 --- a/doc/footer.html +++ b/doc/footer.html @@ -1,6 +1,6 @@
Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
-Generated on $datetime for $projectname by doxygen $doxygenversion
+Generated on $datetime for $projectname by doxygen $doxygenversion diff --git a/doc/mainpage.dox b/doc/mainpage.dox index 6c5930f1f..fefd68625 100644 --- a/doc/mainpage.dox +++ b/doc/mainpage.dox @@ -22,11 +22,12 @@ /// \li spot::formula Base class for an LTL or PSL formula. /// \li spot::parse_infix_psl() Parsing a text string into a /// spot::formula. +/// \li \ref tl /// \li spot::twa Base class for Transition-based /// ω-Automata. -/// \li spot::twa_algorithms Algorithms on ω-Automata. /// \li spot::translator Convert a spot::formula into a /// spot::twa. +/// \li \ref twa_algorithms /// \li spot::kripke Base class for Kripke structures. /// \li spot::twa_product On-the-fly product of two spot::twa. /// \li spot::emptiness_check Base class for all emptiness-check algorithms diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 59cdf4883..53b0a41d1 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -37,6 +37,9 @@ /// \addtogroup tl_rewriting Rewriting Algorithms for Formulas /// \ingroup tl +/// \addtogroup tl_hier Algorithms related to the temporal hierarchy +/// \ingroup tl + /// \addtogroup tl_misc Miscellaneous Algorithms for Formulas /// \ingroup tl diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index fbf024fd9..c567983ed 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -24,7 +24,9 @@ namespace spot { - /// Enum used to change the behavior of is_persistence() or is_recurrence(). + /// \ingroup tl_hier + /// \brief Enum used to change the behavior of is_persistence() or + /// is_recurrence(). /// /// If PR_Auto, both methods will first check the environment variable /// SPOT_PR_CHECK to see if one algorithm or the other is wanted @@ -47,6 +49,7 @@ namespace spot via_Rabin, }; + /// \ingroup tl_hier /// \brief Return true if \a f represents a persistence property. /// /// \param f the formula to check. @@ -57,6 +60,7 @@ namespace spot twa_graph_ptr aut = nullptr, prcheck algo = prcheck::Auto); + /// \ingroup tl_hier /// \brief Return true if \a f represents a recurrence property. /// /// Actually, it calls is_persistence() with the negation of \a f. @@ -78,6 +82,7 @@ namespace spot via_WDBA, }; + /// \ingroup tl_hier /// \brief Return true if \a f has the recurrence property. /// /// Actually, it calls is_persistence() with the negation of \a f. @@ -102,6 +107,7 @@ namespace spot twa_graph_ptr aut = nullptr, ocheck algo = ocheck::Auto); + /// \ingroup tl_hier /// \brief Return the class of \a f in the temporal hierarchy of Manna /// and Pnueli (PODC'90). /// @@ -118,6 +124,7 @@ namespace spot SPOT_API char mp_class(formula f); + /// \ingroup tl_hier /// \brief Return the class of \a f in the temporal hierarchy of Manna /// and Pnueli (PODC'90). /// @@ -132,6 +139,7 @@ namespace spot /// Any ']' ends the processing of the options. SPOT_API std::string mp_class(formula f, const char* opt); + /// \ingroup tl_hier /// \brief Expand a class in the temporal hierarchy of Manna /// and Pnueli (PODC'90). ///