From 1301025bea1932e75c83132071def07537f9a2aa Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 29 May 2013 15:22:19 +0200 Subject: [PATCH] Added visitor pattern for LTL formulas (which hopefully will make the implementation of an adapter to ltl2dstar easier) --- src/formula/Ltl/AbstractLtlFormula.h | 30 ++++++++ src/formula/Ltl/And.h | 22 ++++++ src/formula/Ltl/Ap.h | 23 ++++++ src/formula/Ltl/BoundedEventually.h | 22 ++++++ src/formula/Ltl/BoundedUntil.h | 22 ++++++ src/formula/Ltl/Eventually.h | 22 ++++++ src/formula/Ltl/Globally.h | 22 ++++++ src/formula/Ltl/Next.h | 22 ++++++ src/formula/Ltl/Not.h | 22 ++++++ src/formula/Ltl/Or.h | 22 ++++++ src/formula/Ltl/Until.h | 22 ++++++ .../Ltl/visitor/AbstractLtlFormulaVisitor.cpp | 16 +++++ .../Ltl/visitor/AbstractLtlFormulaVisitor.h | 72 +++++++++++++++++++ 13 files changed, 339 insertions(+) create mode 100644 src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.cpp create mode 100644 src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h index e4afe81c8..f9306a936 100644 --- a/src/formula/Ltl/AbstractLtlFormula.h +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -12,6 +12,21 @@ #include "src/modelchecker/ltl/ForwardDeclarations.h" #include "src/formula/abstract/AbstractFormula.h" +// Forward declaration for formula visitor +namespace storm { +namespace property { +namespace ltl { + +template +class AbstractLtlFormula; + +} +} +} + +#include "visitor/AbstractLtlFormulaVisitor.h" + + namespace storm { namespace property { namespace ltl { @@ -50,6 +65,21 @@ public: * @returns a new AND-object that is identical the called object. */ virtual AbstractLtlFormula* clone() const = 0; + + /*! + * @brief Visits all nodes of a formula tree. + * + * @note Every subclass must implement this method. + * + * This method is given a visitor that visits each node to perform some + * task on it (e.g. Validity checks, conversion, ...). The subclasses are to + * + * + * + * @param visitor The visitor object. + * @return true iff all subtrees are valid. + */ + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const = 0; }; } /* namespace ltl */ diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h index b8f5ad320..2afe2b3fb 100644 --- a/src/formula/Ltl/And.h +++ b/src/formula/Ltl/And.h @@ -38,6 +38,24 @@ class IAndModelChecker { virtual std::vector* checkAnd(const And& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support And. + * + * All visitors that support the formula class And must inherit + * this pure virtual class. + */ +template +class IAndVisitor { + public: + /*! + * @brief Evaluates And formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitAnd(const And& obj) const = 0; +}; + /*! * @brief * Class for an abstract formula tree with AND node as root. @@ -117,6 +135,10 @@ public: return modelChecker.template as()->checkAnd(*this); } + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitAnd(*this); + } + }; } //namespace ltl diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h index 4669c1131..1bf5f2f5b 100644 --- a/src/formula/Ltl/Ap.h +++ b/src/formula/Ltl/Ap.h @@ -35,6 +35,25 @@ class IApModelChecker { virtual std::vector* checkAp(const Ap& obj) const = 0; }; + +/*! + * @brief Interface class for visitors that support Ap. + * + * All visitors that support the formula class Ap must inherit + * this pure virtual class. + */ +template +class IApVisitor { + public: + /*! + * @brief Evaluates And formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitAp(const Ap& obj) const = 0; +}; + /*! * @brief * Class for an abstract formula tree with atomic proposition as root. @@ -98,6 +117,10 @@ public: virtual AbstractLtlFormula* clone() const { return new Ap(this->getAp()); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitAp(*this); + } }; } /* namespace ltl */ diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h index 79868ef8e..acb3a77d0 100644 --- a/src/formula/Ltl/BoundedEventually.h +++ b/src/formula/Ltl/BoundedEventually.h @@ -39,6 +39,24 @@ class IBoundedEventuallyModelChecker { virtual std::vector* checkBoundedEventually(const BoundedEventually& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support BoundedEventually. + * + * All visitors that support the formula class BoundedEventually must inherit + * this pure virtual class. + */ +template +class IBoundedEventuallyVisitor { + public: + /*! + * @brief Evaluates BoundedEventually formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitBoundedEventually(const BoundedEventually& obj) const = 0; +}; + /*! * @brief * Class for an abstract (path) formula tree with a BoundedEventually node as root. @@ -115,6 +133,10 @@ public: virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkBoundedEventually(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitBoundedEventually(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h index 63e6f851f..be33662a7 100644 --- a/src/formula/Ltl/BoundedUntil.h +++ b/src/formula/Ltl/BoundedUntil.h @@ -38,6 +38,24 @@ class IBoundedUntilModelChecker { virtual std::vector* checkBoundedUntil(const BoundedUntil& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support BoundedUntil. + * + * All visitors that support the formula class BoundedUnitl must inherit + * this pure virtual class. + */ +template +class IBoundedUntilVisitor { + public: + /*! + * @brief Visits BoundedUntil formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitBoundedUntil(const BoundedUntil& obj) const = 0; +}; + /*! * @brief * Class for an abstract (path) formula tree with a BoundedUntil node as root. @@ -132,6 +150,10 @@ public: virtual std::vector *check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkBoundedUntil(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitBoundedUntil(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h index 6d5c9a99d..ee6da1243 100644 --- a/src/formula/Ltl/Eventually.h +++ b/src/formula/Ltl/Eventually.h @@ -36,6 +36,24 @@ class IEventuallyModelChecker { virtual std::vector* checkEventually(const Eventually& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support Eventually. + * + * All visitors that support the formula class Eventually must inherit + * this pure virtual class. + */ +template +class IEventuallyVisitor { + public: + /*! + * @brief Visits Eventually formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitEventually(const Eventually& obj) const = 0; +}; + /*! * @brief * Class for an abstract (path) formula tree with an Eventually node as root. @@ -109,6 +127,10 @@ public: virtual std::vector *check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkEventually(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitEventually(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h index 8ac8c5816..0dad8c6ac 100644 --- a/src/formula/Ltl/Globally.h +++ b/src/formula/Ltl/Globally.h @@ -37,6 +37,24 @@ class IGloballyModelChecker { virtual std::vector* checkGlobally(const Globally& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support Globally. + * + * All visitors that support the formula class Globally must inherit + * this pure virtual class. + */ +template +class IGloballyVisitor { + public: + /*! + * @brief Visits Globally formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitGlobally(const Globally& obj) const = 0; +}; + /*! * @brief * Class for an abstract (path) formula tree with a Globally node as root. @@ -111,6 +129,10 @@ public: virtual std::vector *check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkGlobally(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitGlobally(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h index e631755ec..fa8f6f644 100644 --- a/src/formula/Ltl/Next.h +++ b/src/formula/Ltl/Next.h @@ -36,6 +36,24 @@ class INextModelChecker { virtual std::vector* checkNext(const Next& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support Next. + * + * All visitors that support the formula class Next must inherit + * this pure virtual class. + */ +template +class INextVisitor { + public: + /*! + * @brief Visits Next formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitNext(const Next& obj) const = 0; +}; + /*! * @brief * Class for an abstract (path) formula tree with a Next node as root. @@ -109,6 +127,10 @@ public: virtual std::vector *check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkNext(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitNext(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h index 40772b418..88a553e9c 100644 --- a/src/formula/Ltl/Not.h +++ b/src/formula/Ltl/Not.h @@ -36,6 +36,24 @@ class INotModelChecker { virtual std::vector* checkNot(const Not& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support Not. + * + * All visitors that support the formula class Not must inherit + * this pure virtual class. + */ +template +class INotVisitor { + public: + /*! + * @brief Visits Not formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitNot(const Not& obj) const = 0; +}; + /*! * @brief * Class for an abstract formula tree with NOT node as root. @@ -105,6 +123,10 @@ public: virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkNot(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitNot(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h index 4c1e5b535..446fd7982 100644 --- a/src/formula/Ltl/Or.h +++ b/src/formula/Ltl/Or.h @@ -35,6 +35,24 @@ class IOrModelChecker { virtual std::vector* checkOr(const Or& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support Or. + * + * All visitors that support the formula class Or must inherit + * this pure virtual class. + */ +template +class IOrVisitor { + public: + /*! + * @brief Visits Or formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitOr(const Or& obj) const = 0; +}; + /*! * @brief * Class for an abstract formula tree with OR node as root. @@ -111,6 +129,10 @@ public: return modelChecker.template as()->checkOr(*this); } + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitOr(*this); + } + }; } /* namespace ltl */ diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h index 9a02e9a05..3e5720fa1 100644 --- a/src/formula/Ltl/Until.h +++ b/src/formula/Ltl/Until.h @@ -36,6 +36,24 @@ class IUntilModelChecker { virtual std::vector* checkUntil(const Until& obj) const = 0; }; +/*! + * @brief Interface class for visitors that support Until. + * + * All visitors that support the formula class Until must inherit + * this pure virtual class. + */ +template +class IUntilVisitor { + public: + /*! + * @brief Visits Until formula. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual void visitUntil(const Until& obj) const = 0; +}; + /*! * @brief * Class for an abstract (path) formula tree with an Until node as root. @@ -126,6 +144,10 @@ public: virtual std::vector *check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkUntil(*this); } + + virtual void visit(const visitor::AbstractLtlFormulaVisitor& visitor) const { + visitor.template as()->visitUntil(*this); + } }; } //namespace ltl diff --git a/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.cpp b/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.cpp new file mode 100644 index 000000000..99653fca2 --- /dev/null +++ b/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.cpp @@ -0,0 +1,16 @@ +/* + * AbstractLtlFormulaVisitor.cpp + * + * Created on: 29.05.2013 + * Author: thomas + */ + +#include "AbstractLtlFormulaVisitor.h" + +namespace storm { +namespace property { +namespace visitor { + +} /* namespace visitor */ +} /* namespace property */ +} /* namespace storm */ diff --git a/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h b/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h new file mode 100644 index 000000000..b77d58973 --- /dev/null +++ b/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h @@ -0,0 +1,72 @@ +/* + * AbstractLtlFormulaVisitor.h + * + * Created on: 29.05.2013 + * Author: thomas + */ + +#ifndef STORM_PROPERTY_LTL_VISITOR_ABSTRACTLTLFORMULAVISITOR_H_ +#define STORM_PROPERTY_LTL_VISITOR_ABSTRACTLTLFORMULAVISITOR_H_ + +// Forward declaration of visitor +namespace storm { +namespace property { +namespace ltl { +namespace visitor { + +template +class AbstractLtlFormulaVisitor; + +} /* namespace visitor */ +} +} +} + +#include "../AbstractLtlFormula.h" +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +#include + +extern log4cplus::Logger logger; + +namespace storm { +namespace property { +namespace ltl { +namespace visitor { + +template +class AbstractLtlFormulaVisitor { +public: + virtual ~AbstractLtlFormulaVisitor() { + // TODO Auto-generated destructor stub + } + + + /*! + * Returns a pointer to the model checker object that is of the requested type as given by the template parameters. + * @returns A pointer to the model checker object that is of the requested type as given by the template parameters. + * If the model checker is not of the requested type, type casting will fail and result in an exception. + */ + template