Added proper formula string method to filters.

- Lots of debugging
- Changed the way the filter keeps information about the scheduler to use for probability/reward queries.
| This was done by keeping a special action at the first position of the action list.
| Which was not exactly consistent with the idea behind the filter actions.
| Now the filter keeps this information as an enum value in a member variable.
- All but one tests are green. So we almost reestablished full functionality.
|- The last test that still fails is SparseMdpPrctlModelCheckerTest.Dice where the second to last model check returns the wrong result.

Next up: Debug. Then introduce the full range of filter actions.


Former-commit-id: fd311966cc

src/formula/AbstractFilter.h

@@ -15,20 +15,25 @@
 namespace storm {
 namespace property {
 
+/*!
+ *
+ */
+enum OptimizingOperator {MINIMIZE, MAXIMIZE, UNDEFINED};
+
 template <class T>
 class AbstractFilter {
 
 public:
 
-	AbstractFilter() {
+	AbstractFilter(OptimizingOperator opt = UNDEFINED) : opt(opt) {
 		// Intentionally left empty.
 	}
 
-	AbstractFilter(action::AbstractAction<T>* action) {
+	AbstractFilter(action::AbstractAction<T>* action, OptimizingOperator opt = UNDEFINED) : opt(opt) {
 		actions.push_back(action);
 	}
 
-	AbstractFilter(std::vector<action::AbstractAction<T>*> actions) : actions(actions) {
+	AbstractFilter(std::vector<action::AbstractAction<T>*> actions, OptimizingOperator opt = UNDEFINED) : actions(actions), opt(opt) {
 		// Intentionally left empty.
 	}
 
@@ -36,16 +41,30 @@ public:
 		actions.clear();
 	}
 
-	std::string toFormulaString() const {
+	virtual std::string toString() const {
 		std::string desc = "filter(";
+
+		for(auto action : actions) {
+			desc += action->toString();
+			desc += ", ";
+		}
+
+		// Remove the last ", ".
+		if(!actions.empty()) {
+			desc.pop_back();
+			desc.pop_back();
+		}
+
+		desc += ")";
+
 		return desc;
 	}
 
-	std::string toString() const {
+	virtual std::string toPrettyString() const {
 		std::string desc = "Filter: ";
 		desc += "\nActions:";
 		for(auto action : actions) {
-			desc += "\n\t" + action.toString();
+			desc += "\n\t" + action->toString();
 		}
 		return desc;
 	}
@@ -66,9 +85,19 @@ public:
 		return actions.size();
 	}
 
+	void setOptimizingOperator(OptimizingOperator opt) {
+		this->opt = opt;
+	}
+
+	OptimizingOperator getOptimizingOperator() const {
+		return opt;
+	}
+
 protected:
 
 	std::vector<action::AbstractAction<T>*> actions;
+
+	OptimizingOperator opt;
 };
 
 } //namespace property

src/formula/Actions/MinMaxAction.h

@@ -1,68 +0,0 @@
-/*
- * MinMaxAction.h
- *
- *  Created on: Apr 30, 2014
- *      Author: Manuel Sascha Weiand
- */
-
-#ifndef STORM_FORMULA_ACTION_MINMAXACTION_H_
-#define STORM_FORMULA_ACTION_MINMAXACTION_H_
-
-#include "src/formula/Actions/AbstractAction.h"
-
-namespace storm {
-namespace property {
-namespace action {
-
-template <class T>
-class MinMaxAction : public AbstractAction<T> {
-
-public:
-
-	MinMaxAction() : minimize(true) {
-		//Intentionally left empty.
-	}
-
-	explicit MinMaxAction(bool minimize) : minimize(minimize) {
-		//Intentionally left empty.
-	}
-
-	/*!
-	 * Virtual destructor
-	 * To ensure that the right destructor is called
-	 */
-	virtual ~MinMaxAction() {
-		//Intentionally left empty
-	}
-
-	/*!
-	 *
-	 */
-	virtual std::string toString() const override {
-		return minimize ? "min" : "max";
-	}
-
-	/*!
-	 *
-	 */
-	virtual std::string toFormulaString() const override {
-		return minimize ? "min" : "max";
-	}
-
-	/*!
-	 *
-	 */
-	bool getMinimize() {
-		return minimize;
-	}
-
-private:
-	bool minimize;
-
-};
-
-} //namespace action
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ACTION_MINMAXACTION_H_ */

src/formula/Csl/CslFilter.h

@@ -13,7 +13,6 @@
 #include "src/formula/Csl/AbstractPathFormula.h"
 #include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/modelchecker/csl/AbstractModelChecker.h"
-#include "src/formula/Actions/MinMaxAction.h"
 
 namespace storm {
 namespace property {
@@ -24,23 +23,19 @@ class CslFilter : public storm::property::AbstractFilter<T> {
 
 public:
 
-	CslFilter() : child(nullptr) {
+	CslFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr), steadyStateQuery(false) {
 		// Intentionally left empty.
 	}
 
-	CslFilter(AbstractCslFormula<T>* child) : child(child) {
+	CslFilter(AbstractCslFormula<T>* child, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(opt), child(child), steadyStateQuery(steadyStateQuery) {
 		// Intentionally left empty.
 	}
 
-	CslFilter(AbstractCslFormula<T>* child, bool minimize) : child(child) {
-		this->actions.push_back(new storm::property::action::MinMaxAction<T>(minimize));
+	CslFilter(AbstractCslFormula<T>* child, action::AbstractAction<T>* action, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(action, opt), child(child), steadyStateQuery(steadyStateQuery) {
+		// Intentionally left empty
 	}
 
-	CslFilter(AbstractCslFormula<T>* child, action::AbstractAction<T>* action) : child(child) {
-		this->actions.push_back(action);
-	}
-
-	CslFilter(AbstractCslFormula<T>* child, std::vector<action::AbstractAction<T>*> actions) : AbstractFilter<T>(actions), child(child) {
+	CslFilter(AbstractCslFormula<T>* child, std::vector<action::AbstractAction<T>*> actions, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(actions, opt), child(child), steadyStateQuery(steadyStateQuery) {
 		// Intentionally left empty.
 	}
 
@@ -145,12 +140,94 @@ public:
 		return true;
 	}
 
-	std::string toFormulaString() const {
-		std::string desc = "filter(";
+	virtual std::string toString() const override {
+		std::string desc = "";
+
+		if(dynamic_cast<AbstractStateFormula<T>*>(child) == nullptr) {
+
+			// The formula is not a state formula so we have a probability query.
+			if(this->actions.empty()){
+
+				// Since there are no actions given we do legacy support.
+
+				desc += "P ";
+				switch(this->opt) {
+					case MINIMIZE:
+						desc += "min ";
+						break;
+					case MAXIMIZE:
+						desc += "max ";
+						break;
+					default:
+						break;
+				}
+				desc += "= ? ";
+
+			} else {
+				desc = "filter[";
+
+				switch(this->opt) {
+					case MINIMIZE:
+						desc += "min, ";
+						break;
+					case MAXIMIZE:
+						desc += "max, ";
+						break;
+					default:
+						break;
+				}
+
+				for(auto action : this->actions) {
+					desc += action->toString();
+					desc += ", ";
+				}
+
+				// Remove the last ", ".
+				desc.pop_back();
+				desc.pop_back();
+
+				desc += "]";
+			}
+
+		} else {
+
+			if(this->actions.empty()) {
+
+				if(steadyStateQuery) {
+
+					// Legacy support for the steady state query.
+					desc += "S = ? ";
+
+				} else {
+
+					// There are no filter actions but only the raw state formula. So just print that.
+					return child->toString();
+				}
+			} else {
+
+				desc = "filter[";
+
+				for(auto action : this->actions) {
+					desc += action->toString();
+					desc += ", ";
+				}
+
+				// Remove the last ", ".
+				desc.pop_back();
+				desc.pop_back();
+
+				desc += "]";
+			}
+		}
+
+		desc += "(";
+		desc += child->toString();
+		desc += ")";
+
 		return desc;
 	}
 
-	std::string toString() const {
+	virtual std::string toPrettyString() const override{
 		std::string desc = "Filter: ";
 		desc += "\nActions:";
 		for(auto action : this->actions) {
@@ -174,9 +251,9 @@ private:
 		// First, get the model checking result.
 		storm::storage::BitVector result = modelchecker.checkMinMaxOperator(formula);
 
-		if(this->getActionCount() != 0 &&  dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
+		if(this->opt != UNDEFINED) {
 			// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-			result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
+			result = modelchecker.checkMinMaxOperator(formula, this->opt == MINIMIZE ? true : false);
 		} else {
 			result = formula->check(modelchecker);
 		}
@@ -193,9 +270,9 @@ private:
 		// First, get the model checking result.
 		std::vector<T> result;
 
-		if(this->getActionCount() != 0 &&  dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
+		if(this->opt != UNDEFINED) {
 			// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-			result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
+			result = modelchecker.checkMinMaxOperator(formula, this->opt == MINIMIZE ? true : false);
 		} else {
 			result = formula->check(modelchecker, false);
 		}
@@ -208,6 +285,8 @@ private:
 	}
 
 	AbstractCslFormula<T>* child;
+
+	bool steadyStateQuery;
 };
 
 } //namespace csl

src/formula/Csl/ProbabilisticBoundOperator.h

@@ -139,9 +139,9 @@ public:
 		}
 		result += " ";
 		result += std::to_string(bound);
-		result += " [";
+		result += " (";
 		result += pathFormula->toString();
-		result += "]";
+		result += ")";
 		return result;
 	}
 

src/formula/Csl/SteadyStateBoundOperator.h

@@ -135,9 +135,9 @@ public:
 		case GREATER_EQUAL: result += ">= "; break;
 		}
 		result += std::to_string(bound);
-		result += " [";
+		result += " (";
 		result += stateFormula->toString();
-		result += "]";
+		result += ")";
 		return result;
 	}
 

src/formula/Csl/TimeBoundedEventually.h

@@ -50,7 +50,7 @@ public:
 		setInterval(lowerBound, upperBound);
 	}
 
-	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child) : child(nullptr) {
+	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child) : child(child) {
 		setInterval(lowerBound, upperBound);
 	}
 
@@ -104,9 +104,9 @@ public:
 	virtual std::string toString() const override {
 		std::string result = "F";
 		if (upperBound == std::numeric_limits<double>::infinity()) {
-			result = ">=" + std::to_string(lowerBound);
+			result += ">=" + std::to_string(lowerBound);
 		} else {
-			result = "[";
+			result += "[";
 			result += std::to_string(lowerBound);
 			result += ",";
 			result += std::to_string(upperBound);

src/formula/Csl/TimeBoundedUntil.h

@@ -123,9 +123,9 @@ public:
 		std::string result = left->toString();
 		result += " U";
 		if (upperBound == std::numeric_limits<double>::infinity()) {
-			result = ">=" + std::to_string(lowerBound);
+			result += ">=" + std::to_string(lowerBound);
 		} else {
-			result = "[";
+			result += "[";
 			result += std::to_string(lowerBound);
 			result += ",";
 			result += std::to_string(upperBound);

src/formula/Prctl/BoundedNaryUntil.h

@@ -143,7 +143,7 @@ public:
 		std::stringstream result;
 		result << "( " << left->toString();
 		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
-			result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString();
+			result << " U(" << std::get<1>(*it) << "," << std::get<2>(*it) << ") " << std::get<0>(*it)->toString();
 		}
 		result << ")";
 		return result.str();

src/formula/Prctl/PrctlFilter.h

@@ -13,7 +13,6 @@
 #include "src/formula/Prctl/AbstractPathFormula.h"
 #include "src/formula/Prctl/AbstractStateFormula.h"
 #include "src/modelchecker/prctl/AbstractModelChecker.h"
-#include "src/formula/Actions/MinMaxAction.h"
 
 namespace storm {
 namespace property {
@@ -24,23 +23,19 @@ class PrctlFilter : public storm::property::AbstractFilter<T> {
 
 public:
 
-	PrctlFilter() : child(nullptr) {
+	PrctlFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr) {
 		// Intentionally left empty.
 	}
 
-	PrctlFilter(AbstractPrctlFormula<T>* child) : child(child) {
+	PrctlFilter(AbstractPrctlFormula<T>* child, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(opt), child(child) {
 		// Intentionally left empty.
 	}
 
-	PrctlFilter(AbstractPrctlFormula<T>* child, bool minimize) : child(child) {
-		this->actions.push_back(new storm::property::action::MinMaxAction<T>(minimize));
-	}
-
-	PrctlFilter(AbstractPrctlFormula<T>* child, action::AbstractAction<T>* action) : child(child) {
-		this->actions.push_back(action);
+	PrctlFilter(AbstractPrctlFormula<T>* child, action::AbstractAction<T>* action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) {
+		// Intentionally left empty.
 	}
 
-	PrctlFilter(AbstractPrctlFormula<T>* child, std::vector<action::AbstractAction<T>*> actions) : AbstractFilter<T>(actions), child(child) {
+	PrctlFilter(AbstractPrctlFormula<T>* child, std::vector<action::AbstractAction<T>*> actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) {
 		// Intentionally left empty.
 	}
 
@@ -53,8 +48,8 @@ public:
 
 		// Write out the formula to be checked.
 		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toFormulaString());
-		std::cout << "Model checking formula:\t" << this->toFormulaString() << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
+		std::cout << "Model checking formula:\t" << this->toString() << std::endl;
 
 		// Do a dynamic cast to test for the actual formula type and call the correct evaluation function.
 		if(dynamic_cast<AbstractStateFormula<T>*>(child) != nullptr) {
@@ -177,12 +172,94 @@ public:
 		return true;
 	}
 
-	std::string toFormulaString() const {
-		std::string desc = "filter(";
+	virtual std::string toString() const override {
+		std::string desc = "";
+
+		if(dynamic_cast<AbstractStateFormula<T>*>(child) == nullptr) {
+
+			// The formula is not a state formula so we either have a probability query or a reward query.
+			if(this->actions.empty()){
+
+				// There is exactly one action in the list, the minmax action. Again, we do legacy support-
+
+				if(dynamic_cast<AbstractPathFormula<T>*>(child) != nullptr) {
+					// It is a probability query.
+					desc += "P ";
+
+				} else {
+					// It is a reward query.
+					desc += "R ";
+				}
+
+				switch(this->opt) {
+					case MINIMIZE:
+						desc += "min ";
+						break;
+					case MAXIMIZE:
+						desc += "max ";
+						break;
+					default:
+						break;
+				}
+
+				desc += "= ? ";
+
+			} else {
+				desc = "filter[";
+
+				switch(this->opt) {
+					case MINIMIZE:
+						desc += " min, ";
+						break;
+					case MAXIMIZE:
+						desc += " max, ";
+						break;
+					default:
+						break;
+				}
+
+				for(auto action : this->actions) {
+					desc += action->toString();
+					desc += ", ";
+				}
+
+				// Remove the last ", ".
+				desc.pop_back();
+				desc.pop_back();
+
+				desc += "]";
+			}
+
+		} else {
+
+			if(this->actions.empty()) {
+
+				// There are no filter actions but only the raw state formula. So just print that.
+				return child->toString();
+			}
+
+			desc = "filter[";
+
+			for(auto action : this->actions) {
+				desc += action->toString();
+				desc += ", ";
+			}
+
+			// Remove the last ", ".
+			desc.pop_back();
+			desc.pop_back();
+
+			desc += "]";
+		}
+
+		desc += "(";
+		desc += child->toString();
+		desc += ")";
+
 		return desc;
 	}
 
-	std::string toString() const {
+	virtual std::string toPrettyString() const override{
 		std::string desc = "Filter: ";
 		desc += "\nActions:";
 		for(auto action : this->actions) {
@@ -206,9 +283,9 @@ private:
 		// First, get the model checking result.
 		storm::storage::BitVector result;
 
-		if(this->getActionCount() != 0 &&  dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
-			// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-			result = modelchecker.checkMinMaxOperator(*formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
+		if(this->opt != UNDEFINED) {
+			// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
+			result = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
 		} else {
 			result = formula->check(modelchecker);
 		}
@@ -225,9 +302,9 @@ private:
 		// First, get the model checking result.
 		std::vector<T> result;
 
-		if(this->getActionCount() != 0 &&  dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
-			// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-			result = modelchecker.checkMinMaxOperator(*formula, dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
+		if(this->opt != UNDEFINED) {
+			// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
+			result = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
 		} else {
 			result = formula->check(modelchecker, false);
 		}
@@ -243,9 +320,9 @@ private:
 		// First, get the model checking result.
 		std::vector<T> result;
 
-		if(this->getActionCount() != 0 &&  dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
-			// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-			result = modelchecker.checkMinMaxOperator(*formula, dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
+		if(this->opt != UNDEFINED) {
+			// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
+			result = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
 		} else {
 			result = formula->check(modelchecker, false);
 		}

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -139,9 +139,9 @@ public:
 		}
 		result += " ";
 		result += std::to_string(bound);
-		result += " [";
+		result += " (";
 		result += pathFormula->toString();
-		result += "]";
+		result += ")";
 		return result;
 	}
 

src/formula/Prctl/RewardBoundOperator.h

@@ -137,9 +137,9 @@ public:
 		}
 		result += " ";
 		result += std::to_string(bound);
-		result += " [";
+		result += " (";
 		result += pathFormula->toString();
-		result += "]";
+		result += ")";
 		return result;
 	}
 

src/modelchecker/prctl/AbstractModelChecker.h

@@ -233,11 +233,11 @@ public:
 	 * Checks the given formula and determines whether minimum or maximum probabilities are to be computed for the formula.
 	 *
 	 * @param formula The formula to check.
-	 * @param minimumOperator True iff minimum probabilities are to be computed.
+	 * @param optOperator True iff minimum probabilities are to be computed.
 	 * @returns The probabilities to satisfy the formula, represented by a vector.
 	 */
-	virtual std::vector<Type> checkMinMaxOperator(storm::property::prctl::AbstractPathFormula<Type> const & formula, bool minimumOperator) const {
-		minimumOperatorStack.push(minimumOperator);
+	virtual std::vector<Type> checkOptimizingOperator(storm::property::prctl::AbstractPathFormula<Type> const & formula, bool optOperator) const {
+		minimumOperatorStack.push(optOperator);
 		std::vector<Type> result = formula.check(*this, false);
 		minimumOperatorStack.pop();
 		return result;
@@ -247,11 +247,11 @@ public:
 	 * Checks the given formula and determines whether minimum or maximum rewards are to be computed for the formula.
 	 *
 	 * @param formula The formula to check.
-	 * @param minimumOperator True iff minimum rewards are to be computed.
+	 * @param optOperator True iff minimum rewards are to be computed.
 	 * @returns The the rewards accumulated by the formula, represented by a vector.
 	 */
-	virtual std::vector<Type> checkMinMaxOperator(storm::property::prctl::AbstractRewardPathFormula<Type> const & formula, bool minimumOperator) const {
-		minimumOperatorStack.push(minimumOperator);
+	virtual std::vector<Type> checkOptimizingOperator(storm::property::prctl::AbstractRewardPathFormula<Type> const & formula, bool optOperator) const {
+		minimumOperatorStack.push(optOperator);
 		std::vector<Type> result = formula.check(*this, false);
 		minimumOperatorStack.pop();
 		return result;
@@ -261,11 +261,11 @@ public:
 	 * Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula.
 	 *
 	 * @param formula The formula to check.
-	 * @param minimumOperator True iff minimum probabilities/rewards are to be computed.
+	 * @param optOperator True iff minimum probabilities/rewards are to be computed.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	virtual storm::storage::BitVector checkMinMaxOperator(storm::property::prctl::AbstractStateFormula<Type> const & formula, bool minimumOperator) const {
-		minimumOperatorStack.push(minimumOperator);
+	virtual storm::storage::BitVector checkOptimizingOperator(storm::property::prctl::AbstractStateFormula<Type> const & formula, bool optOperator) const {
+		minimumOperatorStack.push(optOperator);
 		storm::storage::BitVector result = formula.check(*this);
 		minimumOperatorStack.pop();
 		return result;

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -488,10 +488,10 @@ public:
 	 *       should be computed for the formula makes no sense in the context of a deterministic model.
 	 *
 	 * @param formula The formula to check.
-	 * @param minimumOperator True iff minimum probabilities/rewards are to be computed.
+	 * @param optOperator True iff minimum probabilities/rewards are to be computed.
 	 * @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector.
 	 */
-	virtual std::vector<Type> checkMinMaxOperator(storm::property::prctl::AbstractPathFormula<Type> const & formula, bool minimumOperator) const override {
+	virtual std::vector<Type> checkOptimizingOperator(storm::property::prctl::AbstractPathFormula<Type> const & formula, bool optOperator) const override {
 
 		LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
 
@@ -506,10 +506,10 @@ public:
 	 *       should be computed for the formula makes no sense in the context of a deterministic model.
 	 *
 	 * @param formula The formula to check.
-	 * @param minimumOperator True iff minimum probabilities/rewards are to be computed.
+	 * @param optOperator True iff minimum probabilities/rewards are to be computed.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	virtual storm::storage::BitVector checkMinMaxOperator(storm::property::prctl::AbstractStateFormula<Type> const & formula, bool minimumOperator) const override {
+	virtual storm::storage::BitVector checkOptimizingOperator(storm::property::prctl::AbstractStateFormula<Type> const & formula, bool optOperator) const override {
 
 		LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
 

src/parser/CslParser.cpp

@@ -11,7 +11,6 @@
 
 // The action class headers.
 #include "src/formula/Actions/AbstractAction.h"
-#include "src/formula/Actions/MinMaxAction.h"
 #include "src/formula/Actions/RangeAction.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
@@ -38,7 +37,6 @@ typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIte
 namespace qi = boost::spirit::qi;
 namespace phoenix = boost::phoenix;
 
-
 namespace storm {
 namespace parser {
 
@@ -60,31 +58,31 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 		stateFormula.name("state formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Or<double>>(qi::_val, qi::_1)];
-		orFormula.name("state formula");
+		orFormula.name("or formula");
 		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::And<double>>(qi::_val, qi::_1)];
-		andFormula.name("state formula");
+		andFormula.name("and formula");
 		notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Not<double>>(qi::_1)];
-		notFormula.name("state formula");
+		notFormula.name("not 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");
+		atomicStateFormula.name("atomic state formula");
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::property::csl::Ap<double>>(qi::_1)];
-		atomicProposition.name("state formula");
+		atomicProposition.name("atomic proposition");
 		probabilisticBoundOperator = (
 				(qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::property::csl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]
 				);
-		probabilisticBoundOperator.name("state formula");
+		probabilisticBoundOperator.name("probabilistic bound operator");
 		steadyStateBoundOperator = (
 				(qi::lit("S") >> comparisonType > qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
 										phoenix::new_<storm::property::csl::SteadyStateBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]
 				);
-		steadyStateBoundOperator.name("state formula");
+		steadyStateBoundOperator.name("steady state bound operator");
 
 		//This block defines rules for parsing probabilistic path formulas
 		pathFormula = (timeBoundedEventually | eventually | globally | next | timeBoundedUntil | until);
@@ -97,16 +95,16 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 				(qi::lit("F") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)[qi::_val =
 								phoenix::new_<storm::property::csl::TimeBoundedEventually<double>>(qi::_1, std::numeric_limits<double>::infinity(), qi::_2)]
 				);
-		timeBoundedEventually.name("path formula (for probabilistic operator)");
+		timeBoundedEventually.name("time bounded eventually");
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Eventually<double> >(qi::_1)];
-		eventually.name("path formula (for probabilistic operator)");
+		eventually.name("eventually");
 		next = (qi::lit("X") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Next<double> >(qi::_1)];
-		next.name("path formula (for probabilistic operator)");
+		next.name("next");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Globally<double> >(qi::_1)];
-		globally.name("path formula (for probabilistic operator)");
+		globally.name("globally");
 		timeBoundedUntil = (
 					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]")  > stateFormula)
 					[qi::_val = phoenix::new_<storm::property::csl::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::property::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)] |
@@ -115,10 +113,10 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 					(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_  > stateFormula)
 					[qi::_val = phoenix::new_<storm::property::csl::TimeBoundedUntil<double>>(qi::_2, std::numeric_limits<double>::infinity(), phoenix::bind(&storm::property::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)]
 				);
-		timeBoundedUntil.name("path formula (for probabilistic operator)");
+		timeBoundedUntil.name("time bounded until");
 		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Until<double>>(phoenix::bind(&storm::property::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
-		until.name("path formula (for probabilistic operator)");
+		until.name("until formula");
 
 		formula = (pathFormula | stateFormula);
 		formula.name("CSL formula");
@@ -128,40 +126,35 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 		noBoundOperator.name("no bound operator");
 		probabilisticNoBoundOperator =
 				(qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1, true)];
+						phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1, storm::property::MINIMIZE)] |
 				(qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1, false)];
+						phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1, storm::property::MAXIMIZE)] |
 				(qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1)];
-		probabilisticNoBoundOperator.name("no bound operator");
+		probabilisticNoBoundOperator.name("probabilistic no bound operator");
 		steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> stateFormula >> qi::lit("]"))[qi::_val =
-				phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1)];
-		steadyStateNoBoundOperator.name("no bound operator");
-
-		minMaxAction = qi::lit("minmax") >> qi::lit(",") >> (
-				qi::lit("min")[qi::_val =
-						phoenix::new_<storm::property::action::MinMaxAction<double>>(true)] |
-				qi::lit("min")[qi::_val =
-						phoenix::new_<storm::property::action::MinMaxAction<double>>(false)]);
-		minMaxAction.name("minmax action for the formula filter");
+				phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1, storm::property::UNDEFINED, true)];
+		steadyStateNoBoundOperator.name("steady state no bound operator");
 
 		rangeAction = (qi::lit("range") >> qi::lit(",") >> qi::uint_ >> qi::lit(",") >> qi::uint_)[qi::_val =
 				phoenix::new_<storm::property::action::RangeAction<double>>(qi::_1, qi::_2)];
 		rangeAction.name("range action for the formula filter");
 
-		abstractAction = (rangeAction | minMaxAction) >> (qi::eps | qi::lit(","));
+		abstractAction = (rangeAction) >> (qi::eps | qi::lit(","));
 		abstractAction.name("filter action");
 
 		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
 					phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_2, qi::_1)] |
-				 (formula)[qi::_val =
-					phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1)] |
 				 (noBoundOperator)[qi::_val =
-					qi::_1];
-		filter.name("PRCTL formula filter");
+					qi::_1] |
+				 (formula)[qi::_val =
+					phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1)];
+
+		filter.name("CSL formula filter");
 
 		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment ) > qi::eoi;
-		start.name("CSL formula filter");
+		start.name("CSL formula filter start");
+
 	}
 
 	qi::rule<Iterator, storm::property::csl::CslFilter<double>*(), Skipper> start;
@@ -173,7 +166,6 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 
 	qi::rule<Iterator, storm::property::action::AbstractAction<double>*(), Skipper> abstractAction;
 	qi::rule<Iterator, storm::property::action::RangeAction<double>*(), Skipper> rangeAction;
-	qi::rule<Iterator, storm::property::action::MinMaxAction<double>*(), Skipper> minMaxAction;
 
 	qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> formula;
 	qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> comment;

src/parser/PrctlParser.cpp

@@ -4,7 +4,6 @@
 
 // The action class headers.
 #include "src/formula/Actions/AbstractAction.h"
-#include "src/formula/Actions/MinMaxAction.h"
 #include "src/formula/Actions/RangeAction.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
@@ -54,31 +53,31 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		stateFormula.name("state formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::Or<double>>(qi::_val, qi::_1)];
-		orFormula.name("state formula");
+		orFormula.name("or formula");
 		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::And<double>>(qi::_val, qi::_1)];
-		andFormula.name("state formula");
+		andFormula.name("and formula");
 		notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::Not<double>>(qi::_1)];
-		notFormula.name("state formula");
+		notFormula.name("not formula");
 
 		//This block defines rules for "atomic" state formulas
 		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
-		atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")");
-		atomicStateFormula.name("state formula");
+		atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")") | qi::lit("[") >> stateFormula >> qi::lit("]");
+		atomicStateFormula.name("atomic state formula");
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::property::prctl::Ap<double>>(qi::_1)];
-		atomicProposition.name("state formula");
+		atomicProposition.name("atomic proposition");
 		probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
 				phoenix::new_<storm::property::prctl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]);
 
-		probabilisticBoundOperator.name("state formula");
+		probabilisticBoundOperator.name("probabilistic bound operator");
 		rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val =
 				phoenix::new_<storm::property::prctl::RewardBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]);
-		rewardBoundOperator.name("state formula");
+		rewardBoundOperator.name("reward bound operator");
 
 		//This block defines rules for parsing probabilistic path formulas
-		pathFormula = (boundedEventually | eventually | next | globally | boundedUntil | until);
+		pathFormula = (boundedEventually | eventually | next | globally | boundedUntil | until | qi::lit("(") >> pathFormula >> qi::lit(")") | qi::lit("[") >> pathFormula >> qi::lit("]"));
 		pathFormula.name("path formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::BoundedEventually<double>>(qi::_2, qi::_1)];
@@ -100,7 +99,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		until.name("path formula (for probabilistic operator)");
 
 		//This block defines rules for parsing reward path formulas
-		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward);
+		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward | qi::lit("(") >> rewardPathFormula >> qi::lit(")") | qi::lit("[") >> rewardPathFormula >> qi::lit("]"));
 		rewardPathFormula.name("path formula (for reward operator)");
 		cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)[qi::_val =
 				phoenix::new_<storm::property::prctl::CumulativeReward<double>>(qi::_1)];
@@ -122,50 +121,44 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator);
 		noBoundOperator.name("no bound operator");
 		probabilisticNoBoundOperator = (
-				(qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, true)] |
-				(qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, false)] |
-				(qi::lit("P") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+				(qi::lit("P") >> qi::lit("min") >> qi::lit("=") > qi::lit("?") >> pathFormula )[qi::_val =
+						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, storm::property::MINIMIZE)] |
+				(qi::lit("P") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> pathFormula )[qi::_val =
+						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, storm::property::MAXIMIZE)] |
+				(qi::lit("P") >> qi::lit("=") > qi::lit("?") >> pathFormula )[qi::_val =
 						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1)]
 				);
 		probabilisticNoBoundOperator.name("no bound operator");
 
 		rewardNoBoundOperator = (
-				(qi::lit("R") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, true)] |
-				(qi::lit("R") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, false)] |
-				(qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
+				(qi::lit("R") >> qi::lit("min") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val =
+						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, storm::property::MINIMIZE)] |
+				(qi::lit("R") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val =
+						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1, storm::property::MAXIMIZE)] |
+				(qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> rewardPathFormula )[qi::_val =
 						phoenix::new_<storm::property::prctl::PrctlFilter<double> >(qi::_1)]
 
 				);
 		rewardNoBoundOperator.name("no bound operator");
 
