Further work on the formuolas.

- Finished the third and last logic: Csl.
- Note that nothing compiles as of yet. This is due to the removal of the NoBoundOperators wich are expected to be replaced by filters.


Former-commit-id: d26ae768f7

src/formula/Csl.h

@@ -15,9 +15,7 @@
 #include "Csl/Next.h"
 #include "Csl/Not.h"
 #include "Csl/Or.h"
-#include "Csl/ProbabilisticNoBoundOperator.h"
 #include "Csl/ProbabilisticBoundOperator.h"
-#include "Csl/SteadyStateNoBoundOperator.h"
 #include "Csl/SteadyStateBoundOperator.h"
 
 #include "Csl/Until.h"

src/formula/Csl/AbstractCslFormula.h

@@ -8,7 +8,7 @@
 #ifndef ABSTRACTCSLFORMULA_H_
 #define ABSTRACTCSLFORMULA_H_
 
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
 
 namespace storm {
 namespace property {
@@ -18,7 +18,7 @@ namespace csl {
  * Abstract base class for all CSL root formulas.
  */
 template <class T>
-class AbstractCslFormula : public virtual storm::property::abstract::AbstractFormula<T>{
+class AbstractCslFormula : public virtual storm::property::AbstractFormula<T>{
 public:
 	virtual ~AbstractCslFormula() {
 		// Intentionally left empty

src/formula/Csl/AbstractNoBoundOperator.h

@@ -1,83 +0,0 @@
-/*
- * AbstractNoBoundOperator.h
- *
- *  Created on: 16.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_
-
-#include "AbstractCslFormula.h"
-#include "src/formula/abstract/IOptimizingOperator.h"
-
-namespace storm {
-namespace property {
-namespace csl {
-
-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 CSL No Bound operators.
- */
-template <class T>
-class AbstractNoBoundOperator: public AbstractCslFormula<T>,
-										 public virtual storm::property::abstract::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::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
-};
-
-} /* namespace csl */
-} /* namespace property */
-} /* namespace storm */
-#endif /* STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ */

src/formula/Csl/AbstractPathFormula.h

@@ -16,7 +16,7 @@ template<class T> class AbstractPathFormula;
 } //namespace property
 } //namespace storm
 
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/Csl/AbstractCslFormula.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
 #include <vector>
