From 895c2b6aad874c9c205d4f7474c22d75b8ac0992 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Mon, 8 Apr 2013 12:21:47 +0200
Subject: [PATCH] Convenient file parser for PRCTL, and correct reward formula
 parsing (together with some necessary code for that)

---
 src/formula/AbstractFormulaChecker.h     |  10 ++-
 src/formula/CumulativeReward.h           |  11 ++-
 src/formula/Formulas.h                   |   3 +
 src/formula/SteadyStateReward.h          | 106 +++++++++++++++++++++++
 src/modelchecker/AbstractModelChecker.h  |  11 +--
 src/modelchecker/DtmcPrctlModelChecker.h |  88 -------------------
 src/parser/PrctlFileParser.cpp           |  71 ++++++++++++---
 src/parser/PrctlFileParser.h             |  38 ++++++--
 src/parser/PrctlParser.cpp               |  31 +++++--
 test/parser/PrctlParserTest.cpp          |  16 ++--
 10 files changed, 251 insertions(+), 134 deletions(-)
 create mode 100644 src/formula/SteadyStateReward.h

diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index 6e74c48a4..c7801e0e2 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -38,6 +38,14 @@ namespace formula {
 template <class T>
 class AbstractFormulaChecker {
 	public:
+		/*!
+		 * Virtual destructor
+		 * To ensure that the right destructor is called
+		 */
+		virtual ~AbstractFormulaChecker() {
+			//intentionally left empty
+		}
+
 		/*!
 		 *	@brief Checks if the given formula is valid in some logic.
 		 *
@@ -53,4 +61,4 @@ class AbstractFormulaChecker {
 } // namespace formula
 } // namespace storm
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index 6275621db..3c38991a8 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -11,7 +11,6 @@
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "boost/integer/integer_mask.hpp"
 #include <string>
 
 namespace storm {
@@ -64,7 +63,7 @@ public:
 	 *
 	 * @param bound The time bound of the reward formula
 	 */
-	CumulativeReward(uint_fast64_t bound) {
+	CumulativeReward(T bound) {
 		this->bound = bound;
 	}
 
@@ -78,7 +77,7 @@ public:
 	/*!
 	 * @returns the time instance for the instantaneous reward operator
 	 */
-	uint_fast64_t getBound() const {
+	T getBound() const {
 		return bound;
 	}
 
@@ -87,7 +86,7 @@ public:
 	 *
 	 * @param bound the new bound.
 	 */
-	void setBound(uint_fast64_t bound) {
+	void setBound(T bound) {
 		this->bound = bound;
 	}
 
@@ -95,7 +94,7 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "C<=";
+		std::string result = "C <= ";
 		result += std::to_string(bound);
 		return result;
 	}
@@ -138,7 +137,7 @@ public:
 	}
 
 private:
-	uint_fast64_t bound;
+	T bound;
 };
 
 } //namespace formula
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 193114cb1..e5864bbc0 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -19,6 +19,7 @@
 #include "Or.h"
 #include "ProbabilisticNoBoundOperator.h"
 #include "ProbabilisticBoundOperator.h"
+
 #include "Until.h"
 #include "Eventually.h"
 #include "Globally.h"
@@ -29,6 +30,8 @@
 #include "ReachabilityReward.h"
 #include "RewardBoundOperator.h"
 #include "RewardNoBoundOperator.h"
+#include "SteadyStateReward.h"
+
 #include "SteadyStateOperator.h"
 
 #include "AbstractFormula.h"
diff --git a/src/formula/SteadyStateReward.h b/src/formula/SteadyStateReward.h
new file mode 100644
index 000000000..799bc50a7
--- /dev/null
+++ b/src/formula/SteadyStateReward.h
@@ -0,0 +1,106 @@
+/*
+ * SteadyStateReward.h
+ *
+ *  Created on: 08.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_STEADYSTATEREWARD_H_
+#define STORM_FORMULA_STEADYSTATEREWARD_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include <string>
+
+namespace storm {
+namespace formula {
+
+template <class T> class SteadyStateReward;
+
+/*!
+ *  @brief Interface class for model checkers that support SteadyStateReward.
+ *
+ *  All model checkers that support the formula class SteadyStateReward must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class ISteadyStateRewardModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates CumulativeReward formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkSteadyStateReward(const SteadyStateReward<T>& obj, bool qualitative) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Steady State Reward node as root.
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class SteadyStateReward: public storm::formula::AbstractPathFormula<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	SteadyStateReward() {
+		// Intentionally left empty
+
+	}
+	virtual ~SteadyStateReward() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		return "S";
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new SteadyState-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		return new SteadyStateReward<T>();
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<ISteadyStateRewardModelChecker>()->checkSteadyStateReward(*this, qualitative);
+	}
+
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  As SteadyStateReward objects have no subformulas, we return true here.
+     *
+     *  @param checker Formula checker object.
+     *  @return true
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return true;
+	}
+};
+
+} /* namespace formula */
+} /* namespace storm */
+#endif /* STEADYSTATEREWARD_H_ */
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 213cb9938..a2a41f1e3 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -60,6 +60,10 @@ public:
 		: model(modelChecker->model) {
 	}
 	
