Almost finished restruction of PRCTL formulas; adapted code (including

test cases) to work correctly with the new structure

src/formula/AbstractFormulaChecker.h

@@ -55,7 +55,7 @@ class AbstractFormulaChecker {
 		 *	@param formula A pointer to some formula object.
 		 *	@return true iff the formula is valid.
 		 */
-		virtual bool conforms(const AbstractFormula<T>* formula) const = 0;
+		virtual bool conforms(const storm::formula::abstract::AbstractFormula<T>* formula) const = 0;
 };
 
 } // namespace formula

src/formula/ComparisonType.h

@@ -0,0 +1,20 @@
+/*
+ * ComparisonType.h
+ *
+ *  Created on: 17.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_COMPARISONTYPE_H_
+#define STORM_FORMULA_COMPARISONTYPE_H_
+
+namespace storm {
+namespace formula {
+
+enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
+
+}
+}
+
+
+#endif /* STORM_FORMULA_COMPARISONTYPE_H_ */

src/formula/Prctl.h

@@ -1,5 +1,5 @@
 /*
- * Formulas.h
+ * Prctl.h
  *
  *  Created on: 06.12.2012
  *      Author: chris
@@ -38,9 +38,12 @@
 
 #include "TimeBoundedUntil.h"
 #include "TimeBoundedEventually.h"
-
-#include "AbstractFormula.h"
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
 */
+#include "Prctl/AbstractPrctlFormula.h"
+#include "Prctl/AbstractStateFormula.h"
+#include "Prctl/AbstractNoBoundOperator.h"
+#include "Prctl/AbstractPathFormula.h"
+
+#include "modelchecker/AbstractModelChecker.h"
+
 #endif /* STORM_FORMULA_FORMULAS_H_ */

src/formula/Prctl/AbstractNoBoundOperator.h

@@ -0,0 +1,80 @@
+/*
+ * AbstractNoBoundOperator.h
+ *
+ *  Created on: 16.04.2013
+ *      Author: thomas
+ */
+
+#ifndef ABSTRACTNOBOUNDOPERATOR_H_
+#define ABSTRACTNOBOUNDOPERATOR_H_
+
+#include "AbstractPrctlFormula.h"
+#include "src/formula/abstract/IOptimizingOperator.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+template <class T>
+class AbstractNoBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support PathNoBoundOperator.
+ *
+ *  All model checkers that support the formula class NoBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class INoBoundOperatorModelChecker {
+public:
+	/*!
+     *  @brief Evaluates NoBoundOperator formula within a model checker.
+     *
+     *  @param obj Formula object with subformulas.
+     *  @return Result of the formula for every node.
+     */
+    virtual std::vector<T>* checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
+
+
+};
+
+template <class T>
+class AbstractNoBoundOperator: public AbstractPrctlFormula<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 prctl */
+} /* namespace formula */
+} /* namespace storm */
+#endif /* ABSTRACTNOBOUNDOPERATOR_H_ */

src/formula/Prctl/AbstractPathFormula.h

@@ -8,9 +8,9 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 
-namespace storm { namespace formula {
+namespace storm { namespace formula { namespace prctl {
 template <class T> class AbstractPathFormula;
-}}
+}}}
 
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/modelchecker/ForwardDeclarations.h"
@@ -39,7 +39,9 @@ public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~AbstractPathFormula() = 0;
+	virtual ~AbstractPathFormula() {
+		// Intentionally left empty
+	}
 
 	/*!
 	 * Clones the called object.

src/formula/Prctl/AbstractPrctlFormula.h

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

src/formula/Prctl/AbstractStateFormula.h

@@ -8,11 +8,11 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 
-namespace storm { namespace formula {
+namespace storm { namespace formula { namespace prctl {
 template <class T> class AbstractStateFormula;
-}}
+}}}
 
-#include "src/formula/abstract/AbstractFormula.h"
+#include "AbstractPrctlFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
@@ -30,13 +30,15 @@ namespace prctl {
  * 	   clone().
  */
 template <class T>
