Added LTL

src/formula/Ltl.h

@@ -0,0 +1,22 @@
+/*
+ * Ltl.h
+ *
+ *  Created on: 22.04.2013
+ *      Author: thomas
+ */
+
+#ifndef LTL_H_
+#define LTL_H_
+
+#include "Ltl/And.h"
+#include "Ltl/Ap.h"
+#include "Ltl/BoundedEventually.h"
+#include "Ltl/BoundedUntil.h"
+#include "Ltl/Eventually.h"
+#include "Ltl/Globally.h"
+#include "Ltl/Next.h"
+#include "Ltl/Not.h"
+#include "Ltl/Or.h"
+#include "Ltl/Until.h"
+
+#endif /* LTL_H_ */

src/formula/Ltl/AbstractLtlFormula.h

@@ -5,12 +5,17 @@
  *      Author: thomas
  */
 
-#ifndef ABSTRACTLTLFORMULA_H_
-#define ABSTRACTLTLFORMULA_H_
+#ifndef STORM_LTL_ABSTRACTLTLFORMULA_H_
+#define STORM_LTL_ABSTRACTLTLFORMULA_H_
+
+#include <vector>
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
+namespace ltl {
 
+template <class T>
 class AbstractLtlFormula {
 public:
 	/**
@@ -32,8 +37,18 @@ public:
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
 	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const = 0;
 };
 
+} /* namespace ltl */
 } /* namespace formula */
 } /* namespace storm */
-#endif /* ABSTRACTLTLFORMULA_H_ */
+#endif /* STORM_LTL_ABSTRACTLTLFORMULA_H_ */

src/formula/Ltl/And.h

@@ -0,0 +1,129 @@
+/*
+ * And.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_LTL_AND_H_
+#define STORM_FORMULA_LTL_AND_H_
+
+#include "AbstractLtlFormula.h"
+#include "src/formula/abstract/And.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+#include <string>
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class And;
+
+/*!
+ *	@brief Interface class for model checkers that support And.
+ *
+ *	All model checkers that support the formula class And must inherit
+ *	this pure virtual class.
+ */
+template <class T>
+class IAndModelChecker {
+	public:
+		/*!
+		 *	@brief Evaluates And formula within a model checker.
+		 *
+		 *	@param obj Formula object with subformulas.
+		 *	@return Result of the formula for every node.
+		 */
+		virtual std::vector<T>* checkAnd(const And<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with AND node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
+ * the model checker works.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class And : public storm::formula::abstract::And<T, AbstractLtlFormula<T>>, public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor.
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 */
+	And() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 * Creates an AND node with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	And(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
+		: storm::formula::abstract::And<T, AbstractLtlFormula<T>>(left, right) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~And() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		And<T>* result = new And();
+		if (this->leftIsSet()) {
+		  result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+		  result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
+	}
+
+};
+
+} //namespace ltl
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_AND_H_ */

src/formula/Ltl/Ap.h

@@ -0,0 +1,98 @@
+/*
+ * Ap.h
+ *
+ *  Created on: 22.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_LTL_AP_H_
+#define STORM_FORMULA_LTL_AP_H_
+
+#include "AbstractLtlFormula.h"
+#include "src/formula/abstract/Ap.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class Ap;
+
+/*!
+ *	@brief Interface class for model checkers that support And.
+ *
+ *	All model checkers that support the formula class And must inherit
+ *	this pure virtual class.
+ */
+template <class T>
+class IApModelChecker {
+	public:
+		/*!
+		 *	@brief Evaluates And formula within a model checker.
+		 *
+		 *	@param obj Formula object with subformulas.
+		 *	@return Result of the formula for every node.
+		 */
+		virtual std::vector<T>* checkAp(const Ap<T>& obj) const = 0;
+};
+
+template <class T>
+class Ap: public storm::formula::abstract::Ap<T>,
+		    public storm::formula::ltl::AbstractLtlFormula<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Ap() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * Creates a new atomic proposition leaf, with the label Ap
+	 *
+	 * @param ap The string representing the atomic proposition
+	 */
+	Ap(std::string ap) :
+		storm::formula::abstract::Ap<T>(ap) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 */
+	virtual ~Ap() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IApModelChecker<T>>.check(*this);
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		return new Ap(this->getAp());
+	}
+};
+
+} /* namespace ltl */
+} /* namespace formula */
+} /* namespace storm */
+#endif /* STORM_FORMULA_LTL_AP_H_ */

src/formula/Ltl/BoundedEventually.h

