Move \ingroup before \brief in all Doxygen comments.
Using \ingroup between \brief and the rest of the documentation causes Doxygen to concatenate the brief with the rest of the doc. * src/sanity/style.test: Warn when \ingroup is found on the line after \brief. * src/kripke/fairkripke.hh, src/kripke/kripke.hh, src/kripke/kripkeprint.hh, src/ltlast/atomic_prop.hh, src/ltlast/automatop.hh, src/ltlast/binop.hh, src/ltlast/bunop.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/ltlfile.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/mark.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh, src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.hh, src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh, src/misc/freelist.hh, src/misc/hash.hh, src/misc/ltstr.hh, src/misc/minato.hh, src/misc/modgray.hh, src/misc/optionmap.hh, src/misc/version.hh, src/saba/explicitstateconjunction.hh, src/saba/saba.hh, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh, src/saba/sabasucciter.hh, src/sabaalgos/sabadotty.hh, src/sabaalgos/sabareachiter.hh, src/ta/ta.hh, src/ta/taproduct.hh, src/ta/tgta.hh, src/taalgos/reachiter.hh, src/taalgos/tgba2ta.hh, src/tgba/futurecondcol.hh, src/tgba/sba.hh, src/tgba/state.hh, src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh, src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh, src/tgbaalgos/bfssteps.hh, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh, src/tgbaalgos/save.hh, src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh: Move \ingroup before \brief.
This commit is contained in:
parent
0ec3f7843a
commit
1ec9cebe58
91 changed files with 151 additions and 138 deletions
|
|
@ -28,8 +28,8 @@ namespace spot
|
|||
{
|
||||
class fair_kripke;
|
||||
|
||||
/// \brief Iterator code for a Fair Kripke structure.
|
||||
/// \ingroup kripke
|
||||
/// \brief Iterator code for a Fair Kripke structure.
|
||||
///
|
||||
/// This iterator can be used to simplify the writing
|
||||
/// of an iterator on a Fair Kripke structure (or lookalike).
|
||||
|
|
@ -62,8 +62,8 @@ namespace spot
|
|||
bdd acc_cond_;
|
||||
};
|
||||
|
||||
/// \brief Interface for a Fair Kripke structure.
|
||||
/// \ingroup kripke
|
||||
/// \brief Interface for a Fair Kripke structure.
|
||||
///
|
||||
/// A Kripke structure is a graph in which each node (=state) is
|
||||
/// labeled by a conjunction of atomic proposition, and a set of
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Iterator code for Kripke structure
|
||||
/// \ingroup kripke
|
||||
/// \brief Iterator code for Kripke structure
|
||||
///
|
||||
/// This iterator can be used to simplify the writing
|
||||
/// of an iterator on a Kripke structure (or lookalike).
|
||||
|
|
@ -55,8 +55,8 @@ namespace spot
|
|||
bdd cond_;
|
||||
};
|
||||
|
||||
/// \brief Interface for a Kripke structure
|
||||
/// \ingroup kripke
|
||||
/// \brief Interface for a Kripke structure
|
||||
///
|
||||
/// A Kripke structure is a graph in which each node (=state) is
|
||||
/// labeled by a conjunction of atomic proposition.
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ namespace spot
|
|||
|
||||
class kripke;
|
||||
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Save the reachable part of Kripke structure in text format.
|
||||
///
|
||||
/// The states will be named with the value returned by the
|
||||
|
|
@ -34,9 +35,9 @@ namespace spot
|
|||
/// function only for debugging. Use
|
||||
/// kripke_save_reachable_renumbered() for large output.
|
||||
///
|
||||
/// \ingroup tgba_io
|
||||
std::ostream& kripke_save_reachable(std::ostream& os, const kripke* k);
|
||||
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Save the reachable part of Kripke structure in text format.
|
||||
///
|
||||
/// States will be renumbered with sequential number. This is much
|
||||
|
|
@ -44,7 +45,6 @@ namespace spot
|
|||
/// state names. The drawback is that any information carried by
|
||||
/// the state name is lost.
|
||||
///
|
||||
/// \ingroup tgba_io
|
||||
std::ostream& kripke_save_reachable_renumbered(std::ostream& os,
|
||||
const kripke* k);
|
||||
|
||||
|
|
|
|||
|
|
@ -36,8 +36,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Atomic propositions.
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief Atomic propositions.
|
||||
class atomic_prop : public ref_formula
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -32,8 +32,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Automaton operators.
|
||||
/// \ingroup eltl_ast
|
||||
/// \brief Automaton operators.
|
||||
///
|
||||
class automatop : public ref_formula
|
||||
{
|
||||
|
|
|
|||
|
|
@ -37,8 +37,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Binary operator.
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief Binary operator.
|
||||
class binop : public ref_formula
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Bounded unary operator.
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief Bounded unary operator.
|
||||
class bunop : public ref_formula
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief A constant (True or False)
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief A constant (True or False)
|
||||
class constant : public formula
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -62,9 +62,9 @@ namespace spot
|
|||
/// \ingroup ltl_algorithm
|
||||
|
||||
|
||||
/// \brief An LTL formula.
|
||||
/// \ingroup ltl_essential
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief An LTL formula.
|
||||
///
|
||||
/// The only way you can work with a formula is to
|
||||
/// build a spot::ltl::visitor or spot::ltl::const_visitor.
|
||||
|
|
@ -353,8 +353,8 @@ namespace spot
|
|||
opkind kind_;
|
||||
};
|
||||
|
||||
/// \brief Strict Weak Ordering for <code>const formula*</code>.
|
||||
/// \ingroup ltl_essentials
|
||||
/// \brief Strict Weak Ordering for <code>const formula*</code>.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type <code>const formula*</code>.
|
||||
|
|
@ -394,9 +394,9 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Hash Function for <code>const formula*</code>.
|
||||
/// \ingroup ltl_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for <code>const formula*</code>.
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// Sgi's \c hash_map whose key are of type <code>const formula*</code>.
|
||||
|
|
|
|||
|
|
@ -34,8 +34,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Multi-operand operators.
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief Multi-operand operators.
|
||||
class multop : public ref_formula
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -32,8 +32,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief A reference-counted LTL formula.
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief A reference-counted LTL formula.
|
||||
class ref_formula : public formula
|
||||
{
|
||||
protected:
|
||||
|
|
|
|||
|
|
@ -34,8 +34,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Unary operators.
|
||||
/// \ingroup ltl_ast
|
||||
/// \brief Unary operators.
|
||||
class unop : public ref_formula
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Formula visitor
|
||||
/// \ingroup ltl_essential
|
||||
/// \brief Formula visitor
|
||||
///
|
||||
/// Implementing visitors is the prefered way
|
||||
/// to traverse a formula, since it does not
|
||||
|
|
|
|||
|
|
@ -33,8 +33,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief A declarative environment.
|
||||
/// \ingroup ltl_environment
|
||||
/// \brief A declarative environment.
|
||||
///
|
||||
/// This environment recognizes all atomic propositions
|
||||
/// that have been previously declared. It will reject other.
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief A laxist environment.
|
||||
/// \ingroup ltl_environment
|
||||
/// \brief A laxist environment.
|
||||
///
|
||||
/// This environment recognizes all atomic propositions.
|
||||
///
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief An environment that describes atomic propositions.
|
||||
/// \ingroup ltl_essential
|
||||
/// \brief An environment that describes atomic propositions.
|
||||
class environment
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Read LTL formulae from a file, one by one
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Read LTL formulae from a file, one by one
|
||||
class ltl_file
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Clone a formula.
|
||||
/// \ingroup ltl_visitor
|
||||
/// \brief Clone a formula.
|
||||
///
|
||||
/// This visitor is public, because it's convenient
|
||||
/// to derive from it and override part of its methods.
|
||||
|
|
@ -60,13 +60,13 @@ namespace spot
|
|||
};
|
||||
|
||||
#if __GNUC__
|
||||
/// \brief Clone a formula.
|
||||
/// \ingroup ltl_essential
|
||||
/// \brief Clone a formula.
|
||||
/// \deprecated Use f->clone() instead.
|
||||
const formula* clone(const formula* f) __attribute__ ((deprecated));
|
||||
#else
|
||||
/// \brief Clone a formula.
|
||||
/// \ingroup ltl_essential
|
||||
/// \brief Clone a formula.
|
||||
/// \deprecated Use f->clone() instead.
|
||||
const formula* clone(const formula* f);
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -29,13 +29,13 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
#if __GNUC__
|
||||
/// \brief Destroys a formula
|
||||
/// \ingroup ltl_essential
|
||||
/// \brief Destroys a formula
|
||||
/// \deprecated Use f->destroy() instead.
|
||||
void destroy(const formula *f) __attribute__ ((deprecated));
|
||||
#else
|
||||
/// \brief Destroys a formula
|
||||
/// \ingroup ltl_essential
|
||||
/// \brief Destroys a formula
|
||||
/// \deprecated Use f->destroy() instead.
|
||||
void destroy(const formula *f);
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Write a formula tree using dot's syntax.
|
||||
/// \ingroup ltl_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,8 +27,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Dump a formula tree.
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Dump a formula tree.
|
||||
/// \param os The stream where it should be output.
|
||||
/// \param f The formula to dump.
|
||||
///
|
||||
|
|
|
|||
|
|
@ -28,8 +28,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Compute the length of a formula.
|
||||
/// \ingroup ltl_misc
|
||||
/// \brief Compute the length of a formula.
|
||||
///
|
||||
/// The length of a formula is the number of atomic propositions,
|
||||
/// constants, and operators (logical and temporal) occurring in
|
||||
|
|
@ -42,8 +42,8 @@ namespace spot
|
|||
/// to have length one.
|
||||
int length(const formula* f);
|
||||
|
||||
/// \brief Compute the length of a formula, squashing Boolean formulae
|
||||
/// \ingroup ltl_misc
|
||||
/// \brief Compute the length of a formula, squashing Boolean formulae
|
||||
///
|
||||
/// This is similar to spot::ltl::length(), except all Boolean
|
||||
/// formulae are assumed to have length one.
|
||||
|
|
|
|||
|
|
@ -29,9 +29,9 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \ingroup ltl_visitor
|
||||
/// \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,9 +54,9 @@ namespace spot
|
|||
virtual const formula* recurse(const formula* f);
|
||||
};
|
||||
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \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,
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ namespace spot
|
|||
class mark_tools
|
||||
{
|
||||
public:
|
||||
/// \brief Mark operators NegClosure and EConcat.
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \brief Mark operators NegClosure and EConcat.
|
||||
///
|
||||
/// \param f The formula to rewrite.
|
||||
const formula* mark_concat_ops(const formula* f);
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Build the negative normal form of \a f.
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \brief Build the negative normal form of \a f.
|
||||
///
|
||||
/// All negations of the formula are pushed in front of the
|
||||
/// atomic propositions.
|
||||
|
|
|
|||
|
|
@ -29,9 +29,9 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \ingroup ltl_visitor
|
||||
/// \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.
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ namespace spot
|
|||
namespace ltl
|
||||
{
|
||||
|
||||
/// \brief Base class for random formula generators
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Base class for random formula generators
|
||||
class random_formula
|
||||
{
|
||||
public:
|
||||
|
|
@ -98,8 +98,8 @@ namespace spot
|
|||
};
|
||||
|
||||
|
||||
/// \brief Generate random LTL formulae.
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Generate random LTL formulae.
|
||||
///
|
||||
/// This class recursively constructs LTL formulae of a given
|
||||
/// size. The formulae will use the use atomic propositions from
|
||||
|
|
@ -151,8 +151,8 @@ namespace spot
|
|||
random_ltl(int size, const atomic_prop_set* ap);
|
||||
};
|
||||
|
||||
/// \brief Generate random Boolean formulae.
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Generate random Boolean formulae.
|
||||
///
|
||||
/// This class recursively constructs Boolean formulae of a given size.
|
||||
/// The formulae will use the use atomic propositions from the
|
||||
|
|
@ -191,8 +191,8 @@ namespace spot
|
|||
random_boolean(const atomic_prop_set* ap);
|
||||
};
|
||||
|
||||
/// \brief Generate random SERE.
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Generate random SERE.
|
||||
///
|
||||
/// This class recursively constructs SERE of a given size.
|
||||
/// The formulae will use the use atomic propositions from the
|
||||
|
|
@ -234,8 +234,8 @@ namespace spot
|
|||
random_boolean rb;
|
||||
};
|
||||
|
||||
/// \brief Generate random PSL formulae.
|
||||
/// \ingroup ltl_io
|
||||
/// \brief Generate random PSL formulae.
|
||||
///
|
||||
/// This class recursively constructs PSL formulae of a given size.
|
||||
/// The formulae will use the use atomic propositions from the
|
||||
|
|
|
|||
|
|
@ -76,8 +76,8 @@ namespace spot
|
|||
#endif
|
||||
/// @}
|
||||
|
||||
/// \brief Check whether a formula is a pure eventuality.
|
||||
/// \ingroup ltl_misc
|
||||
/// \brief Check whether a formula is a pure eventuality.
|
||||
///
|
||||
/// Pure eventuality formulae are defined in
|
||||
/// \verbatim
|
||||
|
|
@ -105,8 +105,8 @@ namespace spot
|
|||
bool is_eventual(const formula* f);
|
||||
#endif
|
||||
|
||||
/// \brief Check whether a formula is purely universal.
|
||||
/// \ingroup ltl_misc
|
||||
/// \brief Check whether a formula is purely universal.
|
||||
///
|
||||
/// Purely universal formulae are defined in
|
||||
/// \verbatim
|
||||
|
|
|
|||
|
|
@ -28,9 +28,9 @@ namespace spot
|
|||
{
|
||||
enum relabeling_style { Abc, Pnn };
|
||||
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \brief Relabel the atomic proposition in a formula.
|
||||
///
|
||||
/// \ingroup ltl_rewriting
|
||||
const formula* relabel(const formula* f, relabeling_style style);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \ingroup ltl_visitor
|
||||
/// \brief Replace <code>true U f</code> and <code>false R g</code> by
|
||||
/// <code>F f</code> and <code>G g</code>.
|
||||
///
|
||||
|
|
@ -39,7 +40,6 @@ namespace spot
|
|||
/// - false R a = G a
|
||||
/// - a W false = G a
|
||||
///
|
||||
/// \ingroup ltl_visitor
|
||||
class simplify_f_g_visitor : public clone_visitor
|
||||
{
|
||||
typedef clone_visitor super;
|
||||
|
|
@ -53,6 +53,7 @@ namespace spot
|
|||
virtual const formula* recurse(const formula* f);
|
||||
};
|
||||
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \brief Replace <code>true U f</code> and <code>false R g</code> by
|
||||
/// <code>F f</code> and <code>G g</code>.
|
||||
///
|
||||
|
|
@ -63,7 +64,6 @@ namespace spot
|
|||
/// - false R a = G a
|
||||
/// - a W false = G a
|
||||
///
|
||||
/// \ingroup ltl_rewriting
|
||||
const formula* simplify_f_g(const formula* f);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -73,8 +73,8 @@ namespace spot
|
|||
// fwd declaration to hide technical details.
|
||||
class ltl_simplifier_cache;
|
||||
|
||||
/// \brief Rewrite or simplify \a f in various ways.
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \brief Rewrite or simplify \a f in various ways.
|
||||
class ltl_simplifier
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -30,9 +30,9 @@ namespace spot
|
|||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \ingroup ltl_visitor
|
||||
/// \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.
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ namespace spot
|
|||
{
|
||||
class formula;
|
||||
|
||||
/// \ingroup ltl_rewriting
|
||||
/// \brief Rewrite a formula to remove the W and M operators.
|
||||
///
|
||||
/// This is necessary if you want to use the formula with a tool
|
||||
|
|
@ -34,7 +35,6 @@ namespace spot
|
|||
/// <code>a W b</code> is replaced by <code>b R (b | a)</code>,
|
||||
/// and <code>a M b</code> is replaced by <code>b U (b & a)</code>.
|
||||
///
|
||||
/// \ingroup ltl_rewriting
|
||||
const formula* unabbreviate_wm(const formula* f);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Manage ranges of variables.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Manage ranges of variables.
|
||||
class bdd_allocator: private free_list
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Comparison functor for BDDs.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Comparison functor for BDDs.
|
||||
struct bdd_less_than :
|
||||
public std::binary_function<const bdd&, const bdd&, bool>
|
||||
{
|
||||
|
|
@ -39,8 +39,8 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Hash functor for BDDs.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Hash functor for BDDs.
|
||||
struct bdd_hash :
|
||||
public std::unary_function<const bdd&, size_t>
|
||||
{
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Manage list of free integers.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Manage list of free integers.
|
||||
class free_list
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -74,8 +74,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief A hash function for pointers.
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief A hash function for pointers.
|
||||
template <class T>
|
||||
struct ptr_hash :
|
||||
public std::unary_function<const T*, size_t>
|
||||
|
|
@ -87,8 +87,8 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief A hash function for strings.
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief A hash function for strings.
|
||||
/// @{
|
||||
#if defined(SPOT_HAVE_UNORDERED_MAP) || defined(SPOT_HAVE_TR1_UNORDERED_MAP)
|
||||
typedef Sgi::hash<std::string> string_hash;
|
||||
|
|
@ -107,8 +107,8 @@ namespace spot
|
|||
/// @}
|
||||
#endif
|
||||
|
||||
/// \brief A hash function that returns identity
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief A hash function that returns identity
|
||||
template<typename T>
|
||||
struct identity_hash:
|
||||
public std::unary_function<const T&, size_t>
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Strict Weak Ordering for \c char*.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Strict Weak Ordering for \c char*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type <code>const char*</code>.
|
||||
|
|
|
|||
|
|
@ -27,9 +27,9 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Generate an irredundant sum-of-products (ISOP) form of a
|
||||
/// BDD function.
|
||||
/// \ingroup misc_tools
|
||||
///
|
||||
/// This algorithm implements a derecursived version the Minato-Morreale
|
||||
/// algorithm presented in the following paper.
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Loopless modular mixed radix Gray code iteration.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Loopless modular mixed radix Gray code iteration.
|
||||
///
|
||||
/// This class is based on the loopless modular mixed radix gray
|
||||
/// code algorithm described in exercise 77 of "The Art of Computer
|
||||
|
|
|
|||
|
|
@ -26,8 +26,9 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Manage a map of options.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Manage a map of options.
|
||||
///
|
||||
/// Each option is defined by a string and is associated to an integer value.
|
||||
class option_map
|
||||
{
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Return Spot's version.
|
||||
/// \ingroup misc_tools
|
||||
/// \brief Return Spot's version.
|
||||
const char* version();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Basic implementation of saba_state_conjunction.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief Basic implementation of saba_state_conjunction.
|
||||
///
|
||||
/// This class provides a basic implementation to
|
||||
/// iterate over a conjunction of states of a saba.
|
||||
|
|
|
|||
|
|
@ -36,8 +36,8 @@ namespace spot
|
|||
/// \addtogroup saba_essentials Essential SABA types
|
||||
/// \ingroup saba
|
||||
|
||||
/// \brief A State-based Alternating (Generalized) Büchi Automaton.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief A State-based Alternating (Generalized) Büchi Automaton.
|
||||
///
|
||||
/// Browsing such automaton can be achieved using two functions:
|
||||
/// \c get_init_state, and \c succ_iter. The former returns
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Complement a TGBA and produce a SABA.
|
||||
/// \ingroup saba
|
||||
/// \brief Complement a TGBA and produce a SABA.
|
||||
///
|
||||
/// The original TGBA is transformed into a States-based
|
||||
/// Büchi Automaton.
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Abstract class for saba states.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief Abstract class for saba states.
|
||||
class saba_state
|
||||
{
|
||||
public:
|
||||
|
|
@ -78,8 +78,8 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Strict Weak Ordering for \c saba_state*.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief Strict Weak Ordering for \c saba_state*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type \c saba_state*.
|
||||
|
|
@ -101,8 +101,8 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief An Equivalence Relation for \c saba_state*.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief An Equivalence Relation for \c saba_state*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// Sgi \c hash_map whose key are of type \c saba_state*.
|
||||
|
|
@ -125,9 +125,9 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Hash Function for \c saba_state*.
|
||||
/// \ingroup saba_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for \c saba_state*.
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// Sgi's \c hash_map whose key are of type \c saba_state*.
|
||||
|
|
@ -155,9 +155,9 @@ namespace spot
|
|||
|
||||
typedef boost::shared_ptr<const saba_state> shared_saba_state;
|
||||
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief Strict Weak Ordering for \c shared_saba_state
|
||||
/// (shared_ptr<const saba_state*>).
|
||||
/// \ingroup saba_essentials
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type \c shared_saba_state.
|
||||
|
|
@ -182,9 +182,9 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief An Equivalence Relation for \c shared_saba_state
|
||||
/// (shared_ptr<const saba_state*>).
|
||||
/// \ingroup saba_essentials
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// Sgi \c hash_map whose key are of type \c shared_saba_state.
|
||||
|
|
@ -210,10 +210,10 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Hash Function for \c shared_saba_state
|
||||
/// (shared_ptr<const saba_state*>).
|
||||
/// \ingroup saba_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for \c shared_saba_state
|
||||
/// (shared_ptr<const saba_state*>).
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// Sgi's \c hash_map whose key are of type
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Iterate over a conjunction of saba_state.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief Iterate over a conjunction of saba_state.
|
||||
///
|
||||
/// This class provides the basic functionalities required to
|
||||
/// iterate over a conjunction of states of a saba.
|
||||
|
|
@ -87,8 +87,8 @@ namespace spot
|
|||
};
|
||||
|
||||
|
||||
/// \brief Iterate over the successors of a saba_state.
|
||||
/// \ingroup saba_essentials
|
||||
/// \brief Iterate over the successors of a saba_state.
|
||||
///
|
||||
/// This class provides the basic functionalities required to
|
||||
/// iterate over the successors of a state of a saba. Since
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@ namespace spot
|
|||
{
|
||||
class saba;
|
||||
|
||||
/// \brief Print reachable states in dot format.
|
||||
/// \ingroup saba_io
|
||||
/// \brief Print reachable states in dot format.
|
||||
std::ostream&
|
||||
saba_dotty_reachable(std::ostream& os,
|
||||
const saba* g);
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Iterate over all reachable states of a spot::saba.
|
||||
/// \ingroup saba_generic
|
||||
/// \brief Iterate over all reachable states of a spot::saba.
|
||||
class saba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
@ -112,9 +112,9 @@ namespace spot
|
|||
seen_map seen; ///< States already seen.
|
||||
};
|
||||
|
||||
/// \ingroup saba_generic
|
||||
/// \brief An implementation of spot::saba_reachable_iterator that browses
|
||||
/// states depth first.
|
||||
/// \ingroup saba_generic
|
||||
class saba_reachable_iterator_depth_first : public saba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
@ -127,9 +127,9 @@ namespace spot
|
|||
std::stack<const saba_state*> todo; ///< A stack of states yet to explore.
|
||||
};
|
||||
|
||||
/// \ingroup saba_generic
|
||||
/// \brief An implementation of spot::saba_reachable_iterator that browses
|
||||
/// states breadth first.
|
||||
/// \ingroup saba_generic
|
||||
class saba_reachable_iterator_breadth_first : public saba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -63,6 +63,18 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
|
|||
grep Copyright $file >/dev/null ||
|
||||
diag "missing copyright"
|
||||
|
||||
# A doxygen comments such as
|
||||
#
|
||||
# | \brief foo
|
||||
# | \ingroup bar
|
||||
# |
|
||||
# | baz
|
||||
#
|
||||
# will be output as "foobaz." But if the first two lines
|
||||
# are reversed, it's output correctly.
|
||||
perl -ne '/(.*\\brief.*\n.*\\ingroup.*)/ && print("$1\n") && exit(1)' \
|
||||
-0777 $file || diag "always put 'ingroup' before 'brief'"
|
||||
|
||||
# Strip comments and strings.
|
||||
sed 's,[ ]*//.*,,;s,"[^"]*","",g' < $file > $tmp
|
||||
|
||||
|
|
|
|||
|
|
@ -44,8 +44,8 @@ namespace spot
|
|||
/// \addtogroup ta_essentials Essential TA types
|
||||
/// \ingroup ta
|
||||
|
||||
/// \brief A Testing Automaton.
|
||||
/// \ingroup ta_essentials
|
||||
/// \brief A Testing Automaton.
|
||||
///
|
||||
/// The Testing Automata (TA) were introduced by
|
||||
/// Henri Hansen, Wojciech Penczek and Antti Valmari
|
||||
|
|
@ -174,8 +174,8 @@ namespace spot
|
|||
|
||||
};
|
||||
|
||||
/// \brief Iterate over the successors of a state.
|
||||
/// \ingroup ta_essentials
|
||||
/// \brief Iterate over the successors of a state.
|
||||
///
|
||||
/// This class provides the basic functionalities required to
|
||||
/// iterate over the successors of a state, as well as querying
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief A state for spot::ta_product.
|
||||
/// \ingroup ta_emptiness_check
|
||||
/// \brief A state for spot::ta_product.
|
||||
///
|
||||
/// This state is in fact a pair of state: the state from the TA
|
||||
/// automaton and that of Kripke structure.
|
||||
|
|
@ -132,9 +132,9 @@ namespace spot
|
|||
|
||||
};
|
||||
|
||||
/// \ingroup ta_emptiness_check
|
||||
/// \brief A lazy product between a Testing automaton and a Kripke structure.
|
||||
/// (States are computed on the fly.)
|
||||
/// \ingroup ta_emptiness_check
|
||||
class ta_product : public ta
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief A Transition-based Generalized Testing Automaton (TGTA).
|
||||
/// \ingroup ta_essentials
|
||||
/// \brief A Transition-based Generalized Testing Automaton (TGTA).
|
||||
///
|
||||
/// Transition-based Generalized Testing Automaton (TGTA) is a new kind of
|
||||
/// automaton that combines features from both TA and TGBA.
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Iterate over all reachable states of a spot::ta.
|
||||
/// \ingroup ta_generic
|
||||
/// \brief Iterate over all reachable states of a spot::ta.
|
||||
class ta_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
@ -94,9 +94,9 @@ namespace spot
|
|||
seen_map seen; ///< States already seen.
|
||||
};
|
||||
|
||||
/// \ingroup ta_generic
|
||||
/// \brief An implementation of spot::ta_reachable_iterator that browses
|
||||
/// states depth first.
|
||||
/// \ingroup ta_generic
|
||||
class ta_reachable_iterator_depth_first : public ta_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
@ -111,9 +111,9 @@ namespace spot
|
|||
std::stack<const state*> todo; ///< A stack of states yet to explore.
|
||||
};
|
||||
|
||||
/// \ingroup ta_generic
|
||||
/// \brief An implementation of spot::ta_reachable_iterator that browses
|
||||
/// states breadth first.
|
||||
/// \ingroup ta_generic
|
||||
class ta_reachable_iterator_breadth_first : public ta_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Build a spot::ta_explicit* (TA) from an LTL formula.
|
||||
/// \ingroup tgba_ta
|
||||
/// \brief Build a spot::ta_explicit* (TA) from an LTL formula.
|
||||
///
|
||||
/// This is based on the following paper.
|
||||
/// \verbatim
|
||||
|
|
@ -85,10 +85,10 @@ namespace spot
|
|||
bool single_pass_emptiness_check = false,
|
||||
bool artificial_livelock_state_mode = false);
|
||||
|
||||
/// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula.
|
||||
/// \ingroup tgba_ta
|
||||
/// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton
|
||||
/// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula.
|
||||
///
|
||||
/// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton
|
||||
/// \param atomic_propositions_set The set of atomic propositions used in the
|
||||
/// input TGBA \a tgba_to_convert
|
||||
///
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Wrap a tgba to offer information about upcoming conditions.
|
||||
/// \ingroup tgba
|
||||
/// \brief Wrap a tgba to offer information about upcoming conditions.
|
||||
///
|
||||
/// This class is a spot::tgba wrapper that simply add a new method,
|
||||
/// future_conditions(), to any spot::tgba.
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief A State-based Generalized Büchi Automaton.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief A State-based Generalized Büchi Automaton.
|
||||
///
|
||||
/// An SBA is a TGBA in which the outgoing transitions of
|
||||
/// a state are either all accepting (in which case the
|
||||
|
|
|
|||
|
|
@ -33,8 +33,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Abstract class for states.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief Abstract class for states.
|
||||
class state
|
||||
{
|
||||
public:
|
||||
|
|
@ -98,8 +98,8 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Strict Weak Ordering for \c state*.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief Strict Weak Ordering for \c state*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type \c state*.
|
||||
|
|
@ -121,8 +121,8 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief An Equivalence Relation for \c state*.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief An Equivalence Relation for \c state*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// Sgi \c hash_map whose key are of type \c state*.
|
||||
|
|
@ -145,9 +145,9 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Hash Function for \c state*.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for \c state*.
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// Sgi's \c hash_map whose key are of type \c state*.
|
||||
|
|
@ -177,9 +177,9 @@ namespace spot
|
|||
|
||||
inline void shared_state_deleter(state* s) { s->destroy(); }
|
||||
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief Strict Weak Ordering for \c shared_state
|
||||
/// (shared_ptr<const state*>).
|
||||
/// \ingroup tgba_essentials
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type \c shared_state.
|
||||
|
|
@ -203,9 +203,9 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief An Equivalence Relation for \c shared_state
|
||||
/// (shared_ptr<const state*>).
|
||||
/// \ingroup tgba_essentials
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// Sgi \c hash_map whose key are of type \c shared_state.
|
||||
|
|
@ -231,9 +231,9 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
/// \brief Hash Function for \c shared_state (shared_ptr<const state*>).
|
||||
/// \ingroup tgba_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for \c shared_state (shared_ptr<const state*>).
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// Sgi's \c hash_map whose key are of type
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Iterate over the successors of a state.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief Iterate over the successors of a state.
|
||||
///
|
||||
/// This class provides the basic functionalities required to
|
||||
/// iterate over the successors of a state, as well as querying
|
||||
|
|
|
|||
|
|
@ -41,8 +41,8 @@ namespace spot
|
|||
/// \addtogroup tgba_essentials Essential TGBA types
|
||||
/// \ingroup tgba
|
||||
|
||||
/// \brief A Transition-based Generalized Büchi Automaton.
|
||||
/// \ingroup tgba_essentials
|
||||
/// \brief A Transition-based Generalized Büchi Automaton.
|
||||
///
|
||||
/// The acronym TGBA (Transition-based Generalized Büchi Automaton)
|
||||
/// was coined by Dimitra Giannakopoulou and Flavio Lerda
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief A concrete spot::tgba implemented using BDDs.
|
||||
/// \ingroup tgba_representation
|
||||
/// \brief A concrete spot::tgba implemented using BDDs.
|
||||
class tgba_bdd_concrete: public tgba
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Multiplies two spot::tgba_bdd_concrete automata.
|
||||
/// \ingroup tgba_algorithms
|
||||
/// \brief Multiplies two spot::tgba_bdd_concrete automata.
|
||||
///
|
||||
/// This function builds the resulting product as another
|
||||
/// spot::tgba_bdd_concrete automaton.
|
||||
|
|
|
|||
|
|
@ -60,8 +60,8 @@ namespace spot
|
|||
|
||||
typedef std::vector<bdd_ordered> acc_list_t;
|
||||
|
||||
/// \brief Build a complemented automaton.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief Build a complemented automaton.
|
||||
///
|
||||
/// The construction comes from:
|
||||
/// \verbatim
|
||||
|
|
|
|||
|
|
@ -28,8 +28,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief A state for spot::tgba_product.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief A state for spot::tgba_product.
|
||||
///
|
||||
/// This state is in fact a pair of state: the state from the left
|
||||
/// automaton and that of the right.
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Build a complemented automaton.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief Build a complemented automaton.
|
||||
///
|
||||
/// It creates an automaton that recognizes the
|
||||
/// negated language of \a aut.
|
||||
|
|
|
|||
|
|
@ -24,9 +24,9 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \ingroup tgba
|
||||
/// \brief Wrap a tgba to offer information about strongly connected
|
||||
/// components.
|
||||
/// \ingroup tgba
|
||||
///
|
||||
/// This class is a spot::tgba wrapper that simply add a new method
|
||||
/// scc_of_state() to retrieve the number of a SCC a state belongs to.
|
||||
|
|
|
|||
|
|
@ -25,9 +25,9 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief Change the labeling-mode of spot::tgba on the fly, producing a
|
||||
/// state-based generalized Büchi automaton.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
///
|
||||
/// This class acts as a proxy in front of a spot::tgba, that should
|
||||
/// label on states on-the-fly. The result is still a spot::tgba,
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Degeneralize a spot::tgba on the fly, producing a TBA.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief Degeneralize a spot::tgba on the fly, producing a TBA.
|
||||
///
|
||||
/// This class acts as a proxy in front of a spot::tgba, that should
|
||||
/// be degeneralized on the fly. The result is still a spot::tgba,
|
||||
|
|
@ -124,8 +124,8 @@ namespace spot
|
|||
tgba_tba_proxy& operator=(const tgba_tba_proxy&);
|
||||
};
|
||||
|
||||
/// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
|
||||
///
|
||||
/// This class acts as a proxy in front of a spot::tgba, that should
|
||||
/// be degeneralized on the fly.
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief A state for spot::tgba_union.
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief A state for spot::tgba_union.
|
||||
///
|
||||
/// This state is in fact a pair.
|
||||
/// If the first member equals 0 and the second is different from 0,
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Complement a weak deterministic Büchi automaton
|
||||
/// \ingroup tgba_on_the_fly_algorithms
|
||||
/// \brief Complement a weak deterministic Büchi automaton
|
||||
/// \param aut a weak deterministic Büchi automaton to complement
|
||||
/// \return a new automaton that recognizes the complement language
|
||||
tgba* wdba_complement(const tgba* aut);
|
||||
|
|
|
|||
|
|
@ -28,8 +28,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps.
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps.
|
||||
///
|
||||
/// This class should be used to compute the shortest path
|
||||
/// between a state of a spot::tgba and the first transition or
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ namespace spot
|
|||
class sba;
|
||||
class tgba;
|
||||
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Degeneralize a spot::tgba into an equivalent sba with
|
||||
/// only one acceptance condition.
|
||||
///
|
||||
|
|
@ -46,7 +47,6 @@ namespace spot
|
|||
/// \a a to be computed prior to its actual degeneralization.
|
||||
///
|
||||
/// \see tgba_sba_proxy, tgba_tba_proxy
|
||||
/// \ingroup tgba_misc
|
||||
sba* degeneralize(const tgba* a, bool use_z_lvl = true,
|
||||
bool use_cust_acc_orders = false,
|
||||
bool use_lvl_cache = true);
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ namespace spot
|
|||
class tgba;
|
||||
class dotty_decorator;
|
||||
|
||||
/// \brief Print reachable states in dot format.
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Print reachable states in dot format.
|
||||
///
|
||||
/// If \a assume_sba is set, this assumes that the automaton
|
||||
/// is an SBA and use double elipse to mark accepting states.
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ namespace spot
|
|||
/// \addtogroup tgba_dotty Decorating the dot output
|
||||
/// \ingroup tgba_io
|
||||
|
||||
/// \brief Choose state and link styles for spot::dotty_reachable.
|
||||
/// \ingroup tgba_dotty
|
||||
/// \brief Choose state and link styles for spot::dotty_reachable.
|
||||
class dotty_decorator
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -27,25 +27,25 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Build an explicit automata from all states of \a aut,
|
||||
/// numbering states in bread first order as they are processed.
|
||||
/// \ingroup tgba_misc
|
||||
tgba_explicit_number* tgba_dupexp_bfs(const tgba* aut);
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Build an explicit automata from all states of \a aut,
|
||||
/// numbering states in depth first order as they are processed.
|
||||
/// \ingroup tgba_misc
|
||||
tgba_explicit_number* tgba_dupexp_dfs(const tgba* aut);
|
||||
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Build an explicit automata from all states of \a aut,
|
||||
/// numbering states in bread first order as they are processed.
|
||||
/// \ingroup tgba_misc
|
||||
tgba_explicit_number*
|
||||
tgba_dupexp_bfs(const tgba* aut,
|
||||
std::map<const state*, const state*,
|
||||
state_ptr_less_than>& relation);
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Build an explicit automata from all states of \a aut,
|
||||
/// numbering states in depth first order as they are processed.
|
||||
/// \ingroup tgba_misc
|
||||
tgba_explicit_number*
|
||||
tgba_dupexp_dfs(const tgba* aut,
|
||||
std::map<const state*, const state*,
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Build a spot::tgba_bdd_concrete from an ELTL formula.
|
||||
/// \ingroup tgba_ltl
|
||||
/// \brief Build a spot::tgba_bdd_concrete from an ELTL formula.
|
||||
///
|
||||
/// This is based on the following paper.
|
||||
/// \verbatim
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Print reachable states in LBTT's format.
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Print reachable states in LBTT's format.
|
||||
///
|
||||
/// \param g The automata to print.
|
||||
/// \param os Where to print.
|
||||
|
|
@ -39,8 +39,8 @@ namespace spot
|
|||
std::ostream& lbtt_reachable(std::ostream& os, const tgba* g,
|
||||
bool sba = false);
|
||||
|
||||
/// \brief Read an automaton in LBTT's format
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Read an automaton in LBTT's format
|
||||
///
|
||||
/// \param is The stream on which the automaton should be input.
|
||||
/// \param error A string in which to write any error message.
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Build a spot::taa* from an LTL formula.
|
||||
/// \ingroup tgba_ltl
|
||||
/// \brief Build a spot::taa* from an LTL formula.
|
||||
///
|
||||
/// This is based on the following.
|
||||
/// \verbatim
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Build a spot::tgba_explicit* from an LTL formula.
|
||||
/// \ingroup tgba_ltl
|
||||
/// \brief Build a spot::tgba_explicit* from an LTL formula.
|
||||
///
|
||||
/// This is based on the following paper.
|
||||
/// \verbatim
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Build a spot::tgba_bdd_concrete from an LTL formula.
|
||||
/// \ingroup tgba_ltl
|
||||
/// \brief Build a spot::tgba_bdd_concrete from an LTL formula.
|
||||
///
|
||||
/// This is based on the following paper.
|
||||
/// \verbatim
|
||||
|
|
|
|||
|
|
@ -28,8 +28,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Print reachable states in Spin never claim format.
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Print reachable states in Spin never claim format.
|
||||
///
|
||||
/// \param os The output stream to print on.
|
||||
/// \param g The (state-based degeneralized) automaton to output.
|
||||
|
|
|
|||
|
|
@ -76,8 +76,8 @@ namespace spot
|
|||
};
|
||||
|
||||
|
||||
/// \brief Build a deterministic automaton, ignoring acceptance conditions.
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Build a deterministic automaton, ignoring acceptance conditions.
|
||||
///
|
||||
/// This create a deterministic automaton that recognizes the
|
||||
/// same language as \a aut would if its acceptance conditions
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@ namespace spot
|
|||
struct tgba_run;
|
||||
class tgba;
|
||||
|
||||
/// \brief Project a tgba_run on a tgba.
|
||||
/// \ingroup tgba_run
|
||||
/// \brief Project a tgba_run on a tgba.
|
||||
///
|
||||
/// If a tgba_run has been generated on a product, or any other
|
||||
/// on-the-fly algorithm with tgba operands,
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ namespace spot
|
|||
class bdd_dict;
|
||||
class tgba;
|
||||
|
||||
/// \brief Construct a tgba randomly.
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Construct a tgba randomly.
|
||||
///
|
||||
/// \param n The number of states wanted in the automata (>0). All states
|
||||
/// will be connected, and there will be no dead state.
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Iterate over all reachable states of a spot::tgba.
|
||||
/// \ingroup tgba_generic
|
||||
/// \brief Iterate over all reachable states of a spot::tgba.
|
||||
class tgba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
@ -95,9 +95,9 @@ namespace spot
|
|||
seen_map seen; ///< States already seen.
|
||||
};
|
||||
|
||||
/// \ingroup tgba_generic
|
||||
/// \brief An implementation of spot::tgba_reachable_iterator that browses
|
||||
/// states depth first.
|
||||
/// \ingroup tgba_generic
|
||||
class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
@ -110,9 +110,9 @@ namespace spot
|
|||
std::stack<const state*> todo; ///< A stack of states yet to explore.
|
||||
};
|
||||
|
||||
/// \ingroup tgba_generic
|
||||
/// \brief An implementation of spot::tgba_reachable_iterator that browses
|
||||
/// states breadth first.
|
||||
/// \ingroup tgba_generic
|
||||
class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@ namespace spot
|
|||
class tgba;
|
||||
struct tgba_run;
|
||||
|
||||
/// \brief Reduce an accepting run.
|
||||
/// \ingroup tgba_run
|
||||
/// \brief Reduce an accepting run.
|
||||
///
|
||||
/// Return a run which is accepting for \a and that is no longer
|
||||
/// that \a org.
|
||||
|
|
|
|||
|
|
@ -27,8 +27,8 @@ namespace spot
|
|||
struct tgba_run;
|
||||
class tgba;
|
||||
|
||||
/// \brief Replay a tgba_run on a tgba.
|
||||
/// \ingroup tgba_run
|
||||
/// \brief Replay a tgba_run on a tgba.
|
||||
///
|
||||
/// This is similar to print_tgba_run(), except that the run is
|
||||
/// actually replayed on the automaton while it is printed. Doing
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Highlight a spot::tgba_run on a spot::tgba.
|
||||
/// \ingroup tgba_dotty
|
||||
/// \brief Highlight a spot::tgba_run on a spot::tgba.
|
||||
///
|
||||
/// An instance of this class can be passed to spot::dotty_reachable.
|
||||
class tgba_run_dotty_decorator: public dotty_decorator
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Save reachable states in text format.
|
||||
/// \ingroup tgba_io
|
||||
/// \brief Save reachable states in text format.
|
||||
std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -24,10 +24,10 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \ingroup tgba_misc
|
||||
/// \brief Duplicate automaton \a a, removing all acceptance sets.
|
||||
///
|
||||
/// This is equivalent to marking all states/transitions as accepting.
|
||||
/// \ingroup tgba_misc
|
||||
sba_explicit_number* strip_acceptance(const tgba* a);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Translate an LTL formula into an optimized spot::tgba.
|
||||
/// \ingroup tgba_ltl
|
||||
/// \brief Translate an LTL formula into an optimized spot::tgba.
|
||||
///
|
||||
/// This class implements a three-step translation:
|
||||
/// - syntactic simplification of the formula
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue