Added visitor pattern for LTL formulas

(which hopefully will make the implementation of an adapter to ltl2dstar
easier)

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 T>
+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<T>* 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<T>& visitor) const = 0;
 };
 
 } /* namespace ltl */

src/formula/Ltl/And.h

@@ -38,6 +38,24 @@ class IAndModelChecker {
 		virtual std::vector<T>* checkAnd(const And<T>& 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 T>
+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<T>& obj) const = 0;
+};
+
 /*!
  * @brief
  * Class for an abstract formula tree with AND node as root.
@@ -117,6 +135,10 @@ public:
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IAndVisitor>()->visitAnd(*this);
+	}
+
 };
 
 } //namespace ltl

src/formula/Ltl/Ap.h

@@ -35,6 +35,25 @@ class IApModelChecker {
 		virtual std::vector<T>* checkAp(const Ap<T>& 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 T>
+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<T>& obj) const = 0;
+};
+
 /*!
  * @brief
  * Class for an abstract formula tree with atomic proposition as root.
@@ -98,6 +117,10 @@ public:
 	virtual AbstractLtlFormula<T>* clone() const {
 		return new Ap(this->getAp());
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IApVisitor>()->visitAp(*this);
+	}
 };
 
 } /* namespace ltl */

src/formula/Ltl/BoundedEventually.h

@@ -39,6 +39,24 @@ class IBoundedEventuallyModelChecker {
         virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& 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 T>
+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<T>& 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<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IBoundedEventuallyVisitor>()->visitBoundedEventually(*this);
+	}
 };
 
 } //namespace ltl

src/formula/Ltl/BoundedUntil.h

@@ -38,6 +38,24 @@ class IBoundedUntilModelChecker {
         virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& 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 T>
+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<T>& 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<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IBoundedUntilVisitor>()->visitBoundedUntil(*this);
+	}
 };
 
 } //namespace ltl

src/formula/Ltl/Eventually.h

@@ -36,6 +36,24 @@ class IEventuallyModelChecker {
         virtual std::vector<T>* checkEventually(const Eventually<T>& 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 T>
+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<T>& 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<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IEventuallyVisitor>()->visitEventually(*this);
+	}
 };
 
 } //namespace ltl

src/formula/Ltl/Globally.h

@@ -37,6 +37,24 @@ class IGloballyModelChecker {
         virtual std::vector<T>* checkGlobally(const Globally<T>& 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 T>
+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<T>& 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<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IGloballyVisitor>()->visitGlobally(*this);
+	}
 };
 
 } //namespace ltl

src/formula/Ltl/Next.h

@@ -36,6 +36,24 @@ class INextModelChecker {
         virtual std::vector<T>* checkNext(const Next<T>& 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 T>
+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<T>& 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<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<INextVisitor>()->visitNext(*this);
+	}
 };
 
 } //namespace ltl

src/formula/Ltl/Not.h

@@ -36,6 +36,24 @@ class INotModelChecker {
         virtual std::vector<T>* checkNot(const Not<T>& 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 T>
+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<T>& obj) const = 0;
+};
+
 /*!
  * @brief
  * Class for an abstract formula tree with NOT node as root.
@@ -105,6 +123,10 @@ public:
 	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<INotVisitor>()->visitNot(*this);
+	}
 };
 
 } //namespace ltl

src/formula/Ltl/Or.h

@@ -35,6 +35,24 @@ class IOrModelChecker {
 		virtual std::vector<T>* checkOr(const Or<T>& 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 T>
+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<T>& obj) const = 0;
+};
+
 /*!
  * @brief
  * Class for an abstract formula tree with OR node as root.
@@ -111,6 +129,10 @@ public:
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IOrVisitor>()->visitOr(*this);
+	}
+
 };
 
 } /* namespace ltl */

src/formula/Ltl/Until.h

@@ -36,6 +36,24 @@ class IUntilModelChecker {
         virtual std::vector<T>* checkUntil(const Until<T>& 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 T>
+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<T>& 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<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
+
+	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+		visitor.template as<IUntilVisitor>()->visitUntil(*this);
+	}
 };
 
 } //namespace ltl

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 */

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 T>
+class AbstractLtlFormulaVisitor;
+
+} /* namespace visitor */
+}
+}
+}
+
+#include "../AbstractLtlFormula.h"
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+#include <typeinfo>
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+namespace property {
+namespace ltl {
+namespace visitor {
+
+template <class T>
+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 <template <class Type> class Target>
+	const Target<T>* as() const {
+		try {
+			const Target<T>* target = dynamic_cast<const Target<T>*>(this);
+			return target;
+		} catch (std::bad_cast& bc) {
+			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<T>).name() << ".");
+			throw bc;
+		}
+		return nullptr;
+	}
+
+	void visit(storm::property::ltl::AbstractLtlFormula<T> const& formula) {
+		formula.visit(*this);
+	}
+};
+
+} /* namespace visitor */
+} /* namespace ltl*/
+} /* namespace property */
+} /* namespace storm */
+#endif /* STORM_PROPERTY_LTL_VISITOR_ABSTRACTLTLFORMULAVISITOR_H_ */