-class AbstractStateFormula : public storm::formula::abstract::AbstractFormula<T> {
+class AbstractStateFormula : public AbstractPrctlFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~AbstractStateFormula() = 0;
+	virtual ~AbstractStateFormula() {
+		// Intentionally left empty
+	}
 
 	/*!
 	 * Clones the called object.
@@ -59,7 +61,7 @@ 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 prctl

src/formula/Prctl/Ap.h

@@ -47,7 +47,8 @@ class IApModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class Ap : public storm::formula::abstract::Ap<T>, public AbstractStateFormula<T> {
+class Ap : public storm::formula::abstract::Ap<T>,
+			  public AbstractStateFormula<T> {
 
 public:
 	/*!

src/formula/Prctl/Eventually.h

@@ -61,7 +61,7 @@ public:
 	 * Empty constructor
 	 */
 	Eventually() {
-		this->child = nullptr;
+		// Intentionally left empty
 	}
 
 	/*!

src/formula/Prctl/Globally.h

@@ -113,16 +113,6 @@ public:
 	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*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);
-	}
 };
 
 } //namespace prctl

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -73,7 +73,7 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+			storm::formula::ComparisonType comparisonRelation,
 			T bound,
 			AbstractPathFormula<T>* pathFormula)
 			: storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
@@ -88,7 +88,7 @@ public:
 	 * @param minimumOperator
 	 */
 	ProbabilisticBoundOperator(
-			typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+			storm::formula::ComparisonType comparisonRelation,
 			T bound,
 			AbstractPathFormula<T>* pathFormula,
 			bool minimumOperator)

src/formula/Prctl/ProbabilisticNoBoundOperator.h

@@ -9,6 +9,7 @@
 #define STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
 
 #include "AbstractPathFormula.h"
+#include "AbstractNoBoundOperator.h"
 #include "src/formula/abstract/ProbabilisticNoBoundOperator.h"
 
 namespace storm {
@@ -47,7 +48,7 @@ namespace prctl {
  */
 template <class T>
 class ProbabilisticNoBoundOperator: public storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>,
-												public AbstractStateFormula<T> {
+												public AbstractNoBoundOperator<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -82,6 +83,29 @@ public:
 	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 formula

src/formula/Prctl/RewardBoundOperator.h

@@ -17,6 +17,20 @@ namespace storm {
 namespace formula {
 namespace prctl {
 
+template <class T> class RewardBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support RewardBoundOperator.
+ *
+ *  All model checkers that support the formula class PathBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IRewardBoundOperatorModelChecker {
+    public:
+        virtual storm::storage::BitVector* checkRewardBoundOperator(const RewardBoundOperator<T>& obj) const = 0;
+};
+
 /*!
  * @brief
  * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root.
@@ -57,7 +71,7 @@ public:
 	 * @param pathFormula The child node
 	 */
 	RewardBoundOperator(
-			typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+			storm::formula::ComparisonType comparisonRelation,
 			T bound,
 			AbstractPathFormula<T>* pathFormula) :
 				storm::formula::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
@@ -74,7 +88,7 @@ public:
 	 * @param minimumOperator
 	 */
 	RewardBoundOperator(
-			typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+			storm::formula::ComparisonType comparisonRelation,
 			T bound,
 			AbstractPathFormula<T>* pathFormula,
 			bool minimumOperator)

src/formula/Prctl/RewardNoBoundOperator.h

@@ -8,6 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
 #define STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
 
+#include "AbstractNoBoundOperator.h"
 #include "AbstractPathFormula.h"
 #include "src/formula/abstract/RewardNoBoundOperator.h"
 
@@ -46,7 +47,8 @@ namespace prctl {
  * @see AbstractFormula
  */
 template <class T>
-class RewardNoBoundOperator: public storm::formula::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>> {
+class RewardNoBoundOperator: public storm::formula::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>,
+									  public storm::formula::prctl::AbstractNoBoundOperator<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -75,7 +77,28 @@ public:
 		// Intentionally left empty
 	}
 
-	//TODO: Clone?
+	virtual AbstractNoBoundOperator<T>* clone() const {
+		RewardNoBoundOperator<T>* result = new RewardNoBoundOperator<T>();
+		if (this->pathFormulaIsSet()) {
+			result->setPathFormula(this->getPathFormula().clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+		return this->getPathFormula().check(modelChecker, qualitative);
+	}
 };
 
 } //namespace prctl

src/formula/Prctl/SteadyStateReward.h

@@ -47,7 +47,7 @@ class ISteadyStateRewardModelChecker {
  */
 template <class T>
 class SteadyStateReward: public storm::formula::abstract::SteadyStateReward<T>,
-								 public storm::formula::AbstractPathFormula<T> {
+								 public AbstractPathFormula<T> {
 public:
 	/*!
 	 * Empty constructor

src/formula/abstract/AbstractFormula.h

@@ -10,6 +10,14 @@
 
 #include <string>
 
+namespace storm {
+namespace formula {
+namespace abstract {
+template <class T> class AbstractFormula;
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
 #include "src/modelchecker/ForwardDeclarations.h"
 #include "src/formula/AbstractFormulaChecker.h"
 

src/formula/abstract/And.h

@@ -33,7 +33,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class And : public AbstractFormula<T> {
+class And : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/Ap.h

@@ -26,7 +26,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T>
-class Ap : public AbstractFormula<T> {
+class Ap : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/BoundedEventually.h

@@ -36,7 +36,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class BoundedEventually : public AbstractFormula<T> {
+class BoundedEventually : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/BoundedNaryUntil.h

@@ -40,7 +40,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class BoundedNaryUntil : public AbstractFormula<T> {
+class BoundedNaryUntil : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/BoundedUntil.h

@@ -34,7 +34,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class BoundedUntil : public AbstractFormula<T> {
+class BoundedUntil : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/CumulativeReward.h

@@ -27,7 +27,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T>
-class CumulativeReward : public AbstractFormula<T> {
+class CumulativeReward : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/Eventually.h

@@ -33,7 +33,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class Eventually : public AbstractFormula<T> {
+class Eventually : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/Globally.h

@@ -34,7 +34,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class Globally : public AbstractFormula<T> {
+class Globally : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/InstantaneousReward.h

@@ -28,7 +28,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T>
-class InstantaneousReward : public AbstractFormula<T> {
+class InstantaneousReward : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/Next.h

@@ -33,7 +33,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class Next : public AbstractFormula<T> {
+class Next : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/Not.h

@@ -31,7 +31,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class Not : public AbstractFormula<T> {
+class Not : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/OptimizingOperator.h

@@ -1,13 +1,18 @@
 #ifndef STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
 #define STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
 
+#include "IOptimizingOperator.h"
+
 namespace storm {
 
 namespace formula {
 
 namespace abstract {
 
-class OptimizingOperator {
+/*!
+ *
+ */
+class OptimizingOperator : public virtual IOptimizingOperator {
 public:
 	/*!
 	 * Empty constructor
@@ -23,11 +28,18 @@ public:
 	OptimizingOperator(bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) {
 	}
 
+	/*!
+	 * Destructor
+	 */
+	virtual ~OptimizingOperator() {
+		// Intentionally left empty
+	}
+
 	/*!
 	 * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
 	 * @returns True if the operator is an optimizing operator.
 	 */
-	bool isOptimalityOperator() const {
+	virtual bool isOptimalityOperator() const {
 		return optimalityOperator;
 	}
 
@@ -37,7 +49,7 @@ public:
 	 * @returns True if the operator is an optimizing operator and it is a minimizing operator and
 	 * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator.
 	 */
-	bool isMinimumOperator() const {
+	virtual bool isMinimumOperator() const {
 		return optimalityOperator && minimumOperator;
 	}
 

src/formula/abstract/Or.h

@@ -31,7 +31,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class Or : public AbstractFormula<T> {
+class Or : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/formula/abstract/PathBoundOperator.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/formula/abstract/OptimizingOperator.h"
 
@@ -45,11 +46,9 @@ namespace abstract {
  * @see AbstractFormula
  */
 template<class T, class FormulaType>
-class PathBoundOperator : public AbstractFormula<T>, public OptimizingOperator {
+class PathBoundOperator : public virtual AbstractFormula<T>, public OptimizingOperator {
 
 public:
-	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
-
 	/*!
 	 * Constructor for non-optimizing operator.
 	 *
@@ -57,7 +56,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	PathBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* pathFormula)
+	PathBoundOperator(storm::formula::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
@@ -70,7 +69,7 @@ public:
 	 * @param pathFormula The child node
 	 * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
 	 */
-	PathBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* pathFormula, bool minimumOperator)
+	PathBoundOperator(storm::formula::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula, bool minimumOperator)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) {
 		// Intentionally left empty
 	}
@@ -114,11 +113,11 @@ public:
 	/*!
 	 * @returns the comparison relation
 	 */
-	const ComparisonType getComparisonOperator() const {
+	const storm::formula::ComparisonType getComparisonOperator() const {
 		return comparisonOperator;
 	}
 
-	void setComparisonOperator(ComparisonType comparisonOperator) {
+	void setComparisonOperator(storm::formula::ComparisonType comparisonOperator) {
 		this->comparisonOperator = comparisonOperator;
 	}
 
@@ -178,7 +177,7 @@ public:
     }
 
 private:
-	ComparisonType comparisonOperator;
+	storm::formula::ComparisonType comparisonOperator;
 	T bound;
 	FormulaType* pathFormula;
 };

src/formula/abstract/PathNoBoundOperator.h

@@ -8,7 +8,6 @@
 #ifndef STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
 #define STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
 
-#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/formula/abstract/OptimizingOperator.h"
@@ -51,12 +50,13 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class PathNoBoundOperator: public storm::formula::AbstractFormula<T>, public OptimizingOperator {
+class PathNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	PathNoBoundOperator() : optimalityOperator(false), minimumOperator(false) {
+	PathNoBoundOperator() :
+		OptimizingOperator(false) {
 		this->pathFormula = nullptr;
 	}
 
@@ -65,7 +65,8 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	PathNoBoundOperator(FormulaType* pathFormula) : optimalityOperator(false), minimumOperator(false) {
+	PathNoBoundOperator(FormulaType* pathFormula) :
+		OptimizingOperator(false) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -77,7 +78,7 @@ public:
 	 * maximizing operator.
 	 */
 	PathNoBoundOperator(FormulaType* pathFormula, bool minimumOperator)
-		: optimalityOperator(true), minimumOperator(minimumOperator) {
+		: OptimizingOperator(minimumOperator) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -142,34 +143,8 @@ public:
 		return checker.conforms(this->pathFormula);
 	}
 
-	/*!
-	 * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
-	 * @returns True if the operator is an optimizing operator.
-	 */
-	bool isOptimalityOperator() const {
-		return optimalityOperator;
-	}
-
-	/*!
-	 * Retrieves whether the operator is a minimizing operator given that it is an optimality
-	 * operator.
-	 * @returns True if the operator is an optimizing operator and it is a minimizing operator and
-	 * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator.
-	 */
-	bool isMinimumOperator() const {
-		return optimalityOperator && minimumOperator;
-	}
-
 private:
 	FormulaType* pathFormula;
-
-	// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
-	// over a nondeterministic model.
-	bool optimalityOperator;
-
-	// In the case this operator is an optimizing operator, this flag indicates whether it is
-	// looking for the minimum or the maximum value.
-	bool minimumOperator;
 };
 
 } //namespace abstract

src/formula/abstract/ProbabilisticBoundOperator.h

@@ -45,8 +45,8 @@ public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticBoundOperator() : PathBoundOperator<T>
-		(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+	ProbabilisticBoundOperator() : PathBoundOperator<T, FormulaType>
+		(LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
 		// Intentionally left empty
 	}
 
@@ -59,8 +59,10 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula)
-			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			storm::formula::ComparisonType comparisonRelation,
+			T bound,
+			FormulaType* pathFormula)
+			: PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -73,8 +75,11 @@ public:
 	 * @param minimumOperator
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula, bool minimumOperator)
-			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
+			storm::formula::ComparisonType comparisonRelation,
+			T bound,
+			FormulaType* pathFormula,
+			bool minimumOperator)
+			: PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula, minimumOperator){
 		// Intentionally left empty
 	}
 
@@ -90,7 +95,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "P ";
-		result += PathBoundOperator<T>::toString();
+		result += PathBoundOperator<T, FormulaType>::toString();
 		return result;
 	}
 };

src/formula/abstract/ProbabilisticNoBoundOperator.h

@@ -47,12 +47,12 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T> {
+class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
+	ProbabilisticNoBoundOperator() : PathNoBoundOperator<T, FormulaType>(nullptr) {
 		// Intentionally left empty
 	}
 
@@ -61,7 +61,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+	ProbabilisticNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T, FormulaType>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -77,7 +77,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+	ProbabilisticNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T, FormulaType>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -86,7 +86,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "P";
-		result += PathNoBoundOperator<T>::toString();
+		result += PathNoBoundOperator<T, FormulaType>::toString();
 		return result;
 	}
 };

src/formula/abstract/RewardBoundOperator.h

@@ -42,7 +42,7 @@ public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardBoundOperator() : PathBoundOperator<T>(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+	RewardBoundOperator() : PathBoundOperator<T, FormulaType>(LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
 		// Intentionally left empty
 	}
 
@@ -54,14 +54,19 @@ public:
 	 * @param pathFormula The child node
 	 */
 	RewardBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula) :
-				PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			storm::formula::ComparisonType comparisonRelation,
+			T bound,
+			FormulaType* pathFormula) :
+				PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
 	RewardBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula, bool minimumOperator)
-			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator) {
+			storm::formula::ComparisonType comparisonRelation,
+			T bound,
+			FormulaType* pathFormula,
+			bool minimumOperator)
+			: PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -70,7 +75,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "R ";
-		result += PathBoundOperator<T>::toString();
+		result += PathBoundOperator<T, FormulaType>::toString();
 		return result;
 	}
 };

src/formula/abstract/RewardNoBoundOperator.h

@@ -51,7 +51,7 @@ public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
+	RewardNoBoundOperator() : PathNoBoundOperator<T, FormulaType>(nullptr) {
 		// Intentionally left empty
 	}
 
@@ -60,7 +60,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+	RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T, FormulaType>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -69,7 +69,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+	RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T, FormulaType>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -78,7 +78,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "R";
-		result += PathNoBoundOperator<T>::toString();
+		result += PathNoBoundOperator<T, FormulaType>::toString();
 		return result;
 	}
 };

src/formula/abstract/StateBoundOperator.h

@@ -40,7 +40,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template<class T>
-class StateBoundOperator : public AbstractFormula<T> {
+class StateBoundOperator : public virtual AbstractFormula<T> {
 
 public:
 	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };

src/formula/abstract/SteadyStateReward.h

@@ -24,7 +24,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T>
-class SteadyStateReward: public AbstractFormula<T> {
+class SteadyStateReward: public virtual AbstractFormula<T> {
 public:
 	/*!
 	 * Empty constructor

src/formula/abstract/Until.h

@@ -33,7 +33,7 @@ namespace abstract {
  * @see AbstractFormula
  */
 template <class T, class FormulaType>
-class Until : public AbstractFormula<T> {
+class Until : public virtual AbstractFormula<T> {
 
 public:
 	/*!

src/modelchecker/AbstractModelChecker.h

@@ -16,7 +16,7 @@ namespace modelchecker {
 }
 
 #include "src/exceptions/InvalidPropertyException.h"
-#include "src/formula/Formulas.h"
+#include "src/formula/Prctl.h"
 #include "src/storage/BitVector.h"
 #include "src/models/AbstractModel.h"
 
@@ -42,22 +42,22 @@ template<class Type>
 class AbstractModelChecker :
 	// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to
 	// be implemented that performs the corresponding check.
-	public virtual storm::formula::IApModelChecker<Type>,
-	public virtual storm::formula::IAndModelChecker<Type>,
-	public virtual storm::formula::IOrModelChecker<Type>,
-	public virtual storm::formula::INotModelChecker<Type>,
-	public virtual storm::formula::IUntilModelChecker<Type>,
-	public virtual storm::formula::IEventuallyModelChecker<Type>,
-	public virtual storm::formula::IGloballyModelChecker<Type>,
-	public virtual storm::formula::INextModelChecker<Type>,
-	public virtual storm::formula::IBoundedUntilModelChecker<Type>,
-	public virtual storm::formula::IBoundedEventuallyModelChecker<Type>,
-	public virtual storm::formula::IPathNoBoundOperatorModelChecker<Type>,
-	public virtual storm::formula::IProbabilisticBoundOperatorModelChecker<Type>,
-	public virtual storm::formula::IRewardBoundOperatorModelChecker<Type>,
-	public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
-	public virtual storm::formula::ICumulativeRewardModelChecker<Type>,
-	public virtual storm::formula::IInstantaneousRewardModelChecker<Type> {
+	public virtual storm::formula::prctl::IApModelChecker<Type>,
+	public virtual storm::formula::prctl::IAndModelChecker<Type>,
+	public virtual storm::formula::prctl::IOrModelChecker<Type>,
+	public virtual storm::formula::prctl::INotModelChecker<Type>,
+	public virtual storm::formula::prctl::IUntilModelChecker<Type>,
+	public virtual storm::formula::prctl::IEventuallyModelChecker<Type>,
+	public virtual storm::formula::prctl::IGloballyModelChecker<Type>,
+	public virtual storm::formula::prctl::INextModelChecker<Type>,
+	public virtual storm::formula::prctl::IBoundedUntilModelChecker<Type>,
+	public virtual storm::formula::prctl::IBoundedEventuallyModelChecker<Type>,
+	public virtual storm::formula::prctl::INoBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::prctl::IProbabilisticBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::prctl::IRewardBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::prctl::IReachabilityRewardModelChecker<Type>,
+	public virtual storm::formula::prctl::ICumulativeRewardModelChecker<Type>,
+	public virtual storm::formula::prctl::IInstantaneousRewardModelChecker<Type> {
 	
 public:
 	/*!
@@ -123,7 +123,7 @@ public:
 	 *
 	 * @param stateFormula The formula to be checked.
 	 */
-	void check(storm::formula::AbstractStateFormula<Type> const& stateFormula) const {
+	void check(storm::formula::prctl::AbstractStateFormula<Type> const& stateFormula) const {
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
 		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
@@ -154,13 +154,13 @@ public:
 	 *
 	 * @param noBoundFormula The formula to be checked.
 	 */
-	void check(storm::formula::PathNoBoundOperator<Type> const& noBoundFormula) const {
+	void check(storm::formula::prctl::AbstractNoBoundOperator<Type> const& noBoundFormula) const {
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
 		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
 		std::vector<Type>* result = nullptr;
 		try {
-			result = noBoundFormula.check(*this);
+			result = this->checkNoBoundOperator(noBoundFormula);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
 			for (auto initialState : *model.getLabeledStates("init")) {
@@ -184,7 +184,7 @@ public:
 	 * @param formula The formula to be checked.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector* checkAp(storm::formula::Ap<Type> const& formula) const {
+	storm::storage::BitVector* checkAp(storm::formula::prctl::Ap<Type> const& formula) const {
 		if (formula.getAp() == "true") {
 			return new storm::storage::BitVector(model.getNumberOfStates(), true);
 		} else if (formula.getAp() == "false") {
@@ -205,7 +205,7 @@ public:
 	 * @param formula The formula to be checked.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector* checkAnd(storm::formula::And<Type> const& formula) const {
+	storm::storage::BitVector* checkAnd(storm::formula::prctl::And<Type> const& formula) const {
 		storm::storage::BitVector* result = formula.getLeft().check(*this);
 		storm::storage::BitVector* right = formula.getRight().check(*this);
 		(*result) &= (*right);
@@ -219,7 +219,7 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	virtual storm::storage::BitVector* checkOr(storm::formula::Or<Type> const& formula) const {
+	virtual storm::storage::BitVector* checkOr(storm::formula::prctl::Or<Type> const& formula) const {
 		storm::storage::BitVector* result = formula.getLeft().check(*this);
 		storm::storage::BitVector* right = formula.getRight().check(*this);
 		(*result) |= (*right);
@@ -233,7 +233,7 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector* checkNot(const storm::formula::Not<Type>& formula) const {
+	storm::storage::BitVector* checkNot(const storm::formula::prctl::Not<Type>& formula) const {
 		storm::storage::BitVector* result = formula.getChild().check(*this);
 		result->complement();
 		return result;
@@ -246,7 +246,7 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector* checkProbabilisticBoundOperator(storm::formula::ProbabilisticBoundOperator<Type> const& formula) const {
+	storm::storage::BitVector* checkProbabilisticBoundOperator(storm::formula::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
 		std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false);
 
@@ -272,7 +272,7 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector* checkRewardBoundOperator(const storm::formula::RewardBoundOperator<Type>& formula) const {
+	storm::storage::BitVector* checkRewardBoundOperator(const storm::formula::prctl::RewardBoundOperator<Type>& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
 		std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false);
 

src/modelchecker/SparseDtmcPrctlModelChecker.h

@@ -64,12 +64,13 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	std::vector<Type>* checkPathNoBoundOperator(storm::formula::PathNoBoundOperator<Type> const& formula) const {
+	std::vector<Type>* checkNoBoundOperator(storm::formula::prctl::AbstractNoBoundOperator<Type> const& formula) const {
 		// Check if the operator was an optimality operator and report a warning in that case.
-		if (formula.isOptimalityOperator()) {
-			LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
-		}
-		return formula.getPathFormula().check(*this, false);
+		//if (formula.isOptimalityOperator()) {
+		//	LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
+		//}
+		// TODO: Reimplement warning
+		return formula.check(*this, false);
 	}
 
 	/*!
@@ -83,7 +84,7 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkBoundedUntil(storm::formula::BoundedUntil<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkBoundedUntil(storm::formula::prctl::BoundedUntil<Type> const& formula, bool qualitative) const {
 		// First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula.
 		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
 		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
@@ -120,7 +121,7 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkNext(storm::formula::Next<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkNext(storm::formula::prctl::Next<Type> const& formula, bool qualitative) const {
 		// First, we need to compute the states that satisfy the child formula of the next-formula.
 		storm::storage::BitVector* nextStates = formula.getChild().check(*this);
 
@@ -149,9 +150,9 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkBoundedEventually(storm::formula::BoundedEventually<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkBoundedEventually(storm::formula::prctl::BoundedEventually<Type> const& formula, bool qualitative) const {
 		// Create equivalent temporary bounded until formula and check it.
-		storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
+		storm::formula::prctl::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::prctl::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
 		return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
 	}
 
@@ -166,9 +167,9 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkEventually(storm::formula::Eventually<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkEventually(storm::formula::prctl::Eventually<Type> const& formula, bool qualitative) const {
 		// Create equivalent temporary until formula and check it.
-		storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone());
+		storm::formula::prctl::Until<Type> temporaryUntilFormula(new storm::formula::prctl::Ap<Type>("true"), formula.getChild().clone());
 		return this->checkUntil(temporaryUntilFormula, qualitative);
 	}
 
@@ -183,9 +184,9 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkGlobally(storm::formula::Globally<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkGlobally(storm::formula::prctl::Globally<Type> const& formula, bool qualitative) const {
 		// Create "equivalent" (equivalent up to negation) temporary eventually formula and check it.
-		storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone()));
+		storm::formula::prctl::Eventually<Type> temporaryEventuallyFormula(new storm::formula::prctl::Not<Type>(formula.getChild().clone()));
 		std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative);
 
 		// Now subtract the resulting vector from the constant one vector to obtain final result.
@@ -204,7 +205,7 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkUntil(storm::formula::Until<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkUntil(storm::formula::prctl::Until<Type> const& formula, bool qualitative) const {
 		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
 		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
 		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
@@ -275,7 +276,7 @@ public:
 	 * @returns The reward values for the given formula for every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact values might not be computed.
 	 */
-	virtual std::vector<Type>* checkInstantaneousReward(storm::formula::InstantaneousReward<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkInstantaneousReward(storm::formula::prctl::InstantaneousReward<Type> const& formula, bool qualitative) const {
 		// Only compute the result if the model has a state-based reward model.
 		if (!this->getModel().hasStateRewards()) {
 			LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
@@ -303,7 +304,7 @@ public:
 	 * @returns The reward values for the given formula for every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact values might not be computed.
 	 */
-	virtual std::vector<Type>* checkCumulativeReward(storm::formula::CumulativeReward<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkCumulativeReward(storm::formula::prctl::CumulativeReward<Type> const& formula, bool qualitative) const {
 		// Only compute the result if the model has at least one reward model.
 		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
 			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@@ -347,7 +348,7 @@ public:
 	 * @returns The reward values for the given formula for every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact values might not be computed.
 	 */
-	virtual std::vector<Type>* checkReachabilityReward(storm::formula::ReachabilityReward<Type> const& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkReachabilityReward(storm::formula::prctl::ReachabilityReward<Type> const& formula, bool qualitative) const {
 		// Only compute the result if the model has at least one reward model.
 		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
 			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");

src/modelchecker/SparseMdpPrctlModelChecker.h

@@ -66,14 +66,14 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	std::vector<Type>* checkPathNoBoundOperator(const storm::formula::PathNoBoundOperator<Type>& formula) const {
+	std::vector<Type>* checkNoBoundOperator(const storm::formula::prctl::AbstractNoBoundOperator<Type>& formula) const {
 		// Check if the operator was an non-optimality operator and report an error in that case.
 		if (!formula.isOptimalityOperator()) {
 			LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
 			throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
 		}
 		minimumOperatorStack.push(formula.isMinimumOperator());
-		std::vector<Type>* result = formula.getPathFormula().check(*this, false);
+		std::vector<Type>* result = formula.check(*this, false);
 		minimumOperatorStack.pop();
 		return result;
 	}
@@ -89,7 +89,7 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::prctl::BoundedUntil<Type>& formula, bool qualitative) const {
 		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
 		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
 		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
@@ -123,7 +123,7 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkNext(const storm::formula::prctl::Next<Type>& formula, bool qualitative) const {
 		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
 		storm::storage::BitVector* nextStates = formula.getChild().check(*this);
 
@@ -151,9 +151,9 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkBoundedEventually(const storm::formula::prctl::BoundedEventually<Type>& formula, bool qualitative) const {
 		// Create equivalent temporary bounded until formula and check it.
-		storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
+		storm::formula::prctl::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::prctl::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
 		return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
 	}
 
@@ -168,9 +168,9 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkEventually(const storm::formula::Eventually<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkEventually(const storm::formula::prctl::Eventually<Type>& formula, bool qualitative) const {
 		// Create equivalent temporary until formula and check it.
-		storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone());
+		storm::formula::prctl::Until<Type> temporaryUntilFormula(new storm::formula::prctl::Ap<Type>("true"), formula.getChild().clone());
 		return this->checkUntil(temporaryUntilFormula, qualitative);
 	}
 
@@ -185,9 +185,9 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkGlobally(const storm::formula::Globally<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkGlobally(const storm::formula::prctl::Globally<Type>& formula, bool qualitative) const {
 		// Create "equivalent" temporary eventually formula and check it.
-		storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone()));
+		storm::formula::prctl::Eventually<Type> temporaryEventuallyFormula(new storm::formula::prctl::Not<Type>(formula.getChild().clone()));
 		std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative);
 
 		// Now subtract the resulting vector from the constant one vector to obtain final result.
@@ -206,7 +206,7 @@ public:
 	 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact probabilities might not be computed.
 	 */
-	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkUntil(const storm::formula::prctl::Until<Type>& formula, bool qualitative) const {
 		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
 		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
 		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
@@ -275,7 +275,7 @@ public:
 	 * @returns The reward values for the given formula for every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact values might not be computed.
 	 */
-	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::prctl::InstantaneousReward<Type>& formula, bool qualitative) const {
 		// Only compute the result if the model has a state-based reward model.
 		if (!this->getModel().hasStateRewards()) {
 			LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
@@ -302,7 +302,7 @@ public:
 	 * @returns The reward values for the given formula for every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact values might not be computed.
 	 */
-	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::prctl::CumulativeReward<Type>& formula, bool qualitative) const {
 		// Only compute the result if the model has at least one reward model.
 		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
 			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@@ -345,7 +345,7 @@ public:
 	 * @returns The reward values for the given formula for every state of the model associated with this model
 	 * checker. If the qualitative flag is set, exact values might not be computed.
 	 */
-	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
+	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::prctl::ReachabilityReward<Type>& formula, bool qualitative) const {
 		// Only compute the result if the model has at least one reward model.
 		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
 			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");

src/parser/CslParser.cpp

@@ -1,229 +0,0 @@
-/*
- * CslParser.cpp
- *
- *  Created on: 08.04.2013
- *      Author: Thomas Heinemann
- */
-
-#include "src/parser/PrctlParser.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;
-
-#include "CslParser.h"
-
-
-namespace storm {
-namespace parser {
-
-template<typename Iterator, typename Skipper>
-struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<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::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::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::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::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::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
-				(qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
-				(qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
-								phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
-				(qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::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::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
-				(qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
-				(qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::LESS, qi::_1, qi::_2)] |
-				(qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::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::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::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::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)] |
-				(qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val =
-								phoenix::new_<storm::formula::TimeBoundedEventually<double>>(0, qi::_1, qi::_2)] |
-				(qi::lit("F") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)[qi::_val =
-								phoenix::new_<storm::formula::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::Eventually<double> >(qi::_1)];
-		eventually.name("path formula (for probabilistic operator)");
-		globally = (qi::lit("G") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
-		globally.name("path formula (for probabilistic operator)");
-		timeBoundedUntil = (
-					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]")  > stateFormula)
-					[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)] |
-					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_  > stateFormula)
-					[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(0, qi::_2, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)] |
-					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_  > stateFormula)
-					[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, std::numeric_limits<double>::infinity(), phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::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::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::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::AbstractFormula<double>*(), Skipper> start;
-
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> stateFormula;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> atomicStateFormula;
-
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> andFormula;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> atomicProposition;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> orFormula;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> notFormula;
-	qi::rule<Iterator, storm::formula::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator;
-	qi::rule<Iterator, storm::formula::SteadyStateBoundOperator<double>*(), Skipper> steadyStateBoundOperator;
-	qi::rule<Iterator, storm::formula::RewardBoundOperator<double>*(), Skipper> rewardBoundOperator;
-
-	qi::rule<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> noBoundOperator;
-	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
-	qi::rule<Iterator, storm::formula::StateNoBoundOperator<double>*(), Skipper> steadyStateNoBoundOperator;
-
-	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> pathFormula;
-	qi::rule<Iterator, storm::formula::TimeBoundedEventually<double>*(), Skipper> timeBoundedEventually;
-	qi::rule<Iterator, storm::formula::Eventually<double>*(), Skipper> eventually;
-	qi::rule<Iterator, storm::formula::Globally<double>*(), Skipper> globally;
-	qi::rule<Iterator, storm::formula::TimeBoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> timeBoundedUntil;
-	qi::rule<Iterator, storm::formula::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> until;
-
-	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> rewardPathFormula;
-	qi::rule<Iterator, storm::formula::CumulativeReward<double>*(), Skipper> cumulativeReward;
-	qi::rule<Iterator, storm::formula::ReachabilityReward<double>*(), Skipper> reachabilityReward;
-	qi::rule<Iterator, storm::formula::InstantaneousReward<double>*(), Skipper> instantaneousReward;
-	qi::rule<Iterator, storm::formula::SteadyStateReward<double>*(), Skipper> steadyStateReward;
-
-
-	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::AbstractFormula<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

@@ -1,53 +0,0 @@
-/*
- * 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/Formulas.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::AbstractFormula<double>* getFormula() {
-		return this->formula;
-	}
-
-private:
-private:
-	storm::formula::AbstractFormula<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_ */

src/parser/PrctlFileParser.cpp

@@ -68,11 +68,11 @@ void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractM
 		//The while loop reads the input file line by line
 		while (std::getline(inputFileStream, line)) {
 			PrctlParser parser(line);
-			storm::formula::AbstractStateFormula<double>* stateFormula = dynamic_cast<storm::formula::AbstractStateFormula<double>*>(parser.getFormula());
+			storm::formula::prctl::AbstractStateFormula<double>* stateFormula = dynamic_cast<storm::formula::prctl::AbstractStateFormula<double>*>(parser.getFormula());
 			if (stateFormula != nullptr) {
 				modelChecker->check(*stateFormula);
 			}
-			storm::formula::PathNoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::formula::PathNoBoundOperator<double>*>(parser.getFormula());
+			storm::formula::prctl::AbstractNoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::formula::prctl::AbstractNoBoundOperator<double>*>(parser.getFormula());
 			if (noBoundFormula != nullptr) {
 				modelChecker->check(*noBoundFormula);
 			}

src/parser/PrctlFileParser.h

@@ -10,7 +10,7 @@
 
 #include "models/Dtmc.h"
 #include "models/Mdp.h"
-#include "formula/Formulas.h"
+#include "formula/Prctl.h"
 #include "modelchecker/AbstractModelChecker.h"
 
 namespace storm {

src/parser/PrctlParser.cpp

@@ -33,7 +33,7 @@ namespace storm {
 namespace parser {
 
 template<typename Iterator, typename Skipper>
-struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper > {
+struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::prctl::AbstractPrctlFormula<double>*(), Skipper > {
 	PrctlGrammar() : PrctlGrammar::base_type(start) {
 		freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
 
@@ -41,13 +41,13 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 		stateFormula %= orFormula;
 		stateFormula.name("state formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
-				phoenix::new_<storm::formula::Or<double>>(qi::_val, qi::_1)];
+				phoenix::new_<storm::formula::prctl::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::And<double>>(qi::_val, qi::_1)];
+				phoenix::new_<storm::formula::prctl::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::Not<double>>(qi::_1)];
+				phoenix::new_<storm::formula::prctl::Not<double>>(qi::_1)];
 		notFormula.name("state formula");
 
 		//This block defines rules for "atomic" state formulas
@@ -55,28 +55,28 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 		atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")");
 		atomicStateFormula.name("state formula");
 		atomicProposition = (freeIdentifierName)[qi::_val =
-				phoenix::new_<storm::formula::Ap<double>>(qi::_1)];
+				phoenix::new_<storm::formula::prctl::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::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
+						phoenix::new_<storm::formula::prctl::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::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+						phoenix::new_<storm::formula::prctl::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::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
+								phoenix::new_<storm::formula::prctl::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::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
+						phoenix::new_<storm::formula::prctl::ProbabilisticBoundOperator<double> >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 		probabilisticBoundOperator.name("state formula");
 		rewardBoundOperator = (
 				(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
+						phoenix::new_<storm::formula::prctl::RewardBoundOperator<double> >(storm::formula::GREATER, qi::_1, qi::_2)] |
 				(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-								phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+								phoenix::new_<storm::formula::prctl::RewardBoundOperator<double> >(storm::formula::GREATER_EQUAL, qi::_1, qi::_2)] |
 				(qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
+										phoenix::new_<storm::formula::prctl::RewardBoundOperator<double> >(storm::formula::LESS, qi::_1, qi::_2)] |
 				(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
+						phoenix::new_<storm::formula::prctl::RewardBoundOperator<double> >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 		rewardBoundOperator.name("state formula");
 
@@ -84,78 +84,77 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 		noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator);
 		noBoundOperator.name("no bound operator");
 		probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-				phoenix::new_<storm::formula::ProbabilisticNoBoundOperator<double> >(qi::_1)];
+				phoenix::new_<storm::formula::prctl::ProbabilisticNoBoundOperator<double> >(qi::_1)];
 		probabilisticNoBoundOperator.name("no bound operator");
 		rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-				phoenix::new_<storm::formula::RewardNoBoundOperator<double> >(qi::_1)];
+				phoenix::new_<storm::formula::prctl::RewardNoBoundOperator<double> >(qi::_1)];
 		rewardNoBoundOperator.name("no bound operator");
 
 		//This block defines rules for parsing probabilistic path formulas
 		pathFormula = (boundedEventually | eventually | globally | boundedUntil | until);
 		pathFormula.name("path formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)];
+				phoenix::new_<storm::formula::prctl::BoundedEventually<double>>(qi::_2, qi::_1)];
 		boundedEventually.name("path formula (for probablistic operator)");
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
+				phoenix::new_<storm::formula::prctl::Eventually<double> >(qi::_1)];
 		eventually.name("path formula (for probablistic operator)");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
+				phoenix::new_<storm::formula::prctl::Globally<double> >(qi::_1)];
 		globally.name("path formula (for probablistic operator)");
-		boundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)
-				[qi::_val = phoenix::new_<storm::formula::BoundedUntil<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3, qi::_2)];
+		boundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::prctl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)
+				[qi::_val = phoenix::new_<storm::formula::prctl::BoundedUntil<double>>(phoenix::bind(&storm::formula::prctl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::prctl::AbstractStateFormula<double>>::get, qi::_a)), qi::_3, qi::_2)];
 		boundedUntil.name("path formula (for probablistic operator)");
-		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
+		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::prctl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::prctl::Until<double>>(phoenix::bind(&storm::formula::prctl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::prctl::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
 		until.name("path formula (for probablistic operator)");
 
 		//This block defines rules for parsing reward path formulas
 		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward);
 		rewardPathFormula.name("path formula (for reward operator)");
 		cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)
-				[qi::_val = phoenix::new_<storm::formula::CumulativeReward<double>>(qi::_1)];
+				[qi::_val = phoenix::new_<storm::formula::prctl::CumulativeReward<double>>(qi::_1)];
 		cumulativeReward.name("path formula (for reward operator)");
 		reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::ReachabilityReward<double>>(qi::_1)];
+				phoenix::new_<storm::formula::prctl::ReachabilityReward<double>>(qi::_1)];
 		reachabilityReward.name("path formula (for reward operator)");
 		instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_)
-						[qi::_val = phoenix::new_<storm::formula::InstantaneousReward<double>>(qi::_1)];
+						[qi::_val = phoenix::new_<storm::formula::prctl::InstantaneousReward<double>>(qi::_1)];
 		instantaneousReward.name("path formula (for reward operator)");
-		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::formula::SteadyStateReward<double>>()];
-
+		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::formula::prctl::SteadyStateReward<double>>()];
 
 		start = (noBoundOperator | stateFormula);
 		start.name("PRCTL formula");
 	}
 
-	qi::rule<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> start;
+	qi::rule<Iterator, storm::formula::prctl::AbstractPrctlFormula<double>*(), Skipper> start;
 
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> stateFormula;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> atomicStateFormula;
+	qi::rule<Iterator, storm::formula::prctl::AbstractStateFormula<double>*(), Skipper> stateFormula;
+	qi::rule<Iterator, storm::formula::prctl::AbstractStateFormula<double>*(), Skipper> atomicStateFormula;
 
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> andFormula;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> atomicProposition;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> orFormula;
-	qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> notFormula;
-	qi::rule<Iterator, storm::formula::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator;
-	qi::rule<Iterator, storm::formula::RewardBoundOperator<double>*(), Skipper> rewardBoundOperator;
+	qi::rule<Iterator, storm::formula::prctl::AbstractStateFormula<double>*(), Skipper> andFormula;
+	qi::rule<Iterator, storm::formula::prctl::AbstractStateFormula<double>*(), Skipper> atomicProposition;
+	qi::rule<Iterator, storm::formula::prctl::AbstractStateFormula<double>*(), Skipper> orFormula;
+	qi::rule<Iterator, storm::formula::prctl::AbstractStateFormula<double>*(), Skipper> notFormula;
+	qi::rule<Iterator, storm::formula::prctl::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator;
+	qi::rule<Iterator, storm::formula::prctl::RewardBoundOperator<double>*(), Skipper> rewardBoundOperator;
 
-	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> noBoundOperator;
-	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
-	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> rewardNoBoundOperator;
+	qi::rule<Iterator, storm::formula::prctl::AbstractNoBoundOperator<double>*(), Skipper> noBoundOperator;
+	qi::rule<Iterator, storm::formula::prctl::AbstractNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
+	qi::rule<Iterator, storm::formula::prctl::AbstractNoBoundOperator<double>*(), Skipper> rewardNoBoundOperator;
 
-	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> pathFormula;
-	qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually;
-	qi::rule<Iterator, storm::formula::Eventually<double>*(), Skipper> eventually;
-	qi::rule<Iterator, storm::formula::Globally<double>*(), Skipper> globally;
-	qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> boundedUntil;
-	qi::rule<Iterator, storm::formula::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> until;
+	qi::rule<Iterator, storm::formula::prctl::AbstractPathFormula<double>*(), Skipper> pathFormula;
+	qi::rule<Iterator, storm::formula::prctl::BoundedEventually<double>*(), Skipper> boundedEventually;
+	qi::rule<Iterator, storm::formula::prctl::Eventually<double>*(), Skipper> eventually;
+	qi::rule<Iterator, storm::formula::prctl::Globally<double>*(), Skipper> globally;
+	qi::rule<Iterator, storm::formula::prctl::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::prctl::AbstractStateFormula<double>>>, Skipper> boundedUntil;
+	qi::rule<Iterator, storm::formula::prctl::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::prctl::AbstractStateFormula<double>>>, Skipper> until;
 
-	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> rewardPathFormula;
-	qi::rule<Iterator, storm::formula::CumulativeReward<double>*(), Skipper> cumulativeReward;
-	qi::rule<Iterator, storm::formula::ReachabilityReward<double>*(), Skipper> reachabilityReward;
-	qi::rule<Iterator, storm::formula::InstantaneousReward<double>*(), Skipper> instantaneousReward;
-	qi::rule<Iterator, storm::formula::SteadyStateReward<double>*(), Skipper> steadyStateReward;
+	qi::rule<Iterator, storm::formula::prctl::AbstractPathFormula<double>*(), Skipper> rewardPathFormula;
+	qi::rule<Iterator, storm::formula::prctl::CumulativeReward<double>*(), Skipper> cumulativeReward;
+	qi::rule<Iterator, storm::formula::prctl::ReachabilityReward<double>*(), Skipper> reachabilityReward;
+	qi::rule<Iterator, storm::formula::prctl::InstantaneousReward<double>*(), Skipper> instantaneousReward;
+	qi::rule<Iterator, storm::formula::prctl::SteadyStateReward<double>*(), Skipper> steadyStateReward;
 
 
 	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
@@ -174,7 +173,7 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
 
 
 	// Prepare resulting intermediate representation of input.
-	storm::formula::AbstractFormula<double>* result_pointer = nullptr;
+	storm::formula::prctl::AbstractPrctlFormula<double>* result_pointer = nullptr;
 
 	PrctlGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> grammar;
 

src/parser/PrctlParser.h

@@ -3,7 +3,7 @@
 
 #include "src/parser/Parser.h"
 
-#include "src/formula/Formulas.h"
+#include "src/formula/Prctl.h"
 //#include <memory>
 
 namespace storm {
@@ -34,12 +34,12 @@ class PrctlParser : Parser {
 		/*!
 		 *	@return a pointer to the parsed formula object
 		 */
-		storm::formula::AbstractFormula<double>* getFormula() {
+		storm::formula::prctl::AbstractPrctlFormula<double>* getFormula() {
 			return this->formula;
 		}
 
 	private:
-		storm::formula::AbstractFormula<double>* formula;
+		storm::formula::prctl::AbstractPrctlFormula<double>* formula;
 
 		/*!
 		 * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas.

src/storm.cpp

@@ -29,7 +29,7 @@
 #include "src/parser/PrctlParser.h"
 #include "src/utility/Settings.h"
 #include "src/utility/ErrorHandling.h"
-#include "src/formula/Formulas.h"
+#include "src/formula/Prctl.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -142,30 +142,30 @@ void cleanUp() {
 void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 
-	storm::formula::Ap<double>* oneFormula = new storm::formula::Ap<double>("one");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* oneFormula = new storm::formula::prctl::Ap<double>("one");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(oneFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	oneFormula = new storm::formula::Ap<double>("two");
-	eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	oneFormula = new storm::formula::prctl::Ap<double>("two");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(oneFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	oneFormula = new storm::formula::Ap<double>("three");
-	eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	oneFormula = new storm::formula::prctl::Ap<double>("three");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(oneFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+	storm::formula::prctl::Ap<double>* done = new storm::formula::prctl::Ap<double>("done");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(done);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
@@ -173,24 +173,24 @@ void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
 }
 
 void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
-	storm::formula::Ap<double>* observe0Greater1Formula = new storm::formula::Ap<double>("observe0Greater1");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(observe0Greater1Formula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* observe0Greater1Formula = new storm::formula::prctl::Ap<double>("observe0Greater1");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(observe0Greater1Formula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	mc->check(*probFormula);
 	delete probFormula;
 
-	storm::formula::Ap<double>* observeIGreater1Formula = new storm::formula::Ap<double>("observeIGreater1");
-	eventuallyFormula = new storm::formula::Eventually<double>(observeIGreater1Formula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* observeIGreater1Formula = new storm::formula::prctl::Ap<double>("observeIGreater1");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(observeIGreater1Formula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	storm::formula::Ap<double>* observeOnlyTrueSenderFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
-	eventuallyFormula = new storm::formula::Eventually<double>(observeOnlyTrueSenderFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* observeOnlyTrueSenderFormula = new storm::formula::prctl::Ap<double>("observeOnlyTrueSender");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(observeOnlyTrueSenderFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
@@ -199,24 +199,24 @@ void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
 }
 
 void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast64_t n) {
-	storm::formula::Ap<double>* electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(electedFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	mc->check(*probFormula);
 	delete probFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), electedFormula, n * 4);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::formula::prctl::BoundedUntil<double>(new storm::formula::prctl::Ap<double>("true"), electedFormula, n * 4);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(electedFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
@@ -225,9 +225,9 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 }
 
 void testCheckingDice(storm::models::Mdp<double>& mdp) {
-	storm::formula::Ap<double>* twoFormula = new storm::formula::Ap<double>("two");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	storm::formula::prctl::Ap<double>* twoFormula = new storm::formula::prctl::Ap<double>("two");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
 
@@ -235,79 +235,79 @@ void testCheckingDice(storm::models::Mdp<double>& mdp) {
 	delete probFormula;
 
 
-	twoFormula = new storm::formula::Ap<double>("two");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	twoFormula = new storm::formula::prctl::Ap<double>("two");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("three");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	twoFormula = new storm::formula::prctl::Ap<double>("three");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("three");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	twoFormula = new storm::formula::prctl::Ap<double>("three");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("four");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	twoFormula = new storm::formula::prctl::Ap<double>("four");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("four");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	twoFormula = new storm::formula::prctl::Ap<double>("four");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("five");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	twoFormula = new storm::formula::prctl::Ap<double>("five");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("five");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	twoFormula = new storm::formula::prctl::Ap<double>("five");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("six");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	twoFormula = new storm::formula::prctl::Ap<double>("six");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	twoFormula = new storm::formula::Ap<double>("six");
-	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	twoFormula = new storm::formula::prctl::Ap<double>("six");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	storm::formula::Ap<double>* doneFormula = new storm::formula::Ap<double>("done");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(doneFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	storm::formula::prctl::Ap<double>* doneFormula = new storm::formula::prctl::Ap<double>("done");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(doneFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
 
-	doneFormula = new storm::formula::Ap<double>("done");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(doneFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	doneFormula = new storm::formula::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(doneFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
@@ -316,46 +316,46 @@ void testCheckingDice(storm::models::Mdp<double>& mdp) {
 }
 
 void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
-	storm::formula::Ap<double>* electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	storm::formula::prctl::Ap<double>* electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(electedFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probMinFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
 
 	mc->check(*probMinFormula);
 	delete probMinFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(electedFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probMaxFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probMaxFormula);
 	delete probMaxFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 25);
-	probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually<double>(electedFormula, 25);
+	probMinFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
 
 	mc->check(*probMinFormula);
 	delete probMinFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 25);
-	probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually<double>(electedFormula, 25);
+	probMaxFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
 
 	mc->check(*probMaxFormula);
 	delete probMaxFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(electedFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
 
-	electedFormula = new storm::formula::Ap<double>("elected");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	electedFormula = new storm::formula::prctl::Ap<double>("elected");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(electedFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
@@ -364,67 +364,67 @@ void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
 }
 
 void testCheckingConsensus(storm::models::Mdp<double>& mdp) {
-	storm::formula::Ap<double>* finishedFormula = new storm::formula::Ap<double>("finished");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(finishedFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	storm::formula::prctl::Ap<double>* finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(finishedFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	storm::formula::Ap<double>* allCoinsEqual0Formula = new storm::formula::Ap<double>("all_coins_equal_0");
-	storm::formula::And<double>* conjunctionFormula = new storm::formula::And<double>(finishedFormula, allCoinsEqual0Formula);
-	eventuallyFormula = new storm::formula::Eventually<double>(conjunctionFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	storm::formula::prctl::Ap<double>* allCoinsEqual0Formula = new storm::formula::prctl::Ap<double>("all_coins_equal_0");
+	storm::formula::prctl::And<double>* conjunctionFormula = new storm::formula::prctl::And<double>(finishedFormula, allCoinsEqual0Formula);
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(conjunctionFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	storm::formula::Ap<double>* allCoinsEqual1Formula = new storm::formula::Ap<double>("all_coins_equal_1");
-	conjunctionFormula = new storm::formula::And<double>(finishedFormula, allCoinsEqual1Formula);
-	eventuallyFormula = new storm::formula::Eventually<double>(conjunctionFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	storm::formula::prctl::Ap<double>* allCoinsEqual1Formula = new storm::formula::prctl::Ap<double>("all_coins_equal_1");
+	conjunctionFormula = new storm::formula::prctl::And<double>(finishedFormula, allCoinsEqual1Formula);
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(conjunctionFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	storm::formula::Ap<double>* agree = new storm::formula::Ap<double>("agree");
-	storm::formula::Not<double>* notAgree = new storm::formula::Not<double>(agree);
-	conjunctionFormula = new storm::formula::And<double>(finishedFormula, notAgree);
-	eventuallyFormula = new storm::formula::Eventually<double>(conjunctionFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	storm::formula::prctl::Ap<double>* agree = new storm::formula::prctl::Ap<double>("agree");
+	storm::formula::prctl::Not<double>* notAgree = new storm::formula::prctl::Not<double>(agree);
+	conjunctionFormula = new storm::formula::prctl::And<double>(finishedFormula, notAgree);
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(conjunctionFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(finishedFormula, 50);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	storm::formula::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually<double>(finishedFormula, 50);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(finishedFormula, 50);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually<double>(finishedFormula, 50);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(finishedFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(finishedFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
 
-	finishedFormula = new storm::formula::Ap<double>("finished");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(finishedFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	finishedFormula = new storm::formula::prctl::Ap<double>("finished");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(finishedFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;

test/functional/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -19,45 +19,52 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
-	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* apFormula = new storm::formula::prctl::Ap<double>("one");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	std::vector<double>* result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("two");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	apFormula = new storm::formula::prctl::Ap<double>("two");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("three");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	apFormula = new storm::formula::prctl::Ap<double>("three");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+	storm::formula::prctl::Ap<double>* done = new storm::formula::prctl::Ap<double>("done");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(done);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
 
 	result = rewardFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
 
 	ASSERT_LT(std::abs((*result)[0] - ((double)11/3)), s->get<double>("precision"));
 
@@ -79,34 +86,40 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
-	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* apFormula = new storm::formula::prctl::Ap<double>("observe0Greater1");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	std::vector<double>* result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("observeIGreater1");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	apFormula = new storm::formula::prctl::Ap<double>("observeIGreater1");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	apFormula = new storm::formula::prctl::Ap<double>("observeOnlyTrueSender");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get<double>("precision"));
 
 	delete probFormula;
@@ -127,34 +140,40 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
-	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+	storm::formula::prctl::Ap<double>* apFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	std::vector<double>* result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), apFormula, 20);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::formula::prctl::BoundedUntil<double>(new storm::formula::prctl::Ap<double>("true"), apFormula, 20);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
 
 	result = rewardFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get<double>("precision"));
 
 	delete rewardFormula;

test/functional/GmmxxMdpPrctModelCheckerTest.cpp

@@ -18,20 +18,22 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
 
-	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("two");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	storm::formula::prctl::Ap<double>* apFormula = new storm::formula::prctl::Ap<double>("two");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	std::vector<double>* result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("two");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("two");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	result = probFormula->check(mc);
 
@@ -40,9 +42,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("three");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("three");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	result = probFormula->check(mc);
 
@@ -51,9 +53,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("three");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("three");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	result = probFormula->check(mc);
 
@@ -62,9 +64,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("four");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("four");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	result = probFormula->check(mc);
 
@@ -73,9 +75,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("four");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("four");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	result = probFormula->check(mc);
 
@@ -84,9 +86,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("done");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("done");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	result = rewardFormula->check(mc);
 
@@ -95,9 +97,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete rewardFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("done");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	result = rewardFormula->check(mc);
 
@@ -114,9 +116,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
 
-	apFormula = new storm::formula::Ap<double>("done");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	result = rewardFormula->check(stateRewardModelChecker);
 
@@ -125,9 +127,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete rewardFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("done");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	result = rewardFormula->check(stateRewardModelChecker);
 
@@ -144,9 +146,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
 
-	apFormula = new storm::formula::Ap<double>("done");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	result = rewardFormula->check(stateAndTransitionRewardModelChecker);
 
@@ -155,9 +157,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	delete rewardFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("done");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	result = rewardFormula->check(stateAndTransitionRewardModelChecker);
 
@@ -180,53 +182,61 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
 
-	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	storm::formula::prctl::Ap<double>* apFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::Eventually<double>* eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	storm::formula::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	std::vector<double>* result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	eventuallyFormula = new storm::formula::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(apFormula, 25);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually<double>(apFormula, 25);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(apFormula, 25);
-	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually<double>(apFormula, 25);
+	probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
 
 	result = probFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	storm::formula::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	storm::formula::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
 
 	result = rewardFormula->check(mc);
 
@@ -235,12 +245,14 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 	delete rewardFormula;
 	delete result;
 
-	apFormula = new storm::formula::Ap<double>("elected");
-	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
-	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+	apFormula = new storm::formula::prctl::Ap<double>("elected");
+	reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
 
 	result = rewardFormula->check(mc);
 
+	ASSERT_NE(nullptr, result);
+
 	ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
 
 	delete rewardFormula;

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;
@@ -155,3 +155,4 @@ TEST(CslParserTest, wrongFormulaTest2) {
 	);
 	delete cslParser;
 }
+*/

test/parser/PrctlParserTest.cpp

@@ -51,9 +51,9 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
-	storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(prctlParser->getFormula());
+	storm::formula::prctl::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::prctl::ProbabilisticBoundOperator<double>*>(prctlParser->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(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]");
@@ -71,9 +71,9 @@ TEST(PrctlParserTest, parseRewardFormulaTest) {
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
-	storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlParser->getFormula());
+	storm::formula::prctl::RewardBoundOperator<double>* op = static_cast<storm::formula::prctl::RewardBoundOperator<double>*>(prctlParser->getFormula());
 
-	ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
+	ASSERT_EQ(storm::formula::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
 
 	ASSERT_EQ("R >= 15.000000 [I=5]", prctlParser->getFormula()->toString());