Added formula classes for CSL

src/formula/Csl.h

@@ -0,0 +1,28 @@
+/*
+ * Csl.h
+ *
+ *  Created on: 19.04.2013
+ *      Author: thomas
+ */
+
+#ifndef CSL_H_
+#define CSL_H_
+
+#include "Csl/And.h"
+#include "Csl/Ap.h"
+#include "Csl/Next.h"
+#include "Csl/Not.h"
+#include "Csl/Or.h"
+#include "Csl/ProbabilisticNoBoundOperator.h"
+#include "Csl/ProbabilisticBoundOperator.h"
+#include "Csl/SteadyStateNoBoundOperator.h"
+#include "Csl/SteadyStateBoundOperator.h"
+
+#include "Csl/Until.h"
+#include "Csl/Eventually.h"
+#include "Csl/Globally.h"
+#include "Csl/TimeBoundedEventually.h"
+#include "Csl/TimeBoundedUntil.h"
+
+
+#endif /* CSL_H_ */

src/formula/Csl/AbstractCslFormula.h

@@ -0,0 +1,28 @@
+/*
+ * AbstractCslFormula.h
+ *
+ *  Created on: 19.04.2013
+ *      Author: thomas
+ */
+
+#ifndef ABSTRACTCSLFORMULA_H_
+#define ABSTRACTCSLFORMULA_H_
+
+#include "src/formula/abstract/AbstractFormula.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T>
+class AbstractCslFormula : public virtual storm::formula::abstract::AbstractFormula<T>{
+public:
+	virtual ~AbstractCslFormula() {
+		// Intentionally left empty
+	}
+};
+
+} /* namespace csl */
+} /* namespace formula */
+} /* namespace storm */
+#endif /* ABSTRACTCSLFORMULA_H_ */

src/formula/Csl/AbstractNoBoundOperator.h

@@ -0,0 +1,80 @@
+/*
+ * AbstractNoBoundOperator.h
+ *
+ *  Created on: 16.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_
+
+#include "AbstractCslFormula.h"
+#include "src/formula/abstract/IOptimizingOperator.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T>
+class AbstractNoBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support PathNoBoundOperator.
+ *
+ *  All model checkers that support the formula class NoBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class INoBoundOperatorModelChecker {
+public:
+	/*!
+     *  @brief Evaluates NoBoundOperator formula within a model checker.
+     *
+     *  @param obj Formula object with subformulas.
+     *  @return Result of the formula for every node.
+     */
+    virtual std::vector<T>* checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
+
+
+};
+
+template <class T>
+class AbstractNoBoundOperator: public AbstractCslFormula<T>/*,
+										 public virtual storm::formula::abstract::IOptimizingOperator*/ {
+public:
+	AbstractNoBoundOperator() {
+		// TODO Auto-generated constructor stub
+
+	}
+	virtual ~AbstractNoBoundOperator() {
+		// TODO Auto-generated destructor stub
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractNoBoundOperator<T>* clone() const = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
+};
+
+} /* namespace csl */
+} /* namespace formula */
+} /* namespace storm */
+#endif /* STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ */

src/formula/Csl/AbstractPathFormula.h

@@ -5,14 +5,18 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_
-#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_
+#ifndef STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_
+#define STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_
 
-namespace storm { namespace formula {
-template <class T> class AbstractPathFormula;
-}}
+namespace storm {
+namespace formula {
+namespace csl {
+template<class T> class AbstractPathFormula;
+} //namespace csl
+} //namespace formula
+} //namespace storm
 
-#include "src/formula/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
 #include <vector>