+	virtual ~AbstractModelChecker() {
+		//intentionally left empty
+	}
+
 	template <template <class T> class Target>
 	const Target<Type>* as() const {
 		try {
@@ -72,8 +76,6 @@ public:
 	}
 
 	/*!
-<<<<<<< HEAD
-=======
 	 * Checks the given state formula on the DTMC and prints the result (true/false) for all initial
 	 * states.
 	 * @param stateFormula The formula to be checked.
@@ -87,9 +89,9 @@ public:
 			result = stateFormula.check(*this);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : model.getLabeledStates("init")) {
+			for (auto initialState : *model.getLabeledStates("init")) {
 				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+				std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
 			}
 			delete result;
 		} catch (std::exception& e) {
@@ -153,7 +155,6 @@ public:
 	}
 
 	/*!
->>>>>>> master
 	 * The check method for a state formula with an And node as root in its formula tree
 	 *
 	 * @param formula The And formula to check
diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
index bc5486cf5..3fa4cc238 100644
--- a/src/modelchecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -41,7 +41,6 @@ namespace modelChecker {
 template<class Type>
 class DtmcPrctlModelChecker : public AbstractModelChecker<Type> {
 
-
 public:
 	/*!
 	 * Constructor
@@ -75,93 +74,6 @@ public:
 		return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>();
 	}
 
-	/*!
-	 * Sets the DTMC model which is checked
-	 * @param model
-	 */
-	void setModel(storm::models::Dtmc<Type>& model) {
-		AbstractModelChecker<Type>::setModel(model);
-	}
-
-	/*!
-	 * The check method for a formula with an AP node as root in its formula tree
-	 *
-	 * @param formula The Ap state formula to check
-	 * @returns The set of states satisfying the formula, represented by a bit vector
-	 */
-	storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const {
-		if (formula.getAp().compare("true") == 0) {
-			return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true);
-		} else if (formula.getAp().compare("false") == 0) {
-			return new storm::storage::BitVector(this->getModel().getNumberOfStates());
-		}
-
-		if (!this->getModel().hasAtomicProposition(formula.getAp())) {
-			LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid.");
-			throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
-		}
-
-		return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp()));
-	}
-
-	/*!
-	 * Checks the given state formula on the DTMC and prints the result (true/false) for all initial
-	 * states.
-	 * @param stateFormula The formula to be checked.
-	 */
-	void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
-		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
-		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
-		storm::storage::BitVector* result = nullptr;
-		try {
-			result = stateFormula.check(*this);
-			LOG4CPLUS_INFO(logger, "Result for initial states:");
-			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : *this->getModel().getLabeledStates("init")) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
-			}
-			delete result;
-		} catch (std::exception& e) {
-			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
-			if (result != nullptr) {
-				delete result;
-			}
-		}
-		std::cout << std::endl;
-		storm::utility::printSeparationLine(std::cout);
-	}
-
-	/*!
-	 * Checks the given operator (with no bound) on the DTMC and prints the result
-	 * (probability/rewards) for all initial states.
-	 * @param noBoundFormula The formula to be checked.
-	 */
-	void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const {
-		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
-		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
-		std::vector<Type>* result = nullptr;
-		try {
-			result = noBoundFormula.check(*this);
-			LOG4CPLUS_INFO(logger, "Result for initial states:");
-			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : *this->getModel().getLabeledStates("init")) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
-			}
-			delete result;
-		} catch (std::exception& e) {
-			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
-			if (result != nullptr) {
-				delete result;
-			}
-		}
-		std::cout << std::endl;
-		storm::utility::printSeparationLine(std::cout);
-	}
-
 	/*!
 	 * The check method for a state formula with a probabilistic operator node without bounds as root
 	 * in its formula tree
diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp
index 9efa1186a..9efefe1a4 100644
--- a/src/parser/PrctlFileParser.cpp
+++ b/src/parser/PrctlFileParser.cpp
@@ -5,32 +5,75 @@
  *      Author: Thomas Heinemann
  */
 
-#include "PrctlFileParser.h"
+#include <sstream>
 