-		minMaxAction = qi::lit("minmax") >> qi::lit(",") >> (
-				qi::lit("min")[qi::_val =
-						phoenix::new_<storm::property::action::MinMaxAction<double>>(true)] |
-				qi::lit("min")[qi::_val =
-						phoenix::new_<storm::property::action::MinMaxAction<double>>(false)]);
-		minMaxAction.name("minmax action for the formula filter");
-
 		rangeAction = (qi::lit("range") >> qi::lit(",") >> qi::uint_ >> qi::lit(",") >> qi::uint_)[qi::_val =
 				phoenix::new_<storm::property::action::RangeAction<double>>(qi::_1, qi::_2)];
 		rangeAction.name("range action for the formula filter");
 
-		abstractAction = (rangeAction | minMaxAction) >> (qi::eps | qi::lit(","));
+		abstractAction = (rangeAction) >> (qi::eps | qi::lit(","));
 		abstractAction.name("filter action");
 
-		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
+		filter = (qi::lit("filter") > qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
 					phoenix::new_<storm::property::prctl::PrctlFilter<double>>(qi::_2, qi::_1)] |
-				 (formula)[qi::_val =
-					phoenix::new_<storm::property::prctl::PrctlFilter<double>>(qi::_1)] |
 				 (noBoundOperator)[qi::_val =
-					qi::_1];
+					qi::_1] |
+				 (formula)[qi::_val =
+					phoenix::new_<storm::property::prctl::PrctlFilter<double>>(qi::_1)];
 		filter.name("PRCTL formula filter");
 
 		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = nullptr]) > qi::eoi;
 		start.name("PRCTL formula filter");