@@ -21,6 +25,7 @@ template <class T> class AbstractPathFormula;
 
 namespace storm {
 namespace formula {
+namespace csl {
 
 /*!
  * @brief
@@ -32,13 +37,15 @@ namespace formula {
  * 	   clone().
  */
 template <class T>
-class AbstractPathFormula : public virtual AbstractFormula<T> {
+class AbstractPathFormula : public virtual storm::formula::abstract::AbstractFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~AbstractPathFormula() { }
+	virtual ~AbstractPathFormula() {
+		// Intentionally left empty
+	}
 
 	/*!
 	 * Clones the called object.
@@ -64,7 +71,8 @@ public:
 	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
 };
 
+} //namespace csl
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */
+#endif /* STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ */

src/formula/Csl/AbstractStateFormula.h

@@ -5,19 +5,24 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
-#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
+#ifndef STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_
+#define STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_
 
-namespace storm { namespace formula {
-template <class T> class AbstractStateFormula;
-}}
+namespace storm {
+namespace formula {
+namespace csl {
+template<class T> class AbstractStateFormula;
+}
+}
+}
 
-#include "src/formula/AbstractFormula.h"
+#include "AbstractCslFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
+namespace csl {
 
 /*!
  * @brief
@@ -29,13 +34,15 @@ namespace formula {
  * 	   clone().
  */
 template <class T>
-class AbstractStateFormula : public AbstractFormula<T> {
+class AbstractStateFormula : public AbstractCslFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~AbstractStateFormula() { }
+	virtual ~AbstractStateFormula() {
+		// Intentionally left empty
+	}
 
 	/*!
 	 * Clones the called object.
@@ -58,11 +65,12 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const = 0; // {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const = 0;
 };
 
+} //namespace csl
 } //namespace formula
 } //namespace storm
 
 
-#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */
+#endif /* STORM_FORMULA_CSL_AbstractSTATEFORMULA_H_ */

src/formula/Csl/And.h

@@ -0,0 +1,129 @@
+/*
+ * And.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_AND_H_
+#define STORM_FORMULA_CSL_AND_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/And.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+#include <string>
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class And;
+
+/*!
+ *	@brief Interface class for model checkers that support And.
+ *
+ *	All model checkers that support the formula class And must inherit
+ *	this pure virtual class.
+ */
+template <class T>
+class IAndModelChecker {
+	public:
+		/*!
+		 *	@brief Evaluates And formula within a model checker.
+		 *
+		 *	@param obj Formula object with subformulas.
+		 *	@return Result of the formula for every node.
+		 */
+		virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with AND node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
+ * the model checker works.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractStateFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class And : public storm::formula::abstract::And<T, AbstractStateFormula<T>>, public AbstractStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor.
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 */
+	And() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 * Creates an AND note with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
+		: storm::formula::abstract::And<T, AbstractStateFormula<T>>(left, right) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~And() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const {
+		And<T>* result = new And();
+		if (this->leftIsSet()) {
+		  result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+		  result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
+	}
+
+};
+
+} //namespace csl
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_AND_H_ */

src/formula/Csl/Ap.h

@@ -0,0 +1,106 @@
+/*
+ * Ap.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_AP_H_
+#define STORM_FORMULA_CSL_AP_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Ap.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Ap;
+
+/*!
+ *  @brief Interface class for model checkers that support Ap.
+ *
+ *  All model checkers that support the formula class Ap must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IApModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Ap formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with atomic proposition as root.
+ *
+ * This class represents the leaves in the formula tree.
+ *
+ * @see AbstractFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Ap : public storm::formula::abstract::Ap<T>,
+			  public AbstractStateFormula<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)
+		: storm::formula::abstract::Ap<T>(ap) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 * At this time, empty...
+	 */
+	virtual ~Ap() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const {
+		return new Ap(this->getAp());
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
+	}
+
+};
+
+} //namespace abstract
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_AP_H_ */

src/formula/Csl/Eventually.h

@@ -0,0 +1,120 @@
+/*
+ * Next.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_CSL_EVENTUALLY_H_
+#define STORM_FORMULA_CSL_EVENTUALLY_H_
+
+#include "src/formula/abstract/Eventually.h"
+#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Eventually;
+
+/*!
+ *  @brief Interface class for model checkers that support Eventually.
+ *
+ *  All model checkers that support the formula class Eventually must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IEventuallyModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Eventually formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with an Eventually node as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @par Semantics
+ * The formula holds iff eventually \e child holds.
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to nullptr before deletion)
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Eventually : public storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>,
+						 public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Eventually() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Eventually(AbstractStateFormula<T>* child)
+		: storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>(child) {
+
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+	 */
+	virtual ~Eventually() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new Eventually-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		Eventually<T>* result = new Eventually<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_EVENTUALLY_H_ */

src/formula/Csl/Globally.h

@@ -0,0 +1,122 @@
+/*
+ * Next.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_CSL_GLOBALLY_H_
+#define STORM_FORMULA_CSL_GLOBALLY_H_
+
+#include "src/formula/abstract/Globally.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Globally;
+
+/*!
+ *  @brief Interface class for model checkers that support Globally.
+ *   
+ *  All model checkers that support the formula class Globally must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IGloballyModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Globally formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Globally node as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @par Semantics
+ * The formula holds iff globally \e child holds.
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to nullptr before deletion)
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Globally : public storm::formula::abstract::Globally<T, AbstractStateFormula<T>>,
+					  public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Globally() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Globally(AbstractStateFormula<T>* child)
+		: storm::formula::abstract::Globally<T, AbstractStateFormula<T>>(child) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+	 */
+	virtual ~Globally() {
+	  //intentionally left empty
+	}
+
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new Globally-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		Globally<T>* result = new Globally<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_GLOBALLY_H_ */

src/formula/Csl/Next.h

@@ -0,0 +1,120 @@
+/*
+ * Next.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_NEXT_H_
+#define STORM_FORMULA_CSL_NEXT_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Next.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Next;
+
+/*!
+ *  @brief Interface class for model checkers that support Next.
+ *   
+ *  All model checkers that support the formula class Next must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class INextModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Next formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkNext(const Next<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Next node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff in the next step, \e child holds
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Next : public storm::formula::abstract::Next<T, AbstractStateFormula<T>>,
+				 public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Next() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Next(AbstractStateFormula<T>* child)
+		: storm::formula::abstract::Next<T, AbstractStateFormula<T>>(child) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Next() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		Next<T>* result = new Next<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_NEXT_H_ */

src/formula/Csl/Not.h

@@ -0,0 +1,116 @@
+/*
+ * Not.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_NOT_H_
+#define STORM_FORMULA_CSL_NOT_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Not.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Not;
+
+/*!
+ *  @brief Interface class for model checkers that support Not.
+ *   
+ *  All model checkers that support the formula class Not must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class INotModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Not formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with NOT node as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractStateFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Not : public storm::formula::abstract::Not<T, AbstractStateFormula<T>>,
+			   public AbstractStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Not() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 * @param child The child node
+	 */
+	Not(AbstractStateFormula<T>* child) :
+		storm::formula::abstract::Not<T, AbstractStateFormula<T>>(child){
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * Also deletes the subtree
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Not() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const {
+		Not<T>* result = new Not<T>();
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_NOT_H_ */

src/formula/Csl/Or.h

@@ -0,0 +1,125 @@
+/*
+ * Or.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_OR_H_
+#define STORM_FORMULA_CSL_OR_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Or.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Or;
+
+/*!
+ *  @brief Interface class for model checkers that support Or.
+ *   
+ *  All model checkers that support the formula class Or must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IOrModelChecker {
+	public:
+		/*!
+         *  @brief Evaluates Or formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+		virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with OR node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
+ * the model checker works.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractStateFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Or : public storm::formula::abstract::Or<T, AbstractStateFormula<T>>,
+			  public AbstractStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor.
+	 * Will create an OR-node without subnotes. The result does not represent a complete formula!
+	 */
+	Or() {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Constructor.
+	 * Creates an OR note with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) :
+		storm::formula::abstract::Or<T, AbstractStateFormula<T>>(left, right) {
+		//intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Or() {
+	  //intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const {
+		Or<T>* result = new Or();
+		if (this->leftIsSet()) {
+		  result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+		  result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+	
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_OR_H_ */

src/formula/Csl/ProbabilisticBoundOperator.h

@@ -0,0 +1,121 @@
+/*
+ * ProbabilisticBoundOperator.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_
+#define STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_
+
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "src/formula/abstract/ProbabilisticBoundOperator.h"
+#include "utility/ConstTemplates.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class ProbabilisticBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support ProbabilisticBoundOperator.
+ *
+ *  All model checkers that support the formula class PathBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IProbabilisticBoundOperatorModelChecker {
+    public:
+        virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
+ * as root.
+ *
+ * Has one Abstract path formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the probability that the path formula holds is inside the bounds
+ * 	  specified in this operator
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see AbstractFormula
+ */
+template<class T>
+class ProbabilisticBoundOperator : public storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>,
+											  public AbstractStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticBoundOperator() : storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>
+		(LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonRelation The relation to compare the actual value and the bound
+	 * @param bound The bound for the probability
+	 * @param pathFormula The child node
+	 */
+	ProbabilisticBoundOperator(
+			storm::formula::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
+			: storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
+		// Intentionally left empty
+	}
+
+	ProbabilisticBoundOperator(
+			storm::formula::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+			: storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula, minimumOperator){
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const {
+		ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
+		result->setComparisonOperator(this->getComparisonOperator());
+		result->setBound(this->getBound());
+		result->setPathFormula(this->getPathFormula().clone());
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ */

src/formula/Csl/ProbabilisticNoBoundOperator.h

@@ -0,0 +1,115 @@
+/*
+ * ProbabilisticNoBoundOperator.h
+ *
+ *  Created on: 12.12.2012
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractNoBoundOperator.h"
+#include "src/formula/abstract/ProbabilisticNoBoundOperator.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
+ * as root.
+ *
+ * Checking a formula with this operator as root returns the probabilities that the path formula holds
+ * (for each state)
+ *
+ * Has one Abstract path formula as sub formula/tree.
+ *
+ * @note
+ * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
+ * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
+ *
+ * @note
+ * 	This class does not contain a check() method like the other formula classes.
+ * 	The check method should only be called by the model checker to infer the correct check function for sub
+ * 	formulas. As this operator can only appear at the root, the method is not useful here.
+ * 	Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead.
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticIntervalOperator
+ * @see AbstractFormula
+ */
+template <class T>
+class ProbabilisticNoBoundOperator: public storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>,
+												public AbstractNoBoundOperator<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticNoBoundOperator() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula)
+		: storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+		: storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula, minimumOperator) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 */
+	virtual ~ProbabilisticNoBoundOperator() {
+		// Intentionally left empty
+	}
+
+	virtual AbstractNoBoundOperator<T>* clone() const {
+		ProbabilisticNoBoundOperator<T>* result = new ProbabilisticNoBoundOperator<T>();
+		if (this->pathFormulaIsSet()) {
+			result->setPathFormula(this->getPathFormula().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+		return this->getPathFormula().check(modelChecker, qualitative);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/Csl/SteadyStateBoundOperator.h

@@ -5,18 +5,19 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_
-#define STORM_FORMULA_STEADYSTATEOPERATOR_H_
+#ifndef STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_
+#define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_
 
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractStateFormula.h"
-#include "src/formula/StateBoundOperator.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/SteadyStateBoundOperator.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
 namespace formula {
 
+namespace csl {
+
 template <class T> class SteadyStateBoundOperator;
 
 /*!
@@ -53,14 +54,15 @@ class ISteadyStateBoundOperatorModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class SteadyStateBoundOperator : public StateBoundOperator<T> {
+class SteadyStateBoundOperator : public storm::formula::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>,
+											public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	SteadyStateBoundOperator() : StateBoundOperator<T>
-		(StateBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+	SteadyStateBoundOperator() : storm::formula::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>
+		(LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
 		// Intentionally left empty
 	}
 
@@ -70,15 +72,15 @@ public:
 	 * @param stateFormula The child node
 	 */
 	SteadyStateBoundOperator(
-		typename StateBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractStateFormula<T>* stateFormula) :
-			StateBoundOperator<T>(comparisonRelation, bound, stateFormula) {
+		storm::formula::ComparisonType comparisonRelation, T bound, AbstractStateFormula<T>* stateFormula) :
+			storm::formula::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>(comparisonRelation, bound, stateFormula) {
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 * Destructor
 	 */
-	virtual std::string toString() const {
-		return "S" + StateBoundOperator<T>::toString();
+	virtual ~SteadyStateBoundOperator() {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -109,7 +111,8 @@ public:
 	
 };
 
+} //namespace csl
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */
+#endif /* STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ */

src/formula/Csl/SteadyStateNoBoundOperator.h

@@ -5,13 +5,16 @@
  *      Author: thomas
  */
 
-#ifndef STORM_FORMULA_STEADYSTATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_STEADYSTATENOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_
+#define STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_
 
-#include "StateNoBoundOperator.h"
+#include "AbstractStateFormula.h"
+#include "AbstractNoBoundOperator.h"
+#include "src/formula/abstract/SteadyStateNoBoundOperator.h"
 
 namespace storm {
 namespace formula {
+namespace csl {
 
 template <class T> class SteadyStateNoBoundOperator;
 
@@ -34,12 +37,13 @@ class ISteadyStateNoBoundOperatorModelChecker {
 };
 
 template <class T>
-class SteadyStateNoBoundOperator: public storm::formula::StateNoBoundOperator<T> {
+class SteadyStateNoBoundOperator: public storm::formula::abstract::SteadyStateNoBoundOperator<T, AbstractStateFormula<T>>,
+											 public AbstractNoBoundOperator<T> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	SteadyStateNoBoundOperator() : StateNoBoundOperator<T>() {
+	SteadyStateNoBoundOperator() : storm::formula::abstract::SteadyStateNoBoundOperator<T, AbstractStateFormula<T>>() {
 		// Intentionally left empty
 
 	}
@@ -49,15 +53,16 @@ public:
 	 *
 	 * @param stateFormula The state formula that forms the subtree
 	 */
-	SteadyStateNoBoundOperator(AbstractStateFormula<T>* stateFormula) : StateNoBoundOperator<T>(stateFormula) {
+	SteadyStateNoBoundOperator(AbstractStateFormula<T>* stateFormula)
+		: storm::formula::abstract::SteadyStateNoBoundOperator<T, AbstractStateFormula<T>>(stateFormula) {
 		// Intentionally left empty
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 * Destructor
 	 */
-	virtual std::string toString() const {
-		return "S" + StateNoBoundOperator<T>::toString();
+	~SteadyStateNoBoundOperator() {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -67,12 +72,11 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	/* TODO: Add clone method to StateNoBoundOperator and use matching return type
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractNoBoundOperator <T>* clone() const {
 		SteadyStateNoBoundOperator<T>* result = new SteadyStateNoBoundOperator<T>();
 		result->setStateFormula(this->getStateFormula().clone());
 		return result;
-	}*/
+	}
 
 	/*!
 	 * Calls the model checker to check this formula.
@@ -83,12 +87,14 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>*  check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>*  check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
 		return modelChecker.template as<ISteadyStateNoBoundOperatorModelChecker>()->checkSteadyStateNoBoundOperator(*this);
 	}
 
 };
 
+} /* namespace csl */
 } /* namespace formula */
 } /* namespace storm */
-#endif /* STORM_FORMULA_STEADYSTATENOBOUNDOPERATOR_H_ */
+
+#endif /* STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ */

src/formula/Csl/TimeBoundedEventually.h

@@ -5,14 +5,16 @@
  *      Author: thomas
  */
 
-#ifndef STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_
+#ifndef STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_
+#define STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_
 
-#include "TimeBoundedOperator.h"
+#include "src/formula/abstract/TimeBoundedEventually.h"
+#include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
 
 namespace storm {
 namespace formula {
+namespace csl {
 
 template<class T> class TimeBoundedEventually;
 
@@ -36,7 +38,8 @@ class ITimeBoundedEventuallyModelChecker {
 
 
 template<class T>
-class TimeBoundedEventually: public storm::formula::TimeBoundedOperator<T> {
+class TimeBoundedEventually: public storm::formula::abstract::TimeBoundedEventually<T, AbstractStateFormula<T>>,
+									  public AbstractPathFormula<T> {
 public:
 	/**
 	 * Simple constructor: Only sets the bounds
@@ -44,46 +47,18 @@ public:
 	 * @param lowerBound
 	 * @param upperBound
 	 */
-	TimeBoundedEventually(T lowerBound, T upperBound) : TimeBoundedOperator<T>(lowerBound, upperBound) {
-		child = nullptr;
+	TimeBoundedEventually(T lowerBound, T upperBound)
+		: storm::formula::abstract::TimeBoundedEventually<T, AbstractStateFormula<T>>(lowerBound, upperBound) {
+		// Intentionally left empty
 	}
 
-	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child) :
-		TimeBoundedOperator<T>(lowerBound, upperBound) {
-		this->child = child;
+	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child)
+		: storm::formula::abstract::TimeBoundedEventually<T, AbstractStateFormula<T>>(lowerBound, upperBound, child) {
+		// Intentionally left empty
 	}
 
 	virtual ~TimeBoundedEventually() {
-		if (child != nullptr) {
-			delete child;
-		}
-	}
-
-
-	/*!
-	 * @returns the child node
-	 */
-	const AbstractStateFormula<T>& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(AbstractStateFormula<T>* child) {
-		this->child = child;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = "F";
-		result += TimeBoundedOperator<T>::toString();
-		result += " ";
-		result += child->toString();
-		return result;
+		// Intentionally left empty
 	}
 
 	/*!
@@ -95,8 +70,8 @@ public:
 	 */
 	virtual AbstractPathFormula<T>* clone() const {
 		TimeBoundedEventually<T>* result = new TimeBoundedEventually<T>(this->getLowerBound(), this->getUpperBound());
-		if (child != nullptr) {
-			result->setChild(child->clone());
+		if (this->childIsSet()) {
+			result->setChild(this->getChild().clone());
 		}
 		return result;
 	}
@@ -113,21 +88,10 @@ public:
 	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*this, qualitative);
 	}
-
-	/*!
-     *  @brief Checks if the subtree conforms to some logic.
-     *
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return checker.conforms(this->child);
-	}
-
-private:
-	AbstractStateFormula<T>* child;
 };
 
+} /* namespace csl */
 } /* namespace formula */
 } /* namespace storm */
-#endif /* STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ */
+
+#endif /* STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ */

src/formula/Csl/TimeBoundedUntil.h

@@ -5,13 +5,16 @@
  *      Author: thomas
  */
 
-#ifndef STORM_FORMULA_TIMEBOUNDEDUNTIL_H_
-#define STORM_FORMULA_TIMEBOUNDEDUNTIL_H_
+#ifndef STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_
+#define STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_
 
-#include "TimeBoundedOperator.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/TimeBoundedUntil.h"
 
 namespace storm {
 namespace formula {
+namespace csl {
 
 template <class T> class TimeBoundedUntil;
 
@@ -34,7 +37,8 @@ class ITimeBoundedUntilModelChecker {
 };
 
 template <class T>
-class TimeBoundedUntil: public storm::formula::TimeBoundedOperator<T> {
+class TimeBoundedUntil: public storm::formula::abstract::TimeBoundedUntil<T, AbstractStateFormula<T>>,
+								public AbstractPathFormula<T> {
 public:
 	/**
 	 * Constructor providing bounds only;
@@ -44,12 +48,10 @@ public:
 	 * @param upperBound
 	 */
 	TimeBoundedUntil(T lowerBound, T upperBound) :
-		TimeBoundedOperator<T>(lowerBound, upperBound) {
-		this->left = nullptr;
-		this->right = nullptr;
+		storm::formula::abstract::TimeBoundedUntil<T, AbstractStateFormula<T>>(lowerBound, upperBound) {
+		// Intentionally left empty
 	}
 
-
 	/**
 	 * Full constructor
 	 * @param lowerBound
@@ -58,62 +60,15 @@ public:
 	 * @param right
 	 */
 	TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula<T>* left, AbstractStateFormula<T>* 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(AbstractStateFormula<T>* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(AbstractStateFormula<T>* newRight) {
-		right = newRight;
-	}
+		storm::formula::abstract::TimeBoundedUntil<T, AbstractStateFormula<T>>(lowerBound, upperBound, left, right) {
 
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const AbstractStateFormula<T>& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const AbstractStateFormula<T>& getRight() const {
-		return *right;
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 * Destructor
 	 */
-	virtual std::string toString() const {
-		std::string result = left->toString();
-		result += " U";
-		result += TimeBoundedOperator<T>::toString();
-		result += " ";
-		result += right->toString();
-		return result;
+	virtual ~TimeBoundedUntil() {
+	   // Intentionally left empty
 	}
 
 	/*!
@@ -125,11 +80,11 @@ public:
 	 */
 	virtual AbstractPathFormula<T>* clone() const {
 		TimeBoundedUntil<T>* result = new TimeBoundedUntil<T>(this->getLowerBound(), this->getUpperBound());
-		if (left != nullptr) {
-			result->setLeft(left->clone());
+		if (this->leftIsSet()) {
+			result->setLeft(this->getLeft().clone());
 		}
-		if (right != nullptr) {
-			result->setRight(right->clone());
+		if (this->rightIsSet()) {
+			result->setRight(this->getRight().clone());
 		}
 		return result;
 	}
@@ -147,22 +102,10 @@ public:
 	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*this, qualitative);
 	}
-
-	/*!
-     *  @brief Checks if the subtree conforms to some logic.
-     *
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return checker.conforms(this->left) && checker.conforms(this->right);
-	}
-
-private:
-	AbstractStateFormula<T>* left;
-	AbstractStateFormula<T>* right;
 };
 
+} /* namespace csl */
 } /* namespace formula */
 } /* namespace storm */
-#endif /* STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ */
+
+#endif /* STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ */

src/formula/Csl/Until.h

@@ -0,0 +1,125 @@
+/*
+ * Until.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_CSL_UNTIL_H_
+#define STORM_FORMULA_CSL_UNTIL_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Until.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+namespace csl {
+
+template <class T> class Until;
+
+/*!
+ *  @brief Interface class for model checkers that support Until.
+ *
+ *  All model checkers that support the formula class Until must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IUntilModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates Until formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkUntil(const Until<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with an Until node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
+ * \e left holds always.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Until : public storm::formula::abstract::Until<T, AbstractStateFormula<T>>,
+				  public AbstractPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Until() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 */
+	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
+		: storm::formula::abstract::Until<T, AbstractStateFormula<T>>(left, right) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Until() {
+	  // Intentionally left empty
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		Until<T>* result = new Until();
+		if (this->leftIsSet()) {
+		  result->setLeft(this->getLeft().clone());
+		}
+		if (this->rightIsSet()) {
+		  result->setRight(this->getRight().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
+	}
+};
+
+} //namespace csl
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_CSL_UNTIL_H_ */

src/formula/Prctl/AbstractNoBoundOperator.h

@@ -5,8 +5,8 @@
  *      Author: thomas
  */
 
-#ifndef ABSTRACTNOBOUNDOPERATOR_H_
-#define ABSTRACTNOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
 
 #include "AbstractPrctlFormula.h"
 #include "src/formula/abstract/IOptimizingOperator.h"
@@ -77,4 +77,4 @@ public:
 } /* namespace prctl */
 } /* namespace formula */
 } /* namespace storm */
-#endif /* ABSTRACTNOBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ */

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -132,7 +132,7 @@ public:
 	}
 };
 
-} //namespace formula
+} //namespace prctl
 } //namespace formula
 } //namespace storm
 

src/formula/Prctl/ProbabilisticNoBoundOperator.h

@@ -108,7 +108,7 @@ public:
 	}
 };
 
-} //namespace formula
+} //namespace prctl
 } //namespace formula
 } //namespace storm
 

src/formula/abstract/StateBoundOperator.h

@@ -11,6 +11,7 @@
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/ComparisonType.h"
 #include "src/modelchecker/AbstractModelChecker.h"
 #include "src/utility/ConstTemplates.h"
 
@@ -39,11 +40,10 @@ namespace abstract {
  * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
  */
-template<class T>
+template<class T, class FormulaType>
 class StateBoundOperator : public virtual AbstractFormula<T> {
 
 public:
-	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
 
 	/*!
 	 * Constructor
@@ -52,7 +52,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param stateFormula The child node
 	 */
-	StateBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* stateFormula)
+	StateBoundOperator(storm::formula::ComparisonType comparisonOperator, T bound, FormulaType* stateFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
 		// Intentionally left empty
 	}

src/formula/abstract/StateNoBoundOperator.h

@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
 #define STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
 
-#include "src/formula/abstract/AbstractFormula.h"
+#include "AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 #include "src/modelchecker/ForwardDeclarations.h"
@@ -47,7 +47,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class StateNoBoundOperator: public storm::formula::AbstractFormula<T> {
+class StateNoBoundOperator: public virtual AbstractFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -90,21 +90,6 @@ public:
 		return stateFormula != nullptr;
 	}
 
-	/*!
-	 * Calls the model checker to check this formula.
-	 * Needed to infer the correct type of formula class.
-	 *
-	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
-	 *       the methods of the model checker should be used.
-	 *
-	 * @note This function is not implemented in this class.
-	 *
-	 * @returns A vector indicating all states that satisfy the formula represented by the called object.
-	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IStateNoBoundOperatorModelChecker>()->checkStateNoBoundOperator(*this);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */

src/formula/abstract/SteadyStateBoundOperator.h

@@ -0,0 +1,74 @@
+/*
+ * 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 formula {
+namespace abstract {
+
+/*!
+ * @brief
+ * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root.
+ *
+ * Has two Abstract state 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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T, class FormulaType>
+class SteadyStateBoundOperator : public StateBoundOperator<T, FormulaType> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	SteadyStateBoundOperator() : StateBoundOperator<T, FormulaType>
+		(LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param stateFormula The child node
+	 */
+	SteadyStateBoundOperator(
+		storm::formula::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 {
+		return "S" + StateBoundOperator<T, FormulaType>::toString();
+	}
+};
+
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_ */

src/formula/abstract/SteadyStateNoBoundOperator.h

@@ -0,0 +1,58 @@
+/*
+ * 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 formula {
+namespace abstract {
+
+template <class T, class FormulaType>
+class SteadyStateNoBoundOperator: public StateNoBoundOperator<T, FormulaType> {
+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 {
+		return "S" + StateNoBoundOperator<T, FormulaType>::toString();
+	}
+
+};
+
+} /* namespace abstract */
+} /* namespace formula */
+} /* namespace storm */
+
+#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_ */

src/formula/abstract/TimeBoundedEventually.h

@@ -0,0 +1,94 @@
+/*
+ * 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 formula {
+namespace abstract {
+
+
+template<class T, class FormulaType>
+class TimeBoundedEventually: public storm::formula::abstract::TimeBoundedOperator<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 {
+		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 conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+
+private:
+	FormulaType* child;
+};
+
+} /* namespace abstract */
+} /* namespace formula */
+} /* namespace storm */
+
+#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_ */

src/formula/abstract/TimeBoundedOperator.h

@@ -30,7 +30,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template<class T>
-class TimeBoundedOperator: public storm::formula::AbstractFormula<T> {
+class TimeBoundedOperator: public virtual AbstractFormula<T> {
 public:
 	/**
 	 * Constructor

src/formula/abstract/TimeBoundedUntil.h

@@ -0,0 +1,135 @@
+/*
+ * 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 formula {
+namespace abstract {
+
+template <class T, class FormulaType>
+class TimeBoundedUntil: public TimeBoundedOperator<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 {
+		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 conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->left) && checker.conforms(this->right);
+	}
+
+private:
+	FormulaType* left;
+	FormulaType* right;
+};
+
+} /* namespace abstract */
+} /* namespace formula */
+} /* namespace storm */
+
+#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_ */

src/parser/CslParser.cpp

@@ -0,0 +1,220 @@
+/*
+ * CslParser.cpp
+ *
+ *  Created on: 08.04.2013
+ *      Author: Thomas Heinemann
+ */
+
+#include "src/parser/CslParser.h"
+#include "src/utility/OsDetection.h"
+#include "src/utility/ConstTemplates.h"
+
+// If the parser fails due to ill-formed data, this exception is thrown.
+#include "src/exceptions/WrongFormatException.h"
+
+// Used for Boost spirit.
+#include <boost/typeof/typeof.hpp>
+#include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/phoenix.hpp>
+
+// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
+#include <boost/spirit/include/classic_position_iterator.hpp>
+#include <boost/spirit/include/support_multi_pass.hpp>
+
+// Needed for file IO.
+#include <fstream>
+#include <iomanip>
+#include <map>
+
+
+// Some typedefs and namespace definitions to reduce code size.
+typedef std::string::const_iterator BaseIteratorType;
+typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
+namespace qi = boost::spirit::qi;
+namespace phoenix = boost::phoenix;
+
+
+namespace storm {
+namespace parser {
+
+template<typename Iterator, typename Skipper>
+struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::csl::AbstractCslFormula<double>*(), Skipper > {
+	CslGrammar() : CslGrammar::base_type(start) {
+		freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
+
+		//This block defines rules for parsing state formulas
+		stateFormula %= orFormula;
+		stateFormula.name("state formula");
+		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::Or<double>>(qi::_val, qi::_1)];
+		orFormula.name("state formula");
+		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::And<double>>(qi::_val, qi::_1)];
+		andFormula.name("state formula");
+		notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::Not<double>>(qi::_1)];
+		notFormula.name("state formula");
+
+		//This block defines rules for "atomic" state formulas
+		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
+		atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")");
+		atomicStateFormula.name("state formula");
+		atomicProposition = (freeIdentifierName)[qi::_val =
+				phoenix::new_<storm::formula::csl::Ap<double>>(qi::_1)];
+		atomicProposition.name("state formula");
+		probabilisticBoundOperator = (
+				(qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+						phoenix::new_<storm::formula::csl::ProbabilisticBoundOperator<double> >(storm::formula::GREATER, qi::_1, qi::_2)] |
+				(qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+						phoenix::new_<storm::formula::csl::ProbabilisticBoundOperator<double> >(storm::formula::GREATER_EQUAL, qi::_1, qi::_2)] |
+				(qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+								phoenix::new_<storm::formula::csl::ProbabilisticBoundOperator<double> >(storm::formula::LESS, qi::_1, qi::_2)] |
+				(qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+						phoenix::new_<storm::formula::csl::ProbabilisticBoundOperator<double> >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)]
+				);
+		probabilisticBoundOperator.name("state formula");
+		steadyStateBoundOperator = (
+				(qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
+										phoenix::new_<storm::formula::csl::SteadyStateBoundOperator<double> >(storm::formula::GREATER, qi::_1, qi::_2)] |
+				(qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
+										phoenix::new_<storm::formula::csl::SteadyStateBoundOperator<double> >(storm::formula::GREATER_EQUAL, qi::_1, qi::_2)] |
+				(qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
+										phoenix::new_<storm::formula::csl::SteadyStateBoundOperator<double> >(storm::formula::LESS, qi::_1, qi::_2)] |
+				(qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
+										phoenix::new_<storm::formula::csl::SteadyStateBoundOperator<double> >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)]
+				);
+		steadyStateBoundOperator.name("state formula");
+
+		//This block defines rules for parsing formulas with noBoundOperators
+		noBoundOperator = (probabilisticNoBoundOperator | steadyStateNoBoundOperator);
+		noBoundOperator.name("no bound operator");
+		probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
+				phoenix::new_<storm::formula::csl::ProbabilisticNoBoundOperator<double> >(qi::_1)];
+		probabilisticNoBoundOperator.name("no bound operator");
+		steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> stateFormula >> qi::lit("]"))[qi::_val =
+				phoenix::new_<storm::formula::csl::SteadyStateNoBoundOperator<double> >(qi::_1)];
+		steadyStateNoBoundOperator.name("no bound operator");
+
+		//This block defines rules for parsing probabilistic path formulas
+		pathFormula = (timeBoundedEventually | eventually | globally | timeBoundedUntil | until);
+		pathFormula.name("path formula");
+		timeBoundedEventually = (
+				(qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)] |
+				(qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val =
+								phoenix::new_<storm::formula::csl::TimeBoundedEventually<double>>(0, qi::_1, qi::_2)] |
+				(qi::lit("F") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)[qi::_val =
+								phoenix::new_<storm::formula::csl::TimeBoundedEventually<double>>(qi::_1, std::numeric_limits<double>::infinity(), qi::_2)]
+				);
+		timeBoundedEventually.name("path formula (for probabilistic operator)");
+		eventually = (qi::lit("F") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::Eventually<double> >(qi::_1)];
+		eventually.name("path formula (for probabilistic operator)");
+		globally = (qi::lit("G") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::Globally<double> >(qi::_1)];
+		globally.name("path formula (for probabilistic operator)");
+		timeBoundedUntil = (
+					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]")  > stateFormula)
+					[qi::_val = phoenix::new_<storm::formula::csl::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)] |
+					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_  > stateFormula)
+					[qi::_val = phoenix::new_<storm::formula::csl::TimeBoundedUntil<double>>(0, qi::_2, phoenix::bind(&storm::formula::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)] |
+					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_  > stateFormula)
+					[qi::_val = phoenix::new_<storm::formula::csl::TimeBoundedUntil<double>>(qi::_2, std::numeric_limits<double>::infinity(), phoenix::bind(&storm::formula::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)]
+				);
+		timeBoundedUntil.name("path formula (for probabilistic operator)");
+		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::csl::Until<double>>(phoenix::bind(&storm::formula::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
+		until.name("path formula (for probabilistic operator)");
+
+		start = (noBoundOperator | stateFormula);
+		start.name("CSL formula");
+	}
+
+	qi::rule<Iterator, storm::formula::csl::AbstractCslFormula<double>*(), Skipper> start;
+
+	qi::rule<Iterator, storm::formula::csl::AbstractStateFormula<double>*(), Skipper> stateFormula;
+	qi::rule<Iterator, storm::formula::csl::AbstractStateFormula<double>*(), Skipper> atomicStateFormula;
+
+	qi::rule<Iterator, storm::formula::csl::AbstractStateFormula<double>*(), Skipper> andFormula;
+	qi::rule<Iterator, storm::formula::csl::AbstractStateFormula<double>*(), Skipper> atomicProposition;
+	qi::rule<Iterator, storm::formula::csl::AbstractStateFormula<double>*(), Skipper> orFormula;
+	qi::rule<Iterator, storm::formula::csl::AbstractStateFormula<double>*(), Skipper> notFormula;
+	qi::rule<Iterator, storm::formula::csl::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator;
+	qi::rule<Iterator, storm::formula::csl::SteadyStateBoundOperator<double>*(), Skipper> steadyStateBoundOperator;
+
+	qi::rule<Iterator, storm::formula::csl::AbstractNoBoundOperator<double>*(), Skipper> noBoundOperator;
+	qi::rule<Iterator, storm::formula::csl::AbstractNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
+	qi::rule<Iterator, storm::formula::csl::AbstractNoBoundOperator<double>*(), Skipper> steadyStateNoBoundOperator;
+
+	qi::rule<Iterator, storm::formula::csl::AbstractPathFormula<double>*(), Skipper> pathFormula;
+	qi::rule<Iterator, storm::formula::csl::TimeBoundedEventually<double>*(), Skipper> timeBoundedEventually;
+	qi::rule<Iterator, storm::formula::csl::Eventually<double>*(), Skipper> eventually;
+	qi::rule<Iterator, storm::formula::csl::Globally<double>*(), Skipper> globally;
+	qi::rule<Iterator, storm::formula::csl::TimeBoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>>, Skipper> timeBoundedUntil;
+	qi::rule<Iterator, storm::formula::csl::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::csl::AbstractStateFormula<double>>>, Skipper> until;
+
+
+	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
+
+};
+
+CslParser::CslParser(std::string formulaString) {
+	// Prepare iterators to input.
+	BaseIteratorType stringIteratorBegin = formulaString.begin();
+	BaseIteratorType stringIteratorEnd = formulaString.end();
+	PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString);
+	PositionIteratorType positionIteratorEnd;
+
+
+	// Prepare resulting intermediate representation of input.
+	storm::formula::csl::AbstractCslFormula<double>* result_pointer = nullptr;
+
+	CslGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> grammar;
+
+	// Now, parse the formula from the given string
+	try {
+		qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer);
+	} catch(const qi::expectation_failure<PositionIteratorType>& e) {
+		// If the parser expected content different than the one provided, display information
+		// about the location of the error.
+		const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
+
+		// Construct the error message including a caret display of the position in the
+		// erroneous line.
+		std::stringstream msg;
+		msg << pos.file << ", line " << pos.line << ", column " << pos.column
+				<< ": parse error: expected " << e.what_ << std::endl << "\t"
+				<< e.first.get_currentline() << std::endl << "\t";
+		int i = 0;
+		for (i = 0; i < pos.column; ++i) {
+			msg << "-";
+		}
+		msg << "^";
+		for (; i < 80; ++i) {
+			msg << "-";
+		}
+		msg << std::endl;
+
+		std::cerr << msg.str();
+
+		// Now propagate exception.
+		throw storm::exceptions::WrongFormatException() << msg.str();
+	}
+
+	// The syntax can be so wrong that no rule can be matched at all
+	// In that case, no expectation failure is thrown, but the parser just returns nullptr
+	// Then, of course the result is not usable, hence we throw a WrongFormatException, too.
+	if (result_pointer == nullptr) {
+		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
+	}
+
+	formula = result_pointer;
+}
+
+CslParser::~CslParser() {
+	// Intentionally left empty
+	// Parsed formula is not deleted with the parser!
+}
+
+} /* namespace parser */
+} /* namespace storm */

src/parser/CslParser.h

@@ -0,0 +1,53 @@
+/*
+ * CslParser.h
+ *
+ *  Created on: 08.04.2013
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_PARSER_CSLPARSER_H_
+#define STORM_PARSER_CSLPARSER_H_
+
+#include "Parser.h"
+
+#include "src/formula/Csl.h"
+//#include <memory>
+
+namespace storm {
+namespace parser {
+
+class CslParser: public storm::parser::Parser {
+public:
+	/*!
+	 * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of
+	 * classes in the namespace storm::formula.
+	 *
+	 * If the string could not be parsed successfully, it will throw a wrongFormatException.
+	 *
+	 * @param formulaString The string representation of the formula
+	 * @throw wrongFormatException If the input could not be parsed successfully
+	 */
+	CslParser(std::string formulaString);
+	virtual ~CslParser();
+
+	/*!
+	 *	@return a pointer to the parsed formula object
+	 */
+	storm::formula::csl::AbstractCslFormula<double>* getFormula() {
+		return this->formula;
+	}
+
+private:
+private:
+	storm::formula::csl::AbstractCslFormula<double>* formula;
+
+	/*!
+	 * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
+	 */
+	template<typename Iterator, typename Skipper>
+	struct CslGrammar;
+};
+
+} /* namespace parser */
+} /* namespace storm */
+#endif /* STORM_PARSER_CSLPARSER_H_ */