@@ -0,0 +1,125 @@
+/*
+ * BoundedUntil.h
+ *
+ *  Created on: 27.11.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
+#define STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
+
+#include "src/formula/abstract/BoundedEventually.h"
+#include "AbstractLtlFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class BoundedEventually;
+
+/*!
+ *  @brief Interface class for model checkers that support BoundedEventually.
+ *   
+ *  All model checkers that support the formula class BoundedEventually must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IBoundedEventuallyModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates BoundedEventually formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a BoundedEventually node as root.
+ *
+ * Has one Abstract state formulas as sub formula/tree.
+ *
+ * @par Semantics
+ * The formula holds iff in at most \e bound steps, formula \e child holds.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class BoundedEventually : public storm::formula::abstract::BoundedEventually<T, AbstractLtlFormula<T>>,
+								  public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	BoundedEventually()  {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child formula subtree
+	 * @param bound The maximal number of steps
+	 */
+	BoundedEventually(AbstractLtlFormula<T>* child, uint_fast64_t bound) :
+		storm::formula::abstract::BoundedEventually<T, AbstractLtlFormula<T>>(child, bound){
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~BoundedEventually() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		BoundedEventually<T>* result = new BoundedEventually<T>();
+		result->setBound(this->getBound());
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ */

src/formula/Ltl/BoundedUntil.h

@@ -0,0 +1,130 @@
+/*
+ * BoundedUntil.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
+#define STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
+
+#include "src/formula/abstract/BoundedUntil.h"
+#include "AbstractLtlFormula.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class BoundedUntil;
+
+/*!
+ *  @brief Interface class for model checkers that support BoundedUntil.
+ *   
+ *  All model checkers that support the formula class BoundedUntil must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IBoundedUntilModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates BoundedUntil formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a BoundedUntil node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
+ * \e left holds.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class BoundedUntil : public storm::formula::abstract::BoundedUntil<T, AbstractLtlFormula<T>>,
+							public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	BoundedUntil() {
+		//Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 * @param bound The maximal number of steps
+	 */
+	BoundedUntil(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right,
+					 uint_fast64_t bound) :
+					 storm::formula::abstract::BoundedUntil<T, AbstractLtlFormula<T>>(left,right,bound) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~BoundedUntil() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		BoundedUntil<T>* result = new BoundedUntil<T>();
+		result->setBound(this->getBound());
+		if (this->leftIsSet()) {
+			result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+			result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ */

src/formula/Ltl/Eventually.h

@@ -0,0 +1,119 @@
+/*
+ * Next.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_LTL_EVENTUALLY_H_
+#define STORM_FORMULA_LTL_EVENTUALLY_H_
+
+#include "src/formula/abstract/Eventually.h"
+#include "AbstractLtlFormula.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class Eventually;
+
+/*!
+ *  @brief Interface class for model checkers that support Eventually.
+ *
+ *  All model checkers that support the formula class Eventually must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IEventuallyModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Eventually formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with an Eventually node as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @par Semantics
+ * The formula holds iff eventually \e child holds.
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to nullptr before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Eventually : public storm::formula::abstract::Eventually<T, AbstractLtlFormula<T>>,
+						 public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Eventually() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Eventually(AbstractLtlFormula<T>* child)
+		: storm::formula::abstract::Eventually<T, AbstractLtlFormula<T>>(child) {
+
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+	 */
+	virtual ~Eventually() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new Eventually-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		Eventually<T>* result = new Eventually<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_EVENTUALLY_H_ */

src/formula/Ltl/Globally.h

@@ -0,0 +1,121 @@
+/*
+ * Next.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_LTL_GLOBALLY_H_
+#define STORM_FORMULA_LTL_GLOBALLY_H_
+
+#include "src/formula/abstract/Globally.h"
+#include "AbstractLtlFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class Globally;
+
+/*!
+ *  @brief Interface class for model checkers that support Globally.
+ *   
+ *  All model checkers that support the formula class Globally must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IGloballyModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Globally formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Globally node as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @par Semantics
+ * The formula holds iff globally \e child holds.
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to nullptr before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Globally : public storm::formula::abstract::Globally<T, AbstractLtlFormula<T>>,
+					  public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Globally() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Globally(AbstractLtlFormula<T>* child)
+		: storm::formula::abstract::Globally<T, AbstractLtlFormula<T>>(child) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+	 */
+	virtual ~Globally() {
+	  //intentionally left empty
+	}
+
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new Globally-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		Globally<T>* result = new Globally<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_GLOBALLY_H_ */

src/formula/Ltl/Next.h

@@ -0,0 +1,119 @@
+/*
+ * Next.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_LTL_NEXT_H_
+#define STORM_FORMULA_LTL_NEXT_H_
+
+#include "AbstractLtlFormula.h"
+#include "src/formula/abstract/Next.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class Next;
+
+/*!
+ *  @brief Interface class for model checkers that support Next.
+ *   
+ *  All model checkers that support the formula class Next must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class INextModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Next formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkNext(const Next<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Next node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff in the next step, \e child holds
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Next : public storm::formula::abstract::Next<T, AbstractLtlFormula<T>>,
+				 public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Next() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Next(AbstractLtlFormula<T>* child)
+		: storm::formula::abstract::Next<T, AbstractLtlFormula<T>>(child) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Next() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		Next<T>* result = new Next<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_NEXT_H_ */

src/formula/Ltl/Not.h

@@ -0,0 +1,116 @@
+/*
+ * Not.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_LTL_NOT_H_
+#define STORM_FORMULA_LTL_NOT_H_
+
+#include "AbstractLtlFormula.h"
+#include "src/formula/abstract/Not.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class Not;
+
+/*!
+ *  @brief Interface class for model checkers that support Not.
+ *   
+ *  All model checkers that support the formula class Not must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class INotModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Not formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkNot(const Not<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with NOT node as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Not : public storm::formula::abstract::Not<T, AbstractLtlFormula<T>>,
+			   public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Not() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 * @param child The child node
+	 */
+	Not(AbstractLtlFormula<T>* child) :
+		storm::formula::abstract::Not<T, AbstractLtlFormula<T>>(child){
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * Also deletes the subtree
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Not() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		Not<T>* result = new Not<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_NOT_H_ */

src/formula/Ltl/Or.h

@@ -0,0 +1,105 @@
+/*
+ * Or.h
+ *
+ *  Created on: 22.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_LTL_OR_H_
+#define STORM_FORMULA_LTL_OR_H_
+
+#include "AbstractLtlFormula.h"
+#include "src/formula/abstract/Or.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class And;
+
+/*!
+ *	@brief Interface class for model checkers that support And.
+ *
+ *	All model checkers that support the formula class And must inherit
+ *	this pure virtual class.
+ */
+template <class T>
+class IOrModelChecker {
+	public:
+		/*!
+		 *	@brief Evaluates And formula within a model checker.
+		 *
+		 *	@param obj Formula object with subformulas.
+		 *	@return Result of the formula for every node.
+		 */
+		virtual std::vector<T>* checkOr(const And<T>& obj) const = 0;
+};
+
+template <class T>
+class Or: public storm::formula::abstract::Or<T, AbstractLtlFormula<T>>,
+			 public storm::formula::ltl::AbstractLtlFormula<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Or() {
+		// Intentionally left empty
+
+	}
+
+	/*!
+	 * Constructor
+	 * Creates an OR node with the parameters as subtrees.
+	 *
+	 * @param left The left subformula
+	 * @param right The right subformula
+	 */
+	Or(AbstractLtlFormula<T> left, AbstractLtlFormula<T> right)
+		: storm::formula::abstract::Or<T,AbstractLtlFormula<T>>(left, right) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 */
+	virtual ~Or() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		Or<T>* result = new Or();
+		if (this->leftIsSet()) {
+		  result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+		  result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
+	}
+
+};
+
+} /* namespace ltl */
+} /* namespace formula */
+} /* namespace storm */
+#endif /* OR_H_ */

src/formula/Ltl/Until.h

@@ -0,0 +1,124 @@
+/*
+ * Until.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_LTL_UNTIL_H_
+#define STORM_FORMULA_LTL_UNTIL_H_
+
+#include "AbstractLtlFormula.h"
+#include "src/formula/abstract/Until.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace ltl {
+
+template <class T> class Until;
+
+/*!
+ *  @brief Interface class for model checkers that support Until.
+ *
+ *  All model checkers that support the formula class Until must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IUntilModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Until formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkUntil(const Until<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with an Until node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
+ * \e left holds always.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractLtlFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Until : public storm::formula::abstract::Until<T, AbstractLtlFormula<T>>,
+				  public AbstractLtlFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Until() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 */
+	Until(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
+		: storm::formula::abstract::Until<T, AbstractLtlFormula<T>>(left, right) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Until() {
+	  // Intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractLtlFormula<T>* clone() const {
+		Until<T>* result = new Until();
+		if (this->leftIsSet()) {
+		  result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+		  result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
+	}
+};
+
+} //namespace ltl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_LTL_UNTIL_H_ */