+
 	}
 
 	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> start;
@@ -177,7 +170,6 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 
 	qi::rule<Iterator, storm::property::action::AbstractAction<double>*(), Skipper> abstractAction;
 	qi::rule<Iterator, storm::property::action::RangeAction<double>*(), Skipper> rangeAction;
-	qi::rule<Iterator, storm::property::action::MinMaxAction<double>*(), Skipper> minMaxAction;
 
 	qi::rule<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper> formula;
 	qi::rule<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper> comment;

test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@@ -22,11 +22,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
     
-	std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
     
 	ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -35,11 +35,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
 	apFormula = new storm::property::prctl::Ap<double>("three");
 	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, true);
     
 	ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -48,11 +48,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
 	apFormula = new storm::property::prctl::Ap<double>("four");
 	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, true);
     
 	ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
     
 	ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -61,11 +61,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
 	apFormula = new storm::property::prctl::Ap<double>("done");
 	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -82,11 +82,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
 	apFormula = new storm::property::prctl::Ap<double>("done");
 	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
     
 	ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -103,11 +103,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
 	apFormula = new storm::property::prctl::Ap<double>("done");
 	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
     
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
     
 	ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -130,11 +130,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
 
-	std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -143,11 +143,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
 
-	result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true);
+	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -156,11 +156,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 

