diff --git a/ChangeLog b/ChangeLog index 404680e6f..0340194ef 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,17 @@ 2003-04-18 Alexandre DURET-LUTZ + * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, + src/ltlast/constant.hh, src/ltlast/formula.hh, + src/ltlast/multop.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, + src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, + src/ltlparse/public.hh, src/ltlvisit/clone.hh, + src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, + src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh, + src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add + Doxygen comments. + * src/visitor.hh: Do not use const_sel. This clarify + the code and helps Doxygen. + * configure.ac: Output doc/Doxyfile and doc/Makefile. * doc/Makefile.am, doc/Doxyfile.in: New files. * Makefile.am (SUBDIRS): Add doc. diff --git a/doc/Doxyfile.in b/doc/Doxyfile.in index c7a539a3a..145d4f250 100644 --- a/doc/Doxyfile.in +++ b/doc/Doxyfile.in @@ -64,7 +64,7 @@ FILE_PATTERNS = *.cc \ RECURSIVE = YES EXCLUDE = EXCLUDE_SYMLINKS = NO -EXCLUDE_PATTERNS = +EXCLUDE_PATTERNS = *test/* EXAMPLE_PATH = EXAMPLE_PATTERNS = EXAMPLE_RECURSIVE = NO @@ -159,7 +159,7 @@ ENABLE_PREPROCESSING = YES MACRO_EXPANSION = NO EXPAND_ONLY_PREDEF = NO SEARCH_INCLUDES = YES -INCLUDE_PATH = +INCLUDE_PATH = @top_srcdir@/src INCLUDE_FILE_PATTERNS = PREDEFINED = EXPAND_AS_DEFINED = diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 5b5ec078e..f293f10d6 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -9,17 +9,22 @@ namespace spot { namespace ltl { - + + /// Atomic propositions. class atomic_prop : public formula { public: + /// Build an atomic proposition with name \a name in + /// environment \a env. atomic_prop(const std::string& name, environment& env); virtual ~atomic_prop(); virtual void accept(visitor& visitor); virtual void accept(const_visitor& visitor) const; + /// Get the name of the atomic proposition. const std::string& name() const; + /// Get the environment of the atomic proposition. environment& env() const; private: std::string name_; diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index e7c10ba7e..8ebd996fb 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -7,12 +7,15 @@ namespace spot { namespace ltl { - + + /// Binary operator. class binop : public formula { public: - // And and Or are not here. Because they - // are often nested we represent them as multops. + /// Different kinds of binary opertaors + /// + /// And and Or are not here. Because they + /// are often nested we represent them as multops. enum type { Xor, Implies, Equiv, U, R }; binop(type op, formula* first, formula* second); @@ -21,12 +24,18 @@ namespace spot virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; + /// Get the first operand. const formula* first() const; + /// Get the first operand. formula* first(); + /// Get the second operand. const formula* second() const; + /// Get the second operand. formula* second(); + /// Get the type of this operator. type op() const; + /// Get the type of this operator, as a string. const char* op_name() const; private: diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index dcd4b3b58..731dcf14f 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -7,7 +7,8 @@ namespace spot { namespace ltl { - + + /// A constant (True or False) class constant : public formula { public: @@ -19,10 +20,9 @@ namespace spot virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; - const formula* child() const; - formula* child(); - + /// Return the value of the constant. type val() const; + /// Return the value of the constant as a string. const char* val_name() const; private: diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index f46e19eb0..5784d3575 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -8,6 +8,10 @@ namespace spot namespace ltl { + /// \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. class formula { public: diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index c7912d15d..a849c9230 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -9,15 +9,30 @@ namespace spot namespace ltl { + /// \brief Multi-operand operators. + /// + /// These operators are considered commutative and associative. class multop : public formula { public: enum type { Or, And }; - multop::multop(type op); - // A multop usually has at least two arguments. + /// \brief Build a spot::ltl::multop with no child. + /// + /// This has little value unless you call multop::add later. + multop(type op); + /// \brief Build a spot::ltl::multop with two children. + /// + /// If one of the children itself is a spot::ltl::multop + /// with the same type, it will be merged. I.e., children + /// if that child will be added, and that child itself will + /// be destroyed. multop(type op, formula* first, formula* second); - // More arguments can be added. + /// \brief Add another child to this operator. + /// + /// If \a f itself is a spot::ltl::multop with the same type, it + /// will be merged. I.e., children of \a f will be added, and + /// that \a f will will be destroyed. void add(formula* f); virtual ~multop(); @@ -25,11 +40,20 @@ namespace spot virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; + /// Get the number of children. unsigned size() const; + /// \brief Get the nth children. + /// + /// Starting with \a n = 0. const formula* nth(unsigned n) const; + /// \brief Get the nth children. + /// + /// Starting with \a n = 0. formula* nth(unsigned n); + /// Get the type of this operator. type op() const; + /// Get the type of this operator, as a string. const char* op_name() const; private: diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index b6ce7831d..659f45b44 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -8,6 +8,7 @@ namespace spot namespace ltl { + /// Unary operator. class unop : public formula { public: @@ -19,10 +20,14 @@ namespace spot virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; + /// Get the sole operand of this operator. const formula* child() const; + /// Get the sole operand of this operator. formula* child(); + /// Get the type of this operator. type op() const; + /// Get the type of this operator, as a string. const char* op_name() const; private: diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index 672fa38fe..6535f2145 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -2,29 +2,44 @@ # define SPOT_LTLAST_VISITOR_HH #include "predecl.hh" -#include "misc/const_sel.hh" namespace spot { namespace ltl { - template - struct generic_visitor + /// \brief Formula visitor that can modify the formula. + /// + /// Writing visitors is the prefered way + /// to traverse a formula, since it doesn't + /// involve any cast. + /// + /// If you do not need to modify the visited formula, inherit from + /// spot::ltl:const_visitor instead. + struct visitor { - virtual void visit(typename const_sel::t* node) - = 0; - - virtual void visit(typename const_sel::t* node) - = 0; - - virtual void visit(typename const_sel::t* node) = 0; - - virtual void visit(typename const_sel::t* node) = 0; - - virtual void visit(typename const_sel::t* node) = 0; + virtual void visit(atomic_prop* node) = 0; + virtual void visit(constant* node) = 0; + virtual void visit(binop* node) = 0; + virtual void visit(unop* node) = 0; + virtual void visit(multop* node) = 0; + }; + + /// \brief Formula visitor that cannot modify the formula. + /// + /// Writing visitors is the prefered way + /// to traverse a formula, since it doesn't + /// involve any cast. + /// + /// If you want to modify the visited formula, inherit from + /// spot::ltl:visitor instead. + struct const_visitor + { + virtual void visit(const atomic_prop* node) = 0; + virtual void visit(const constant* node) = 0; + virtual void visit(const binop* node) = 0; + virtual void visit(const unop* node) = 0; + virtual void visit(const multop* node) = 0; }; - struct visitor : public generic_visitor {}; - struct const_visitor : public generic_visitor {}; } } diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh index db4010e3e..df0c3ac56 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -9,13 +9,19 @@ namespace spot namespace ltl { + /// \brief A laxist environment. + /// + /// The environment recognize all atomic propositions. + /// + /// This is a singleton. Use default_environment::instance() + /// to obtain the instance. class default_environment : public environment { public: virtual formula* require(const std::string& prop_str); virtual const std::string& name(); - /* This class is a singleton. */ + /// Get the sole instance of spot::ltl::default_environment. static default_environment& instance(); protected: default_environment(); diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index 859c68051..299613d4b 100644 --- a/src/ltlenv/environment.hh +++ b/src/ltlenv/environment.hh @@ -9,20 +9,32 @@ namespace spot namespace ltl { + /// An environment that describe atomic propositions. class environment { public: - // Check whether the environment contains the atomic proposition - // described by prop_str. - // Note this is NOT a const method. Some environment will - // "create" the atomic proposition when asked. - // We return a formula instead of an atomic_prop, because this - // will allow nifty tricks (e.g., we could name formulae in an - // environment, and let the parser build a larger tree from - // these). + /// \brief Obtain the formula associated to \a prop_str + /// + /// Usually \a prop_str, is the name of an atomic proposition, + /// a spot::ltl::require simply returns the associated + /// spot::ltl::atomic_prop. + /// + /// Note this is not a \c const method. Some environment will + /// "create" the atomic proposition when asked. + /// + /// We return a spot::ltl::formula instead of an + /// spot::ltl::atomic_prop, because this + /// will allow nifty tricks (e.g., we could name formulae in an + /// environment, and let the parser build a larger tree from + /// these). + /// + /// \return 0 iff \a prop_str is not part of the environment, + /// or the associated spot::ltl::formula otherwise. virtual formula* require(const std::string& prop_str) = 0; + /// Get the name of the environment. virtual const std::string& name() = 0; + // FIXME: More functions will be needed later, but // it's enough for now. }; diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index ebb8be038..29e7fdf25 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -13,16 +13,38 @@ namespace spot { namespace ltl { + /// \brief A parse diagnostic with its location. typedef std::pair parse_error; + /// \brief A list of parser diagnostics, as filled by parse. typedef std::list parse_error_list; - // Beware: this function is *not* reentrant. + /// \brief Build a formula from an LTL string. + /// \param ltl_string The string to parse. + /// \param error_list A list that will be filled with + /// parse errors that occured during parsing. + /// \param env The environment into which parsing should take place. + /// \param debug When true, causes the parser to trace its execution. + /// \return A pointer to the formula built from \a ltl_string, or + /// 0 if the input was unparsable. + /// + /// Note that the parser usually tries to recover from errors. It can + /// return an non zero value even if it encountered error during the + /// parsing of \a ltl_string. If you want to make sure \a ltl_string + /// was parsed succesfully, check \a error_list for emptiness. + /// + /// \warning This function is not reentrant. formula* parse(const std::string& ltl_string, parse_error_list& error_list, environment& env = default_environment::instance(), bool debug = false); - // Return true iff any diagnostic was output to os. + + /// \brief Format diagnostics produced by spot::ltl::parse. + /// \param os Where diagnostics should be output. + /// \param ltl_string The string that were parsed. + /// \param error_list The error list filled by spot::ltl::parse while + /// parsing \a ltl_string. + /// \return \c true iff any diagnostic was output. bool format_parse_errors(std::ostream& os, const std::string& ltl_string, parse_error_list& error_list); diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 5627a958d..c9c2d6fca 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -8,8 +8,12 @@ namespace spot { namespace ltl { - // This visitor is public, because it's convenient - // to derive from it and override part of its methods. + /// \brief Clone a formula. + /// + /// This visitor is public, because it's convenient + /// to derive from it and override part of its methods. + /// But if you just want the functionality, consider using + /// spot::ltl::clone instead. class clone_visitor : public const_visitor { public: @@ -30,6 +34,7 @@ namespace spot formula* result_; }; + /// \brief Clone a formula. formula* clone(const formula* f); } } diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh index 88bc4644b..2af9606b4 100644 --- a/src/ltlvisit/dotty.hh +++ b/src/ltlvisit/dotty.hh @@ -8,6 +8,12 @@ namespace spot { namespace ltl { + /// \brief Write a formula tree using dot's syntax. + /// \param f The formula to translate. + /// \param os The stream where it should be output. + /// + /// \c dot is part of the GraphViz package + /// http://www.research.att.com/sw/tools/graphviz/ void dotty(const formula& f, std::ostream& os); } } diff --git a/src/ltlvisit/dump.hh b/src/ltlvisit/dump.hh index c1ef7cf29..fb30dd0ee 100644 --- a/src/ltlvisit/dump.hh +++ b/src/ltlvisit/dump.hh @@ -1,13 +1,18 @@ #ifndef SPOT_LTLVISIT_DUMP_HH # define SPOT_LTLVISIT_DUMP_HH -#include +#include "ltlast/formula.hh" #include namespace spot { namespace ltl { + /// \brief Dump a formula tree. + /// \param f The formula to dump. + /// \param os The stream where it should be output. + /// + /// This is useful to display a formula when debugging. void dump(const formula& f, std::ostream& os); } } diff --git a/src/ltlvisit/equals.hh b/src/ltlvisit/equals.hh index 2c292302c..a4f8a4d92 100644 --- a/src/ltlvisit/equals.hh +++ b/src/ltlvisit/equals.hh @@ -5,8 +5,12 @@ namespace spot { namespace ltl { - // This visitor is public, because it's convenient - // to derive from it and override part of its methods. + /// \brief Check for equality between two formulae. + /// + /// This visitor is public, because it's convenient + /// to derive from it and override some of its methods. + /// But if you just want the functionality, consider using + /// spot::ltl::equals instead. class equals_visitor : public const_visitor { public: @@ -28,7 +32,14 @@ namespace spot bool result_; }; - + + /// \brief Check whether two formulae are syntaxically equal. + /// \return \c true iff \a f1 equals \a f2. + /// + /// This tests for syntaxic equality rather than semantic equality. + /// Two formulae are equals of their abstract syntax tree are equals. + /// ltl::multop children can be permuted or repeated without + /// impact on the result of this comparison. bool equals(const formula* f1, const formula* f2); } } diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 8d8b25d57..711f13ec3 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -7,8 +7,17 @@ namespace spot { namespace ltl { - // This visitor is public, because it's convenient - // to derive from it and override part of its methods. + /// \brief Clone and rewrite a formula to remove most of the + /// abbreviated logical operators. + /// + /// This will rewrite binary operators such as binop::Implies, + /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, + /// and multop::And. + /// + /// This visitor is public, because it's convenient + /// to derive from it and override some of its methods. + /// But if you just want the functionality, consider using + /// spot::ltl::unabbreviate_logic instead. class unabbreviate_logic_visitor : public clone_visitor { typedef clone_visitor super; @@ -22,6 +31,12 @@ namespace spot virtual formula* recurse(const formula* f); }; + /// \brief Clone rewrite a formula to remove most of the abbreviated + /// logical operators. + /// + /// This will rewrite binary operators such as binop::Implies, + /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, + /// and multop::And. formula* unabbreviate_logic(const formula* f); } } diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index 8373380fc..443a836c9 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -8,9 +8,20 @@ namespace spot { namespace ltl { - /* Return the negative normal form of F, i.e., all negations - of the formula are pushed in front of the atomic propositions. - If NEGATED is true, return the normal form of !F instead. */ + /// \brief Build the negative normal form of \a f. + /// + /// All negations of the formula are pushed in front of the + /// atomic propositions. + /// + /// \param f The formula to normalize. + /// \param negated If \c true, return the negative normal form of + /// \c !f + /// + /// Note that this will not remove abbreviated operators. If you + /// want to remove abbreviations, call spot::ltl::unabbreviate_logic + /// or spot::ltl::unabbreviate_ltl first. (Calling these functions + /// after spot::ltl::negative_normal_form would likely produce a + /// formula which is not in negative normal form.) formula* negative_normal_form(const formula* f, bool negated = false); } } diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh index 8aa652160..347ca0994 100644 --- a/src/ltlvisit/tunabbrev.hh +++ b/src/ltlvisit/tunabbrev.hh @@ -8,6 +8,19 @@ namespace spot { namespace ltl { + /// \brief Clone and rewrite a formula to remove most of the + /// abbreviated LTL and logical operators. + /// + /// The rewriting performed on logical operator is + /// the same as the one done by spot::ltl::unabbreviate_logic_visitor. + /// + /// This will also rewrite unary operators such as unop::F, + /// and unop::G, using only binop::U, and binop::R. + /// + /// This visitor is public, because it's convenient + /// to derive from it and override some of its methods. + /// But if you just want the functionality, consider using + /// spot::ltl::unabbreviate_ltl instead. class unabbreviate_ltl_visitor : public unabbreviate_logic_visitor { typedef unabbreviate_logic_visitor super; @@ -20,6 +33,14 @@ namespace spot formula* recurse(const formula* f); }; + /// \brief Clone and rewrite a formula to remove most of the + /// abbreviated LTL and logical operators. + /// + /// The rewriting performed on logical operator is + /// the same as the one done by spot::ltl::unabbreviate_logic. + /// + /// This will also rewrite unary operators such as unop::F, + /// and unop::G, using only binop::U, and binop::R. formula* unabbreviate_ltl(const formula* f); } }