Commit 49b76bcf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent f56e1e8a
<hr size="1">
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>.
<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>
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>
</html>
......@@ -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
......
......@@ -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
......
......@@ -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
/// <code>SPOT_PR_CHECK</code> 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).
///
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment