Created new base class OptimizingOperator.

Inheriting from this class where appropriate, added constructors accepting minimumOperator argument.

src/formula/NoBoundOperator.h

@@ -11,6 +11,7 @@
 #include "src/formula/AbstractFormula.h"
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/OptimizingOperator.h"
 
 #include "src/modelchecker/ForwardDeclarations.h"
 
@@ -69,12 +70,12 @@ class INoBoundOperatorModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class NoBoundOperator: public storm::formula::AbstractFormula<T> {
+class NoBoundOperator: public storm::formula::AbstractFormula<T>, public OptimizingOperator {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	NoBoundOperator() : optimalityOperator(false), minimumOperator(false) {
+	NoBoundOperator() {
 		this->pathFormula = nullptr;
 	}
 
@@ -83,7 +84,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	NoBoundOperator(AbstractPathFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
+	NoBoundOperator(AbstractPathFormula<T>* pathFormula) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -95,7 +96,7 @@ public:
 	 * maximizing operator.
 	 */
 	NoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
-		: optimalityOperator(true), minimumOperator(minimumOperator) {
+		: OptimizingOperator(minimumOperator) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -154,34 +155,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:
 	AbstractPathFormula<T>* 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 formula */

src/formula/OptimizingOperator.h

@@ -0,0 +1,56 @@
+#ifndef STORM_FORMULA_OPTIMIZINGOPERATOR_H_
+#define STORM_FORMULA_OPTIMIZINGOPERATOR_H_
+
+namespace storm {
+
+namespace formula {
+
+class OptimizingOperator {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	OptimizingOperator() : optimalityOperator(false), minimumOperator(false) {
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param minimumOperator A flag indicating whether this operator is a minimizing or a maximizing operator.
+	 */
+	OptimizingOperator(bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) {
+	}
+
+	/*!
+	 * 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:
+	// 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 formula */
+
+} /* namespace storm */
+
+#endif /* STORM_FORMULA_OPTIMIZINGOPERATOR_H_ */

src/formula/PathBoundOperator.h

@@ -11,6 +11,8 @@
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/OptimizingOperator.h"
+
 #include "src/modelchecker/ForwardDeclarations.h"
 #include "src/utility/ConstTemplates.h"
 
@@ -42,7 +44,7 @@ template <class T> class PathBoundOperator;
  * @see AbstractFormula
  */
 template<class T>
-class PathBoundOperator : public AbstractStateFormula<T> {
+class PathBoundOperator : public AbstractStateFormula<T>, public OptimizingOperator {
 
 public:
 	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@@ -55,8 +57,7 @@ public:
 	 * @param pathFormula The child node
 	 */
 	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
-		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula),
-		  optimalityOperator(false), minimumOperator(false) {
+		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
 	
@@ -69,8 +70,7 @@ public:
 	 * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
 	 */
 	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
-		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula),
-		  optimalityOperator(true), minimumOperator(minimumOperator) {
+		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -176,36 +176,10 @@ 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:
 	ComparisonType comparisonOperator;
 	T bound;
 	AbstractPathFormula<T>* 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 formula

src/formula/ProbabilisticBoundOperator.h

@@ -11,6 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
 #include "src/formula/PathBoundOperator.h"
+#include "src/formula/OptimizingOperator.h"
 #include "utility/ConstTemplates.h"
 
 namespace storm {
@@ -72,8 +73,14 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
-				PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
+			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+		// Intentionally left empty
+	}
+
+	ProbabilisticBoundOperator(
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
 		// Intentionally left empty
 	}
 

src/formula/RewardBoundOperator.h

@@ -74,6 +74,12 @@ public:
 		// Intentionally left empty
 	}
 
+	RewardBoundOperator(
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator) {
+		// Intentionally left empty
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */