Done with PrCTL.

- Began removing NoBoundFormulas, since they might not be needed anymore. This task will be taken over by filters if they are to be implemented.

Next up: CSL


Former-commit-id: 6164f73737

src/formula/Prctl.h

@@ -17,7 +17,6 @@
 #include "Prctl/Next.h"
 #include "Prctl/Not.h"
 #include "Prctl/Or.h"
-#include "Prctl/ProbabilisticNoBoundOperator.h"
 #include "Prctl/ProbabilisticBoundOperator.h"
 
 #include "Prctl/Until.h"
@@ -29,12 +28,10 @@
 #include "Prctl/CumulativeReward.h"
 #include "Prctl/ReachabilityReward.h"
 #include "Prctl/RewardBoundOperator.h"
-#include "Prctl/RewardNoBoundOperator.h"
 #include "Prctl/SteadyStateReward.h"
 
 #include "Prctl/AbstractPrctlFormula.h"
 #include "Prctl/AbstractStateFormula.h"
-#include "Prctl/AbstractNoBoundOperator.h"
 #include "Prctl/AbstractPathFormula.h"
 
 #include "modelchecker/prctl/AbstractModelChecker.h"

src/formula/Prctl/AbstractNoBoundOperator.h

@@ -1,83 +0,0 @@
-/*
- * AbstractNoBoundOperator.h
- *
- *  Created on: 16.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
-
-#include "src/formula/AbstractFormula.h"
-#include "src/formula/abstract/IOptimizingOperator.h"
-
-namespace storm {
-namespace property {
-namespace prctl {
-
-template <class T>
-class AbstractNoBoundOperator;
-
-/*!
- *  @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 INoBoundOperatorModelChecker {
-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> checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
-
-
-};
-
-/*!
- * Interface class for all PRCTL No bound operators
- */
-template <class T>
-class AbstractNoBoundOperator: public storm::property::AbstractFormula<T>,
-										 public virtual storm::property::IOptimizingOperator {
-public:
-	AbstractNoBoundOperator() {
-		// Intentionally left empty.
-
-	}
-	virtual ~AbstractNoBoundOperator() {
-		// 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
-	 *
-	 * @note This function is not implemented in this class.
-	 * @returns a new AND-object that is identical the called object.
-	 */
-	virtual AbstractNoBoundOperator<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.
-	 *
-	 * @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::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
-};
-
-} /* namespace prctl */
-} /* namespace property */
-} /* namespace storm */
-#endif /* STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ */

src/formula/Prctl/AbstractPathFormula.h

@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 
-#include "src/formula/AbstractFormula.h"
+#include "src/formula/Prctl/AbstractPrctlFormula.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 #include <vector>
@@ -31,7 +31,7 @@ namespace prctl {
  * @note This class is intentionally not derived from AbstractPrctlFormula, as path formulas are not complete PRCTL formulas.
  */
 template <class T>
-class AbstractPathFormula : public virtual storm::property::AbstractFormula<T> {
+class AbstractPathFormula : public virtual storm::property::prctl::AbstractPrctlFormula<T> {
 
 public:
 	/*!

src/formula/Prctl/AbstractPrctlFormula.h

@@ -0,0 +1,31 @@
+/*
+ * AbstractPrctlFormula.h
+ *
+ *  Created on: 16.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_
+#define STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_
+
+#include "src/formula/AbstractFormula.h"
+
+namespace storm {
+namespace property {
+namespace prctl {
+
+/*!
+ * Interface class for all PRCTL root formulas.
+ */
+template<class T>
+class AbstractPrctlFormula : public virtual storm::property::AbstractFormula<T> {
+public:
+	virtual ~AbstractPrctlFormula() {
+		// Intentionally left empty
+	}
+};
+
+} /* namespace prctl */
+} /* namespace property */
+} /* namespace storm */
+#endif /* ABSTRACTPRCTLFORMULA_H_ */

src/formula/Prctl/AbstractStateFormula.h