test/functional/parser/CslParserTest.cpp

@@ -58,7 +58,7 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) {
 	ASSERT_EQ(0.5, op->getBound());
 
 	// Test the string representation for the parsed formula.
-	ASSERT_EQ("P > 0.500000 [F a]", formula->toString());
+	ASSERT_EQ("P > 0.500000 (F a)", formula->toString());
 
 	delete formula;
 }
@@ -78,7 +78,7 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
 	ASSERT_EQ(15.0, op->getBound());
 
 	// Test the string representation for the parsed formula.
-	ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", formula->toString());
+	ASSERT_EQ("S >= 15.000000 (P < 0.200000 (a U[0.000000,3.000000] b))", formula->toString());
 
 	delete formula;
 }
@@ -94,7 +94,7 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
 	ASSERT_NE(formula, nullptr);
 
 	// The input was parsed correctly.
-	ASSERT_EQ("S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]", formula->toString());
+	ASSERT_EQ("S = ? (P <= 0.500000 (F[0.000000,3.000000] a))", formula->toString());
 
 	delete formula;
 }
@@ -110,7 +110,7 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
 	ASSERT_NE(formula, nullptr);
 
 	// The input was parsed correctly.
-	ASSERT_EQ("P = ? [a U[3.000000,4.000000] (b & !c)]", formula->toString());
+	ASSERT_EQ("P = ? (a U[3.000000,4.000000] (b & !c))", formula->toString());
 
 	delete formula;
 }
