diff --git a/src/formula/AP.h b/src/formula/AP.h
index 00a3e8734..8bda0df06 100644
--- a/src/formula/AP.h
+++ b/src/formula/AP.h
@@ -25,74 +25,76 @@ namespace formula {
  */
 template <class T>
 class AP : public PCTLStateFormula<T> {
-   private:
-   std::string ap;
-   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;
-      }
-
-   	/*!
-   	 * Constructor
-   	 *
-   	 * Creates a new atomic proposition leaf, with the label AP
-   	 *
-   	 * @param ap The string representing the atomic proposition
-   	 */
-      AP(char* ap) {
-    	 //TODO: Does that really work?
-         this->ap = ap;
-      }
-
-      /*!
-       * Destructor.
-       * At this time, empty...
-       */
-      virtual ~AP() { }
-
-      /*!
-       * @returns the name of the atomic proposition
-       */
-      std::string getAP() {
-         return ap;
-      }
-
-      /*!
-       * @returns a string representation of the leaf.
-       *
-       */
-      virtual std::string toString() {
-         return getAP();
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * @returns a new AP-object that is identical the called object.
-       */
-      virtual PCTLStateFormula<T>* clone() {
-    	  return new AP(ap);
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-       */
-      virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkAP(this);
-      }
+
+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;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * Creates a new atomic proposition leaf, with the label AP
+	 *
+	 * @param ap The string representing the atomic proposition
+	 */
+	AP(char* ap) {
+	 //TODO: Does that really work?
+		this->ap = ap;
+	}
+
+	/*!
+	 * Destructor.
+	 * At this time, empty...
+	 */
+	virtual ~AP() { }
+
+	/*!
+	 * @returns the name of the atomic proposition
+	 */
+	std::string getAP() {
+		return ap;
+	}
+
+	/*!
+	 * @returns a string representation of the leaf.
+	 *
+	 */
+	virtual std::string toString() {
+		return getAP();
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * @returns a new AP-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+	  return new AP(ap);
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkAP(this);
+	}
+
+private:
+	std::string ap;
 };
 
 } //namespace formula
