Working in the new structure of the formula tree.

-Done with LTL.
-Working on PrCTL.


Former-commit-id: 1ec3c6993a

src/formula/abstract/AbstractFormula.h → src/formula/AbstractFormula.h

@@ -5,25 +5,21 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_
-#define STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_
+#define STORM_FORMULA_ABSTRACTFORMULA_H_
 
 #include <string>
 
 namespace storm {
 namespace property {
-namespace abstract {
 template <class T> class AbstractFormula;
-} //namespace abstract
 } //namespace property
 } //namespace storm
 
-
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
-namespace abstract {
 
 //abstract
 /*!
@@ -58,7 +54,7 @@ public:
 	virtual ~AbstractFormula() {
 		// Intentionally left empty.
 	}
-	
+
 	/*!
 	 *	@brief Return string representation of this formula.
 	 *
@@ -67,7 +63,7 @@ public:
 	 *	@returns a string representation of the formula
 	 */
 	virtual std::string toString() const = 0;
-	
+
 	/*!
 	 *	@brief Checks if all subtrees are valid in some logic.
 	 *
@@ -85,8 +81,7 @@ public:
 	virtual bool validate(const AbstractFormulaChecker<T>& checker) const = 0;
 };
 
-} // namespace abstract
 } // namespace property
 } // namespace storm
 
-#endif /* STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */

src/formula/AbstractFormulaChecker.h

@@ -10,7 +10,7 @@ template <class T> class AbstractFormulaChecker;
 } //namespace storm
 
 
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
 
 namespace storm {
 namespace property {
@@ -64,7 +64,7 @@ class AbstractFormulaChecker {
 		 *	@param formula A pointer to some formula object.
 		 *	@return true iff the formula is valid.
 		 */
-		virtual bool validate(const storm::property::abstract::AbstractFormula<T>* formula) const = 0;
+		virtual bool validate(const AbstractFormula<T>* formula) const = 0;
 };
 
 } // namespace property

src/formula/abstract/IOptimizingOperator.h → src/formula/IOptimizingOperator.h

@@ -5,12 +5,11 @@
  *      Author: thomas
  */
 
-#ifndef STORM_FORMULA_ABSTRACT_IOPTIMIZINGOPERATOR_H_
+#ifndef STORM_FORMULA_IOPTIMIZINGOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_IOPTIMIZINGOPERATOR_H_
+#define STORM_FORMULA_IOPTIMIZINGOPERATOR_H_
 
 namespace storm {
 namespace property {
-namespace abstract {
 
 /*!
  * @brief Interface for optimizing operators
@@ -20,6 +19,10 @@ namespace abstract {
 class IOptimizingOperator {
 public:
 
+	virtual ~IOptimizingOperator() {
+		// Intentionally left empty
+	}
+
 	/*!
 	 * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
 	 * @returns True if the operator is an optimizing operator.
@@ -35,7 +38,6 @@ public:
 	virtual bool isMinimumOperator() const = 0;
 };
 
-} /* namespace abstract */
 } /* namespace property */
 } /* namespace storm */
-#endif /* IOPTIMIZINGOPERATOR_H_ */
+#endif /* STORM_FORMULA_IOPTIMIZINGOPERATOR_H_ */

src/formula/Ltl/AbstractLtlFormula.h

@@ -10,7 +10,7 @@
 
 #include <vector>
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
 
 // Forward declaration for formula visitor
 namespace storm {
@@ -35,7 +35,7 @@ namespace ltl {
  * Interface class for all LTL root formulas.
  */
 template <class T>
-class AbstractLtlFormula : public virtual storm::property::abstract::AbstractFormula<T> {
+class AbstractLtlFormula : public virtual storm::property::AbstractFormula<T> {
 public:
 	/**
 	 * Empty destructor

src/formula/Ltl/And.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_AND_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/abstract/And.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
 #include <string>
@@ -71,27 +70,29 @@ class IAndVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class And : public storm::property::abstract::And<T, AbstractLtlFormula<T>>, public AbstractLtlFormula<T> {
+class And : public AbstractLtlFormula<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;
 	}
 
 	/*!
 	 * Constructor.
-	 * Creates an AND node with the parameters as subtrees.
+	 * Creates an AND note with the parameters as subtrees.
 	 *
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	And(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
+	And(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right) {
-		: storm::property::abstract::And<T, AbstractLtlFormula<T>>(left, right) {
+		this->left = left;
-		//intentionally left empty
+		this->right = right;
 	}
 
 	/*!
@@ -101,7 +102,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;
+		}
 	}
 
 	/*!
@@ -139,6 +145,81 @@ public:
 		visitor.template as<IAndVisitor>()->visitAnd(*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(AbstractLtlFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractLtlFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractLtlFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* left;
+	AbstractLtlFormula<T>* right;
+
 };
 
 } //namespace ltl

src/formula/Ltl/Ap.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_AP_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Ap.h"
 
 namespace storm {
 namespace property {
@@ -63,8 +62,7 @@ class IApVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Ap: public storm::property::abstract::Ap<T>,
+class Ap: public storm::property::ltl::AbstractLtlFormula<T> {
-		    public storm::property::ltl::AbstractLtlFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -80,13 +78,13 @@ public:
 	 *
 	 * @param ap The string representing the atomic proposition
 	 */
-	Ap(std::string ap) :
+	Ap(std::string ap) {
-		storm::property::abstract::Ap<T>(ap) {
+		this->ap = ap;
-		// Intentionally left empty
 	}
 
 	/*!
 	 * Destructor
+	 * At this time, empty...
 	 */
 	virtual ~Ap() {
 		// Intentionally left empty
@@ -121,6 +119,36 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<IApVisitor>()->visitAp(*this);
 	}
+
+	/*!
+	 * @returns a string representation of the leaf.
+	 *
+	 */
+	virtual std::string toString() const override {
+		return getAp();
+	}
+
+	/*!
+	 *  @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;
+	}
+
+private:
+	std::string ap;
 };
 
 } /* namespace ltl */

src/formula/Ltl/BoundedEventually.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
 #define STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
 
-#include "src/formula/abstract/BoundedEventually.h"
 #include "AbstractLtlFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
@@ -72,15 +71,16 @@ class IBoundedEventuallyVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class BoundedEventually : public storm::property::abstract::BoundedEventually<T, AbstractLtlFormula<T>>,
+class BoundedEventually : public AbstractLtlFormula<T> {
-								  public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
-	BoundedEventually()  {
+	BoundedEventually() {
-		//intentionally left empty
+		this->child = nullptr;
+		bound = 0;
 	}
 
 	/*!
@@ -89,9 +89,9 @@ public:
 	 * @param child The child formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedEventually(AbstractLtlFormula<T>* child, uint_fast64_t bound) :
+	BoundedEventually(AbstractLtlFormula<T>* child, uint_fast64_t bound) {
-		storm::property::abstract::BoundedEventually<T, AbstractLtlFormula<T>>(child, bound){
+		this->child = child;
-		//intentionally left empty
+		this->bound = bound;
 	}
 
 	/*!
@@ -101,9 +101,12 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~BoundedEventually() {
-	  //intentionally left empty
+	  if (child != nullptr) {
+		  delete child;
+	  }
 	}
 
+
 	/*!
 	 * Clones the called object.
 	 *
@@ -137,6 +140,72 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<IBoundedEventuallyVisitor>()->visitBoundedEventually(*this);
 	}
+
+	/*!
+	 * @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 AbstractLtlFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* child;
+	uint_fast64_t bound;
+
 };
 
 } //namespace ltl

src/formula/Ltl/BoundedUntil.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
 #define STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
 
-#include "src/formula/abstract/BoundedUntil.h"
+#include "src/formula/Ltl/AbstractLtlFormula.h"
-#include "AbstractLtlFormula.h"
 #include <cstdint>
 #include <string>
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
@@ -72,15 +71,17 @@ class IBoundedUntilVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class BoundedUntil : public storm::property::abstract::BoundedUntil<T, AbstractLtlFormula<T>>,
+class BoundedUntil : public AbstractLtlFormula<T> {
-							public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	BoundedUntil() {
-		//Intentionally left empty
+		this->left = NULL;
+		this->right = NULL;
+		bound = 0;
 	}
 
 	/*!
@@ -91,9 +92,10 @@ public:
 	 * @param bound The maximal number of steps
 	 */
 	BoundedUntil(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right,
-					 uint_fast64_t bound) :
+					 uint_fast64_t bound) {
-					 storm::property::abstract::BoundedUntil<T, AbstractLtlFormula<T>>(left,right,bound) {
+		this->left = left;
-		//intentionally left empty
+		this->right = right;
+		this->bound = bound;
 	}
 
 	/*!
@@ -103,19 +105,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) {
-	 *	@brief Return string representation of this formula.
+		  delete right;
-	 *
+	  }
-	 * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
-	 * root of a path formula); hence this function is overwritten in this class.
-	 *
-	 * @return A string representation of the formula.
-	 */
-	virtual std::string toString() const {
-		return "(" + storm::property::abstract::BoundedUntil<T, AbstractLtlFormula<T>>::toString() + ")";
 	}
 
 	/*!
@@ -154,6 +149,102 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<IBoundedUntilVisitor>()->visitBoundedUntil(*this);
 	}
+
+	/*!
+	 *	@brief Return string representation of this formula.
+	 *
+	 * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
+	 * root of a path formula); hence this function is overwritten in this class.
+	 *
+	 * @return 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(AbstractLtlFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractLtlFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractLtlFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* left;
+	AbstractLtlFormula<T>* right;
+	uint_fast64_t bound;
 };
 
 } //namespace ltl

src/formula/Ltl/Eventually.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_LTL_EVENTUALLY_H_
 #define STORM_FORMULA_LTL_EVENTUALLY_H_
 
-#include "src/formula/abstract/Eventually.h"
+#include "src/formula/Ltl/AbstractLtlFormula.h"
-#include "AbstractLtlFormula.h"
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
@@ -69,15 +68,15 @@ class IEventuallyVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Eventually : public storm::property::abstract::Eventually<T, AbstractLtlFormula<T>>,
+class Eventually : public AbstractLtlFormula<T> {
-						 public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	Eventually() {
-		// Intentionally left empty
+		this->child = nullptr;
 	}
 
 	/*!
@@ -85,9 +84,8 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Eventually(AbstractLtlFormula<T>* child)
+	Eventually(AbstractLtlFormula<T>* child) {
-		: storm::property::abstract::Eventually<T, AbstractLtlFormula<T>>(child) {
+		this->child = child;
-
 	}
 
 	/*!
@@ -97,7 +95,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;
+	  }
 	}
 
 	/*!
@@ -131,6 +131,51 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<IEventuallyVisitor>()->visitEventually(*this);
 	}
+
+	/*!
+	 * @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 AbstractLtlFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* child;
 };
 
 } //namespace ltl

src/formula/Ltl/Globally.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_LTL_GLOBALLY_H_
 #define STORM_FORMULA_LTL_GLOBALLY_H_
 
-#include "src/formula/abstract/Globally.h"
 #include "AbstractLtlFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
@@ -70,15 +69,15 @@ class IGloballyVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Globally : public storm::property::abstract::Globally<T, AbstractLtlFormula<T>>,
+class Globally : public AbstractLtlFormula<T> {
-					  public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	Globally() {
-		//intentionally left empty
+		this->child = nullptr;
 	}
 
 	/*!
@@ -86,9 +85,8 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Globally(AbstractLtlFormula<T>* child)
+	Globally(AbstractLtlFormula<T>* child) {
-		: storm::property::abstract::Globally<T, AbstractLtlFormula<T>>(child) {
+		this->child = child;
-		//intentionally left empty
 	}
 
 	/*!
@@ -98,10 +96,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.
 	 *
@@ -133,6 +132,51 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<IGloballyVisitor>()->visitGlobally(*this);
 	}
+
+	/*!
+	 * @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 AbstractLtlFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractLtlFormula<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:
+		AbstractLtlFormula<T>* child;
 };
 
 } //namespace ltl

src/formula/Ltl/Next.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_NEXT_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Next.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -69,15 +68,15 @@ class INextVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Next : public storm::property::abstract::Next<T, AbstractLtlFormula<T>>,
+class Next : public AbstractLtlFormula<T> {
-				 public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	Next() {
-		//intentionally left empty
+		this->child = NULL;
 	}
 
 	/*!
@@ -85,9 +84,8 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Next(AbstractLtlFormula<T>* child)
+	Next(AbstractLtlFormula<T>* child) {
-		: storm::property::abstract::Next<T, AbstractLtlFormula<T>>(child) {
+		this->child = child;
-		//intentionally left empty
 	}
 
 	/*!
@@ -97,7 +95,9 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~Next() {
-	  //intentionally left empty
+	  if (child != NULL) {
+		  delete child;
+	  }
 	}
 
 	/*!
@@ -131,6 +131,53 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<INextVisitor>()->visitNext(*this);
 	}
+
+	/*!
+	 * @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 AbstractLtlFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* child;
 };
 
 } //namespace ltl

src/formula/Ltl/Not.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_NOT_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Not.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -66,24 +65,23 @@ class INotVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Not : public storm::property::abstract::Not<T, AbstractLtlFormula<T>>,
+class Not : public AbstractLtlFormula<T> {
-			   public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	Not() {
-		//intentionally left empty
+		this->child = NULL;
 	}
 
 	/*!
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(AbstractLtlFormula<T>* child) :
+	Not(AbstractLtlFormula<T>* child) {
-		storm::property::abstract::Not<T, AbstractLtlFormula<T>>(child){
+		this->child = child;
-		//intentionally left empty
 	}
 
 	/*!
@@ -93,7 +91,9 @@ public:
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
 	virtual ~Not() {
-	  //intentionally left empty
+	  if (child != NULL) {
+		  delete child;
+	  }
 	}
 
 	/*!
@@ -127,6 +127,51 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<INotVisitor>()->visitNot(*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 AbstractLtlFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* child;
 };
 
 } //namespace ltl

src/formula/Ltl/Or.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_OR_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Or.h"
 
 namespace storm {
 namespace property {
@@ -68,34 +67,44 @@ class IOrVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Or: public storm::property::abstract::Or<T, AbstractLtlFormula<T>>,
+class Or: public storm::property::ltl::AbstractLtlFormula<T> {
-			 public storm::property::ltl::AbstractLtlFormula<T> {
+
 public:
+
 	/*!
-	 * Empty constructor
+	 * Empty constructor.
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
 	 */
 	Or() {
-		// Intentionally left empty
+		left = NULL;
-
+		right = NULL;
 	}
 
 	/*!
-	 * Constructor
+	 * Constructor.
-	 * Creates an OR node with the parameters as subtrees.
+	 * Creates an AND note with the parameters as subtrees.
 	 *
-	 * @param left The left subformula
+	 * @param left The left sub formula
-	 * @param right The right subformula
+	 * @param right The right sub formula
 	 */
-	Or(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
+	Or(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right) {
-		: storm::property::abstract::Or<T,AbstractLtlFormula<T>>(left, right) {
+		this->left = left;
-		// Intentionally left empty
+		this->right = right;
 	}
 
 	/*!
-	 * Destructor
+	 * 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
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
 	}
 
 	/*!
@@ -133,6 +142,79 @@ public:
 		visitor.template as<IOrVisitor>()->visitOr(*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(AbstractLtlFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractLtlFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractLtlFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* left;
+	AbstractLtlFormula<T>* right;
 };
 
 } /* namespace ltl */

src/formula/Ltl/Until.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_UNTIL_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Until.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -70,15 +69,16 @@ class IUntilVisitor {
  * @see AbstractLtlFormula
  */
 template <class T>
-class Until : public storm::property::abstract::Until<T, AbstractLtlFormula<T>>,
+class Until : public AbstractLtlFormula<T> {
-				  public AbstractLtlFormula<T> {
 
 public:
+
 	/*!
 	 * Empty constructor
 	 */
 	Until() {
-		// Intentionally left empty
+		this->left = NULL;
+		this->right = NULL;
 	}
 
 	/*!
@@ -87,9 +87,9 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	Until(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
+	Until(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right) {
-		: storm::property::abstract::Until<T, AbstractLtlFormula<T>>(left, right) {
+		this->left = left;
-		// Intentionally left empty
+		this->right = right;
 	}
 
 	/*!
@@ -99,19 +99,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) {
-	 *	@brief Return string representation of this formula.
+		  delete right;
-	 *
+	  }
-	 * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
-	 * root of a path formula); hence this function is overwritten in this class.
-	 *
-	 * @return A string representation of the formula.
-	 */
-	virtual std::string toString() const {
-		return "(" + storm::property::abstract::Until<T, AbstractLtlFormula<T>>::toString() + ")";
 	}
 
 	/*!
@@ -148,6 +141,83 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
 		visitor.template as<IUntilVisitor>()->visitUntil(*this);
 	}
+
+	/*!
+	 *	@brief Return string representation of this formula.
+	 *
+	 * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
+	 * root of a path formula); hence this function is overwritten in this class.
+	 *
+	 * @return A string representation of the formula.
+	 */
+	virtual std::string toString() const {
+		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(AbstractLtlFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractLtlFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractLtlFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractLtlFormula<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:
+	AbstractLtlFormula<T>* left;
+	AbstractLtlFormula<T>* right;
 };
 
 } //namespace ltl

src/formula/Prctl/AbstractNoBoundOperator.h

@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
 
-#include "AbstractPrctlFormula.h"
+#include "src/formula/AbstractFormula.h"
 #include "src/formula/abstract/IOptimizingOperator.h"
 
 namespace storm {
@@ -42,8 +42,8 @@ public:
  * Interface class for all PRCTL No bound operators
  */
 template <class T>
-class AbstractNoBoundOperator: public AbstractPrctlFormula<T>,
+class AbstractNoBoundOperator: public storm::property::AbstractFormula<T>,
-										 public virtual storm::property::abstract::IOptimizingOperator {
+										 public virtual storm::property::IOptimizingOperator {
 public:
 	AbstractNoBoundOperator() {
 		// Intentionally left empty.

src/formula/Prctl/AbstractPathFormula.h

@@ -8,11 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 
-namespace storm { namespace property { namespace prctl {
+#include "src/formula/AbstractFormula.h"
-template <class T> class AbstractPathFormula;
-}}}
-
-#include "src/formula/abstract/AbstractFormula.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 #include <vector>
@@ -35,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::abstract::AbstractFormula<T> {
+class AbstractPathFormula : public virtual storm::property::AbstractFormula<T> {
 
 public:
 	/*!

src/formula/Prctl/AbstractPrctlFormula.h

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

src/formula/Prctl/AbstractStateFormula.h

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

src/formula/Prctl/And.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_AND_H_
 #define STORM_FORMULA_PRCTL_AND_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
-#include "src/formula/abstract/And.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 #include <string>
@@ -54,15 +53,17 @@ class IAndModelChecker {
  * @see AbstractPrctlFormula
  */
 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)
+	And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
-		: storm::property::abstract::And<T, AbstractStateFormula<T>>(left, right) {
+		this->left = left;
-		//intentionally left empty
+		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 prctl

src/formula/Prctl/Ap.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_AP_H_
 #define STORM_FORMULA_PRCTL_AP_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
-#include "src/formula/abstract/Ap.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
@@ -47,10 +46,10 @@ class IApModelChecker {
  * @see AbstractStateFormula
  */
 template <class T>
-class Ap : public storm::property::abstract::Ap<T>,
+class Ap : public AbstractStateFormula<T> {
-			  public AbstractStateFormula<T> {
 
 public:
+
 	/*!
 	 * Constructor
 	 *
@@ -58,9 +57,8 @@ public:
 	 *
 	 * @param ap The string representing the atomic proposition
 	 */
-	Ap(std::string ap)
+	Ap(std::string ap) {
-		: storm::property::abstract::Ap<T>(ap) {
+		this->ap = ap;
-		// Intentionally left empty
 	}
 
 	/*!
@@ -95,6 +93,35 @@ 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/Prctl/Not.h

@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_NOT_H_
 
 #include "AbstractStateFormula.h"
-#include "src/formula/abstract/Not.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
@@ -50,24 +49,22 @@ class INotModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class Not : public storm::property::abstract::Not<T, AbstractStateFormula<T>>,
+class Not : public AbstractStateFormula<T> {
-			   public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
 	Not() {
-		//intentionally left empty
+		this->child = NULL;
 	}
 
 	/*!
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(AbstractStateFormula<T>* child) :
+	Not(AbstractStateFormula<T>* child) {
-		storm::property::abstract::Not<T, AbstractStateFormula<T>>(child){
+		this->child = child;
-		//intentionally left empty
 	}
 
 	/*!
@@ -77,7 +74,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 +106,51 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::prctl::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 FormulaType& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(FormulaType* 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/Or.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_OR_H_
 #define STORM_FORMULA_PRCTL_OR_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
-#include "src/formula/abstract/Or.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -52,28 +51,28 @@ class IOrModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class Or : public storm::property::abstract::Or<T, AbstractStateFormula<T>>,
+class Or : public AbstractStateFormula<T> {
-			  public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor.
-	 * Will create an OR-node without subnotes. The result does not represent a complete formula!
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
 	 */
 	Or() {
-		//intentionally left empty
+		left = NULL;
+		right = NULL;
 	}
 
 	/*!
 	 * Constructor.
-	 * Creates an OR note with the parameters as subtrees.
+	 * Creates an AND note with the parameters as subtrees.
 	 *
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) :
+	Or(FormulaType* left, FormulaType* right) {
-		storm::property::abstract::Or<T, AbstractStateFormula<T>>(left, right) {
+		this->left = left;
-		//intentionally left empty
+		this->right = right;
 	}
 
 	/*!
@@ -83,7 +82,12 @@ public:
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
 	virtual ~Or() {
-	  //intentionally left empty
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
 	}
 
 	/*!
@@ -116,6 +120,81 @@ public:
 	virtual storm::storage::BitVector check(const storm::modelchecker::prctl::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(FormulaType* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(FormulaType* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const FormulaType& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const FormulaType& 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/formula/Prctl/ProbabilisticBoundOperator.h

@@ -10,7 +10,6 @@
 
 #include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
-#include "src/formula/abstract/ProbabilisticBoundOperator.h"
 #include "utility/constants.h"
 
 namespace storm {

src/formula/abstract/And.h

@@ -1,164 +0,0 @@
-/*
- * And.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_AND_H_
-#define STORM_FORMULA_ABSTRACT_AND_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <string>
-#include <type_traits>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Logic-abstract Class for an abstract formula tree with AND node as root.
- *
- * Has two formulas as sub formulas/trees; the type is the template parameter FormulaType
- *
- * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
- * the model checker works.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @see AbstractFormula
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "validate" of the subformulas are needed.
- */
-template <class T, class FormulaType>
-class And : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::And<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor.
-	 * Will create an AND-node without subnotes. Will not represent a complete formula!
-	 */
-	And() {
-		left = NULL;
-		right = NULL;
-	}
-
-	/*!
-	 * Constructor.
-	 * Creates an AND note with the parameters as subtrees.
-	 *
-	 * @param left The left sub formula
-	 * @param right The right sub formula
-	 */
-	And(FormulaType* left, FormulaType* 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 ~And() {
-		if (left != NULL) {
-			delete left;
-		}
-		if (right != NULL) {
-			delete right;
-		}
-	}
-
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(FormulaType* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(FormulaType* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const FormulaType& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const FormulaType& 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 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);
-    }
-
-
-private:
-	FormulaType* left;
-	FormulaType* right;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_AND_H_ */

src/formula/abstract/Ap.h

@@ -1,84 +0,0 @@
-/*
- * Ap.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_AP_H_
-#define STORM_FORMULA_ABSTRACT_AP_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Logic-abstract Class for an abstract formula tree with atomic proposition as root.
- *
- * This class represents the leaves in the formula tree.
- *
- * @see AbstractFormula
- */
-template <class T>
-class Ap : public virtual AbstractFormula<T> {
-
-public:
-	/*!
-	 * Constructor
-	 *
-	 * Creates a new atomic proposition leaf, with the label Ap
-	 *
-	 * @param ap The string representing the atomic proposition
-	 */
-	Ap(std::string ap) {
-		this->ap = ap;
-	}
-
-	/*!
-	 * Destructor.
-	 * At this time, empty...
-	 */
-	virtual ~Ap() { }
-
-	/*!
-	 * @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();
-	}
-	
-	/*!
-     *  @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;
-	}
-
-private:
-	std::string ap;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_ABSTRCT_AP_H_ */

src/formula/abstract/BoundedEventually.h

@@ -1,151 +0,0 @@
-/*
- * BoundedUntil.h
- *
- *  Created on: 27.11.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <cstdint>
-#include <string>
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedEventually node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff in at most \e bound steps, formula \e child holds.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "validate" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class BoundedEventually : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::BoundedEventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	BoundedEventually() {
-		this->child = nullptr;
-		bound = 0;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param child The child formula subtree
-	 * @param bound The maximal number of steps
-	 */
-	BoundedEventually(FormulaType* child, uint_fast64_t bound) {
-		this->child = child;
-		this->bound = bound;
-	}
-
-	/*!
-	 * Destructor.
-	 *
-	 * Also deletes the subtrees.
-	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-	 */
-	virtual ~BoundedEventually() {
-	  if (child != nullptr) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @returns the child node
-	 */
-	const FormulaType& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(FormulaType* 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;
-	}
-
-	/*!
-	 * @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);
-	}
-
-
-private:
-	FormulaType* child;
-	uint_fast64_t bound;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_ */

src/formula/abstract/BoundedNaryUntil.h

@@ -1,175 +0,0 @@
-/*
- * BoundedNaryUntil.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
-#define STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include <cstdint>
-#include <string>
-#include <vector>
-#include <tuple>
-#include <sstream>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedNaryUntil node as root.
- *
- * Has at least two formulas as sub formulas and an interval
- * associated with all but the first sub formula. We'll call the first one
- * \e left and all other one \e right.
- *
- * @par Semantics
- * The formula holds iff \e left holds until eventually any of the \e right
- * formulas holds after a number of steps contained in the interval
- * associated with this formula.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class BoundedNaryUntil : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::BoundedNaryUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	BoundedNaryUntil() {
-		this->left = nullptr;
-		this->right = new std::vector<std::tuple<FormulaType*,T,T>>();
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param left The left formula subtree
-	 * @param right The left formula subtree
-	 */
-	BoundedNaryUntil(FormulaType* left, std::vector<std::tuple<FormulaType*,T,T>>* right) {
-		this->left = left;
-		this->right = right;
-	}
-
-	/*!
-	 * Destructor.
-	 *
-	 * Also deletes the subtrees.
-	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-	 */
-	virtual ~BoundedNaryUntil() {
-	  if (left != nullptr) {
-		  delete left;
-	  }
-	  if (right != nullptr) {
-		  delete right;
-	  }
-	}
-
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(FormulaType* newLeft) {
-		left = newLeft;
-	}
-
-	void setRight(std::vector<std::tuple<FormulaType*,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(FormulaType* newRight, T upperBound, T lowerBound) {
-		this->right->push_back(std::tuple<FormulaType*,T,T>(newRight, upperBound, lowerBound));
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const FormulaType& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child nodes.
-	 */
-	const std::vector<std::tuple<FormulaType*,T,T>>& getRight() const {
-		return *right;
-	}
-
-	/*!
-	 * @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;
-	}
-
-
-private:
-	FormulaType* left;
-	std::vector<std::tuple<FormulaType*,T,T>>* right;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_ */

src/formula/abstract/BoundedUntil.h

@@ -1,182 +0,0 @@
-/*
- * BoundedUntil.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
-#define STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include <cstdint>
-#include <string>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedUntil node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
- * \e left holds.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class BoundedUntil : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::BoundedUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	BoundedUntil() {
-		this->left = NULL;
-		this->right = NULL;
-		bound = 0;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param left The left formula subtree
-	 * @param right The left formula subtree
-	 * @param bound The maximal number of steps
-	 */
-	BoundedUntil(FormulaType* left, FormulaType* right,
-					 uint_fast64_t bound) {
-		this->left = left;
-		this->right = right;
-		this->bound = bound;
-	}
-
-	/*!
-	 * Destructor.
-	 *
-	 * Also deletes the subtrees.
-	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-	 */
-	virtual ~BoundedUntil() {
-	  if (left != NULL) {
-		  delete left;
-	  }
-	  if (right != NULL) {
-		  delete right;
-	  }
-	}
-
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(FormulaType* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(FormulaType* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const FormulaType& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const FormulaType& 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;
-	}
-
-	/*!
-	 * @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);
-	}
-
-private:
-	FormulaType* left;
-	FormulaType* right;
-	uint_fast64_t bound;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_ */

src/formula/abstract/CumulativeReward.h

@@ -1,101 +0,0 @@
-/*
- * InstantaneousReward.h
- *
- *  Created on: 26.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_CUMULATIVEREWARD_H_
-#define STORM_FORMULA_ABSTRACT_CUMULATIVEREWARD_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <string>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a Cumulative Reward node as root.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @see AbstractPathFormula
- * @see AbstractFormula
- */
-template <class T>
-class CumulativeReward : public virtual AbstractFormula<T> {
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	CumulativeReward() {
-		bound = 0;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param bound The time bound of the reward formula
-	 */
-	CumulativeReward(T bound) {
-		this->bound = bound;
-	}
-
-	/*!
-	 * Empty destructor.
-	 */
-	virtual ~CumulativeReward() {
-		// Intentionally left empty.
-	}
-
-	/*!
-	 * @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;
-	}
-
-	/*!
-	 * @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;
-	}
-
-private:
-	T bound;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */

src/formula/abstract/Eventually.h

@@ -1,125 +0,0 @@
-/*
- * Next.h
- *
- *  Created on: 26.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
-#define STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with an Eventually node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff eventually \e child holds.
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Eventually : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::Eventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	Eventually() {
-		this->child = nullptr;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param child The child node
-	 */
-	Eventually(FormulaType* child) {
-		this->child = child;
-	}
-
-	/*!
-	 * Constructor.
-	 *
-	 * Also deletes the subtree.
-	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
-	 */
-	virtual ~Eventually() {
-	  if (child != nullptr) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @returns the child node
-	 */
-	const FormulaType& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(FormulaType* 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;
-	}
-
-	/*!
-	 * @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);
-	}
-
-private:
-	FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_EVENTUALLY_H_ */

src/formula/abstract/Globally.h

@@ -1,126 +0,0 @@
-/*
- * Next.h
- *
- *  Created on: 26.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_GLOBALLY_H_
-#define STORM_FORMULA_ABSTRACT_GLOBALLY_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a Globally node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff globally \e child holds.
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Globally : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::Globally<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	Globally() {
-		this->child = nullptr;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param child The child node
-	 */
-	Globally(FormulaType* child) {
-		this->child = child;
-	}
-
-	/*!
-	 * Constructor.
-	 *
-	 * Also deletes the subtree.
-	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
-	 */
-	virtual ~Globally() {
-	  if (child != nullptr) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @returns the child node
-	 */
-	const FormulaType& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(FormulaType* 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;
-	}
-
-	/*!
-	 * @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);
-	}
-
-private:
-	FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_GLOBALLY_H_ */

src/formula/abstract/InstantaneousReward.h

@@ -1,101 +0,0 @@
-/*
- * InstantaneousReward.h
- *
- *  Created on: 26.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_
-#define STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <cstdint>
-#include <string>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a Instantaneous Reward node as root.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @see AbstractFormula
- */
-template <class T>
-class InstantaneousReward : public virtual AbstractFormula<T> {
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	InstantaneousReward() {
-		bound = 0;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param bound The time instance of the reward formula
-	 */
-	InstantaneousReward(uint_fast64_t bound) {
-		this->bound = bound;
-	}
-
-	/*!
-	 * Empty destructor.
-	 */
-	virtual ~InstantaneousReward() {
-		// Intentionally left empty.
-	}
-
-	/*!
-	 * @returns the time instance for the instantaneous reward operator
-	 */
-	uint_fast64_t getBound() const {
-		return bound;
-	}
-
-	/*!
-	 * Sets the the time instance for the instantaneous reward operator
-	 *
-	 * @param bound the new bound.
-	 */
-	void setBound(uint_fast64_t bound) {
-		this->bound = bound;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const 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;
-	}
-
-private:
-	uint_fast64_t bound;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */

src/formula/abstract/Next.h

@@ -1,128 +0,0 @@
-/*
- * Next.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_NEXT_H_
-#define STORM_FORMULA_ABSTRACT_NEXT_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a Next node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff in the next step, \e child holds
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Next : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::Next<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	Next() {
-		this->child = NULL;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param child The child node
-	 */
-	Next(FormulaType* child) {
-		this->child = child;
-	}
-
-	/*!
-	 * Constructor.
-	 *
-	 * Also deletes the subtree.
-	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-	 */
-	virtual ~Next() {
-	  if (child != NULL) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @returns the child node
-	 */
-	const FormulaType& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(FormulaType* 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;
-	}
-
-	/*!
-	 * @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);
-    }
-
-private:
-	FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_NEXT_H_ */

src/formula/abstract/Not.h

@@ -1,122 +0,0 @@
-/*
- * Not.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_NOT_H_
-#define STORM_FORMULA_ABSTRACT_NOT_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with NOT node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Not : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::Not<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	Not() {
-		this->child = NULL;
-	}
-
-	/*!
-	 * Constructor
-	 * @param child The child node
-	 */
-	Not(FormulaType* child) {
-		this->child = child;
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * Also deletes the subtree
-	 * (this behavior can be prevented by setting them to NULL before deletion)
-	 */
-	virtual ~Not() {
-	  if (child != NULL) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @returns The child node
-	 */
-	const FormulaType& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(FormulaType* 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;
-	}
-
-	/*!
-	 * @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);
-	}
-
-private:
-	FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_NOT_H_ */

src/formula/abstract/OptimizingOperator.h

@@ -1,72 +0,0 @@
-#ifndef STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
-
-#include "IOptimizingOperator.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- *
- */
-class OptimizingOperator : public virtual IOptimizingOperator {
-public:
-	/*!
-	 * Empty constructor
-	 */
-	OptimizingOperator() : optimalityOperator(false), minimumOperator(false) {
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param minimumOperator A flag indicating whether this operator is a minimizing or a maximizing operator.
-	 */
-	OptimizingOperator(bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) {
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~OptimizingOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
-	 * @returns True if the operator is an optimizing operator.
-	 */
-	virtual bool isOptimalityOperator() const {
-		return optimalityOperator;
-	}
-
-	/*!
-	 * Retrieves whether the operator is a minimizing operator given that it is an optimality
-	 * operator.
-	 * @returns True if the operator is an optimizing operator and it is a minimizing operator and
-	 * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator.
-	 */
-	virtual bool isMinimumOperator() const {
-		return optimalityOperator && minimumOperator;
-	}
-
-private:
-	// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
-	// over a nondeterministic model.
-	bool optimalityOperator;
-
-	// In the case this operator is an optimizing operator, this flag indicates whether it is
-	// looking for the minimum or the maximum value.
-	bool minimumOperator;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_ */

src/formula/abstract/Or.h

@@ -1,161 +0,0 @@
-/*
- * Or.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_OR_H_
-#define STORM_FORMULA_ABSTRACT_OR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with OR node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
- * the model checker works.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Or : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::Or<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor.
-	 * Will create an AND-node without subnotes. Will not represent a complete formula!
-	 */
-	Or() {
-		left = NULL;
-		right = NULL;
-	}
-
-	/*!
-	 * Constructor.
-	 * Creates an AND note with the parameters as subtrees.
-	 *
-	 * @param left The left sub formula
-	 * @param right The right sub formula
-	 */
-	Or(FormulaType* left, FormulaType* right) {
-		this->left = left;
-		this->right = right;
-	}
-
-	/*!
-	 * Destructor.
-	 *
-	 * The subtrees are deleted with the object
-	 * (this behavior can be prevented by setting them to NULL before deletion)
-	 */
-	virtual ~Or() {
-	  if (left != NULL) {
-		  delete left;
-	  }
-	  if (right != NULL) {
-		  delete right;
-	  }
-	}
-	
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(FormulaType* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(FormulaType* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const FormulaType& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const FormulaType& 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 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);
-    }
-
-private:
-	FormulaType* left;
-	FormulaType* right;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_OR_H_ */

src/formula/abstract/PathBoundOperator.h

@@ -1,194 +0,0 @@
-/*
- * PathBoundOperator.h
- *
- *  Created on: 27.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/ComparisonType.h"
-
-#include "src/formula/abstract/OptimizingOperator.h"
-
-#include "src/utility/constants.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * 	  The formula holds iff the probability that the path formula holds is inside the bounds
- * 	  specified in this operator
- *
- * The subtree is seen as part of the object and deleted with it
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathNoBoundOperator
- */
-template<class T, class FormulaType>
-class PathBoundOperator : public virtual AbstractFormula<T>, public OptimizingOperator {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::PathBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Constructor for non-optimizing operator.
-	 *
-	 * @param comparisonOperator The relation for the bound.
-	 * @param bound The bound for the probability
-	 * @param pathFormula The child node
-	 */
-	PathBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula)
-		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
-		// Intentionally left empty
-	}
-	
-	/*!
-	 * Constructor for optimizing operator.
-	 *
-	 * @param comparisonOperator The relation for the bound.
-	 * @param bound The bound for the probability
-	 * @param pathFormula The child node
-	 * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
-	 */
-	PathBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula, bool minimumOperator)
-		: OptimizingOperator(minimumOperator), 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 ~PathBoundOperator() {
-	 if (pathFormula != nullptr) {
-		 delete pathFormula;
-	 }
-	}
-
-	/*!
-	 * @returns the child node (representation of a formula)
-	 */
-	const FormulaType& getPathFormula () const {
-		return *pathFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param pathFormula the path formula that becomes the new child node
-	 */
-	void setPathFormula(FormulaType* 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;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = "";
-		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;
-	}
-
-	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;
-		}
-	}
-
-	/*!
-     *  @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);
-    }
-
-private:
-	storm::property::ComparisonType comparisonOperator;
-	T bound;
-	FormulaType* pathFormula;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_ */

src/formula/abstract/PathNoBoundOperator.h

@@ -1,160 +0,0 @@
-/*
- * PathNoBoundOperator.h
- *
- *  Created on: 27.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/abstract/OptimizingOperator.h"
-
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-/*!
- * @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 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)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathBoundOperator
- */
-template <class T, class FormulaType>
-class PathNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::PathNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	PathNoBoundOperator() :
-		OptimizingOperator(false) {
-		this->pathFormula = nullptr;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	PathNoBoundOperator(FormulaType* pathFormula) {
-		this->pathFormula = pathFormula;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 * @param minimumOperator A flag indicating whether this operator is a minimizing or a
-	 * maximizing operator.
-	 */
-	PathNoBoundOperator(FormulaType* pathFormula, bool minimumOperator)
-		: OptimizingOperator(minimumOperator) {
-		this->pathFormula = pathFormula;
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~PathNoBoundOperator() {
-		if (pathFormula != NULL) {
-			delete pathFormula;
-		}
-	}
-
-	/*!
-	 * @returns the child node (representation of an abstract path formula)
-	 */
-	const FormulaType& getPathFormula () const {
-		return *pathFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param pathFormula the path formula that becomes the new child node
-	 */
-	void setPathFormula(FormulaType* 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 a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result;
-		if (this->isOptimalityOperator()) {
-			if (this->isMinimumOperator()) {
-				result += "min";
-			} else {
-				result += "max";
-			}
-		}
-		result += " = ? [";
-		result += this->getPathFormula().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->pathFormula);
-	}
-
-private:
-	FormulaType* pathFormula;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_ */

src/formula/abstract/ProbabilisticBoundOperator.h

@@ -1,114 +0,0 @@
-/*
- * ProbabilisticBoundOperator.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/PathBoundOperator.h"
-#include "src/formula/abstract/OptimizingOperator.h"
-#include "utility/constants.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one Abstract path formula as sub formula/tree.
- *
- * @par Semantics
- * 	  The formula holds iff the probability that the path formula holds is inside the bounds
- * 	  specified in this operator
- *
- * The subtree is seen as part of the object and deleted with it
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see AbstractFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
- */
-template<class T, class FormulaType>
-class ProbabilisticBoundOperator : public PathBoundOperator<T, FormulaType> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::ProbabilisticBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	ProbabilisticBoundOperator() : PathBoundOperator<T, FormulaType>
-		(LESS_EQUAL, storm::utility::constantZero<T>(), nullptr) {
-		// Intentionally left empty
-	}
-
-
-	/*!
-	 * Constructor
-	 *
-	 * @param comparisonRelation The relation to compare the actual value and the bound
-	 * @param bound The bound for the probability
-	 * @param pathFormula The child node
-	 */
-	ProbabilisticBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			FormulaType* pathFormula)
-			: PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param comparisonRelation
-	 * @param bound
-	 * @param pathFormula
-	 * @param minimumOperator
-	 */
-	ProbabilisticBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			FormulaType* pathFormula,
-			bool minimumOperator)
-			: PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula, minimumOperator){
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~ProbabilisticBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = "P ";
-		result += PathBoundOperator<T, FormulaType>::toString();
-		return result;
-	}
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_ */

src/formula/abstract/ProbabilisticNoBoundOperator.h

@@ -1,104 +0,0 @@
-/*
- * ProbabilisticNoBoundOperator.h
- *
- *  Created on: 12.12.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "PathNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @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)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathNoBoundOperator
- * @see ProbabilisticBoundOperator
- */
-template <class T, class FormulaType>
-class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::ProbabilisticNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	ProbabilisticNoBoundOperator() : PathNoBoundOperator<T, FormulaType>(nullptr) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	ProbabilisticNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T, FormulaType>(pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~ProbabilisticNoBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	ProbabilisticNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T, FormulaType>(pathFormula, minimumOperator) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = "P";
-		result += PathNoBoundOperator<T, FormulaType>::toString();
-		return result;
-	}
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/abstract/RewardBoundOperator.h

@@ -1,106 +0,0 @@
-/*
- * RewardBoundOperator.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_
-
-#include "PathBoundOperator.h"
-#include "utility/constants.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a R (reward) operator node over a reward interval as root.
- *
- * Has a reward path formula as sub formula/tree.
- *
- * @par Semantics
- * 	  The formula holds iff the reward of the reward path formula is inside the bounds
- * 	  specified in this operator
- *
- * The subtree is seen as part of the object and deleted with it
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathBoundOperator
- * @see RewardNoBoundOperator
- */
-template<class T, class FormulaType>
-class RewardBoundOperator : public PathBoundOperator<T, FormulaType> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::RewardBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	RewardBoundOperator() : PathBoundOperator<T, FormulaType>(LESS_EQUAL, storm::utility::constantZero<T>(), nullptr) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param comparisonRelation The relation to compare the actual value and the bound
-	 * @param bound The bound for the probability
-	 * @param pathFormula The child node
-	 */
-	RewardBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			FormulaType* pathFormula) :
-				PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 * @param comparisonRelation
-	 * @param bound
-	 * @param pathFormula
-	 * @param minimumOperator
-	 */
-	RewardBoundOperator(
-			storm::property::ComparisonType comparisonRelation,
-			T bound,
-			FormulaType* pathFormula,
-			bool minimumOperator)
-			: PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula, minimumOperator) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~RewardBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = "R ";
-		result += PathBoundOperator<T, FormulaType>::toString();
-		return result;
-	}
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_ */

src/formula/abstract/RewardNoBoundOperator.h

@@ -1,103 +0,0 @@
-/*
- * RewardNoBoundOperator.h
- *
- *  Created on: 25.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_
-
-#include "AbstractFormula.h"
-#include "PathNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @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 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)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathNoBoundOperator
- * @see RewardBoundOperator
- */
-template <class T, class FormulaType>
-class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::RewardNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	RewardNoBoundOperator() : PathNoBoundOperator<T, FormulaType>(nullptr) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T, FormulaType>(pathFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param pathFormula The child node.
-	 */
-	RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T, FormulaType>(pathFormula, minimumOperator) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~RewardNoBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = "R";
-		result += PathNoBoundOperator<T, FormulaType>::toString();
-		return result;
-	}
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_ */

src/formula/abstract/StateBoundOperator.h

@@ -1,174 +0,0 @@
-/*
- * BoundOperator.h
- *
- *  Created on: 27.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/ComparisonType.h"
-#include "src/utility/constants.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * 	  The formula holds iff the probability that the state formula holds is inside the bounds
- * 	  specified in this operator
- *
- * The subtree is seen as part of the object and deleted with it
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see StateNoBoundOperator
- */
-template<class T, class FormulaType>
-class StateBoundOperator : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::StateBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-
-	/*!
-	 * Constructor
-	 *
-	 * @param comparisonOperator The relation for the bound.
-	 * @param bound The bound for the probability
-	 * @param stateFormula The child node
-	 */
-	StateBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* stateFormula)
-		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * The subtree is deleted with the object
-	 * (this behavior can be prevented by setting them to NULL before deletion)
-	 */
-	virtual ~StateBoundOperator() {
-	 if (stateFormula != nullptr) {
-		 delete stateFormula;
-	 }
-	}
-
-	/*!
-	 * @returns the child node (representation of a formula)
-	 */
-	const FormulaType& getStateFormula () const {
-		return *stateFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param stateFormula the state formula that becomes the new child node
-	 */
-	void setStateFormula(FormulaType* 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;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = " ";
-		switch (comparisonOperator) {
-		case LESS: result += "< "; break;
-		case LESS_EQUAL: result += "<= "; break;
-		case GREATER: result += "> "; break;
-		case GREATER_EQUAL: result += ">= "; break;
-		}
-		result += std::to_string(bound);
-		result += " [";
-		result += stateFormula->toString();
-		result += "]";
-		return result;
-	}
-
-	bool meetsBound(T value) const {
-		switch (comparisonOperator) {
-		case LESS: return value < bound; break;
-		case LESS_EQUAL: return value <= bound; break;
-		case GREATER: return value > bound; break;
-		case GREATER_EQUAL: return value >= bound; break;
-		default: return false;
-		}
-	}
-
-	/*!
-     *  @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);
-    }
-
-private:
-	ComparisonType comparisonOperator;
-	T bound;
-	FormulaType* stateFormula;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_ */

src/formula/abstract/StateNoBoundOperator.h

@@ -1,126 +0,0 @@
-/*
- * StateNoBoundOperator.h
- *
- *  Created on: 09.04.2013
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with an operator without declaration of bounds.
- * as root.
- *
- * Checking a formula with this operator as root returns the probabilities that the path formula holds
- * (for each state)
- *
- * Has one 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)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see StateBoundOperator
- */
-template <class T, class FormulaType>
-class StateNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::StateNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	StateNoBoundOperator() {
-		stateFormula = nullptr;
-	}
-
-	/*!
-	 * Constructor
-	 */
-	StateNoBoundOperator(FormulaType* stateFormula) {
-		this->stateFormula = stateFormula;
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * Deletes the subtree
-	 */
-	virtual ~StateNoBoundOperator() {
-		if (stateFormula != nullptr) {
-			delete stateFormula;
-		}
-	}
-
-	const FormulaType& getStateFormula() const {
-		return *(this->stateFormula);
-	}
-
-	void setStateFormula(FormulaType* 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 a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result;
-		result += " = ? [";
-		result += this->getStateFormula().toString();
-		result += "]";
-		return result;
-	}
-
-	/*!
-     *  @brief Checks if the subtree conforms to some logic.
-     *
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
-		return checker.validate(this->stateFormula);
-	}
-
-private:
-	FormulaType* stateFormula;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-#endif /* STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_ */

src/formula/abstract/SteadyStateBoundOperator.h

@@ -1,77 +0,0 @@
-/*
- * SteadyState.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_
-
-#include "StateBoundOperator.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff \e child holds  SteadyStateOperator step, \e child holds
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class SteadyStateBoundOperator : public StateBoundOperator<T, FormulaType> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::SteadyStateBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	SteadyStateBoundOperator() : StateBoundOperator<T, FormulaType>
-		(LESS_EQUAL, storm::utility::constantZero<T>(), nullptr) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param stateFormula The child node
-	 */
-	SteadyStateBoundOperator(
-		storm::property::ComparisonType comparisonRelation, T bound, FormulaType* stateFormula) :
-			StateBoundOperator<T, FormulaType>(comparisonRelation, bound, stateFormula) {
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~SteadyStateBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		return "S" + StateBoundOperator<T, FormulaType>::toString();
-	}
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_ */

src/formula/abstract/SteadyStateNoBoundOperator.h

@@ -1,76 +0,0 @@
-/*
- * SteadyStateNoBoundOperator.h
- *
- *  Created on: 09.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_
-
-#include "StateNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a steady state operator as root, without explicit declaration of bounds.
- *
- * Checking a formula with this operator as root returns the exact bound parameter for the corresponding subformula.
- * (for each state)
- *
- * Has one formula as sub formula/tree.
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- */
-template <class T, class FormulaType>
-class SteadyStateNoBoundOperator: public StateNoBoundOperator<T, FormulaType> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::SteadyStateNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	SteadyStateNoBoundOperator() : StateNoBoundOperator<T, FormulaType>() {
-		// Intentionally left empty
-
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param stateFormula The state formula that forms the subtree
-	 */
-	SteadyStateNoBoundOperator(FormulaType* stateFormula)
-		: StateNoBoundOperator<T, FormulaType>(stateFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~SteadyStateNoBoundOperator() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		return "S" + StateNoBoundOperator<T, FormulaType>::toString();
-	}
-
-};
-
-} /* namespace abstract */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_ */

src/formula/abstract/SteadyStateReward.h

@@ -1,62 +0,0 @@
-/*
- * SteadyStateReward.h
- *
- *  Created on: 08.04.2013
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_
-#define STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <string>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a Steady State Reward node as root.
- *
- * @see AbstractFormula
- */
-template <class T>
-class SteadyStateReward: public virtual AbstractFormula<T> {
-public:
-	/*!
-	 * Empty constructor
-	 */
-	SteadyStateReward() {
-		// Intentionally left empty
-
-	}
-	virtual ~SteadyStateReward() {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * @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 abstract
-} //namespace property
-} //namespace storm
-#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_ */

src/formula/abstract/TimeBoundedEventually.h

@@ -1,107 +0,0 @@
-/*
- * TimeBoundedEventually.h
- *
- *  Created on: 10.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_
-
-#include "TimeBoundedOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * Class for a formula tree with a time bounded eventually operator as root.
- *
- * Has two subformulas.
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- */
-template<class T, class FormulaType>
-class TimeBoundedEventually: public storm::property::abstract::TimeBoundedOperator<T> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::TimeBoundedEventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/**
-	 * Simple constructor: Only sets the bounds
-	 *
-	 * @param lowerBound
-	 * @param upperBound
-	 */
-	TimeBoundedEventually(T lowerBound, T upperBound) : TimeBoundedOperator<T>(lowerBound, upperBound) {
-		child = nullptr;
-	}
-
-	TimeBoundedEventually(T lowerBound, T upperBound, FormulaType* child) :
-		TimeBoundedOperator<T>(lowerBound, upperBound) {
-		this->child = child;
-	}
-
-	virtual ~TimeBoundedEventually() {
-		if (child != nullptr) {
-			delete child;
-		}
-	}
-
-	/*!
-	 * @returns the child node
-	 */
-	const FormulaType& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(FormulaType* 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 a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = "F";
-		result += TimeBoundedOperator<T>::toString();
-		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);
-	}
-
-private:
-	FormulaType* child;
-};
-
-} /* namespace abstract */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_ */

src/formula/abstract/TimeBoundedOperator.h

@@ -1,112 +0,0 @@
-/*
- * TimeBoundedOperator.h
- *
- *  Created on: 10.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
-
-#include <limits>
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "exceptions/InvalidArgumentException.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a operator node as root that uses a time interval
- * (with upper and lower bound)
- *
- * This class does not provide support for sub formulas; this has to be done in concrete subclasses of this abstract class.
- *
- *
- * @see AbstractFormula
- * @see AbstractFormula
- * @see AbstractFormula
- */
-template<class T>
-class TimeBoundedOperator: public virtual AbstractFormula<T> {
-public:
-	/**
-	 * Constructor
-	 *
-	 * @param lowerBound The lower bound
-	 * @param upperBound The upper bound
-	 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
-	 */
-	TimeBoundedOperator(T lowerBound, T upperBound) {
-		setInterval(lowerBound, upperBound);
-	}
-
-	/**
-	 * Destructor
-	 */
-	virtual ~TimeBoundedOperator() {
-		// Intentionally left empty
-	}
-
-	/**
-	 * 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;
-	}
-
-
-	/*!
-	 * @returns a string representation of the Interval of the formula
-	 * 			May be used in subclasses to simplify string output.
-	 */
-	virtual std::string toString() const override {
-		std::string result = "";
-		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 += "]";
-		}
-		return result;
-	}
-
-private:
-	T lowerBound, upperBound;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_ */

src/formula/abstract/TimeBoundedUntil.h

@@ -1,149 +0,0 @@
-/*
- * TimeBoundedUntil.h
- *
- *  Created on: 10.04.2013
- *      Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_
-#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_
-
-#include "TimeBoundedOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-
-/**
- * @brief
- * Class for an abstract formula tree with an time bounded until operator as root.
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- */
-template <class T, class FormulaType>
-class TimeBoundedUntil: public TimeBoundedOperator<T> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::TimeBoundedUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/**
-	 * Constructor providing bounds only;
-	 * Sub formulas are set to null.
-	 *
-	 * @param lowerBound
-	 * @param upperBound
-	 */
-	TimeBoundedUntil(T lowerBound, T upperBound) :
-		TimeBoundedOperator<T>(lowerBound, upperBound) {
-		this->left = nullptr;
-		this->right = nullptr;
-	}
-
-
-	/**
-	 * Full constructor
-	 * @param lowerBound
-	 * @param upperBound
-	 * @param left
-	 * @param right
-	 */
-	TimeBoundedUntil(T lowerBound, T upperBound, FormulaType* left, FormulaType* right) :
-		TimeBoundedOperator<T>(lowerBound, upperBound) {
-		this->left = left;
-		this->right = right;
-	}
-
-	virtual ~TimeBoundedUntil() {
-	   if (left != nullptr) {
-	   	delete left;
-	   }
-	   if (right != nullptr) {
-	   	delete right;
-	   }
-	}
-
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(FormulaType* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(FormulaType* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const FormulaType& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const FormulaType& 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 a string representation of the formula
-	 */
-	virtual std::string toString() const override {
-		std::string result = left->toString();
-		result += " U";
-		result += TimeBoundedOperator<T>::toString();
-		result += " ";
-		result += right->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->left) && checker.validate(this->right);
-	}
-
-private:
-	FormulaType* left;
-	FormulaType* right;
-};
-
-} /* namespace abstract */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_ */

src/formula/abstract/Until.h

@@ -1,159 +0,0 @@
-/*
- * Until.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_UNTIL_H_
-#define STORM_FORMULA_ABSTRACT_UNTIL_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with an Until node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
- * \e left holds always.
- *
- * The subtrees are seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * 		  "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Until : public virtual AbstractFormula<T> {
-
-	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
-	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
-				  "Instantiaton of FormulaType for storm::property::abstract::Until<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	Until() {
-		this->left = NULL;
-		this->right = NULL;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param left The left formula subtree
-	 * @param right The left formula subtree
-	 */
-	Until(FormulaType* left, FormulaType* right) {
-		this->left = left;
-		this->right = right;
-	}
-
-	/*!
-	 * Destructor.
-	 *
-	 * Also deletes the subtrees.
-	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-	 */
-	virtual ~Until() {
-	  if (left != NULL) {
-		  delete left;
-	  }
-	  if (right != NULL) {
-		  delete right;
-	  }
-	}
-
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(FormulaType* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(FormulaType* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const FormulaType& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const FormulaType& 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 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);
-    }
-
-private:
-	FormulaType* left;
-	FormulaType* right;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_UNTIL_H_ */