@@ -127,7 +127,7 @@ TEST(CslParserTest, parseComplexFormulaTest) {
 	ASSERT_NE(formula, nullptr);
 
 	// The input was parsed correctly.
-	ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))", formula->toString());
+	ASSERT_EQ("(S <= 0.500000 (P <= 0.500000 (a U c)) & (P > 0.500000 (G b) | !P < 0.400000 (G P > 0.900000 (F>=7.000000 (a & b)))))", formula->toString());
 
 	delete formula;
 }

test/functional/parser/PrctlParserTest.cpp

@@ -63,7 +63,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 	ASSERT_EQ(0.5, op->getBound());
 
 	// Test the string representation for the parsed formula.
-	ASSERT_EQ("P > 0.500000 [F a]", formula->toString());
+	ASSERT_EQ("P > 0.500000 (F a)", formula->toString());
 
 	delete formula;
 
@@ -86,7 +86,7 @@ TEST(PrctlParserTest, parseRewardFormulaTest) {
 	ASSERT_EQ(15.0, op->getBound());
 
 	// Test the string representation for the parsed formula.
-	ASSERT_EQ("R >= 15.000000 [I=5]", formula->toString());
+	ASSERT_EQ("R >= 15.000000 (I=5)", formula->toString());
 
 	delete formula;
 }
