Intruduced legacy support.

- Every PRCTL formula that worked before works now and behaves in the same way. One exception:
|- Formulas of the type Pmin<0.5[Phi] and Rmin<0.5[Psi] result in a parsing error, as the comparison operator already implies the scheduler to be used.
|  Also, the modelchecker now actually uses the comparison operator in order to choose the correct scheduler for MDPs.


Former-commit-id: d942d18e7e

src/formula/AbstractFilter.h

@@ -10,7 +10,7 @@
 
 #include <vector>
 #include "src/formula/AbstractFormula.h"
-#include "src/formula/Actions/Action.h"
+#include "src/formula/Actions/AbstractAction.h"
 
 namespace storm {
 namespace property {
@@ -24,11 +24,11 @@ public:
 		// Intentionally left empty.
 	}
 
-	AbstractFilter(action::Action<T>* action) {
+	AbstractFilter(action::AbstractAction<T>* action) {
 		actions.push_back(action);
 	}
 
-	AbstractFilter(std::vector<action::Action<T>*> actions) : actions(actions) {
+	AbstractFilter(std::vector<action::AbstractAction<T>*> actions) : actions(actions) {
 		// Intentionally left empty.
 	}
 
@@ -50,7 +50,7 @@ public:
 		return desc;
 	}
 
-	void addAction(action::Action<T>* action) {
+	void addAction(action::AbstractAction<T>* action) {
 		actions.push_back(action);
 	}
 
@@ -58,7 +58,7 @@ public:
 		actions.pop_back();
 	}
 
-	action::Action<T>* getAction(uint_fast64_t pos) const {
+	action::AbstractAction<T>* getAction(uint_fast64_t pos) const {
 		return actions[pos];
 	}
 
@@ -68,7 +68,7 @@ public:
 
 protected:
 
-	std::vector<action::Action<T>*> actions;
+	std::vector<action::AbstractAction<T>*> actions;
 };
 
 } //namespace property

src/formula/Actions/AbstractAction.h

@@ -38,7 +38,7 @@ public:
 	/*!
 	 *
 	 */
-	virtual storm::storage::BitVector<T> evaluate(storm::storage::BitVector<T> input) const {
+	virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const {
 		return input;
 	}
 

src/formula/Actions/MinMaxAction.h

@@ -15,7 +15,7 @@ namespace property {
 namespace action {
 
 template <class T>
-class MinMaxAction : AbstractAction<T> {
+class MinMaxAction : public AbstractAction<T> {
 
 public:
 

src/formula/Actions/RangeAction.h

@@ -10,12 +10,14 @@
 
 #include "src/formula/Actions/AbstractAction.h"
 
+#include <string>
+
 namespace storm {
 namespace property {
 namespace action {
 
 template <class T>
-class RangeAction : AbstractAction<T> {
+class RangeAction : public AbstractAction<T> {
 
 public:
 
@@ -49,8 +51,19 @@ public:
 	/*!
 	 *
 	 */
-	virtual storm::storage::BitVector<T> evaluate(storm::storage::BitVector<T> input) const override {
-		storm::storage::BitVector<T> out(to - from  + 1, input.begin() + from, input.begin() + to);
+	virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const override {
+		//Initialize the output vector.
+		storm::storage::BitVector out(to - from  + 1);
+
+		storm::storage::BitVector::const_iterator it = input.begin();
+
+		//Proceed the set index iterator to the first set bit within the range.
+		for(; *it < from; ++it);
+
+		//Fill the output vector.
+		for(; *it <= to; ++it) {
+			out.set(*it-from);
+		}
 		return out;
 	}
 
@@ -58,14 +71,22 @@ public:
 	 *
 	 */
 	virtual std::string toString() const override {
-		return "range, " + from + ", " + to;
+		std::string out = "range, ";
+		out += std::to_string(from);
+		out += ", ";
+		out += std::to_string(to);
+		return out;
 	}
 
 	/*!
 	 *
 	 */
 	virtual std::string toFormulaString() const override {
-		return "\"range\", " + from + ", " + to;
+		std::string out = "\"range\", ";
+		out += std::to_string(from);
+		out += ", ";
+		out += std::to_string(to);
+		return out;
 	}
 
 private:

src/formula/Prctl/PrctlFilter.h

@@ -12,13 +12,15 @@
 #include "src/formula/Prctl/AbstractPrctlFormula.h"
 #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 {
 namespace prctl {
 
 template <class T>
-class PrctlFilter : storm::property::AbstractFilter<T> {
+class PrctlFilter : public storm::property::AbstractFilter<T> {
 
 public:
 
@@ -26,24 +28,28 @@ public:
 		// Intentionally left empty.
 	}
 
-	PrctlFilter(AbstractPrctlFormula* child) : child(child) {
+	PrctlFilter(AbstractPrctlFormula<T>* child) : child(child) {
 		// Intentionally left empty.
 	}
 
-	PrctlFilter(AbstractPrctlFormula* child, action::Action<T>* action) : child(child) {
-		actions.push_back(action);
+	PrctlFilter(AbstractPrctlFormula<T>* child, bool minimize) : child(child) {
+		this->actions.push_back(new storm::property::action::MinMaxAction<T>(minimize));
 	}
 
-	PrctlFilter(AbstractPrctlFormula* child, std::vector<action::Action<T>*> actions) : child(child), actions(actions) {
+	PrctlFilter(AbstractPrctlFormula<T>* child, action::AbstractAction<T>* action) : child(child) {
+		this->actions.push_back(action);
+	}
+
+	PrctlFilter(AbstractPrctlFormula<T>* child, std::vector<action::AbstractAction<T>*> actions) : AbstractFilter<T>(actions), child(child) {
 		// Intentionally left empty.
 	}
 
 	virtual ~PrctlFilter() {
-		actions.clear();
+		this->actions.clear();
 		delete child;
 	}
 
-	void check(AbstractModelChecker const & modelchecker) const {
+	void check(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
 
 		// Write out the formula to be checked.
 		std::cout << std::endl;
@@ -68,13 +74,13 @@ public:
 
 			// Now write out the result.
 
-			if(actions.empty()) {
+			if(this->actions.empty()) {
 
 				// There is no filter action given. So provide legacy support:
 				// Return the results for all states labeled with "init".
 				LOG4CPLUS_INFO(logger, "Result for initial states:");
 				std::cout << "Result for initial states:" << std::endl;
-				for (auto initialState : modelchecker.getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
+				for (auto initialState : modelchecker.getModel().getInitialStates()) {
 					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
 					std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
 				}
@@ -100,13 +106,13 @@ public:
 
 			// Now write out the result.
 
-			if(actions.empty()) {
+			if(this->actions.empty()) {
 
 				// There is no filter action given. So provide legacy support:
 				// Return the results for all states labeled with "init".
 				LOG4CPLUS_INFO(logger, "Result for initial states:");
 				std::cout << "Result for initial states:" << std::endl;
-				for (auto initialState : modelchecker.getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
+				for (auto initialState : modelchecker.getModel().getInitialStates()) {
 					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
 					std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
 				}
@@ -147,61 +153,61 @@ public:
 	std::string toString() const {
 		std::string desc = "Filter: ";
 		desc += "\nActions:";
-		for(auto action : actions) {
-			desc += "\n\t" + action.toString();
+		for(auto action : this->actions) {
+			desc += "\n\t" + action->toString();
 		}
 		desc += "\nFormula:\n\t" + child->toString();
 		return desc;
 	}
 
-	void setChild(AbstractPrctlFormula* child) {
+	void setChild(AbstractPrctlFormula<T>* child) {
 		this->child = child;
 	}
 
-	AbstractFormula* getChild() const {
+	AbstractPrctlFormula<T>* getChild() const {
 		return child;
 	}
 
 private:
 
-	BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractStateFormula<T>* formula) const {
+	storm::storage::BitVector evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractStateFormula<T>* formula) const {
 		// First, get the model checking result.
-		BitVector result = modelchecker.checkMinMaxOperator(formula);
+		storm::storage::BitVector result;
 
-		if(getActionCount() != 0 &&  dynamic_cast<MinMaxAction<T>*>(getAction(0)) != nullptr) {
+		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<MinMaxAction<T>*>(getAction(0))->getMinimize());
+			result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
 		} else {
 			result = formula->check(modelchecker);
 		}
 
 
 		// Now apply all filter actions and return the result.
-		for(auto action : actions) {
+		for(auto action : this->actions) {
 			result = action->evaluate(result);
 		}
 		return result;
 	}
 
-	std::vector<T> evaluate(AbstractModelChecker const & modelchecker, AbstractPathFormula<T>* formula) const {
+	std::vector<T> evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractPathFormula<T>* formula) const {
 		// First, get the model checking result.
 		std::vector<T> result;
 
-		if(getActionCount() != 0 &&  dynamic_cast<MinMaxAction<T>*>(getAction(0)) != nullptr) {
+		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<MinMaxAction<T>*>(getAction(0))->getMinimize());
+			result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
 		} else {
 			result = formula->check(modelchecker, false);
 		}
 
 		// Now apply all filter actions and return the result.
-		for(auto action : actions) {
+		for(auto action : this->actions) {
 			result = action->evaluate(result);
 		}
 		return result;
 	}
 
-	AbstractPrctlFormula* child;
+	AbstractPrctlFormula<T>* child;
 };
 
 } //namespace prctl

src/modelchecker/prctl/AbstractModelChecker.h

@@ -187,7 +187,7 @@ public:
 	 * @param formula The formula to check.
 	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
+	virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::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);
 
@@ -211,7 +211,7 @@ public:
 	 * @param formula The formula to check.
 	 * @return The set of states satisfying the formula represented by a bit vector.
 	 */
-	storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const {
+	virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::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/prctl/SparseMdpPrctlModelChecker.h

@@ -69,6 +69,80 @@ namespace storm {
                     return AbstractModelChecker<Type>::template getModel<storm::models::Mdp<Type>>();
                 }
 
+            	/*!
+            	 * Checks the given formula that is a P operator over a path formula featuring a value bound.
+            	 *
+            	 * @param formula The formula to check.
+            	 * @return The set of states satisfying the formula represented by a bit vector.
+            	 */
+            	virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const override {
+
+            		// For P< and P<= the MDP satisfies the formula iff the probability maximizing scheduler is used.
+            		// For P> and P>=                "              iff the probability minimizing         "        .
+					if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) {
+						this->minimumOperatorStack.push(false);
+					}
+					else {
+						this->minimumOperatorStack.push(true);
+					}
+
+            		// First, we need to compute the probability for satisfying the path formula for each state.
+            		std::vector<Type> quantitativeResult = formula.getPathFormula().check(*this, false);
+
+            		//Remove the minimizing operator entry from the stack.
+            		this->minimumOperatorStack.pop();
+
+            		// Create resulting bit vector that will hold the yes/no-answer for every state.
+            		storm::storage::BitVector result(quantitativeResult.size());
+
+            		// Now, we can compute which states meet the bound specified in this operator and set the
+            		// corresponding bits to true in the resulting vector.
+            		for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
+            			if (formula.meetsBound(quantitativeResult[i])) {
+            				result.set(i, true);
+            			}
+            		}
+
+            		return result;
+            	}
+
+            	/*!
+            	 * Checks the given formula that is an R operator over a reward formula featuring a value bound.
+            	 *
+            	 * @param formula The formula to check.
+            	 * @return The set of states satisfying the formula represented by a bit vector.
+            	 */
+            	virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const override {
+
+            		// For R< and R<= the MDP satisfies the formula iff the reward maximizing scheduler is used.
+					// For R> and R>=                "              iff the reward minimizing         "        .
+					if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) {
+						this->minimumOperatorStack.push(false);
+					}
+					else {
+						this->minimumOperatorStack.push(true);
+					}
+
+            		// First, we need to compute the probability for satisfying the path formula for each state.
+            		std::vector<Type> quantitativeResult = formula.getPathFormula().check(*this, false);
+
+            		//Remove the minimizing operator entry from the stack.
+					this->minimumOperatorStack.pop();
+
+            		// Create resulting bit vector that will hold the yes/no-answer for every state.
+            		storm::storage::BitVector result(quantitativeResult.size());
+
+            		// Now, we can compute which states meet the bound specified in this operator and set the
+            		// corresponding bits to true in the resulting vector.
+            		for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
+            			if (formula.meetsBound(quantitativeResult[i])) {
+            				result.set(i, true);
+            			}
+            		}
+
+            		return result;
+            	}
+
                 /*!
                  * Computes the probability to satisfy phi until psi within a limited number of steps for each state.
                  *

src/parser/PrctlFileParser.cpp

@@ -14,7 +14,7 @@
 namespace storm {
 namespace parser {
 
-std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser(std::string filename) {
+std::list<storm::property::prctl::PrctlFilter<double>*> PrctlFileParser(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream;
 	inputFileStream.open(filename, std::ios::in);
@@ -24,7 +24,7 @@ std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser
 		throw storm::exceptions::FileIoException() << message << filename;
 	}
 
-	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> result;
+	std::list<storm::property::prctl::PrctlFilter<double>*> result;
 
 	std::string line;
 	//The while loop reads the input file line by line

src/parser/PrctlFileParser.h

@@ -9,6 +9,7 @@
 #define STORM_PARSER_PRCTLFILEPARSER_H_
 
 #include "formula/Prctl.h"
+#include "src/formula/Prctl/PrctlFilter.h"
 
 #include <list>
 
@@ -21,7 +22,7 @@ namespace parser {
  * @param filename
  * @return The list of parsed formulas
  */
-std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser(std::string filename);
+std::list<storm::property::prctl::PrctlFilter<double>*> PrctlFileParser(std::string filename);
 
 } /* namespace parser */
 } /* namespace storm */

src/parser/PrctlParser.cpp

@@ -2,7 +2,7 @@
 #include "src/utility/OsDetection.h"
 #include "src/utility/constants.h"
 
-// The action class header.
+// The action class headers.
 #include "src/formula/Actions/AbstractAction.h"
 #include "src/formula/Actions/MinMaxAction.h"
 #include "src/formula/Actions/RangeAction.h"
@@ -70,24 +70,12 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::property::prctl::Ap<double>>(qi::_1)];
 		atomicProposition.name("state formula");
-		probabilisticBoundOperator = (
-				(qi::lit("P") >> qi::lit("min") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3, true)] |
-				(qi::lit("P") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3, false)] |
-				(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 = ((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");
-		rewardBoundOperator = (
-				(qi::lit("R") >> qi::lit("min") > comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::RewardBoundOperator<double> >(qi::_1, qi::_2, qi::_3, true)] |
-				(qi::lit("R") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::property::prctl::RewardBoundOperator<double> >(qi::_1, qi::_2, qi::_3, false)] |
-				(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 = ((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");
 
 		//This block defines rules for parsing probabilistic path formulas
@@ -115,31 +103,66 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		//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::property::prctl::CumulativeReward<double>>(qi::_1)];
+		cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)[qi::_val =
+				phoenix::new_<storm::property::prctl::CumulativeReward<double>>(qi::_1)];
 		cumulativeReward.name("path formula (for reward operator)");
 		reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::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::property::prctl::InstantaneousReward<double>>(qi::_1)];
+		instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_)[qi::_val =
+				phoenix::new_<storm::property::prctl::InstantaneousReward<double>>(qi::_1)];
 		instantaneousReward.name("path formula (for reward operator)");
 		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()];
 
 		formula = (pathFormula | stateFormula);
 		formula.name("PRCTL formula");
 
-		minMaxAction = qi::lit("minmax") >> qi::lit(",") >> (qi::lit("min")[qi::_val = phoenix::new_<storm::property::action::MinMaxAction<double>>(true)] | qi::lit("min")[qi::_val = storm::property::action::MinMaxAction<double>(false)]);
+		//This block defines rules for parsing formulas with noBoundOperators
+		//Note that this is purely for legacy support.
+		//NoBoundOperators are no longer part of the formula tree and are therefore deprecated.
+		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 =
+						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 =
+						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 = (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.name("filter action");
 
-		filter = ((qi::eps | qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]")) >> (formula | (qi::lit("(") >> formula >> qi::lit(")"))))
-				[qi::_val = phoenix::new_<storm::property::prctl::PrctlFilter<double>>(qi::_2, qi::_1)];
+		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];
 		filter.name("PRCTL formula filter");
 
 		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment) > qi::eoi;
@@ -149,6 +172,10 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> start;
 	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> filter;
 
+	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> noBoundOperator;
+	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> probabilisticNoBoundOperator;
+	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> rewardNoBoundOperator;
+
 	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;
@@ -198,7 +225,7 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
 
 
 	// Prepare resulting intermediate representation of input.
-	storm::property::prctl::AbstractPrctlFormula<double>* result_pointer = nullptr;
+	storm::property::prctl::PrctlFilter<double>* result_pointer = nullptr;
 
 	PrctlGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> grammar;
 

src/parser/PrctlParser.h

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