-#define LINELENGTH 100
+#include "PrctlFileParser.h"
+#include "PrctlParser.h"
+#include "modelchecker/EigenDtmcPrctlModelChecker.h"
+#include "modelchecker/GmmxxDtmcPrctlModelChecker.h"
+#include "modelchecker/GmmxxMdpPrctlModelChecker.h"
 
 namespace storm {
 namespace parser {
 
-PrctlFileParser::PrctlFileParser(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker) {
-	// Open file and initialize result.
-	std::ifstream inputFileStream(filename, std::ios::in);
-
-	// TODO: Right now, this parses the whole contents of the file into a string first.
-	// While this is usually not necessary, because there exist adapters that make an input stream
-	// iterable in both directions without storing it into a string, using the corresponding
-	// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
-	while(!inputFileStream.eof()) {
-		char line[LINELENGTH];
-		inputFileStream.getline(line, LINELENGTH);
+PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library) {
 
+	storm::modelChecker::DtmcPrctlModelChecker<double>* modelChecker = nullptr;
+	switch(library) {
+	//case EIGEN:
+		//Eigen Model Checker is not completely implemented at the moment, thus using Eigen is not possible...
+		//Current behaviour: Fall back to GMMXX...
+		//modelChecker = new storm::modelChecker::EigenDtmcPrctlModelChecker<double>(dtmc);
+	//	break;
+	case GMMXX:
+	default:					//Note: GMMXX is default, hence default branches here, too.
+		modelChecker = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+		break;
 	}
+	check(filename, modelChecker);
+	delete modelChecker;
+}
 
+PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library) {
+	storm::modelChecker::MdpPrctlModelChecker<double>* modelChecker = nullptr;
+	switch(library) {
+	//case EIGEN:
+		//Eigen MDP Model Checker is not implemented yet
+		//Current behaviour: Fall back to GMMXX...
+	//	break;
+	case GMMXX:
+	default:					//Note: GMMXX is default, hence default branches here, too.
+		modelChecker = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);
+		break;
+	}
+	check(filename, modelChecker);
+	delete modelChecker;
 }
 
 PrctlFileParser::~PrctlFileParser() {
 	//intentionally left empty
-	//formulas are not deleted with the parser!
+}
+
+void PrctlFileParser::check(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker) {
+	// Open file
+	std::ifstream inputFileStream(filename, std::ios::in);
+
+	while(!inputFileStream.eof()) {
+		std::string line;
+		//The while loop reads the input file line by line
+		while (std::getline(inputFileStream, line)) {
+			PrctlParser parser(line);
+			storm::formula::AbstractStateFormula<double>* stateFormula = dynamic_cast<storm::formula::AbstractStateFormula<double>*>(parser.getFormula());
+			if (stateFormula != nullptr) {
+				modelChecker->check(*stateFormula);
+			}
+			storm::formula::NoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::formula::NoBoundOperator<double>*>(parser.getFormula());
+			if (noBoundFormula != nullptr) {
+				modelChecker->check(*noBoundFormula);
+			}
+			delete parser.getFormula();
+		}
+	}
 }
 
 } /* namespace parser */
diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h
index 83bad00c5..e0d64c499 100644
--- a/src/parser/PrctlFileParser.h
+++ b/src/parser/PrctlFileParser.h
@@ -8,7 +8,9 @@
 #ifndef STORM_PARSER_PRCTLFILEPARSER_H_
 #define STORM_PARSER_PRCTLFILEPARSER_H_
 
-#include "PrctlParser.h"
+#include "models/Dtmc.h"
+#include "models/Mdp.h"
+#include "formula/Formulas.h"
 #include "modelchecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -23,22 +25,44 @@ namespace parser {
  */
 class PrctlFileParser {
 public:
+	enum libraries {
+		GMMXX,
+		EIGEN
+	};
+
 	/*!
-	 * Reads the formula from the given file and parses it into a formula tree, consisting of
-	 * classes in the namespace storm::formula.
+	 * Reads a given file of formulas and checks each of these against a given DTMC.
 	 *
-	 * If the contents of the file could not be parsed successfully, it will throw a wrongFormatException.
+	 * @param filename The name of the file to parse
+	 * @param dtmc		 The DTMC model to check
+	 * @param library  Specifies the library that should perform the algebraic operations during model checking (default is GMMxx)
+	 */
+	PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library=GMMXX);
+
+	/*!
+	 * Reads a given file of formulas and checks each of these against a given MDP.
 	 *
 	 * @param filename The name of the file to parse
-	 * @throw wrongFormatException If the input could not be parsed successfully
+	 * @param mdp		 The MDP model to check
+	 * @param library  Specifies the library that should perform the algebraic operations during model checking (default is GMMxx, which at the moment also is the only implemented version...)
+	 */
+	PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library=GMMXX);
+
+protected:
+	/*!
+	 * Does the actual checking.
+	 * This procedure is equal for all model types (only the model checker is different, so it has to be created in
+	 * different methods beforehand)
+	 *
+	 * @param filename     The name of the file to parse
+	 * @param modelChecker The model checker that checks the formula (has to know its model!)
 	 */