diff --git a/src/formula/And.h b/src/formula/And.h
index 8a1cd9696..16f0b6d8e 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -32,121 +32,122 @@ namespace formula {
  */
 template <class T>
 class And : public PCTLStateFormula<T> {
-   private:
-      PCTLStateFormula<T>* left;
-      PCTLStateFormula<T>* right;
-   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(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
-         this->left = left;
-         this->right = right;
-      }
-
-      /*!
-       * Destructor.
-       *
-       * The subtrees are deleted with the object
-       * (this behavior can be prevented by setting them to NULL before deletion)
-       */
-      virtual ~And() {
-    	   if (left != NULL) {
-    		   delete left;
-    	   }
-    	   if (right != NULL) {
-    		   delete right;
-    	   }
-      }
-
-      /*!
-       * Sets the left child node.
-       *
-       * @param newLeft the new left child.
-       */
-      void setLeft(PCTLStateFormula<T>* newLeft) {
-         left = newLeft;
-      }
-
-      /*!
-       * Sets the right child node.
-       *
-       * @param newRight the new right child.
-       */
-      void setRight(PCTLStateFormula<T>* newRight) {
-         right = newRight;
-      }
-
-      /*!
-       * @returns a pointer to the left child node
-       */
-      PCTLStateFormula<T>* getLeft() {
-         return left;
-      }
-
-      /*!
-       * @returns a pointer to the right child node
-       */
-      PCTLStateFormula<T>* getRight() {
-         return right;
-      }
-
-      /*!
-       * @returns a string representation of the formula
-       */
-      virtual std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " && ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new AND-object that is identical the called object.
-       */
-      virtual PCTLStateFormula<T>* clone() {
-      	And<T>* result = new And();
-     	   if (this->left != NULL) {
-     		  result->setLeft(left->clone());
-     	   }
-     	   if (this->right != NULL) {
-     		  result->setRight(right->clone());
-     	   }
-     	   return result;
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-       */
-      virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	   return modelChecker->checkAnd(this);
-      }
 
+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(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~And() {
+		if (left != NULL) {
+			delete left;
+		}
+		if (right != NULL) {
+			delete right;
+		}
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " && ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		And<T>* result = new And();
+		if (this->left != NULL) {
+		  result->setLeft(left->clone());
+		}
+		if (this->right != NULL) {
+		  result->setRight(right->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+		return modelChecker->checkAnd(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 3e48dc132..c0061691c 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -36,142 +36,145 @@ namespace formula {
  */
 template <class T>
 class BoundedUntil : public PCTLPathFormula<T> {
-      PCTLStateFormula<T>* left;
-      PCTLStateFormula<T>* right;
-      uint_fast64_t bound;
-   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(PCTLStateFormula<T>* left, PCTLStateFormula<T>* 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(PCTLStateFormula<T>* newLeft) {
-         left = newLeft;
-      }
-
-      /*!
-       * Sets the right child node.
-       *
-       * @param newRight the new right child.
-       */
-      void setRight(PCTLStateFormula<T>* newRight) {
-         right = newRight;
-      }
-
-      /*!
-       * @returns a pointer to the left child node
-       */
-      PCTLStateFormula<T>* getLeft() {
-         return left;
-      }
-
-      /*!
-       * @returns a pointer to the right child node
-       */
-      PCTLStateFormula<T>* getRight() {
-         return right;
-      }
-
-      /*!
-       * @returns the maximally allowed number of steps for the bounded until operator
-       */
-      uint_fast64_t getBound() {
-         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() {
-         std::string result = "(";
-         result += left->toString();
-         result += " U<=";
-         result +=  boost::lexical_cast<std::string>(bound);
-         result += " ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new BoundedUntil-object that is identical the called object.
-       */
-      virtual PCTLPathFormula<T>* clone() {
-     	   BoundedUntil<T>* result = new BoundedUntil();
-     	   result->setBound(bound);
-     	   if (left != NULL) {
-     	   	result->setLeft(left->clone());
-     	   }
-     	   if (right != NULL) {
-     	   	result->setRight(right->clone());
-     	   }
-     	   return result;
-      }
-
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A vector indicating the probability that the formula holds for each state.
-       */
-      virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkBoundedUntil(this);
-      }
+
+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(PCTLStateFormula<T>* left, PCTLStateFormula<T>* 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(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns the maximally allowed number of steps for the bounded until operator
+	 */
+	uint_fast64_t getBound() {
+		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() {
+		std::string result = "(";
+		result += left->toString();
+		result += " U<=";
+		result +=  boost::lexical_cast<std::string>(bound);
+		result += " ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() {
+		BoundedUntil<T>* result = new BoundedUntil();
+		result->setBound(bound);
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			result->setRight(right->clone());
+		}
+		return result;
+	}
+
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkBoundedUntil(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
+	uint_fast64_t bound;
 };
 
 } //namespace formula
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 6000366ff..4ec120b80 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -32,90 +32,92 @@ namespace formula {
  */
 template <class T>
 class Next : public PCTLPathFormula<T> {
-   private:
-      PCTLStateFormula<T>* child;
-   public:
-      /*!
-       * Empty constructor
-       */
-      Next() {
-         this->child = NULL;
-      }
-
-      /*!
-       * Constructor
-       *
-       * @param child The child node
-       */
-      Next(PCTLStateFormula<T>* 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
-       */
-      PCTLStateFormula<T>* getChild() {
-         return child;
-      }
-
-      /*!
-       * Sets the subtree
-       * @param child the new child node
-       */
-      void setChild(PCTLStateFormula<T>* child) {
-         this->child = child;
-      }
-
-      /*!
-       * @returns a string representation of the formula
-       */
-      virtual std::string toString() {
-         std::string result = "(";
-         result += " X ";
-         result += child->toString();
-         result += ")";
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new BoundedUntil-object that is identical the called object.
-       */
-      virtual PCTLPathFormula<T>* clone() {
-      	Next<T>* result = new Next<T>();
-      	if (child != NULL) {
-      		result->setChild(child);
-      	}
-      	return result;
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A vector indicating the probability that the formula holds for each state.
-       */
-      virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkNext(this);
-      }
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Next() {
+		this->child = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Next(PCTLStateFormula<T>* 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
+	 */
+	PCTLStateFormula<T>* getChild() {
+		return child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += " X ";
+		result += child->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() {
+		Next<T>* result = new Next<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkNext(this);
+	}
+
+private:
+	PCTLStateFormula<T>* child;
 };
 
 } //namespace formula
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 59f100f70..dfcb7c100 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -28,87 +28,89 @@ namespace formula {
  */
 template <class T>
 class Not : public PCTLStateFormula<T> {
-   private:
-      PCTLStateFormula<T>* child;
-   public:
-      /*!
-       * Empty constructor
-       */
-      Not() {
-         this->child = NULL;
-      }
-
-      /*!
-       * Constructor
-       * @param child The child node
-       */
-      Not(PCTLStateFormula<T>* child) {
-         this->child = child;
-      }
-
-      /*!
-       * Destructor
-       *
-       * Also deletes the subtree
-       * (this behavior can be prevented by setting them to NULL before deletion)
-       */
-      virtual ~Not() {
-    	  if (child != NULL) {
-    		  delete child;
-    	  }
-      }
-
-      /*!
-       * @returns The child node
-       */
-      PCTLStateFormula<T>* getChild() {
-         return child;
-      }
-
-      /*!
-       * Sets the subtree
-       * @param child the new child node
-       */
-      void setChild(PCTLStateFormula<T>* child) {
-         this->child = child;
-      }
-
-      /*!
-       * @returns a string representation of the formula
-       */
-      virtual std::string toString() {
-         std::string result = "!";
-         result += child->toString();
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new AND-object that is identical the called object.
-       */
-      virtual PCTLStateFormula<T>* clone() {
-      	Not<T>* result = new Not<T>();
-      	if (child != NULL) {
-      		result->setChild(child);
-      	}
-      	return result;
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-       */
-      virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkNot(this);
-      }
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Not() {
+		this->child = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 * @param child The child node
+	 */
+	Not(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * Also deletes the subtree
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Not() {
+	  if (child != NULL) {
+		  delete child;
+	  }
+	}
+
+	/*!
+	 * @returns The child node
+	 */
+	PCTLStateFormula<T>* getChild() {
+		return child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "!";
+		result += child->toString();
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		Not<T>* result = new Not<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkNot(this);
+	}
+
+private:
+	PCTLStateFormula<T>* child;
 };
 
 } //namespace formula
diff --git a/src/formula/Or.h b/src/formula/Or.h
index a5cdbc659..51a2f88fd 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -31,120 +31,122 @@ namespace formula {
  */
 template <class T>
 class Or : public PCTLStateFormula<T> {
-   private:
-      PCTLStateFormula<T>* left;
-      PCTLStateFormula<T>* right;
-   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(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
-         this->left = left;
-         this->right = right;
-      }
-
-      /*!
-       * Destructor.
-       *
-       * The subtrees are deleted with the object
-       * (this behavior can be prevented by setting them to NULL before deletion)
-       */
-      virtual ~Or() {
-    	  if (left != NULL) {
-    		  delete left;
-    	  }
-    	  if (right != NULL) {
-    		  delete right;
-    	  }
-      }
-
-      /*!
-       * Sets the left child node.
-       *
-       * @param newLeft the new left child.
-       */
-      void setLeft(PCTLStateFormula<T>* newLeft) {
-         left = newLeft;
-      }
-
-      /*!
-       * Sets the right child node.
-       *
-       * @param newRight the new right child.
-       */
-      void setRight(PCTLStateFormula<T>* newRight) {
-         right = newRight;
-      }
-
-      /*!
-       * @returns a pointer to the left child node
-       */
-      PCTLStateFormula<T>* getLeft() {
-         return left;
-      }
-
-      /*!
-       * @returns a pointer to the right child node
-       */
-      PCTLStateFormula<T>* getRight() {
-         return right;
-      }
-
-      /*!
-       * @returns a string representation of the formula
-       */
-      virtual std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " || ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new AND-object that is identical the called object.
-       */
-      virtual PCTLStateFormula<T>* clone() {
-      	Or<T>* result = new Or();
-     	   if (this->left != NULL) {
-     		  result->setLeft(left->clone());
-     	   }
-     	   if (this->right != NULL) {
-     		  result->setRight(right->clone());
-     	   }
-     	   return result;
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-       */
-      virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkOr(this);
-      }
+
+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(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Or() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " || ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		Or<T>* result = new Or();
+		if (this->left != NULL) {
+		  result->setLeft(left->clone());
+		}
+		if (this->right != NULL) {
+		  result->setRight(right->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkOr(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h
index 70255f8b3..b795244e3 100644
--- a/src/formula/PCTLPathFormula.h
+++ b/src/formula/PCTLPathFormula.h
@@ -27,34 +27,35 @@ namespace formula {
  */
 template <class T>
 class PCTLPathFormula : public PCTLFormula<T> {
-   public:
-		/*!
-		 * empty destructor
-		 */
-	   virtual ~PCTLPathFormula() { }
 
-	   /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @note This function is not implemented in this class.
-       * @returns a new AND-object that is identical the called object.
-	    */
-      virtual PCTLPathFormula<T>* clone() = 0;
+public:
+	/*!
+	 * empty destructor
+	 */
+	virtual ~PCTLPathFormula() { }
 
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @note This function is not implemented in this class.
-       *
-       * @returns A vector indicating the probability that the formula holds for each state.
-       */
-      virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h
index de8d0e117..daf369510 100644
--- a/src/formula/PCTLStateFormula.h
+++ b/src/formula/PCTLStateFormula.h
@@ -27,34 +27,35 @@ namespace formula {
  */
 template <class T>
 class PCTLStateFormula : public PCTLFormula<T> {
-   public:
-		/*!
-		 * empty destructor
-		 */
-	   virtual ~PCTLStateFormula() { }
 
-	   /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @note This function is not implemented in this class.
-       * @returns a new AND-object that is identical the called object.
-	    */
-      virtual PCTLStateFormula<T>* clone() = 0;
+public:
+	/*!
+	 * empty destructor
+	 */
+	virtual ~PCTLStateFormula() { }
 
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @note This function is not implemented in this class.
-       *
-       * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-       */
-   	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h
index 12f51a4ce..b1e7bf0b9 100644
--- a/src/formula/PCTLformula.h
+++ b/src/formula/PCTLformula.h
@@ -27,17 +27,18 @@ namespace formula {
  */
 template <class T>
 class PCTLFormula {
-   public:
-		/*!
-		 * virtual destructor
-		 */
-	   virtual ~PCTLFormula() { }
-
-	   /*!
-	    * @note This function is not implemented in this class.
-	    * @returns a string representation of the formula
-	    */
-      virtual std::string toString() = 0;
+
+public:
+	/*!
+	 * virtual destructor
+	 */
+	virtual ~PCTLFormula() { }
+
+	/*!
+	 * @note This function is not implemented in this class.
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index 89978f30f..b0585fd58 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -34,128 +34,131 @@ namespace formula {
  */
 template<class T>
 class ProbabilisticOperator : public PCTLStateFormula<T> {
-      T lower;
-      T upper;
-      PCTLPathFormula<T>* pathFormula;
-   public:
-      /*!
-       * Empty constructor
-       */
-      ProbabilisticOperator() {
-      	upper = mrmc::misc::constGetZero(&upper);
-      	lower = mrmc::misc::constGetZero(&lower);
-      	pathFormula = NULL;
-      }
-
-      /*!
-       * Constructor
-       *
-       * @param lowerBound The lower bound for the probability
-       * @param upperBound The upper bound for the probability
-       * @param pathFormula The child node (can be omitted, is then set to NULL)
-       */
-      ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
-         this->lower = lowerBound;
-         this->upper = upperBound;
-         this->pathFormula = pathFormula;
-      }
-
-      /*!
-       * Destructor
-       *
-       * The subtree is deleted with the object
-       * (this behavior can be prevented by setting them to NULL before deletion)
-       */
-      virtual ~ProbabilisticOperator() {
-    	 if (pathFormula != NULL) {
-    		 delete pathFormula;
-    	 }
-      }
-
-      /*!
-       * @returns the child node (representation of a PCTL path formula)
-       */
-      PCTLPathFormula<T>* getPathFormula () {
-         return pathFormula;
-      }
-
-      /*!
-       * @returns the lower bound for the probability
-       */
-      T getLowerBound() {
-         return lower;
-      }
-
-      /*!
-       * @returns the upper bound for the probability
-       */
-      T getUpperBound() {
-         return upper;
-      }
-
-      /*!
-       * Sets the child node
-       *
-       * @param pathFormula the path formula that becomes the new child node
-       */
-      void setPathFormula(PCTLPathFormula<T>* pathFormula) {
-         this->pathFormula = pathFormula;
-      }
-
-      /*!
-       * Sets the interval in which the probability that the path formula holds may lie.
-       *
-       * @param lowerBound The lower bound for the probability
-       * @param upperBound The upper bound for the probability
-       */
-      void setInterval(T lowerBound, T upperBound) {
-         this->lower = lowerBound;
-         this->upper = upperBound;
-      }
-
-      /*!
-       * @returns a string representation of the formula
-       */
-      virtual std::string toString() {
-         std::string result = "(";
-         result += " P[";
-         result += lower;
-         result += ";";
-         result += upper;
-         result += "] ";
-         result += pathFormula->toString();
-         result += ")";
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new AND-object that is identical the called object.
-       */
-      virtual PCTLStateFormula<T>* clone() {
-      	ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
-      	result->setInterval(lower, upper);
-      	if (pathFormula != NULL) {
-      		result->setPathFormula(pathFormula->clone());
-      	}
-      	return result;
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-       */
-      virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkProbabilisticOperator(this);
-      }
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticOperator() {
+		upper = mrmc::misc::constGetZero(&upper);
+		lower = mrmc::misc::constGetZero(&lower);
+		pathFormula = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param lowerBound The lower bound for the probability
+	 * @param upperBound The upper bound for the probability
+	 * @param pathFormula The child node (can be omitted, is then set to NULL)
+	 */
+	ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
+		this->lower = lowerBound;
+		this->upper = upperBound;
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~ProbabilisticOperator() {
+	 if (pathFormula != NULL) {
+		 delete pathFormula;
+	 }
+	}
+
+	/*!
+	 * @returns the child node (representation of a PCTL path formula)
+	 */
+	PCTLPathFormula<T>* getPathFormula () {
+		return pathFormula;
+	}
+
+	/*!
+	 * @returns the lower bound for the probability
+	 */
+	T getLowerBound() {
+		return lower;
+	}
+
+	/*!
+	 * @returns the upper bound for the probability
+	 */
+	T getUpperBound() {
+		return upper;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 * Sets the interval in which the probability that the path formula holds may lie.
+	 *
+	 * @param lowerBound The lower bound for the probability
+	 * @param upperBound The upper bound for the probability
+	 */
+	void setInterval(T lowerBound, T upperBound) {
+		this->lower = lowerBound;
+		this->upper = upperBound;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += " P[";
+		result += lower;
+		result += ";";
+		result += upper;
+		result += "] ";
+		result += pathFormula->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
+		result->setInterval(lower, upper);
+		if (pathFormula != NULL) {
+			result->setPathFormula(pathFormula->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkProbabilisticOperator(this);
+	}
+
+private:
+	T lower;
+	T upper;
+	PCTLPathFormula<T>* pathFormula;
 };
 
 } //namespace formula
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 39f361e11..df80ee0e0 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -33,117 +33,120 @@ namespace formula {
  */
 template <class T>
 class Until : public PCTLPathFormula<T> {
-      PCTLStateFormula<T>* left;
-      PCTLStateFormula<T>* right;
-   public:
-      /*!
-       * Empty constructor
-       */
-      Until() {
-         this->left = NULL;
-         this->right = NULL;
-      }
-
-      /*!
-       * Constructor
-       *
-       * @param left The left formula subtree
-       * @param right The left formula subtree
-       */
-      Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
-         this->left = left;
-         this->right = right;
-      }
-
-      /*!
-       * Destructor.
-       *
-       * Also deletes the subtrees.
-       * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-       */
-      virtual ~Until() {
-    	  if (left != NULL) {
-    		  delete left;
-    	  }
-    	  if (right != NULL) {
-    		  delete right;
-    	  }
-      }
-
-      /*!
-       * Sets the left child node.
-       *
-       * @param newLeft the new left child.
-       */
-      void setLeft(PCTLStateFormula<T>* newLeft) {
-         left = newLeft;
-      }
-
-      /*!
-       * Sets the right child node.
-       *
-       * @param newRight the new right child.
-       */
-      void setRight(PCTLStateFormula<T>* newRight) {
-         right = newRight;
-      }
-
-      /*!
-       * @returns a pointer to the left child node
-       */
-      PCTLStateFormula<T>* getLeft() {
-         return left;
-      }
-
-      /*!
-       * @returns a pointer to the right child node
-       */
-      PCTLStateFormula<T>* getRight() {
-         return right;
-      }
-
-      /*!
-       * @returns a string representation of the formula
-       */
-      virtual std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " U ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      /*!
-       * Clones the called object.
-       *
-       * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-       *
-       * @returns a new BoundedUntil-object that is identical the called object.
-       */
-      virtual PCTLPathFormula<T>* clone() {
-     	   Until<T>* result = new Until();
-     	   if (left != NULL) {
-     	   	result->setLeft(left->clone());
-     	   }
-     	   if (right != NULL) {
-     	   	result->setRight(right->clone());
-     	   }
-     	   return result;
-      }
-
-      /*!
-       * Calls the model checker to check this formula.
-       * Needed to infer the correct type of formula class.
-       *
-       * @note This function should only be called in a generic check function of a model checker class. For other uses,
-       *       the methods of the model checker should be used.
-       *
-       * @returns A vector indicating the probability that the formula holds for each state.
-       */
-      virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-    	  return modelChecker->checkUntil(this);
-      }
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Until() {
+		this->left = NULL;
+		this->right = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 */
+	Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Until() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " U ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() {
+		Until<T>* result = new Until();
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			result->setRight(right->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkUntil(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula