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

doxygen: improve formula documentation

* doc/Doxyfile.in: Adjust to hide SPOT_API.
* doc/mainpage.dox: Adjust like to parse_infix_psl().
* src/tl/formula.hh: Document most methods of formula,
and fix the definition of the comparisons operator.
* src/ltlparse/public.hh, src/tl/apcollect.hh, src/tl/declenv.hh,
src/tl/defaultenv.hh, src/tl/dot.hh, src/tl/environment.hh,
src/tl/length.hh, src/tl/mark.hh, src/tl/nenoform.hh, src/tl/print.hh,
src/tl/randomltl.hh, src/tl/relabel.hh, src/tl/simpfg.hh,
src/tl/simplify.hh, src/tl/unabbrev.hh: Adjust doxygen group.
parent ca95e4d1
......@@ -1970,7 +1970,7 @@ ENABLE_PREPROCESSING = YES
# The default value is: NO.
# This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
MACRO_EXPANSION = NO
MACRO_EXPANSION = YES
# If the EXPAND_ONLY_PREDEF and MACRO_EXPANSION tags are both set to YES then
# the macro expansion is limited to the macros specified with the PREDEFINED and
......@@ -2010,7 +2010,7 @@ INCLUDE_FILE_PATTERNS =
# recursively expanded use the := operator instead of the = operator.
# This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
PREDEFINED =
PREDEFINED = SPOT_API=
# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this
# tag can be used to specify a list of macro names that should be expanded. The
......
......@@ -20,7 +20,7 @@
/// \section pointers Handy starting points
///
/// \li spot::formula Base class for an LTL or PSL formula.
/// \li spot::parse_infix_psl Parsing a text string into a
/// \li spot::parse_infix_psl() Parsing a text string into a
/// spot::formula.
/// \li spot::twa Base class for Transition-based
/// ω-Automata.
......
......@@ -32,7 +32,7 @@
namespace spot
{
/// \addtogroup ltl_io
/// \addtogroup tl_io
/// @{
#ifndef SWIG
......
......@@ -29,7 +29,7 @@
namespace spot
{
/// \addtogroup ltl_misc
/// \addtogroup tl_misc
/// @{
/// Set of atomic propositions.
......
......@@ -29,7 +29,7 @@
namespace spot
{
/// \ingroup ltl_environment
/// \ingroup tl_environment
/// \brief A declarative environment.
///
/// This environment recognizes all atomic propositions
......
......@@ -27,7 +27,7 @@
namespace spot
{
/// \ingroup ltl_environment
/// \ingroup tl_environment
/// \brief A laxist environment.
///
/// This environment recognizes all atomic propositions.
......
......@@ -26,7 +26,7 @@
namespace spot
{
/// \ingroup ltl_io
/// \ingroup tl_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.
......
......@@ -27,7 +27,7 @@
namespace spot
{
/// \ingroup ltl_essential
/// \ingroup tl_environment
/// \brief An environment that describes atomic propositions.
class environment
{
......
......@@ -21,6 +21,25 @@
/// \brief LTL/PSL formula interface
#pragma once
/// \defgroup tl Temporal Logic
///
/// Spot supports the future-time fragment of LTL, and the linear-time
/// fragment of and PSL formulas. The former is included in the
/// latter. Both types of formulas are represented by instances of
/// the spot::formula class.
/// \addtogroup tl_essentials Essential Temporal Logic Types
/// \ingroup tl
/// \addtogroup tl_io Input and Output of Formulas
/// \ingroup tl
/// \addtogroup tl_rewriting Rewriting Algorithms for Formulas
/// \ingroup tl
/// \addtogroup tl_misc Miscellaneous Algorithms for Formulas
/// \ingroup tl
#include "misc/common.hh"
#include <memory>
#include <cstdint>
......@@ -37,24 +56,26 @@
namespace spot
{
/// \ingroup tl_essentials
/// \brief Operator types
enum class op: uint8_t
{
ff,
tt,
eword,
ap,
ff, ///< False
tt, ///< True
eword, ///< Empty word
ap, ///< Atomic proposition
// unary operators
Not,
X,
F,
G,
Closure,
NegClosure,
NegClosureMarked,
Not, ///< Negation
X, ///< Next
F, ///< Eventually
G, ///< Globally
Closure, ///< PSL Closure
NegClosure, ///< Negated PSL Closure
NegClosureMarked, ///< marked version of the Negated PSL Clusure
// binary operators
Xor,
Implies,
Equiv,
Xor, ///< Exclusive Or
Implies, ///< Implication
Equiv, ///< Equivalence
U, ///< until
R, ///< release (dual of until)
W, ///< weak until
......@@ -68,14 +89,20 @@ namespace spot
And, ///< (omega-Rational) And
AndRat, ///< Rational And
AndNLM, ///< Non-Length-Matching Rational-And
Concat,
Fusion,
Concat, ///< Concatenation
Fusion, ///< Fusion
// star-like operators
Star, ///< Star
FStar, ///< Fustion Star
};
#ifndef SWIG
/// \brief Actual storage for formula nodes.
///
/// spot::formula objects contain references to instances of this
/// class, and delegate most of their methods. Because
/// spot::formula is meant to be the public interface, most of the
/// methods are documented there, rather than here.
class SPOT_API fnode final
{
public:
......@@ -135,9 +162,6 @@ namespace spot
return true;
}
/// \brief Remove operator \a o and return the child.
///
/// This works only for unary operators.
const fnode* get_child_of(op o) const
{
if (op_ != o)
......@@ -146,12 +170,6 @@ namespace spot
return nth(0);
}
/// \brief Remove all operators in \a l and return the child.
///
/// This works only for a list of unary operators.
/// For instance if \c f is a formula for XG(a U b),
/// then <code>f.get_child_of({op::X, op::G})</code>
/// will return the subformula a U b.
const fnode* get_child_of(std::initializer_list<op> l) const
{
auto c = this;
......@@ -276,151 +294,91 @@ namespace spot
// Properties //
////////////////
/// Whether the formula use only boolean operators.
bool is_boolean() const
{
return is_.boolean;
}
/// Whether the formula use only AND, OR, and NOT operators.
bool is_sugar_free_boolean() const
{
return is_.sugar_free_boolean;
}
/// \brief Whether the formula is in negative normal form.
///
/// A formula is in negative normal form if the not operators
/// occur only in front of atomic propositions.
bool is_in_nenoform() const
{
return is_.in_nenoform;
}
/// Whether the formula is syntactically stutter_invariant
bool is_syntactic_stutter_invariant() const
{
return is_.syntactic_si;
}
/// Whether the formula avoids the F and G operators.
bool is_sugar_free_ltl() const
{
return is_.sugar_free_ltl;
}
/// Whether the formula uses only LTL operators.
bool is_ltl_formula() const
{
return is_.ltl_formula;
}
/// Whether the formula uses only PSL operators.
bool is_psl_formula() const
{
return is_.psl_formula;
}
/// Whether the formula uses only SERE operators.
bool is_sere_formula() const
{
return is_.sere_formula;
}
/// Whether a SERE describes a finite language, or an LTL
/// formula uses no temporal operator but X.
bool is_finite() const
{
return is_.finite;
}
/// \brief Whether the formula is purely eventual.
///
/// Pure eventuality formulae are defined in
/** \verbatim
@InProceedings{ etessami.00.concur,
author = {Kousha Etessami and Gerard J. Holzmann},
title = {Optimizing {B\"u}chi Automata},
booktitle = {Proceedings of the 11th International Conference on
Concurrency Theory (Concur'2000)},
pages = {153--167},
year = {2000},
editor = {C. Palamidessi},
volume = {1877},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
///
/// A word that satisfies a pure eventuality can be prefixed by
/// anything and still satisfies the formula.
bool is_eventual() const
{
return is_.eventual;
}
/// \brief Whether a formula is purely universal.
///
/// Purely universal formulae are defined in
/** \verbatim
@InProceedings{ etessami.00.concur,
author = {Kousha Etessami and Gerard J. Holzmann},
title = {Optimizing {B\"u}chi Automata},
booktitle = {Proceedings of the 11th International Conference on
Concurrency Theory (Concur'2000)},
pages = {153--167},
year = {2000},
editor = {C. Palamidessi},
volume = {1877},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
///
/// Any (non-empty) suffix of a word that satisfies a purely
/// universal formula also satisfies the formula.
bool is_universal() const
{
return is_.universal;
}
/// Whether a PSL/LTL formula is syntactic safety property.
bool is_syntactic_safety() const
{
return is_.syntactic_safety;
}
/// Whether a PSL/LTL formula is syntactic guarantee property.
bool is_syntactic_guarantee() const
{
return is_.syntactic_guarantee;
}
/// Whether a PSL/LTL formula is syntactic obligation property.
bool is_syntactic_obligation() const
{
return is_.syntactic_obligation;
}
/// Whether a PSL/LTL formula is syntactic recurrence property.
bool is_syntactic_recurrence() const
{
return is_.syntactic_recurrence;
}
/// Whether a PSL/LTL formula is syntactic persistence property.
bool is_syntactic_persistence() const
{
return is_.syntactic_persistence;
}
/// Whether the formula has an occurrence of EConcatMarked.
bool is_marked() const
{
return !is_.not_marked;
}
/// Whether the formula accepts [*0].
bool accepts_eword() const
{
return is_.accepting_eword;
......@@ -541,15 +499,6 @@ namespace spot
SPOT_API
int atomic_prop_cmp(const fnode* f, const fnode* g);
/// \brief Strict Weak Ordering for <code>const fnode*</code>
/// inside n-ary operators
/// \ingroup ltl_essentials
///
/// This is the comparison functor used by to order the
/// n-ary operands. It keeps Boolean formulae first in
/// order to speed up implication checks.
///
/// Also keep literal alphabetically ordered.
struct formula_ptr_less_than_bool_first
{
bool
......@@ -620,6 +569,8 @@ namespace spot
#endif // SWIG
/// \ingroup tl_essentials
/// \brief Main class for temporal logic formula
class SPOT_API formula final
{
const fnode* ptr_;
......@@ -685,34 +636,30 @@ namespace spot
return false;
if (SPOT_UNLIKELY(!ptr_))
return true;
return id() < other.id();
if (id() < other.id())
return true;
if (id() > other.id())
return false;
// The case where id()==other.id() but ptr_ != other.ptr_ is
// very unlikely (we would need to build more that UINT_MAX
// formulas), so let's just compare pointer, and ignore the fact
// that it may give some nondeterminism.
return ptr_ < other.ptr_;
}
bool operator<=(const formula& other) const noexcept
{
if (SPOT_UNLIKELY(!other.ptr_))
return !ptr_;
if (SPOT_UNLIKELY(!ptr_))
return true;
return id() <= other.id();
return *this == other || *this < other;
}
bool operator>(const formula& other) const noexcept
{
if (SPOT_UNLIKELY(!ptr_))
return false;
if (SPOT_UNLIKELY(!other.ptr_))
return true;
return id() > other.id();
return !(*this <= other);
}
bool operator>=(const formula& other) const noexcept
{
if (SPOT_UNLIKELY(!ptr_))
return !!other.ptr_;
if (SPOT_UNLIKELY(!other.ptr_))
return true;
return id() >= other.id();
return !(*this < other);
}
bool operator==(const formula& other) const noexcept
......@@ -744,16 +691,22 @@ namespace spot
// Forwarded functions //
/////////////////////////
/// Unbounded constant to use as end of range for bounded operators.
static constexpr uint8_t unbounded()
{
return fnode::unbounded();
}
/// Build an atomic proposition.
static formula ap(const std::string& name)
{
return formula(fnode::ap(name));
}
/// \brief Build a unary operator.
/// \pre \a o should be one of op::Not, op::X, op::F, op::G,
/// op::Closure, op::NegClosure, op::NegClosureMarked.
/// @{
static formula unop(op o, const formula& f)
{
return formula(fnode::unop(o, f.ptr_->clone()));
......@@ -765,6 +718,7 @@ namespace spot
return formula(fnode::unop(o, f.to_node_()));
}
#endif // !SWIG
/// @}
#ifdef SWIG
#define SPOT_DEF_UNOP(Name) \
......@@ -783,15 +737,46 @@ namespace spot
return unop(op::Name, std::move(f)); \
}
#endif // !SWIG
/// \brief Construct a negation
/// @{
SPOT_DEF_UNOP(Not);
/// @}
/// \brief Construct an X
/// @{
SPOT_DEF_UNOP(X);
/// @}
/// \brief Construct an F
/// @{
SPOT_DEF_UNOP(F);
/// @}
/// \brief Construct a G
/// @{
SPOT_DEF_UNOP(G);
/// @}
/// \brief Construct a PSL Closure
/// @{
SPOT_DEF_UNOP(Closure);
/// @}
/// \brief Construct a negated PSL Closure
/// @{
SPOT_DEF_UNOP(NegClosure);
/// @}
/// \brief Construct a marked negated PSL Closure
/// @{
SPOT_DEF_UNOP(NegClosureMarked);
/// @}
#undef SPOT_DEF_UNOP
/// \brief Construct a binary operator
/// \pre \a o should be one of op::Xor, op::Implies, op::Equiv,
/// op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked,
/// or op::UConcat.
static formula binop(op o, const formula& f, const formula& g)
{
return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
......@@ -839,18 +824,62 @@ namespace spot
return binop(op::Name, std::move(f), std::move(g)); \
}
#endif // !SWIG
/// \brief Construct an Xor formula
/// @{
SPOT_DEF_BINOP(Xor);
/// @}
/// \brief Construct an Implies formula
/// @{
SPOT_DEF_BINOP(Implies);
/// @}
/// \brief Construct an Equiv formula
/// @{
SPOT_DEF_BINOP(Equiv);
/// @}
/// \brief Construct an U formula
/// @{
SPOT_DEF_BINOP(U);
/// @}
/// \brief Construct an R formula
/// @{
SPOT_DEF_BINOP(R);
/// @}
/// \brief Construct an W formula
/// @{
SPOT_DEF_BINOP(W);
/// @}
/// \brief Construct an < formula
/// @{
SPOT_DEF_BINOP(M);
/// @}
/// \brief Construct an <>-> PSL formula
/// @{
SPOT_DEF_BINOP(EConcat);
/// @}
/// \brief Construct a marked <>-> PSL formula
/// @{
SPOT_DEF_BINOP(EConcatMarked);
/// @}
/// \brief Construct an []-> PSL formula
/// @{
SPOT_DEF_BINOP(UConcat);
/// @}
#undef SPOT_DEF_BINOP
/// \brief Construct an n-ary operator
///
/// \pre \a o should be one of op::Or, op::OrRat, op::And,
/// op::AndRat, op::AndNLM, op::Concat, op::Fusion.
/// @{
static formula multop(op o, const std::vector<formula>& l)
{
std::vector<const fnode*> tmp;
......@@ -872,6 +901,7 @@ namespace spot
return formula(fnode::multop(o, std::move(tmp)));
}
#endif // !SWIG
/// @}
#ifdef SWIG
#define SPOT_DEF_MULTOP(Name) \
......@@ -891,15 +921,46 @@ namespace spot
return multop(op::Name, std::move(l)); \
}
#endif // !SWIG
/// \brief Construct an Or formula.
/// @{
SPOT_DEF_MULTOP(Or);
/// @}
/// \brief Construct an Or SERE.
/// @{
SPOT_DEF_MULTOP(OrRat);
/// @}
/// \brief Construct an And formula.
/// @{
SPOT_DEF_MULTOP(And);
/// @}
/// \brief Construct an And SERE.
/// @{
SPOT_DEF_MULTOP(AndRat);
/// @}
/// \brief Construct a non-length-matching And SERE.
/// @{
SPOT_DEF_MULTOP(AndNLM);
/// @}
/// \brief Construct a Concatenation SERE.
/// @{
SPOT_DEF_MULTOP(Concat);
/// @}
/// \brief Construct a Fusion SERE.
/// @{
SPOT_DEF_MULTOP(Fusion);
/// @}
#undef SPOT_DEF_MULTOP
/// \brief Define a bounded unary-operator (i.e. star-like)
///
/// \pre \a o should be op::Star or op::FStar.
/// @{
static formula bunop(op o, const formula& f,
uint8_t min = 0U,
uint8_t max = unbounded())
......@@ -915,6 +976,7 @@ namespace spot
return formula(fnode::bunop(o, f.to_node_(), min, max));
}
#endif // !SWIG
///@}
#if SWIG
#define SPOT_DEF_BUNOP(Name) \
......@@ -939,15 +1001,59 @@ namespace spot
return bunop(op::Name, std::move(f), min, max); \
}
#endif
/// \brief Create SERE for f[*min..max]
/// @{
SPOT_DEF_BUNOP(Star);
/// @}
/// \brief Create SERE for f[:*min..max]
///
/// This operator is a generalization of the (+) operator
/// defined in the following paper.
/** \verbatim
@InProceedings{ dax.09.atva,
author = {Christian Dax and Felix Klaedtke and Stefan Leue},
title = {Specification Languages for Stutter-Invariant Regular
Properties},
booktitle = {Proceedings of the 7th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'09)},
pages = {244--254},
year = {2009},
volume = {5799},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
/// @{
SPOT_DEF_BUNOP(FStar);