-	PrctlFileParser(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker);
+	void check(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker);
 
 	/*!
 	 * Destructor.
 	 * At this time, empty
 	 *
-	 * Will not delete the constructed formula!
 	 */
 	virtual ~PrctlFileParser();
 };
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index e7f166138..3d7db0c7c 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -69,13 +69,13 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 				);
 		probabilisticBoundOperator.name("state formula");
 		rewardBoundOperator = (
-				(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
+				(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
-				(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
+				(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
 								phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
-				(qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
+				(qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
 										phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
-				(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
+				(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 		rewardBoundOperator.name("state formula");
@@ -86,7 +86,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 		probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
 				phoenix::new_<storm::formula::ProbabilisticNoBoundOperator<double> >(qi::_1)];
 		probabilisticNoBoundOperator.name("no bound operator");
-		rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
+		rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val =
 				phoenix::new_<storm::formula::RewardNoBoundOperator<double> >(qi::_1)];
 		rewardNoBoundOperator.name("no bound operator");
 
@@ -109,6 +109,20 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 				phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
 		until.name("path formula");
 
+		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward);
+		rewardPathFormula.name("path formula (for reward operator)");
+		cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)
+				[qi::_val = phoenix::new_<storm::formula::CumulativeReward<double>>(qi::_1)];
+		cumulativeReward.name("path formula (for reward operator)");
+		reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::ReachabilityReward<double>>(qi::_1)];
+		reachabilityReward.name("path formula (for reward operator)");
+		instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_)
+						[qi::_val = phoenix::new_<storm::formula::InstantaneousReward<double>>(qi::_1)];
+		instantaneousReward.name("path formula (for reward operator)");
+		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::formula::SteadyStateReward<double>>()];
+
+
 		start = (noBoundOperator | stateFormula);
 		start.name("PRCTL formula");
 	}
@@ -136,6 +150,13 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 	qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> boundedUntil;
 	qi::rule<Iterator, storm::formula::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> until;
 
+	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> rewardPathFormula;
+	qi::rule<Iterator, storm::formula::CumulativeReward<double>*(), Skipper> cumulativeReward;
+	qi::rule<Iterator, storm::formula::ReachabilityReward<double>*(), Skipper> reachabilityReward;
+	qi::rule<Iterator, storm::formula::InstantaneousReward<double>*(), Skipper> instantaneousReward;
+	qi::rule<Iterator, storm::formula::SteadyStateReward<double>*(), Skipper> steadyStateReward;
+
+
 	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
 
 };
diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp
index c3f7d9fcf..6c1fd4032 100644
--- a/test/parser/PrctlParserTest.cpp
+++ b/test/parser/PrctlParserTest.cpp
@@ -66,7 +66,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 TEST(PrctlParserTest, parseRewardFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser("R >= 15 [ a U !b ]")
+			prctlParser = new storm::parser::PrctlParser("R >= 15 [ I=5 ]")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
@@ -76,7 +76,7 @@ TEST(PrctlParserTest, parseRewardFormulaTest) {
 	ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
 
-	ASSERT_EQ(prctlParser->getFormula()->toString(), "R >= 15.000000 [a U !b]");
+	ASSERT_EQ("R >= 15.000000 [I=5]", prctlParser->getFormula()->toString());
 
 	delete prctlParser->getFormula();
 	delete prctlParser;
@@ -85,13 +85,13 @@ TEST(PrctlParserTest, parseRewardFormulaTest) {
 TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser("R = ? [ a U <= 4 b & (!c) ]")
+			prctlParser = new storm::parser::PrctlParser("R = ? [ F a ]")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
 
-	ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [a U<=4 (b & !c)]");
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [F a]");
 
 	delete prctlParser->getFormula();
 	delete prctlParser;
@@ -101,13 +101,13 @@ TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
 TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser("P = ? [ F <= 42 !a ]")
+			prctlParser = new storm::parser::PrctlParser("P = ? [ a U <= 4 b & (!c) ]")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
 
-	ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [F<=42 !a]");
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]");
 
 	delete prctlParser->getFormula();
 	delete prctlParser;
@@ -117,13 +117,13 @@ TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
 TEST(PrctlParserTest, parseComplexFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser("P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ])")
+			prctlParser = new storm::parser::PrctlParser("R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
 
-	ASSERT_EQ(prctlParser->getFormula()->toString(), "(P <= 0.500000 [F a] & (R > 15.000000 [G P > 0.900000 [F<=7 (a & b)]] | !P < 0.400000 [G !b]))");
+	ASSERT_EQ("(R <= 0.500000 [S] & (R > 15.000000 [C <= 0.500000] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", prctlParser->getFormula()->toString());
 	delete prctlParser->getFormula();
 	delete prctlParser;