Derived PRCTL formula classes from abstract ones

src/formula/Prtl/AbstractPathFormula.h → src/formula/Prctl/AbstractPathFormula.h

@@ -12,7 +12,7 @@ namespace storm { namespace formula {
 template <class T> class AbstractPathFormula;
 }}
 
-#include "src/formula/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
 #include <vector>
@@ -21,6 +21,7 @@ template <class T> class AbstractPathFormula;
 
 namespace storm {
 namespace formula {
+namespace prctl {
 
 /*!
  * @brief
@@ -32,13 +33,13 @@ namespace formula {
  * 	   clone().
  */
 template <class T>
-class AbstractPathFormula : public virtual AbstractFormula<T> {
+class AbstractPathFormula : public virtual storm::formula::abstract::AbstractFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~AbstractPathFormula() { }
+	virtual ~AbstractPathFormula() = 0;
 
 	/*!
 	 * Clones the called object.
@@ -64,6 +65,7 @@ public:
 	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
 };
 
+} //namespace prctl
 } //namespace formula
 } //namespace storm
 

src/formula/Prtl/AbstractStateFormula.h → src/formula/Prctl/AbstractStateFormula.h

@@ -12,12 +12,13 @@ namespace storm { namespace formula {
 template <class T> class AbstractStateFormula;
 }}
 
-#include "src/formula/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
+namespace prctl {
 
 /*!
  * @brief
@@ -29,13 +30,13 @@ namespace formula {
  * 	   clone().
  */
 template <class T>
-class AbstractStateFormula : public AbstractFormula<T> {
+class AbstractStateFormula : public storm::formula::abstract::AbstractFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~AbstractStateFormula() { }
+	virtual ~AbstractStateFormula() = 0;
 
 	/*!
 	 * Clones the called object.
@@ -61,6 +62,7 @@ public:
 	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const = 0; // {
 };
 
+} //namespace prctl
 } //namespace formula
 } //namespace storm
 

src/formula/Prctl/And.h

@@ -0,0 +1,129 @@
+/*
+ * And.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_PRCTL_AND_H_
+#define STORM_FORMULA_PRCTL_AND_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/And.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+#include <string>
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 storm::storage::BitVector* 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 AbstractStateFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class And : public storm::formula::abstract::And<T, AbstractStateFormula<T>>, public AbstractStateFormula<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 note with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
+		: storm::formula::abstract::And<T, AbstractStateFormula<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 AbstractStateFormula<T>* clone() const {
+		And<T>* result = new And();
+		if (this->left != NULL) {
+		  result->setLeft(left->clone());
+		}
+		if (this->right != NULL) {
+		  result->setRight(right->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 storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
+	}
+
+};
+
+} //namespace prctl
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_PRCTL_AND_H_ */

src/formula/Prctl/BoundedEventually.h

@@ -0,0 +1,126 @@
+/*
+ * BoundedUntil.h
+ *
+ *  Created on: 27.11.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
+#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
+
+#include "src/formula/abstract/BoundedEventually.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl{
+
+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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class BoundedEventually : public storm::formula::abstract::BoundedEventually<T, AbstractStateFormula<T>>,
+								  public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	BoundedEventually()  {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child formula subtree
+	 * @param bound The maximal number of steps
+	 */
+	BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) :
+		storm::formula::abstract::BoundedEventually<T, AbstractStateFormula<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 AbstractPathFormula<T>* clone() const {
+		BoundedEventually<T>* result = new BoundedEventually<T>();
+		result->setBound(bound);
+		if (child != nullptr) {
+			result->setChild(child->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 prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */

src/formula/Prctl/BoundedNaryUntil.h

@@ -0,0 +1,141 @@
+/*
+ * BoundedNaryUntil.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_
+#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_
+
+#include "src/formula/abstract/BoundedNaryUntil.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+#include <vector>
+#include <tuple>
+#include <sstream>
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+
+template <class T> class BoundedNaryUntil;
+
+/*!
+ *  @brief Interface class for model checkers that support BoundedNaryUntil.
+ *   
+ *  All model checkers that support the formula class BoundedNaryUntil must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IBoundedNaryUntilModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates BoundedNaryUntil formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root.
+ *
+ * Has at least two Abstract state formulas as sub formulas and an interval
+ * associated with all but the first sub formula. We'll call the first one
+ * \e left and all other one \e right.
+ *
+ * @par Semantics
+ * The formula holds iff \e left holds until eventually any of the \e right
+ * formulas holds after a number of steps contained in the interval
+ * associated with this formula.
+ *
+ * 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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class BoundedNaryUntil : public storm::formula::abstract::BoundedNaryUntil<T, AbstractStateFormula<T>>,
+								 public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	BoundedNaryUntil() {
+
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 */
+	BoundedNaryUntil(AbstractStateFormula<T>* left, std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right) :
+		storm::formula::abstract::BoundedNaryUntil<T, AbstractStateFormula<T>>(left, right){
+
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~BoundedNaryUntil() {
+		//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 BoundedNaryUntil-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>();
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newright = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
+			for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+				newright->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it)));
+			}
+			result->setRight(newright);
+		}
+		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<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
+	}
+
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */

src/formula/Prctl/BoundedUntil.h

@@ -0,0 +1,131 @@
+/*
+ * BoundedUntil.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
+#define STORM_FORMULA_BOUNDEDUNTIL_H_
+
+#include "src/formula/abstract/BoundedUntil.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class BoundedUntil : public storm::formula::abstract::BoundedUntil<T, AbstractStateFormula>,
+							public AbstractPathFormula<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(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
+					 uint_fast64_t bound) :
+					 storm::formula::abstract::BoundedUntil<T, AbstractStateFormula>(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 AbstractPathFormula<T>* clone() const {
+		BoundedUntil<T>* result = new BoundedUntil<T>();
+		result->setBound(bound);
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			result->setRight(right->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 prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */

src/formula/Csl/CumulativeReward.h → src/formula/Prctl/CumulativeReward.h

@@ -10,12 +10,13 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/formula/abstract/CumulativeReward.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
 namespace storm {
-
 namespace formula {
+namespace prctl {
 
 template <class T> class CumulativeReward;
 
@@ -48,7 +49,8 @@ class ICumulativeRewardModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class CumulativeReward : public AbstractPathFormula<T> {
+class CumulativeReward : public storm::formula::abstract::CumulativeReward<T>,
+								 public AbstractPathFormula<T> {
 
 public:
 	/*!
@@ -140,8 +142,8 @@ private:
 	T bound;
 };
 
+} //namespace prctl
 } //namespace formula
-
 } //namespace storm
 
 #endif /* STORM_FORMULA_INSTANTANEOUSREWARD_H_ */

src/formula/Prctl/Eventually.h

@@ -0,0 +1,120 @@
+/*
+ * Next.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_EVENTUALLY_H_
+#define STORM_FORMULA_EVENTUALLY_H_
+
+#include "src/formula/abstract/Eventually.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Eventually : public storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>,
+						 public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Eventually() {
+		this->child = nullptr;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Eventually(AbstractStateFormula<T>* child)
+		: storm::formula::abstract::Eventually<T, AbstractStateFormula<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 AbstractPathFormula<T>* clone() const {
+		Eventually<T>* result = new Eventually<T>();
+		if (child != nullptr) {
+			result->setChild(child);
+		}
+		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 prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_EVENTUALLY_H_ */

src/formula/Prctl/Globally.h

@@ -0,0 +1,132 @@
+/*
+ * Next.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_GLOBALLY_H_
+#define STORM_FORMULA_GLOBALLY_H_
+
+#include "src/formula/abstract/Globally.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Globally : public storm::formula::abstract::Globally<T, AbstractStateFormula<T>>,
+					  public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Globally() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Globally(AbstractStateFormula<T>* child)
+		: storm::formula::abstract::Globally<T, AbstractStateFormula<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 AbstractPathFormula<T>* clone() const {
+		Next<T>* result = new Next<T>();
+		if (child != nullptr) {
+			result->setChild(child);
+		}
+		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);
+	}
+	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_GLOBALLY_H_ */

src/formula/Prtl/InstantaneousReward.h → src/formula/Prctl/InstantaneousReward.h

@@ -10,13 +10,14 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/formula/abstract/InstantaneousReward.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 
 namespace storm {
-
 namespace formula {
+namespace prctl {
 
 template <class T> class InstantaneousReward;
 
@@ -49,14 +50,15 @@ class IInstantaneousRewardModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class InstantaneousReward : public AbstractPathFormula<T> {
+class InstantaneousReward : public storm::formula::abstract::InstantaneousReward,
+									 public AbstractPathFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
 	InstantaneousReward() {
-		bound = 0;
+		//intentionally left empty
 	}
 
 	/*!
@@ -64,8 +66,9 @@ public:
 	 *
 	 * @param bound The time instance of the reward formula
 	 */
-	InstantaneousReward(uint_fast64_t bound) {
-		this->bound = bound;
+	InstantaneousReward(uint_fast64_t bound) :
+		storm::formula::abstract::InstantaneousReward<T>(bound) {
+		//intentionally left empty
 	}
 
 	/*!
@@ -75,31 +78,6 @@ public:
 		// Intentionally left empty.
 	}
 
-	/*!
-	 * @returns the time instance for the instantaneous reward operator
-	 */
-	uint_fast64_t getBound() const {
-		return bound;
-	}
-
-	/*!
-	 * Sets the the time instance for the instantaneous reward operator
-	 *
-	 * @param bound the new bound.
-	 */
-	void setBound(uint_fast64_t bound) {
-		this->bound = bound;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = "I=";
-		result += std::to_string(bound);
-		return result;
-	}
-
 	/*!
 	 * Clones the called object.
 	 *
@@ -124,25 +102,10 @@ public:
 	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this, qualitative);
 	}
-	
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     *  
-     *  As InstantaneousReward formulas have no subformulas, we return true here.
-     * 
-     *  @param checker Formula checker object.
-     *  @return true
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return true;
-	}
-
-private:
-	uint_fast64_t bound;
 };
 
+} //namespace prctl
 } //namespace formula
-
 } //namespace storm
 
 #endif /* STORM_FORMULA_INSTANTANEOUSREWARD_H_ */

src/formula/Prctl/Next.h

@@ -0,0 +1,120 @@
+/*
+ * Next.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_NEXT_H_
+#define STORM_FORMULA_NEXT_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Next.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Next : public storm::formula::abstract::Next<T, AbstractStateFormula<T>>,
+				 public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Next() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Next(AbstractStateFormula<T>* child)
+		: storm::formula::abstract::Next<T, AbstractStateFormula<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 AbstractPathFormula<T>* clone() const {
+		Next<T>* result = new Next<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		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 prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_NEXT_H_ */

src/formula/Prctl/Not.h

@@ -0,0 +1,152 @@
+/*
+ * Not.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_NOT_H_
+#define STORM_FORMULA_NOT_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 storm::storage::BitVector* 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 AbstractStateFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Not : public AbstractStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Not() {
+		this->child = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 * @param child The child node
+	 */
+	Not(AbstractStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * Also deletes the subtree
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Not() {
+	  if (child != NULL) {
+		  delete child;
+	  }
+	}
+
+	/*!
+	 * @returns The child node
+	 */
+	const AbstractStateFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "!";
+		result += child->toString();
+		return result;
+	}
+
+	/*!
+	 * 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 AbstractStateFormula<T>* clone() const {
+		Not<T>* result = new Not<T>();
+		if (child != NULL) {
+			result->setChild(child->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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
+	}
+	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+
+private:
+	AbstractStateFormula<T>* child;
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_NOT_H_ */

src/formula/Prctl/Or.h

@@ -0,0 +1,187 @@
+/*
+ * Or.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_OR_H_
+#define STORM_FORMULA_OR_H_
+
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+template <class T> class Or;
+
+/*!
+ *  @brief Interface class for model checkers that support Or.
+ *   
+ *  All model checkers that support the formula class Or must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IOrModelChecker {
+	public:
+		/*!
+         *  @brief Evaluates Or formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+		virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with OR node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * As OR 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 AbstractStateFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Or : public AbstractStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor.
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 */
+	Or() {
+		left = NULL;
+		right = NULL;
+	}
+
+	/*!
+	 * Constructor.
+	 * Creates an AND note with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Or() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(AbstractStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractStateFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractStateFormula<T>& getRight() const {
+		return *right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "(";
+		result += left->toString();
+		result += " | ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * 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 AbstractStateFormula<T>* clone() const {
+		Or<T>* result = new Or();
+		if (this->left != NULL) {
+		  result->setLeft(left->clone());
+		}
+		if (this->right != NULL) {
+		  result->setRight(right->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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
+	}
+	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
+
+private:
+	AbstractStateFormula<T>* left;
+	AbstractStateFormula<T>* right;
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_OR_H_ */

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -0,0 +1,130 @@
+/*
+ * ProbabilisticBoundOperator.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
+#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
+
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "src/formula/PathBoundOperator.h"
+#include "src/formula/OptimizingOperator.h"
+#include "utility/ConstTemplates.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+template <class T> class ProbabilisticBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support ProbabilisticBoundOperator.
+ *
+ *  All model checkers that support the formula class PathBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IProbabilisticBoundOperatorModelChecker {
+    public:
+        virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
+ * as root.
+ *
+ * Has one Abstract path formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the probability that the path formula holds is inside the bounds
+ * 	  specified in this operator
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see AbstractFormula
+ */
+template<class T>
+class ProbabilisticBoundOperator : public PathBoundOperator<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticBoundOperator() : PathBoundOperator<T>
+		(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonRelation The relation to compare the actual value and the bound
+	 * @param bound The bound for the probability
+	 * @param pathFormula The child node
+	 */
+	ProbabilisticBoundOperator(
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
+			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+		// Intentionally left empty
+	}
+
+	ProbabilisticBoundOperator(
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "P ";
+		result += PathBoundOperator<T>::toString();
+		return result;
+	}
+
+	/*!
+	 * 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 AbstractStateFormula<T>* clone() const {
+		ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
+		result->setComparisonOperator(this->getComparisonOperator());
+		result->setBound(this->getBound());
+		result->setPathFormula(this->getPathFormula().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 storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
+	}
+};
+
+} //namespace formula
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */

src/formula/Prctl/ProbabilisticNoBoundOperator.h

@@ -0,0 +1,91 @@
+/*
+ * ProbabilisticNoBoundOperator.h
+ *
+ *  Created on: 12.12.2012
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
+
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
+#include "PathNoBoundOperator.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
+ * as root.
+ *
+ * Checking a formula with this operator as root returns the probabilities that the path formula holds
+ * (for each state)
+ *
+ * Has one Abstract path formula as sub formula/tree.
+ *
+ * @note
+ * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
+ * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
+ *
+ * @note
+ * 	This class does not contain a check() method like the other formula classes.
+ * 	The check method should only be called by the model checker to infer the correct check function for sub
+ * 	formulas. As this operator can only appear at the root, the method is not useful here.
+ * 	Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead.
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticIntervalOperator
+ * @see AbstractFormula
+ */
+template <class T>
+class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "P";
+		result += PathNoBoundOperator<T>::toString();
+		return result;
+	}
+};
+
+} //namespace formula
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/Prtl/ReachabilityReward.h → src/formula/Prctl/ReachabilityReward.h

@@ -14,6 +14,7 @@
 
 namespace storm {
 namespace formula {
+namespace prctl {
 
 template <class T> class ReachabilityReward;
 
@@ -145,6 +146,7 @@ private:
 	AbstractStateFormula<T>* child;
 };
 
+} //namespace prctl
 } //namespace formula
 } //namespace storm
 

src/formula/Prtl/RewardBoundOperator.h → src/formula/Prctl/RewardBoundOperator.h

@@ -15,6 +15,7 @@
 
 namespace storm {
 namespace formula {
+namespace prctl {
 
 template <class T> class RewardBoundOperator;
 
@@ -118,6 +119,7 @@ public:
 	}
 };
 
+} //namespace prctl
 } //namespace formula
 } //namespace storm
 

src/formula/Prtl/RewardNoBoundOperator.h → src/formula/Prctl/RewardNoBoundOperator.h

@@ -14,6 +14,7 @@
 
 namespace storm {
 namespace formula {
+namespace prctl {
 
 /*!
  * @brief
@@ -83,7 +84,8 @@ public:
 	}
 };
 
-} /* namespace formula */
-} /* namespace storm */
+} //namespace prctl
+} //namespace formula
+} //namespace storm
 
 #endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */

src/formula/Prctl/StateBoundOperator.h

@@ -0,0 +1,199 @@
+/*
+ * BoundOperator.h
+ *
+ *  Created on: 27.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_
+#define STORM_FORMULA_STATEBOUNDOPERATOR_H_
+
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/utility/ConstTemplates.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+template <class T> class StateBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support StateBoundOperator.
+ *   
+ *  All model checkers that support the formula class StateBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IStateBoundOperatorModelChecker {
+    public:
+        virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
+ * as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the probability that the state formula holds is inside the bounds
+ * 	  specified in this operator
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see AbstractFormula
+ */
+template<class T>
+class StateBoundOperator : public AbstractStateFormula<T> {
+
+public:
+	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
+
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonOperator The relation for the bound.
+	 * @param bound The bound for the probability
+	 * @param stateFormula The child node
+	 */
+	StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula)
+		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~StateBoundOperator() {
+	 if (stateFormula != nullptr) {
+		 delete stateFormula;
+	 }
+	}
+
+	/*!
+	 * @returns the child node (representation of a Abstract state formula)
+	 */
+	const AbstractStateFormula<T>& getStateFormula () const {
+		return *stateFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param stateFormula the state formula that becomes the new child node
+	 */
+	void setStateFormula(AbstractStateFormula<T>* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
+	/*!
+	 * @returns the comparison relation
+	 */
+	const ComparisonType getComparisonOperator() const {
+		return comparisonOperator;
+	}
+
+	void setComparisonOperator(ComparisonType comparisonOperator) {
+		this->comparisonOperator = comparisonOperator;
+	}
+
+	/*!
+	 * @returns the bound for the measure
+	 */
+	const T& getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the interval in which the probability that the path formula holds may lie in.
+	 *
+	 * @param bound The bound for the measure
+	 */
+	void setBound(T bound) {
+		this->bound = bound;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = " ";
+		switch (comparisonOperator) {
+		case LESS: result += "< "; break;
+		case LESS_EQUAL: result += "<= "; break;
+		case GREATER: result += "> "; break;
+		case GREATER_EQUAL: result += ">= "; break;
+		}
+		result += std::to_string(bound);
+		result += " [";
+		result += stateFormula->toString();
+		result += "]";
+		return result;
+	}
+
+	bool meetsBound(T value) const {
+		switch (comparisonOperator) {
+		case LESS: return value < bound; break;
+		case LESS_EQUAL: return value <= bound; break;
+		case GREATER: return value > bound; break;
+		case GREATER_EQUAL: return value >= bound; break;
+		default: return false;
+		}
+	}
+
+	/*!
+	 * 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 AbstractStateFormula<T>* clone() const = 0;
+
+	/*!
+	 * 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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IStateBoundOperatorModelChecker>()->checkStateBoundOperator(*this);
+	}
+	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->stateFormula);
+    }
+
+private:
+	ComparisonType comparisonOperator;
+	T bound;
+	AbstractStateFormula<T>* stateFormula;
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */

src/formula/Prctl/StateNoBoundOperator.h

@@ -0,0 +1,150 @@
+/*
+ * StateNoBoundOperator.h
+ *
+ *  Created on: 09.04.2013
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_STATENOBOUNDOPERATOR_H_
+#define STORM_FORMULA_STATENOBOUNDOPERATOR_H_
+
+#include "src/formula/AbstractFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+template <class T> class StateNoBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support PathNoBoundOperator.
+ *
+ *  All model checkers that support the formula class NoBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IStateNoBoundOperatorModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates NoBoundOperator formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkStateNoBoundOperator(const StateNoBoundOperator<T>& obj) const = 0;
+};
+
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with an operator without declaration of probabilities
+ * as root.
+ *
+ * Checking a formula with this operator as root returns the probabilities that the path formula holds
+ * (for each state)
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @note
+ * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
+ * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
+ *
+ * @note
+ * 	This class does not contain a check() method like the other formula classes.
+ * 	The check method should only be called by the model checker to infer the correct check function for sub
+ * 	formulas. As this operator can only appear at the root, the method is not useful here.
+ * 	Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead.
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see SteadyStateNoBoundOperator
+ * @see AbstractFormula
+ */
+template <class T>
+class StateNoBoundOperator: public storm::formula::AbstractFormula<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	StateNoBoundOperator() {
+		stateFormula = nullptr;
+	}
+
+	/*!
+	 * Constructor
+	 */
+	StateNoBoundOperator(AbstractStateFormula<T>* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * Deletes the subtree
+	 */
+	virtual ~StateNoBoundOperator() {
+		if (stateFormula != nullptr) {
+			delete stateFormula;
+		}
+	}
+
+	const AbstractStateFormula<T>& getStateFormula() const {
+		return *(this->stateFormula);
+	}
+
+	void setStateFormula(AbstractStateFormula<T>* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
+	/*!
+	 * 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 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<IStateNoBoundOperatorModelChecker>()->checkStateNoBoundOperator(*this);
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result;
+		result += " = ? [";
+		result += this->getStateFormula().toString();
+		result += "]";
+		return result;
+	}
+
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->stateFormula);
+	}
+
+private:
+	AbstractStateFormula<T>* stateFormula;
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+#endif /* STORM_FORMULA_STATENOBOUNDOPERATOR_H_ */

src/formula/Prtl/SteadyStateReward.h → src/formula/Prctl/SteadyStateReward.h

@@ -15,6 +15,7 @@
 
 namespace storm {
 namespace formula {
+namespace prctl {
 
 template <class T> class SteadyStateReward;
 
@@ -101,6 +102,7 @@ public:
 	}
 };
 
-} /* namespace formula */
-} /* namespace storm */
+} //namespace prctl
+} //namespace formula
+} //namespace storm
 #endif /* STORM_FORMULA_STEADYSTATEREWARD_H_ */

src/formula/Prctl/Until.h

@@ -0,0 +1,185 @@
+/*
+ * Until.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_UNTIL_H_
+#define STORM_FORMULA_UNTIL_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Until : public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Until() {
+		this->left = NULL;
+		this->right = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 */
+	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Until() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(AbstractStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractStateFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractStateFormula<T>& getRight() const {
+		return *right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = left->toString();
+		result += " U ";
+		result += right->toString();
+		return result;
+	}
+
+	/*!
+	 * 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 AbstractPathFormula<T>* clone() const {
+		Until<T>* result = new Until();
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			result->setRight(right->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);
+	}
+	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
+
+private:
+	AbstractStateFormula<T>* left;
+	AbstractStateFormula<T>* right;
+};
+
+} //namespace prctl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_UNTIL_H_ */