@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 
-#include "src/formula/AbstractFormula.h"
+#include "src/formula/Prctl/AbstractPrctlFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
@@ -26,7 +26,7 @@ namespace prctl {
  * 	   clone().
  */
 template <class T>
-class AbstractStateFormula : public virtual storm::property::AbstractFormula<T> {
+class AbstractStateFormula : public virtual storm::property::prctl::AbstractPrctlFormula<T> {
 
 public:
 	/*!

src/formula/Prctl/BoundedEventually.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_
 #define STORM_FORMULA_PRCTL_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"
@@ -56,15 +55,14 @@ class IBoundedEventuallyModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class BoundedEventually : public storm::property::abstract::BoundedEventually<T, AbstractStateFormula<T>>,
-								  public AbstractPathFormula<T> {
+class BoundedEventually : public AbstractPathFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	BoundedEventually()  {
-		//intentionally left empty
+	BoundedEventually() : child(nullptr), bound(0){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -73,9 +71,8 @@ public:
 	 * @param child The child formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) :
-		storm::property::abstract::BoundedEventually<T, AbstractStateFormula<T>>(child, bound){
-		//intentionally left empty
+	BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) : child(child), bound(bound){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -85,7 +82,9 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~BoundedEventually() {
-	  //intentionally left empty
+	  if (child != nullptr) {
+		  delete child;
+	  }
 	}
 
 	/*!
@@ -117,6 +116,70 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "F<=";
+		result += std::to_string(bound);
+		result += " ";
+		result += child->toString();
+		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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool childIsSet() const {
+		return child != nullptr;
+	}
+
+	/*!
+	 * @returns the maximally allowed number of steps for the bounded until operator
+	 */
+	uint_fast64_t getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the maximally allowed number of steps for the bounded until operator
+	 *
+	 * @param bound the new bound.
+	 */
+	void setBound(uint_fast64_t bound) {
+		this->bound = bound;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
+	uint_fast64_t bound;
 };
 
 } //namespace prctl

src/formula/Prctl/BoundedNaryUntil.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_
 #define STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_
 
-#include "src/formula/abstract/BoundedNaryUntil.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
 #include "src/formula/Prctl/AbstractStateFormula.h"
 #include <cstdint>
@@ -63,15 +62,16 @@ class IBoundedNaryUntilModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class BoundedNaryUntil : public storm::property::abstract::BoundedNaryUntil<T, AbstractStateFormula<T>>,
-								 public AbstractPathFormula<T> {
+class BoundedNaryUntil : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	BoundedNaryUntil() {
-
+		this->left = nullptr;
+		this->right = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
 	}
 
 	/*!
@@ -80,9 +80,9 @@ public:
 	 * @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::property::abstract::BoundedNaryUntil<T, AbstractStateFormula<T>>(left, right){
-
+	BoundedNaryUntil(AbstractStateFormula<T>* left, std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right) {
+		this->left = left;
+		this->right = right;
 	}
 
 	/*!
@@ -92,10 +92,14 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~BoundedNaryUntil() {
-		//intentionally left empty
+	  if (left != nullptr) {
+		  delete left;
+	  }
+	  if (right != nullptr) {
+		  delete right;
+	  }
 	}
 
-
 	/*!
 	 * Clones the called object.
 	 *
@@ -132,6 +136,89 @@ public:
 		return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::stringstream result;
+		result << "( " << left->toString();
+		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+			result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString();
+		}
+		result << ")";
+		return result.str();
+	}
+
+	/*!
+     *  @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		bool res = checker.validate(this->left);
+		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+			res &= checker.validate(std::get<0>(*it));
+		}
+		return res;
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(AbstractStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	void setRight(std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 *
+	 * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool leftIsSet() const {
+		return left != nullptr;
+	}
+
+	/*!
+	 *
+	 * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool rightIsSet() const {
+		return right != nullptr;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void addRight(AbstractStateFormula<T>* newRight, T upperBound, T lowerBound) {
+		this->right->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(newRight, upperBound, lowerBound));
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractStateFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child nodes.
+	 */
+	const std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>& getRight() const {
+		return *right;
+	}
+
+
+private:
+	AbstractStateFormula<T>* left;
+	std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right;
 };
 
 } //namespace prctl

src/formula/Prctl/BoundedUntil.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_
 #define STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_
 
-#include "src/formula/abstract/BoundedUntil.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
 #include "src/formula/Prctl/AbstractStateFormula.h"
 #include <cstdint>
@@ -56,15 +55,15 @@ class IBoundedUntilModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class BoundedUntil : public storm::property::abstract::BoundedUntil<T, AbstractStateFormula<T>>,
-							public AbstractPathFormula<T> {
+class BoundedUntil : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	BoundedUntil() {
-		//Intentionally left empty
+	BoundedUntil() : left(nullptr), right(nullptr), bound(0){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -74,12 +73,11 @@ public:
 	 * @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::property::abstract::BoundedUntil<T, AbstractStateFormula<T>>(left,right,bound) {
-		//intentionally left empty
+	BoundedUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right, uint_fast64_t bound) {
+		this->left = left;
+		this->right = right;
+		this->bound = bound;
 	}
-
 	/*!
 	 * Destructor.
 	 *
@@ -87,7 +85,12 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~BoundedUntil() {
-	  //intentionally left empty
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
 	}
 
 	/*!
@@ -122,6 +125,97 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = left->toString();
+		result += " U<=";
+		result += std::to_string(bound);
+		result += " ";
+		result += right->toString();
+		return result;
+	}
+
+	/*!
+	 *  @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->left) && checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool leftIsSet() const {
+		return left != nullptr;
+	}
+
+	/*!
+	 *
+	 * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool rightIsSet() const {
+		return right != nullptr;
+	}
+
+	/*!
+	 * @returns the maximally allowed number of steps for the bounded until operator
+	 */
+	uint_fast64_t getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the maximally allowed number of steps for the bounded until operator
+	 *
+	 * @param bound the new bound.
+	 */
+	void setBound(uint_fast64_t bound) {
+		this->bound = bound;
+	}
+
+private:
+	AbstractStateFormula<T>* left;
+	AbstractStateFormula<T>* right;
+	uint_fast64_t bound;
 };
 
 } //namespace prctl

src/formula/Prctl/CumulativeReward.h

@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/CumulativeReward.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
@@ -49,14 +48,13 @@ class ICumulativeRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class CumulativeReward : public storm::property::abstract::CumulativeReward<T>,
-								 public AbstractPathFormula<T> {
+class CumulativeReward : public AbstractPathFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	CumulativeReward() {
+	CumulativeReward() : bound(0){
 		// Intentionally left empty
 	}
 
@@ -65,9 +63,8 @@ public:
 	 *
 	 * @param bound The time bound of the reward formula
 	 */
-	CumulativeReward(T bound) :
-		storm::property::abstract::CumulativeReward<T>(bound) {
-		// Intentionally left empty
+	CumulativeReward(T bound) : bound(bound){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -101,6 +98,46 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "C <= ";
+		result += std::to_string(bound);
+		return result;
+	}
+
+	/*!
+	 *  @brief Checks if all subtrees conform to some logic.
+	 *
+	 *  As CumulativeReward objects have no subformulas, we return true here.
+	 *
+	 *  @param checker Formula checker object.
+	 *  @return true
+	 */
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+		return true;
+	}
+
+	/*!
+	 * @returns the time instance for the instantaneous reward operator
+	 */
+	T getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the the time instance for the instantaneous reward operator
+	 *
+	 * @param bound the new bound.
+	 */
+	void setBound(T bound) {
+		this->bound = bound;
+	}
+
+private:
+	T bound;
 };
 
 } //namespace prctl

src/formula/Prctl/Eventually.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_PRCTL_EVENTUALLY_H_
 #define STORM_FORMULA_PRCTL_EVENTUALLY_H_
 
-#include "src/formula/abstract/Eventually.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
 #include "src/formula/Prctl/AbstractStateFormula.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
@@ -53,15 +52,15 @@ class IEventuallyModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class Eventually : public storm::property::abstract::Eventually<T, AbstractStateFormula<T>>,
-						 public AbstractPathFormula<T> {
+class Eventually : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	Eventually() {
-		// Intentionally left empty
+	Eventually() : child(nullptr) {
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -69,9 +68,8 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Eventually(AbstractStateFormula<T>* child)
-		: storm::property::abstract::Eventually<T, AbstractStateFormula<T>>(child) {
-
+	Eventually(AbstractStateFormula<T>* child) : child(child){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -81,7 +79,9 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
 	 */
 	virtual ~Eventually() {
-		//intentionally left empty
+	  if (child != nullptr) {
+		  delete child;
+	  }
 	}
 
 	/*!
@@ -111,6 +111,51 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "F ";
+		result += child->toString();
+		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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool childIsSet() const {
+		return child != nullptr;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
 };
 
 } //namespace prctl

src/formula/Prctl/Globally.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_
 #define STORM_FORMULA_PRCTL_GLOBALLY_H_
 
-#include "src/formula/abstract/Globally.h"
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
@@ -54,15 +53,15 @@ class IGloballyModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class Globally : public storm::property::abstract::Globally<T, AbstractStateFormula<T>>,
-					  public AbstractPathFormula<T> {
+class Globally : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	Globally() {
-		//intentionally left empty
+	Globally() : child(nullptr){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -70,9 +69,8 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Globally(AbstractStateFormula<T>* child)
-		: storm::property::abstract::Globally<T, AbstractStateFormula<T>>(child) {
-		//intentionally left empty
+	Globally(AbstractStateFormula<T>* child) : child(child){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -82,7 +80,9 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
 	 */
 	virtual ~Globally() {
-	  //intentionally left empty
+	  if (child != nullptr) {
+		  delete child;
+	  }
 	}
 
 
@@ -113,6 +113,51 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "G ";
+		result += child->toString();
+		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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool childIsSet() const {
+		return child != nullptr;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
 };
 
 } //namespace prctl

src/formula/Prctl/InstantaneousReward.h

@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/InstantaneousReward.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
 #include <string>
@@ -50,15 +49,15 @@ class IInstantaneousRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class InstantaneousReward : public storm::property::abstract::InstantaneousReward<T>,
-									 public AbstractPathFormula<T> {
+class InstantaneousReward : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	InstantaneousReward() {
-		//intentionally left empty
+	InstantaneousReward() : bound(0) {
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -66,9 +65,8 @@ public:
 	 *
 	 * @param bound The time instance of the reward formula
 	 */
-	InstantaneousReward(uint_fast64_t bound) :
-		storm::property::abstract::InstantaneousReward<T>(bound) {
-		//intentionally left empty
+	InstantaneousReward(uint_fast64_t bound) : bound(bound) {
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -102,6 +100,46 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "I=";
+		result += std::to_string(bound);
+		return result;
+	}
+
+	/*!
+	 *  @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return true;
+	}
+
+	/*!
+	 * @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;
+	}
+
+private:
+	uint_fast64_t bound;
 };
 
 } //namespace prctl

src/formula/Prctl/Next.h

@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/Next.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -53,15 +52,15 @@ class INextModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class Next : public storm::property::abstract::Next<T, AbstractStateFormula<T>>,
-				 public AbstractPathFormula<T> {
+class Next : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	Next() {
-		//intentionally left empty
+	Next() : child(nullptr){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -69,19 +68,20 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Next(AbstractStateFormula<T>* child)
-		: storm::property::abstract::Next<T, AbstractStateFormula<T>>(child) {
-		//intentionally left empty
+	Next(AbstractStateFormula<T>* child) : child(child){
+		// Intentionally left empty.
 	}
 
 	/*!
 	 * Constructor.
 	 *
 	 * Also deletes the subtree.
-	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 * (this behavior can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~Next() {
-	  //intentionally left empty
+	  if (child != NULL) {
+		  delete child;
+	  }
 	}
 
 	/*!
@@ -111,6 +111,53 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "(";
+		result += " X ";
+		result += child->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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool childIsSet() const {
+		return child != nullptr;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
 };
 
 } //namespace prctl

src/formula/Prctl/Not.h

@@ -129,7 +129,7 @@ public:
 	/*!
 	 * @returns The child node
 	 */
-	const FormulaType& getChild() const {
+	const AbstractStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -137,7 +137,7 @@ public:
 	 * Sets the subtree
 	 * @param child the new child node
 	 */
-	void setChild(FormulaType* child) {
+	void setChild(AbstractStateFormula<T>* child) {
 		this->child = child;
 	}
 

src/formula/Prctl/Or.h

@@ -70,7 +70,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	Or(FormulaType* left, FormulaType* right) {
+	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -148,7 +148,7 @@ public:
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(FormulaType* newLeft) {
+	void setLeft(AbstractStateFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -157,21 +157,21 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(FormulaType* newRight) {
+	void setRight(AbstractStateFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const FormulaType& getLeft() const {
+	const AbstractStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const FormulaType& getRight() const {
+	const AbstractStateFormula<T>& getRight() const {
 		return *right;
 	}
 

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -11,6 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
 #include "utility/constants.h"
+#include "src/formula/ComparisonType.h"
 
 namespace storm {
 namespace property {
@@ -52,54 +53,39 @@ class IProbabilisticBoundOperatorModelChecker {
  * @see AbstractPrctlFormula
  */
 template<class T>
-class ProbabilisticBoundOperator : public storm::property::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>,
-											  public AbstractStateFormula<T> {
+class ProbabilisticBoundOperator : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticBoundOperator()  {
-		// Intentionally left empty
+	ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr) {
+		// Intentionally left empty.
 	}
 
-
 	/*!
-	 * Constructor
+	 * Constructor for non-optimizing operator.
 	 *
-	 * @param comparisonRelation The relation to compare the actual value and the bound
+	 * @param comparisonOperator The relation for the bound.
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	ProbabilisticBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			AbstractPathFormula<T>* pathFormula)
-			: storm::property::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 *
-	 * @param comparisonRelation
-	 * @param bound
-	 * @param pathFormula
-	 * @param minimumOperator
-	 */
-	ProbabilisticBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			AbstractPathFormula<T>* pathFormula,
-			bool minimumOperator)
-			: storm::property::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula, minimumOperator){
-		// Intentionally left empty
+	ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
+		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+		// Intentionally left empty.
 	}
 
 	/*!
+	 * Destructor
 	 *
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
 	virtual ~ProbabilisticBoundOperator() {
-		// Intentionally left empty
+	 if (pathFormula != nullptr) {
+		 delete pathFormula;
+	 }
 	}
 
 	/*!
@@ -129,6 +115,101 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->pathFormula);
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "P ";
+		switch (comparisonOperator) {
+		case LESS: result += "<"; break;
+		case LESS_EQUAL: result += "<="; break;
+		case GREATER: result += ">"; break;
+		case GREATER_EQUAL: result += ">="; break;
+		}
+		result += " ";
+		result += std::to_string(bound);
+		result += " [";
+		result += pathFormula->toString();
+		result += "]";
+		return result;
+	}
+
+	/*!
+	 * @returns the child node (representation of a formula)
+	 */
+	const AbstractPathFormula<T>& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(AbstractPathFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 *
+	 * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool pathFormulaIsSet() const {
+		return pathFormula != nullptr;
+	}
+
+	/*!
+	 * @returns the comparison relation
+	 */
+	const storm::property::ComparisonType getComparisonOperator() const {
+		return comparisonOperator;
+	}
+
+	void setComparisonOperator(storm::property::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;
+	}
+
+	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;
+		}
+	}
+
+private:
+	storm::property::ComparisonType comparisonOperator;
+	T bound;
+	AbstractPathFormula<T>* pathFormula;
 };
 
 } //namespace prctl

src/formula/Prctl/ProbabilisticNoBoundOperator.h

@@ -1,115 +0,0 @@
-/*
- * ProbabilisticNoBoundOperator.h
- *
- *  Created on: 12.12.2012
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
-
-#include "AbstractPathFormula.h"
-#include "AbstractNoBoundOperator.h"
-#include "src/formula/abstract/ProbabilisticNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace prctl {
-
-/*!
- * @brief
- * Class for an 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 AbstractPrctlFormula
- */
-template <class T>
-class ProbabilisticNoBoundOperator: public storm::property::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>,
-												public AbstractNoBoundOperator<T> {
-public:
-	/*!
-	 * Empty constructor
-	 */
-	ProbabilisticNoBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula)
-		: storm::property::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
-		: storm::property::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula, minimumOperator) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~ProbabilisticNoBoundOperator() {
-		// Intentionally left empty
-	}
-
-	virtual AbstractNoBoundOperator<T>* clone() const override {
-		ProbabilisticNoBoundOperator<T>* result = new ProbabilisticNoBoundOperator<T>();
-		if (this->pathFormulaIsSet()) {
-			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.
-	 *
-	 * @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::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
-		return this->getPathFormula().check(modelChecker, qualitative);
-	}
-};
-
-} //namespace prctl
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/Prctl/ReachabilityReward.h

@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "../abstract/Eventually.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -50,14 +49,13 @@ class IReachabilityRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class ReachabilityReward : public storm::property::abstract::Eventually<T, AbstractStateFormula<T>>,
-									public AbstractPathFormula<T> {
+class ReachabilityReward : public AbstractPathFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	ReachabilityReward() {
+	ReachabilityReward() : child(nullptr){
 		// Intentionally left empty
 	}
 
@@ -66,8 +64,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	ReachabilityReward(AbstractStateFormula<T>* child) :
-		storm::property::abstract::Eventually<T, AbstractStateFormula<T>>(child){
+	ReachabilityReward(AbstractStateFormula<T>* child) : child(child){
 		// Intentionally left empty
 	}
 
@@ -78,7 +75,9 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
 	 */
 	virtual ~ReachabilityReward() {
-		// Intentionally left empty
+		if (child != nullptr) {
+			delete child;
+		}
 	}
 
 	/*!
@@ -108,6 +107,51 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "F ";
+		result += child->toString();
+		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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool childIsSet() const {
+		return child != nullptr;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
 };
 
 } //namespace prctl

src/formula/Prctl/RewardBoundOperator.h

@@ -10,8 +10,8 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/RewardBoundOperator.h"
 #include "utility/constants.h"
+#include "src/formula/ComparisonType.h"
 
 namespace storm {
 namespace property {
@@ -52,48 +52,38 @@ class IRewardBoundOperatorModelChecker {
  * @see AbstractPrctlFormula
  */
 template<class T>
-class RewardBoundOperator : public storm::property::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>,
-									 public AbstractStateFormula<T> {
+class RewardBoundOperator : public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardBoundOperator() {
+	RewardBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr){
 		// Intentionally left empty
 	}
 
 	/*!
-	 * Constructor
+	 * Constructor for non-optimizing operator.
 	 *
-	 * @param comparisonRelation The relation to compare the actual value and the bound
+	 * @param comparisonOperator The relation for the bound.
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	RewardBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			AbstractPathFormula<T>* pathFormula) :
-				storm::property::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
+	RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
+		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
 
-
 	/*!
-	 * Constructor
+	 * Destructor
 	 *
-	 * @param comparisonRelation
-	 * @param bound
-	 * @param pathFormula
-	 * @param minimumOperator
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
-	RewardBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			AbstractPathFormula<T>* pathFormula,
-			bool minimumOperator)
-			: storm::property::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula, minimumOperator) {
-		// Intentionally left empty
+	virtual ~RewardBoundOperator() {
+	 if (pathFormula != nullptr) {
+		 delete pathFormula;
+	 }
 	}
 
 	/*!
@@ -123,6 +113,101 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IRewardBoundOperatorModelChecker>()->checkRewardBoundOperator(*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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->pathFormula);
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "R ";
+		switch (comparisonOperator) {
+		case LESS: result += "<"; break;
+		case LESS_EQUAL: result += "<="; break;
+		case GREATER: result += ">"; break;
+		case GREATER_EQUAL: result += ">="; break;
+		}
+		result += " ";
+		result += std::to_string(bound);
+		result += " [";
+		result += pathFormula->toString();
+		result += "]";
+		return result;
+	}
+
+	/*!
+	 * @returns the child node (representation of a formula)
+	 */
+	const AbstractPathFormula<T>& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(AbstractPathFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 *
+	 * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool pathFormulaIsSet() const {
+		return pathFormula != nullptr;
+	}
+
+	/*!
+	 * @returns the comparison relation
+	 */
+	const storm::property::ComparisonType getComparisonOperator() const {
+		return comparisonOperator;
+	}
+
+	void setComparisonOperator(storm::property::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;
+	}
+
+	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;
+		}
+	}
+
+private:
+	storm::property::ComparisonType comparisonOperator;
+	T bound;
+	AbstractPathFormula<T>* pathFormula;
 };
 
 } //namespace prctl

src/formula/Prctl/RewardNoBoundOperator.h

@@ -1,108 +0,0 @@
-/*
- * RewardNoBoundOperator.h
- *
- *  Created on: 25.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
-
-#include "AbstractNoBoundOperator.h"
-#include "AbstractPathFormula.h"
-#include "src/formula/abstract/RewardNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace prctl {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a R (reward) operator without declaration of reward values
- * as root.
- *
- * Checking a formula with this operator as root returns the reward for the reward path formula 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 checkRewardNoBoundOperator 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 AbstractPrctlFormula
- */
-template <class T>
-class RewardNoBoundOperator: public storm::property::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>,
-									  public storm::property::prctl::AbstractNoBoundOperator<T> {
-public:
-	/*!
-	 * Empty constructor
-	 */
-	RewardNoBoundOperator()  {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula)
-		: storm::property::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
-		: storm::property::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula, minimumOperator) {
-		// Intentionally left empty
-	}
-
-	virtual AbstractNoBoundOperator<T>* clone() const override {
-		RewardNoBoundOperator<T>* result = new RewardNoBoundOperator<T>();
-		if (this->pathFormulaIsSet()) {
-			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.
-	 *
-	 * @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::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
-		return this->getPathFormula().check(modelChecker, qualitative);
-	}
-};
-
-} //namespace prctl
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_ */

src/formula/Prctl/SteadyStateReward.h

@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/SteadyStateReward.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
@@ -46,8 +45,7 @@ class ISteadyStateRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class SteadyStateReward: public storm::property::abstract::SteadyStateReward<T>,
-								 public AbstractPathFormula<T> {
+class SteadyStateReward: public AbstractPathFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -83,6 +81,25 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ISteadyStateRewardModelChecker>()->checkSteadyStateReward(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		return "S";
+	}
+
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  As SteadyStateReward objects have no subformulas, we return true here.
+     *
+     *  @param checker Formula checker object.
+     *  @return true
+     */
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+		return true;
+	}
 };
 
 } //namespace prctl

src/formula/Prctl/Until.h

@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/Until.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -54,15 +53,15 @@ class IUntilModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class Until : public storm::property::abstract::Until<T, AbstractStateFormula<T>>,
-				  public AbstractPathFormula<T> {
+class Until : public AbstractPathFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	Until() {
-		// Intentionally left empty
+	Until() : left(nullptr), right(nullptr){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -71,9 +70,8 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
-		: storm::property::abstract::Until<T, AbstractStateFormula<T>>(left, right) {
-		// Intentionally left empty
+	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) : left(left), right(right){
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -83,7 +81,12 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~Until() {
-	  // Intentionally left empty
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
 	}
 
 	/*!
@@ -116,6 +119,78 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = left->toString();
+		result += " U ";
+		result += right->toString();
+		return result;
+	}
+
+	/*!
+	 *  @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->left) && checker.validate(this->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;
+	}
+
+	/*!
+	 *
+	 * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool leftIsSet() const {
+		return left != nullptr;
+	}
+
+	/*!
+	 *
+	 * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool rightIsSet() const {
+		return right != nullptr;
+	}
+
+private:
+	AbstractStateFormula<T>* left;
+	AbstractStateFormula<T>* right;
 };
 
 } //namespace prctl

src/modelchecker/prctl/AbstractModelChecker.h

@@ -56,7 +56,6 @@ class AbstractModelChecker :
 	public virtual storm::property::prctl::INextModelChecker<Type>,
 	public virtual storm::property::prctl::IBoundedUntilModelChecker<Type>,
 	public virtual storm::property::prctl::IBoundedEventuallyModelChecker<Type>,
-	public virtual storm::property::prctl::INoBoundOperatorModelChecker<Type>,
 	public virtual storm::property::prctl::IProbabilisticBoundOperatorModelChecker<Type>,
 	public virtual storm::property::prctl::IRewardBoundOperatorModelChecker<Type>,
 	public virtual storm::property::prctl::IReachabilityRewardModelChecker<Type>,