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

* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.

* src/ltlast/formula.hh: More Doxygen comments.
* src/tgba/tgba.hh: Use <tt> in Doxygen comments.
parent ecda9e26
2003-06-26 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-06-26 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
* src/ltlast/formula.hh: More Doxygen comments.
* src/tgba/tgba.hh: Use <tt> in Doxygen comments.
* doc/mainpage.dox: New file. * doc/mainpage.dox: New file.
* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox. * doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox * doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox
......
...@@ -17,7 +17,9 @@ namespace spot ...@@ -17,7 +17,9 @@ namespace spot
public: public:
virtual ~formula(); virtual ~formula();
/// Entry point for vspot::ltl::visitor instances.
virtual void accept(visitor& v) = 0; virtual void accept(visitor& v) = 0;
/// Entry point for vspot::ltl::const_visitor instances.
virtual void accept(const_visitor& v) const = 0; virtual void accept(const_visitor& v) const = 0;
/// \brief clone this formula /// \brief clone this formula
...@@ -29,7 +31,7 @@ namespace spot ...@@ -29,7 +31,7 @@ namespace spot
/// \brief increment reference counter if any /// \brief increment reference counter if any
virtual void ref_(); virtual void ref_();
/// \brief decrement reference counter if any, return true when /// \brief decrement reference counter if any, return true when
/// the instance must be delete (usually when the counter hits 0). /// the instance must be deleted (usually when the counter hits 0).
virtual bool unref_(); virtual bool unref_();
}; };
......
...@@ -20,12 +20,6 @@ namespace spot ...@@ -20,12 +20,6 @@ namespace spot
/// transitions), and a path can be accepted only if it traverse /// transitions), and a path can be accepted only if it traverse
/// at least one transition of each set infinitely often. /// at least one transition of each set infinitely often.
/// ///
/// Actually we do not really encode accepting sets but their
/// complement: promise sets. Formulae such as 'a U b' and
/// 'F b' make the promise to fulfil 'b' enventually. A path can
/// be accepted if for each promise it traverse infinitely often
/// a transition that does not make this promise.
///
/// Browsing such automaton can be achieved using two functions. /// Browsing such automaton can be achieved using two functions.
/// \c get_init_state, and \c succ_iter. The former returns /// \c get_init_state, and \c succ_iter. The former returns
/// the initial state while the latter allows to explore the /// the initial state while the latter allows to explore the
...@@ -89,11 +83,11 @@ namespace spot ...@@ -89,11 +83,11 @@ namespace spot
virtual bdd all_accepting_conditions() const = 0; virtual bdd all_accepting_conditions() const = 0;
/// \brief Return the conjuction of all negated accepting /// \brief Return the conjuction of all negated accepting
/// variables. /// variables.
/// ///
/// For instance if the automaton uses variables \c Acc[a], /// For instance if the automaton uses variables <tt>Acc[a]</tt>,
/// \c Acc[b] and \c Acc[c] to describe accepting sets, /// <tt>Acc[b]</tt> and <tt>Acc[c]</tt> to describe accepting sets,
/// this function should return \c !Acc[a]\&!Acc[b]\&!Acc[c]. /// this function should return <tt>!Acc[a]\&!Acc[b]\&!Acc[c]</tt>.
/// ///
/// This is useful when making products: each operand conditions /// This is useful when making products: each operand conditions
/// set should be augmented with the neg_accepting_conditions() of /// set should be augmented with the neg_accepting_conditions() of
......
...@@ -41,7 +41,7 @@ namespace spot ...@@ -41,7 +41,7 @@ namespace spot
/// only concerned by atomic propositions (which label the /// only concerned by atomic propositions (which label the
/// transitions) and Next variables (the destination). Typically, /// transitions) and Next variables (the destination). Typically,
/// a transition should bear the variable \c Acc[b] if it doesn't /// a transition should bear the variable \c Acc[b] if it doesn't
/// check for `b' and have a destination of the form <tt>a U b</tt>, /// check for `b' and have a destination of the form <tt>a U b</tt>,
/// or <tt>F b</tt>. /// or <tt>F b</tt>.
/// ///
/// To summarize, \c accepting_conditions contains three kinds of /// To summarize, \c accepting_conditions contains three kinds of
...@@ -52,7 +52,7 @@ namespace spot ...@@ -52,7 +52,7 @@ namespace spot
/// \li "Acc" variables. /// \li "Acc" variables.
bdd accepting_conditions; bdd accepting_conditions;
/// The set of all accepting conditions used by the Automaton. /// \brief The set of all accepting conditions used by the Automaton.
/// ///
/// The goal of the emptiness check is to ensure that /// The goal of the emptiness check is to ensure that
/// a strongly connected component walks through each /// a strongly connected component walks through each
...@@ -79,10 +79,10 @@ namespace spot ...@@ -79,10 +79,10 @@ namespace spot
/// \brief The (positive) conjunction of all variables which are /// \brief The (positive) conjunction of all variables which are
/// not atomic propositions. /// not atomic propositions.
bdd notvar_set; bdd notvar_set;
/// The (positive) conjunction of all variables which are not /// \brief The (positive) conjunction of all variables which are not
/// accepting conditions. /// accepting conditions.
bdd notacc_set; bdd notacc_set;
/// The negative conjunction of all variables which are accepting /// \brief The negative conjunction of all variables which are accepting
/// conditions. /// conditions.
bdd negacc_set; bdd negacc_set;
......
Supports Markdown
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