Commit 36aadba7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* 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.
parent 8c6dff00
......@@ -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
......
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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,
......
// 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.
......
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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.
......
......@@ -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
......
......@@ -30,6 +30,7 @@ namespace spot
{
/// \brief Replace <code>true U f</code> and <code>false R g</code> by
/// <code>F f</code> and <code>G g</code>.
/// \ingroup ltl_visitor
class simplify_f_g_visitor : public clone_visitor
{
typedef clone_visitor super;
......@@ -45,6 +46,7 @@ namespace spot
/// \brief Replace <code>true U f</code> and <code>false R g</code> by
/// <code>F f</code> and <code>G g</code>.
/// \ingroup ltl_rewriting
formula* simplify_f_g(const formula* f);
}
}
......
......@@ -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);
}
......
......@@ -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);
/// @}
}
}
......
// 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.
......
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