test/parser/CslParserTest.cpp

@@ -8,7 +8,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "src/parser/CslParser.h"
-/*
+
 TEST(CslParserTest, parseApOnlyTest) {
 	std::string ap = "ap";
 	storm::parser::CslParser* cslParser = nullptr;
@@ -50,9 +50,9 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) {
 
 	ASSERT_NE(cslParser->getFormula(), nullptr);
 
-	storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(cslParser->getFormula());
+	storm::formula::csl::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::csl::ProbabilisticBoundOperator<double>*>(cslParser->getFormula());
 
-	ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER, op->getComparisonOperator());
+	ASSERT_EQ(storm::formula::GREATER, op->getComparisonOperator());
 	ASSERT_EQ(0.5, op->getBound());
 
 	ASSERT_EQ(cslParser->getFormula()->toString(), "P > 0.500000 [F a]");
@@ -70,9 +70,9 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
 
 	ASSERT_NE(cslParser->getFormula(), nullptr);
 
-	storm::formula::SteadyStateBoundOperator<double>* op = static_cast<storm::formula::SteadyStateBoundOperator<double>*>(cslParser->getFormula());
+	storm::formula::csl::SteadyStateBoundOperator<double>* op = static_cast<storm::formula::csl::SteadyStateBoundOperator<double>*>(cslParser->getFormula());
 
-	ASSERT_EQ(storm::formula::StateBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
+	ASSERT_EQ(storm::formula::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
 
 	ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", cslParser->getFormula()->toString());
@@ -84,13 +84,13 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
 TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
 	storm::parser::CslParser* cslParser = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F a ] ]")
+			cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F<=3 a ] ]")
 	);
 
 	ASSERT_NE(cslParser->getFormula(), nullptr);
 
 
-	ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F a]]");
+	ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]");
 
 	delete cslParser->getFormula();
 	delete cslParser;
@@ -113,6 +113,7 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
 
 }
 
+
 TEST(CslParserTest, parseComplexFormulaTest) {
 	storm::parser::CslParser* cslParser = nullptr;
 	ASSERT_NO_THROW(
@@ -128,6 +129,7 @@ TEST(CslParserTest, parseComplexFormulaTest) {
 }
 
 
+
 TEST(CslParserTest, wrongProbabilisticFormulaTest) {
 	storm::parser::CslParser* cslParser = nullptr;
 	ASSERT_THROW(
@@ -155,4 +157,3 @@ TEST(CslParserTest, wrongFormulaTest2) {
 	);
 	delete cslParser;
 }
-*/