@@ -40,7 +40,7 @@ namespace csl {
  * 		This class is intentionally not derived from AbstractCslFormula, as a path formula is not a complete CSL formula.
  */
 template <class T>
-class AbstractPathFormula : public virtual storm::property::abstract::AbstractFormula<T> {
+class AbstractPathFormula : public virtual storm::property::csl::AbstractCslFormula<T> {
 
 public:
 	/*!

src/formula/Csl/AbstractStateFormula.h

@@ -8,15 +8,7 @@
 #ifndef STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_
 #define STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_
 
-namespace storm {
-namespace property {
-namespace csl {
-template<class T> class AbstractStateFormula;
-}
-}
-}
-
-#include "AbstractCslFormula.h"
+#include "src/formula/Csl/AbstractCslFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
@@ -34,7 +26,7 @@ namespace csl {
  * 	   clone().
  */
 template <class T>
-class AbstractStateFormula : public AbstractCslFormula<T> {
+class AbstractStateFormula : public storm::property::csl::AbstractCslFormula<T> {
 
 public:
 	/*!

src/formula/Csl/And.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_CSL_AND_H_
 #define STORM_FORMULA_CSL_AND_H_
 
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/And.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 #include <string>
@@ -54,15 +53,17 @@ class IAndModelChecker {
  * @see AbstractCslFormula
  */
 template <class T>
-class And : public storm::property::abstract::And<T, AbstractStateFormula<T>>, public AbstractStateFormula<T> {
+class And : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor.
 	 * Will create an AND-node without subnotes. Will not represent a complete formula!
 	 */
 	And() {
-		//intentionally left empty
+		left = NULL;
+		right = NULL;
 	}
 
 	/*!
@@ -72,9 +73,9 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
-		: storm::property::abstract::And<T, AbstractStateFormula<T>>(left, right) {
-		//intentionally left empty
+	And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
 	}
 
 	/*!
@@ -84,7 +85,12 @@ public:
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
 	virtual ~And() {
-		//intentionally left empty
+		if (left != NULL) {
+			delete left;
+		}
+		if (right != NULL) {
+			delete right;
+		}
 	}
 
 	/*!
@@ -118,6 +124,80 @@ public:
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "(";
+		result += left->toString();
+		result += " & ";
+		result += right->toString();
+		result += ")";
+		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 csl

src/formula/Csl/Ap.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_CSL_AP_H_
 #define STORM_FORMULA_CSL_AP_H_
 
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Ap.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
@@ -47,10 +46,10 @@ class IApModelChecker {
  * @see AbstractStateFormula
  */
 template <class T>
-class Ap : public storm::property::abstract::Ap<T>,
-			  public AbstractStateFormula<T> {
+class Ap : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Constructor
 	 *
@@ -58,9 +57,8 @@ public:
 	 *
 	 * @param ap The string representing the atomic proposition
 	 */
-	Ap(std::string ap)
-		: storm::property::abstract::Ap<T>(ap) {
-		// Intentionally left empty
+	Ap(std::string ap) {
+		this->ap = ap;
 	}
 
 	/*!
@@ -95,6 +93,36 @@ public:
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *	As atomic propositions 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 name of the atomic proposition
+	 */
+	const std::string& getAp() const {
+		return ap;
+	}
+
+	/*!
+	 * @returns a string representation of the leaf.
+	 *
+	 */
+	virtual std::string toString() const override {
+		return getAp();
+	}
+
+private:
+	std::string ap;
+
 };
 
 } //namespace abstract

src/formula/Csl/Eventually.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_CSL_EVENTUALLY_H_
 #define STORM_FORMULA_CSL_EVENTUALLY_H_
 
-#include "src/formula/abstract/Eventually.h"
 #include "src/formula/Csl/AbstractPathFormula.h"
 #include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
@@ -53,15 +52,15 @@ class IEventuallyModelChecker {
  * @see AbstractCslFormula
  */
 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::csl::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 csl

src/formula/Csl/Globally.h

@@ -8,9 +8,8 @@
 #ifndef STORM_FORMULA_CSL_GLOBALLY_H_
 #define STORM_FORMULA_CSL_GLOBALLY_H_
 
-#include "src/formula/abstract/Globally.h"
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
@@ -54,15 +53,15 @@ class IGloballyModelChecker {
  * @see AbstractCslFormula
  */
 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,10 +80,11 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
 	 */
 	virtual ~Globally() {
-	  //intentionally left empty
+	  if (child != nullptr) {
+		  delete child;
+	  }
 	}
 
-
 	/*!
 	 * Clones the called object.
 	 *
@@ -113,6 +112,51 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::csl::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 csl

src/formula/Csl/Next.h

@@ -8,9 +8,8 @@
 #ifndef STORM_FORMULA_CSL_NEXT_H_
 #define STORM_FORMULA_CSL_NEXT_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Next.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -53,15 +52,15 @@ class INextModelChecker {
  * @see AbstractCslFormula
  */
 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::csl::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 csl

src/formula/Csl/Not.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_CSL_NOT_H_
 #define STORM_FORMULA_CSL_NOT_H_
 
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Not.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
@@ -50,24 +49,23 @@ class INotModelChecker {
  * @see AbstractCslFormula
  */
 template <class T>
-class Not : public storm::property::abstract::Not<T, AbstractStateFormula<T>>,
-			   public AbstractStateFormula<T> {
+class Not : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	Not() {
-		//intentionally left empty
+		this->child = NULL;
 	}
 
 	/*!
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(AbstractStateFormula<T>* child) :
-		storm::property::abstract::Not<T, AbstractStateFormula<T>>(child){
-		//intentionally left empty
+	Not(AbstractStateFormula<T>* child) {
+		this->child = child;
 	}
 
 	/*!
@@ -77,7 +75,9 @@ public:
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
 	virtual ~Not() {
-	  //intentionally left empty
+	  if (child != NULL) {
+		  delete child;
+	  }
 	}
 
 	/*!
@@ -107,6 +107,51 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string 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 node is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool childIsSet() const {
+		return child != nullptr;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
 };
 
 } //namespace csl

src/formula/Csl/Or.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_CSL_OR_H_
 #define STORM_FORMULA_CSL_OR_H_
 
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Or.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -52,39 +51,45 @@ class IOrModelChecker {
  * @see AbstractCslFormula
  */
 template <class T>
-class Or : public storm::property::abstract::Or<T, AbstractStateFormula<T>>,
-			  public AbstractStateFormula<T> {
+class Or : public AbstractStateFormula<T> {
 
 public:
-	/*!
-	 * Empty constructor.
-	 * Will create an OR-node without subnotes. The result does not represent a complete formula!
-	 */
-	Or() {
-		//intentionally left empty
-	}
 
 	/*!
-	 * Constructor.
-	 * Creates an OR 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) :
-		storm::property::abstract::Or<T, AbstractStateFormula<T>>(left, right) {
-		//intentionally left empty
-	}
+		 * Empty constructor.
+		 * Will create an OR-node without subnotes. Will not represent a complete formula!
+		 */
+		Or() {
+			left = NULL;
+			right = NULL;
+		}
 
-	/*!
-	 * Destructor.
-	 *
-	 * The subtrees are deleted with the object
-	 * (this behavior can be prevented by setting them to NULL before deletion)
-	 */
-	virtual ~Or() {
-	  //intentionally left empty
-	}
+		/*!
+		 * Constructor.
+		 * Creates an OR 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;
+		  }
+		}
 
 	/*!
 	 * Clones the called object.
@@ -116,6 +121,81 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "(";
+		result += left->toString();
+		result += " | ";
+		result += right->toString();
+		result += ")";
+		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 csl

src/formula/Csl/ProbabilisticBoundOperator.h

@@ -8,9 +8,9 @@
 #ifndef STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_
 #define STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_
 
-#include "AbstractStateFormula.h"
-#include "AbstractPathFormula.h"
-#include "src/formula/abstract/ProbabilisticBoundOperator.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/ComparisonType.h"
 #include "utility/constants.h"
 
 namespace storm {
@@ -53,36 +53,39 @@ class IProbabilisticBoundOperatorModelChecker {
  * @see AbstractCslFormula
  */
 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() : storm::property::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>
-		(LESS_EQUAL, storm::utility::constantZero<T>(), nullptr) {
-		// 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
+	ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
+		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+		// Intentionally left empty.
 	}
 
-	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
+	/*!
+	 * Destructor
+	 *
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~ProbabilisticBoundOperator() {
+	 if (pathFormula != nullptr) {
+		 delete pathFormula;
+	 }
 	}
 
 	/*!
@@ -112,6 +115,101 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::csl::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 csl

src/formula/Csl/ProbabilisticNoBoundOperator.h

@@ -1,115 +0,0 @@
-/*
- * ProbabilisticNoBoundOperator.h
- *
- *  Created on: 12.12.2012
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_
-
-#include "AbstractPathFormula.h"
-#include "AbstractNoBoundOperator.h"
-#include "src/formula/abstract/ProbabilisticNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace csl {
-
-/*!
- * @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 DtmccslModelChecker 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 AbstractCslFormula
- */
-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::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
-		return this->getPathFormula().check(modelChecker, qualitative);
-	}
-};
-
-} //namespace csl
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/Csl/SteadyStateBoundOperator.h

@@ -9,13 +9,11 @@
 #define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_
 
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/SteadyStateBoundOperator.h"
 #include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/ComparisonType.h"
 
 namespace storm {
-
 namespace property {
-
 namespace csl {
 
 template <class T> class SteadyStateBoundOperator;
@@ -54,33 +52,39 @@ class ISteadyStateBoundOperatorModelChecker {
  * @see AbstractCslFormula
  */
 template <class T>
-class SteadyStateBoundOperator : public storm::property::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>,
-											public AbstractStateFormula<T> {
+class SteadyStateBoundOperator : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	SteadyStateBoundOperator() : storm::property::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>
-		(LESS_EQUAL, storm::utility::constantZero<T>(), nullptr) {
+	SteadyStateBoundOperator() : comparisonOperator(LESS), bound(storm::utility::constantZero<T>()), stateFormula(nullptr) {
 		// Intentionally left empty
 	}
 
 	/*!
 	 * Constructor
 	 *
+	 * @param comparisonOperator The relation for the bound.
+	 * @param bound The bound for the probability
 	 * @param stateFormula The child node
 	 */
-	SteadyStateBoundOperator(
-		storm::property::ComparisonType comparisonRelation, T bound, AbstractStateFormula<T>* stateFormula) :
-			storm::property::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>(comparisonRelation, bound, stateFormula) {
+	SteadyStateBoundOperator(storm::property::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 ~SteadyStateBoundOperator() {
-		// Intentionally left empty
+		if (stateFormula != nullptr) {
+		 delete stateFormula;
+		}
 	}
 
 	/*!
@@ -108,7 +112,100 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<ISteadyStateBoundOperatorModelChecker>()->checkSteadyStateBoundOperator(*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->stateFormula);
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "S ";
+		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;
+	}
+
+	/*!
+	 * @returns the child node (representation of a 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;
+	}
+
+	/*!
+	 *
+	 * @return True if the state formula is set, i.e. it does not point to nullptr; false otherwise
+	 */
+	bool stateFormulaIsSet() const {
+		return stateFormula != nullptr;
+	}
+
+	/*!
+	 * @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;
+	}
+
+	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:
+	ComparisonType comparisonOperator;
+	T bound;
+	AbstractStateFormula<T>* stateFormula;
 };
 
 } //namespace csl

src/formula/Csl/SteadyStateNoBoundOperator.h

@@ -1,100 +0,0 @@
-/*
- * SteadyStateNoBoundOperator.h
- *
- *  Created on: 09.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_
-
-#include "AbstractStateFormula.h"
-#include "AbstractNoBoundOperator.h"
-#include "src/formula/abstract/SteadyStateNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace csl {
-
-template <class T> class SteadyStateNoBoundOperator;
-
-/*!
- *  @brief Interface class for model checkers that support SteadyStateOperator.
- *
- *  All model checkers that support the formula class SteadyStateOperator must inherit
- *  this pure virtual class.
- */
-template <class T>
-class ISteadyStateNoBoundOperatorModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates SteadyStateOperator formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>  checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator<T>& obj) const = 0;
-};
-
-template <class T>
-class SteadyStateNoBoundOperator: public storm::property::abstract::SteadyStateNoBoundOperator<T, AbstractStateFormula<T>>,
-											 public AbstractNoBoundOperator<T> {
-public:
-	/*!
-	 * Empty constructor
-	 */
-	SteadyStateNoBoundOperator() : storm::property::abstract::SteadyStateNoBoundOperator<T, AbstractStateFormula<T>>() {
-		// Intentionally left empty
-
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param stateFormula The state formula that forms the subtree
-	 */
-	SteadyStateNoBoundOperator(AbstractStateFormula<T>* stateFormula)
-		: storm::property::abstract::SteadyStateNoBoundOperator<T, AbstractStateFormula<T>>(stateFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	~SteadyStateNoBoundOperator() {
-		// 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 AbstractNoBoundOperator <T>* clone() const override {
-		SteadyStateNoBoundOperator<T>* result = new SteadyStateNoBoundOperator<T>();
-		result->setStateFormula(this->getStateFormula().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::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
-		return modelChecker.template as<ISteadyStateNoBoundOperatorModelChecker>()->checkSteadyStateNoBoundOperator(*this);
-	}
-
-};
-
-} /* namespace csl */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ */

src/formula/Csl/TimeBoundedEventually.h

@@ -8,9 +8,8 @@
 #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_
 #define STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_
 
-#include "src/formula/abstract/TimeBoundedEventually.h"
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 
 namespace storm {
 namespace property {
@@ -38,27 +37,27 @@ class ITimeBoundedEventuallyModelChecker {
 
 
 template<class T>
-class TimeBoundedEventually: public storm::property::abstract::TimeBoundedEventually<T, AbstractStateFormula<T>>,
-									  public AbstractPathFormula<T> {
+class TimeBoundedEventually: public AbstractPathFormula<T> {
 public:
+
 	/**
 	 * Simple constructor: Only sets the bounds
 	 *
 	 * @param lowerBound
 	 * @param upperBound
 	 */
-	TimeBoundedEventually(T lowerBound, T upperBound)
-		: storm::property::abstract::TimeBoundedEventually<T, AbstractStateFormula<T>>(lowerBound, upperBound) {
-		// Intentionally left empty
+	TimeBoundedEventually(T lowerBound, T upperBound) : child(nullptr) {
+		setInterval(lowerBound, upperBound);
 	}
 
-	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child)
-		: storm::property::abstract::TimeBoundedEventually<T, AbstractStateFormula<T>>(lowerBound, upperBound, child) {
-		// Intentionally left empty
+	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child) : child(nullptr) {
+		setInterval(lowerBound, upperBound);
 	}
 
 	virtual ~TimeBoundedEventually() {
-		// Intentionally left empty
+		if (child != nullptr) {
+			delete child;
+		}
 	}
 
 	/*!
@@ -88,6 +87,94 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->child);
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = "F";
+		if (upperBound == std::numeric_limits<double>::infinity()) {
+			result = ">=" + std::to_string(lowerBound);
+		} else {
+			result = "[";
+			result += std::to_string(lowerBound);
+			result += ",";
+			result += std::to_string(upperBound);
+			result += "]";
+		}
+		result += " ";
+		result += child->toString();
+		return result;
+	}
+
+	/*!
+	 * @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;
+	}
+
+	/**
+	 * Getter for lowerBound attribute
+	 *
+	 * @return lower bound of the operator.
+	 */
+	T getLowerBound() const {
+		return lowerBound;
+	}
+
+	/**
+	 * Getter for upperBound attribute
+	 * @return upper bound of the operator.
+	 */
+	T getUpperBound() const {
+		return upperBound;
+	}
+
+	/**
+	 * Set the time interval for the time bounded operator
+	 *
+	 * @param lowerBound
+	 * @param upperBound
+	 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
+	 */
+	void setInterval(T lowerBound, T upperBound) {
+		if (lowerBound > upperBound) {
+			throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound");
+		}
+		this->lowerBound = lowerBound;
+		this->upperBound = upperBound;
+	}
+
+private:
+	AbstractStateFormula<T>* child;
+	T lowerBound, upperBound;
 };
 
 } /* namespace csl */

src/formula/Csl/TimeBoundedUntil.h

@@ -8,9 +8,8 @@
 #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_
 #define STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/TimeBoundedUntil.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 
 namespace storm {
 namespace property {
@@ -37,9 +36,9 @@ class ITimeBoundedUntilModelChecker {
 };
 
 template <class T>
-class TimeBoundedUntil: public storm::property::abstract::TimeBoundedUntil<T, AbstractStateFormula<T>>,
-								public AbstractPathFormula<T> {
+class TimeBoundedUntil: public AbstractPathFormula<T> {
 public:
+
 	/**
 	 * Constructor providing bounds only;
 	 * Sub formulas are set to null.
@@ -47,11 +46,11 @@ public:
 	 * @param lowerBound
 	 * @param upperBound
 	 */
-	TimeBoundedUntil(T lowerBound, T upperBound) :
-		storm::property::abstract::TimeBoundedUntil<T, AbstractStateFormula<T>>(lowerBound, upperBound) {
-		// Intentionally left empty
+	TimeBoundedUntil(T lowerBound, T upperBound) : left(nullptr), right(nullptr) {
+		setInterval(lowerBound, upperBound);
 	}
 
+
 	/**
 	 * Full constructor
 	 * @param lowerBound
@@ -59,16 +58,20 @@ public:
 	 * @param left
 	 * @param right
 	 */
-	TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) :
-		storm::property::abstract::TimeBoundedUntil<T, AbstractStateFormula<T>>(lowerBound, upperBound, left, right) {
-
+	TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) : left(left), right(right) {
+		setInterval(lowerBound, upperBound);
 	}
 
 	/*!
 	 * Destructor
 	 */
 	virtual ~TimeBoundedUntil() {
-	   // Intentionally left empty
+	   if (left != nullptr) {
+		delete left;
+	   }
+	   if (right != nullptr) {
+		delete right;
+	   }
 	}
 
 	/*!
@@ -102,6 +105,121 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*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 validate(const AbstractFormulaChecker<T>& checker) const override {
+		return checker.validate(this->left) && checker.validate(this->right);
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const override {
+		std::string result = left->toString();
+		result += " U";
+		if (upperBound == std::numeric_limits<double>::infinity()) {
+			result = ">=" + std::to_string(lowerBound);
+		} else {
+			result = "[";
+			result += std::to_string(lowerBound);
+			result += ",";
+			result += std::to_string(upperBound);
+			result += "]";
+		}
+		result += " ";
+		result += right->toString();
+		return result;
+	}
+
+	/*!
+	 * 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;
+	}
+
+	/**
+	 * Getter for lowerBound attribute
+	 *
+	 * @return lower bound of the operator.
+	 */
+	T getLowerBound() const {
+		return lowerBound;
+	}
+
+	/**
+	 * Getter for upperBound attribute
+	 * @return upper bound of the operator.
+	 */
+	T getUpperBound() const {
+		return upperBound;
+	}
+
+	/**
+	 * Set the time interval for the time bounded operator
+	 *
+	 * @param lowerBound
+	 * @param upperBound
+	 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
+	 */
+	void setInterval(T lowerBound, T upperBound) {
+		if (lowerBound > upperBound) {
+			throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound");
+		}
+		this->lowerBound = lowerBound;
+		this->upperBound = upperBound;
+	}
+
+private:
+	AbstractStateFormula<T>* left;
+	AbstractStateFormula<T>* right;
+	T lowerBound, upperBound;
 };
 
 } /* namespace csl */

src/formula/Csl/Until.h

@@ -8,9 +8,8 @@
 #ifndef STORM_FORMULA_CSL_UNTIL_H_
 #define STORM_FORMULA_CSL_UNTIL_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Until.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -54,15 +53,14 @@ class IUntilModelChecker {
  * @see AbstractCslFormula
  */
 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 +69,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 +80,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 +118,78 @@ public:
 	virtual std::vector<T> check(const storm::modelchecker::csl::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 csl

src/formula/Prctl/AbstractStateFormula.h

@@ -26,7 +26,7 @@ namespace prctl {
  * 	   clone().
  */
 template <class T>
-class AbstractStateFormula : public virtual storm::property::prctl::AbstractPrctlFormula<T> {
+class AbstractStateFormula : public storm::property::prctl::AbstractPrctlFormula<T> {
 
 public:
 	/*!

src/formula/Prctl/Globally.h

@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_
 #define STORM_FORMULA_PRCTL_GLOBALLY_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
@@ -85,7 +85,6 @@ public:
 	  }
 	}
 
-
 	/*!
 	 * Clones the called object.
 	 *

src/formula/Prctl/Next.h

@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_NEXT_H_
 #define STORM_FORMULA_PRCTL_NEXT_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {

src/formula/Prctl/Not.h

@@ -52,6 +52,7 @@ template <class T>
 class Not : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */

src/formula/Prctl/Or.h

@@ -54,9 +54,10 @@ template <class T>
 class Or : public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor.
-	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 * Will create an OR-node without subnotes. Will not represent a complete formula!
 	 */
 	Or() {
 		left = NULL;
@@ -65,7 +66,7 @@ public:
 
 	/*!
 	 * Constructor.
-	 * Creates an AND note with the parameters as subtrees.
+	 * Creates an OR note with the parameters as subtrees.
 	 *
 	 * @param left The left sub formula
 	 * @param right The right sub formula

src/modelchecker/csl/AbstractModelChecker.h

@@ -46,7 +46,6 @@ class AbstractModelChecker :
 	public virtual storm::property::csl::INextModelChecker<Type>,
 	public virtual storm::property::csl::ITimeBoundedUntilModelChecker<Type>,
 	public virtual storm::property::csl::ITimeBoundedEventuallyModelChecker<Type>,
-	public virtual storm::property::csl::INoBoundOperatorModelChecker<Type>,
 	public virtual storm::property::csl::IProbabilisticBoundOperatorModelChecker<Type> {
 	
 public: