alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2003-04-18 15:02:55 +00:00
parent 4b8b02e811
commit d35817ccd9
19 changed files with 239 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,5 +1,17 @@
2003-04-18 Alexandre DURET-LUTZ <aduret@src.lip6.fr>
* 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.

4
doc/Doxyfile.in
View file

@ -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 =

7
src/ltlast/atomic_prop.hh
View file

@ -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_;

15
src/ltlast/binop.hh
View file

@ -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:

8
src/ltlast/constant.hh
View file

@ -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:

4
src/ltlast/formula.hh
View file

@ -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:

30
src/ltlast/multop.hh
View file

@ -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:

5
src/ltlast/unop.hh
View file

@ -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:

47
src/ltlast/visitor.hh
View file

@ -2,29 +2,44 @@
# define SPOT_LTLAST_VISITOR_HH
#include "predecl.hh"
#include "misc/const_sel.hh"
namespace spot {
namespace ltl {
template <bool WantConst>
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<atomic_prop, WantConst>::t* node)
= 0;
virtual void visit(typename const_sel<constant, WantConst>::t* node)
= 0;
virtual void visit(typename const_sel<binop, WantConst>::t* node) = 0;
virtual void visit(typename const_sel<unop, WantConst>::t* node) = 0;
virtual void visit(typename const_sel<multop, WantConst>::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<false> {};
struct const_visitor : public generic_visitor<true> {};
}
}

8
src/ltlenv/defaultenv.hh
View file

@ -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();

28
src/ltlenv/environment.hh
View file

@ -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.
};

26
src/ltlparse/public.hh
View file

@ -13,16 +13,38 @@ namespace spot
{
namespace ltl
{
/// \brief A parse diagnostic with its location.
typedef std::pair<yy::Location, std::string> parse_error;
/// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<parse_error> 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);

9
src/ltlvisit/clone.hh
View file

@ -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);
}
}

6
src/ltlvisit/dotty.hh
View file

@ -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);
}
}

7
src/ltlvisit/dump.hh
View file

@ -1,13 +1,18 @@
#ifndef SPOT_LTLVISIT_DUMP_HH
# define SPOT_LTLVISIT_DUMP_HH
#include <ltlast/formula.hh>
#include "ltlast/formula.hh"
#include <iostream>
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);
}
}

17
src/ltlvisit/equals.hh
View file

@ -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);
}
}

19
src/ltlvisit/lunabbrev.hh
View file

@ -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);
}
}

17
src/ltlvisit/nenoform.hh
View file

@ -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);
}
}

21
src/ltlvisit/tunabbrev.hh
View file

@ -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);
}
}