@@ -102,7 +102,7 @@ TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
 	ASSERT_NE(formula, nullptr);
 
 	// The input was parsed correctly.
-	ASSERT_EQ("R = ? [F a]", formula->toString());
+	ASSERT_EQ("R = ? (F a)", formula->toString());
 
 	delete formula;
 }
@@ -118,7 +118,7 @@ TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
 	ASSERT_NE(formula, nullptr);
 
 	// The input was parsed correctly.
-	ASSERT_EQ("P = ? [a U<=4 (b & !c)]", formula->toString());
+	ASSERT_EQ("P = ? (a U<=4 (b & !c))", formula->toString());
 
 	delete formula;
 }
@@ -134,7 +134,7 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
 	ASSERT_NE(formula, nullptr);
 
 	// The input was parsed correctly.
-	ASSERT_EQ("(R <= 0.500000 [S] & (R > 15.000000 [C <= 0.500000] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", formula->toString());
+	ASSERT_EQ("(R <= 0.500000 (S) & (R > 15.000000 (C <= 0.500000) | !P < 0.400000 (G P > 0.900000 (F<=7 (a & b)))))", formula->toString());
 
 	delete formula;
 }

test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@@ -22,11 +22,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
 
-	std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -35,11 +35,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
 
-	result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true);
+	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -48,11 +48,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
 
 	ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
 	ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -78,7 +78,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
     
-	std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
     
 	ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
@@ -89,7 +89,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     storm::property::prctl::And<double>* andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
 	eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, true);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, true);
 
 	ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -100,7 +100,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
     eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
     
 	ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
@@ -112,7 +112,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     andFormula = new storm::property::prctl::And<double>(apFormula, notFormula);
     eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
     
-	result = mc.checkMinMaxOperator(*eventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
     
 	ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
@@ -121,11 +121,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     apFormula = new storm::property::prctl::Ap<double>("finished");
 	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
     
-	result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true);
+	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
     
 	ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
-	result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false);
+	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
 
 	ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
@@ -134,11 +134,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     apFormula = new storm::property::prctl::Ap<double>("finished");
 	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
     
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
     
 	ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
 
-	result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
+	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
 	ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());