Commit to switch workplace.

src/ir/Assignment.h

@@ -35,7 +35,7 @@ public:
 	}
 
 	std::string toString() {
-		return variableName + "' = " + expression->toString();
+		return "(" + variableName + "' = " + expression->toString() + ")";
 	}
 
 private:

src/ir/BooleanVariable.h

@@ -18,7 +18,7 @@ public:
 
 	}
 
-	BooleanVariable(std::string variableName) : Variable(variableName) {
+	BooleanVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = nullptr) : Variable(variableName,  initialValue) {
 
 	}
 
@@ -27,7 +27,12 @@ public:
 	}
 
 	virtual std::string toString() {
-		return getVariableName() + ": bool;";
+		std::string result = getVariableName() + ": bool";
+		if (this->getInitialValue() != nullptr) {
+			result += " init " + this->getInitialValue()->toString();
+		}
+		result += ";";
+		return result;
 	}
 };
 

src/ir/IR.h

@@ -16,6 +16,8 @@
 #include "BooleanVariable.h"
 #include "IntegerVariable.h"
 #include "Module.h"
+#include "StateReward.h"
+#include "TransitionReward.h"
 #include "RewardModel.h"
 #include "Program.h"
 

src/ir/IntegerVariable.h

@@ -16,11 +16,11 @@ namespace ir {
 
 class IntegerVariable : public Variable {
 public:
-	IntegerVariable() {
+	IntegerVariable() : lowerBound(nullptr), upperBound(nullptr) {
 
 	}
 
-	IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound) : Variable(variableName), lowerBound(lowerBound), upperBound(upperBound) {
+	IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = nullptr) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
 
 	}
 
@@ -29,7 +29,12 @@ public:
 	}
 
 	virtual std::string toString() {
-		return getVariableName() + ": int[" + lowerBound->toString() + ".." + upperBound->toString() + "];";
+		std::string result = getVariableName() + ": [" + lowerBound->toString() + ".." + upperBound->toString() + "]";
+		if (this->getInitialValue() != nullptr) {
+			result += " init " + this->getInitialValue()->toString();
+		}
+		result += ";";
+		return result;
 	}
 
 private:

src/ir/Module.h

@@ -34,7 +34,6 @@ public:
 		for (auto variable : booleanVariables) {
 			result += "\t" + variable.toString() + "\n";
 		}
-		result += "\n";
 		for (auto variable : integerVariables) {
 			result += "\t" + variable.toString() + "\n";
 		}

src/ir/Program.h

@@ -19,9 +19,9 @@ namespace ir {
 class Program {
 public:
 
-	enum ModelType {DTMC, CTMC, MDP, CTMDP};
+	enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP};
 
-	Program() : modelType(DTMC), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() {
+	Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() {
 
 	}
 
@@ -30,6 +30,12 @@ public:
 
 	}
 
+	Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules)
+		: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards() {
+
+	}
+
+
 	Program(ModelType modelType, std::vector<storm::ir::Module> modules) : modelType(modelType), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(modules), rewards() {
 
 	}
@@ -37,10 +43,11 @@ public:
 	std::string toString() {
 		std::string result = "";
 		switch (modelType) {
-		case DTMC: result += "dtmc\n"; break;
-		case CTMC: result += "ctmc\n"; break;
-		case MDP: result += "mdp\n"; break;
-		case CTMDP: result += "ctmdp\n"; break;
+		case UNDEFINED: result += "undefined\n\n"; break;
+		case DTMC: result += "dtmc\n\n"; break;
+		case CTMC: result += "ctmc\n\n"; break;
+		case MDP: result += "mdp\n\n"; break;
+		case CTMDP: result += "ctmdp\n\n"; break;
 		}
 		for (auto element : booleanUndefinedConstantExpressions) {
 			result += "const bool " + element.first + ";\n";
@@ -51,8 +58,15 @@ public:
 		for (auto element : doubleUndefinedConstantExpressions) {
 			result += "const double " + element.first + ";\n";
 		}
+		result += "\n";
 		for (auto mod : modules) {
 			result += mod.toString();
+			result += "\n";
+		}
+
+		for (auto rewardModel : rewards) {
+			result += rewardModel.second.toString();
+			result +="\n";
 		}
 
 		return result;

src/ir/RewardModel.h

@@ -13,7 +13,31 @@ namespace storm {
 namespace ir {
 
 class RewardModel {
-
+public:
+	RewardModel() : rewardModelName(""), stateRewards(), transitionRewards() {
+
+	}
+
+	RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
+
+	}
+
+	std::string toString() {
+		std::string result = "rewards \"" + rewardModelName + "\n";
+		for (auto reward : stateRewards) {
+			result += reward.toString() + "\n";
+		}
+		for (auto reward : transitionRewards) {
+			result += reward.toString() + "\n";
+		}
+		result += "endrewards\n";
+		return result;
+	}
+
+private:
+	std::string rewardModelName;
+	std::vector<storm::ir::StateReward> stateRewards;
+	std::vector<storm::ir::TransitionReward> transitionRewards;
 };
 
 }

src/ir/StateReward.h

@@ -0,0 +1,40 @@
+/*
+ * StateReward.h
+ *
+ *  Created on: Jan 10, 2013
+ *      Author: chris
+ */
+
+#ifndef STATEREWARD_H_
+#define STATEREWARD_H_
+
+#include "expressions/BaseExpression.h"
+
+namespace storm {
+
+namespace ir {
+
+class StateReward {
+public:
+	StateReward() : statePredicate(nullptr), rewardValue(nullptr) {
+
+	}
+
+	StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
+
+	}
+
+	std::string toString() {
+		return statePredicate->toString() + ": " + rewardValue->toString() + ";";
+	}
+
+private:
+	std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
+	std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
+};
+
+}
+
+}
+
+#endif /* STATEREWARD_H_ */

src/ir/TransitionReward.h

@@ -0,0 +1,41 @@
+/*
+ * TransitionReward.h
+ *
+ *  Created on: Jan 10, 2013
+ *      Author: chris
+ */
+
+#ifndef TRANSITIONREWARD_H_
+#define TRANSITIONREWARD_H_
+
+#include "expressions/BaseExpression.h"
+
+namespace storm {
+
+namespace ir {
+
+class TransitionReward {
+public:
+	TransitionReward() : commandName(""), statePredicate(nullptr), rewardValue(nullptr) {
+
+	}
+
+	TransitionReward(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
+
+	}
+
+	std::string toString() {
+		return "[" + commandName + "] " + statePredicate->toString() + ": " + rewardValue->toString() + ";";
+	}
+
+private:
+	std::string commandName;
+	std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
+	std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
+};
+
+}
+
+}
+
+#endif /* TRANSITIONREWARD_H_ */

src/ir/Variable.h

@@ -14,11 +14,11 @@ namespace ir {
 
 class Variable {
 public:
-	Variable() {
+	Variable() : variableName(""), initialValue(nullptr) {
 
 	}
 
-	Variable(std::string variableName) : variableName(variableName) {
+	Variable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = nullptr) : variableName(variableName), initialValue(initialValue) {
 
 	}
 
@@ -34,8 +34,13 @@ public:
 		return variableName;
 	}
 
+	std::shared_ptr<storm::ir::expressions::BaseExpression> getInitialValue() {
+		return initialValue;
+	}
+
 private:
 	std::string variableName;
+	std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue;
 };
 
 }

src/ir/expressions/BinaryRelationExpression.h

@@ -35,7 +35,7 @@ public:
 	virtual std::string toString() const {
 		std::string result = left->toString();
 		switch (relation) {
-		case EQUAL: result += " == "; break;
+		case EQUAL: result += " = "; break;
 		case LESS: result += " < "; break;
 		case LESS_OR_EQUAL: result += " <= "; break;
 		case GREATER: result += " > "; break;

src/parser/PrismParser.h

@@ -8,13 +8,20 @@
 #ifndef PRISMPARSER_H_
 #define PRISMPARSER_H_
 
+#include <boost/typeof/typeof.hpp>
 #include <boost/spirit/include/qi.hpp>
 #include <boost/spirit/include/phoenix.hpp>
+#include <boost/spirit/include/support_multi_pass.hpp>
+#include <boost/spirit/include/classic_position_iterator.hpp>
 #include <boost/fusion/include/adapt_struct.hpp>
 #include <boost/fusion/include/io.hpp>
 
 #include "src/ir/IR.h"
 
+#include <istream>
+#include <fstream>
+#include <iomanip>
+
 namespace storm {
 
 namespace parser {
@@ -26,43 +33,43 @@ namespace phoenix = boost::phoenix;
 class PrismParser {
 
 public:
-	void test() {
-		std::string testInput = "" \
-				"" \
-				"const bool d; const int c; const double x;" \
-				"module test " \
-				" a : bool;" \
-				"endmodule" \
-				"module test2 endmodule";
-		getProgram(testInput);
+	void test(std::string const& fileName) {
+		std::ifstream inputFileStream(fileName, std::ios::in);
+		getProgram(inputFileStream, fileName);
+		inputFileStream.close();
 	}
 
-	void getProgram(std::string inputString) {
+	void getProgram(std::istream& inputStream, std::string const& fileName) {
+		typedef std::istreambuf_iterator<char> base_iterator_type;
+		base_iterator_type in_begin(inputStream);
+
+		typedef boost::spirit::multi_pass<base_iterator_type> forward_iterator_type;
+		forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin);
+		forward_iterator_type fwd_end;
+
+		typedef boost::spirit::classic::position_iterator2<forward_iterator_type> pos_iterator_type;
+		pos_iterator_type position_begin(fwd_begin, fwd_end, fileName);
+		pos_iterator_type position_end;
+
 		storm::ir::Program result;
-		prismGrammar<std::string::const_iterator> grammar(result);
-		std::string::const_iterator it = inputString.begin();
-		std::string::const_iterator end = inputString.end();
-
-		storm::ir::Program realResult;
-		bool r = phrase_parse(it, end, grammar, ascii::space, realResult);
-
-		if (r && it == end) {
-			std::cout << "Parsing successful!" << std::endl;
-			std::cout << realResult.toString() << std::endl;
-		} else {
-			std::string rest(it, end);
-			std::cout << "-------------------------\n";
-			std::cout << "Parsing failed\n";
-			std::cout << "stopped at: \"" << rest << "\"\n";
-			std::cout << "-------------------------\n";
+		prismGrammar<pos_iterator_type,  BOOST_TYPEOF(ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol)> grammar;
+		try {
+			phrase_parse(position_begin, position_end, grammar, ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
+		} catch(const qi::expectation_failure<pos_iterator_type>& e) {
+			const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
+			std::stringstream msg;
+			msg << "parse error at file '" << pos.file << "' line " << pos.line << " column " << pos.column << std::endl << "'" << e.first.get_currentline() << "'" << std::endl << std::setw(pos.column) << " " << "^- here";
+			throw storm::exceptions::WrongFileFormatException() << msg.str();
 		}
+
+		std::cout << result.toString();
 	}
 
 private:
-	template<typename Iterator>
-	struct prismGrammar : qi::grammar<Iterator, storm::ir::Program(), ascii::space_type> {
+	template<typename Iterator, typename Skipper>
+	struct prismGrammar : qi::grammar<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>>, Skipper> {
 
-		prismGrammar(storm::ir::Program& program) : prismGrammar::base_type(start), program(program) {
+		prismGrammar() : prismGrammar::base_type(start) {
 			freeIdentifierName %= qi::lexeme[(qi::alpha >> *(qi::alnum)) - allVariables_ - allConstants_];
 
 			booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BooleanLiteral>(qi::_1))];
@@ -84,120 +91,167 @@ private:
 			integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
 			integerExpression %= integerPlusExpression;
 
-			atomicDoubleExpression %= (qi::lit("(") >> doubleExpression >> qi::lit(")") | doubleConstantExpression);
-			doubleMultExpression %= atomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
-			doublePlusExpression %= doubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> doubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
-			doubleExpression %= doublePlusExpression;
+			constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
+			constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+			constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+			constantIntegerExpression %= constantIntegerPlusExpression;
+
+			// This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants.
+			constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression);
+			constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+			constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+			constantDoubleExpression %= constantDoublePlusExpression;
 
+			// This block defines all expressions of type boolean.
 			relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
-			atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
-			andExpression = atomicBooleanExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
+			atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression);
+			notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
+			andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
 			orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))];
 			booleanExpression %= orExpression;
 
-			expression %= (booleanExpression | integerExpression | doubleExpression);
+			// This block defines all expressions of type boolean that are by syntax constant. That is, they are evaluable given the values for all constants.
+			constantRelativeExpression = (constantIntegerExpression >> relations_ >> constantIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
+			constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
+			constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
+			constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
+			constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))];
+			constantBooleanExpression %= constantOrExpression;
 
-			booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::BooleanVariable>(qi::_1), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableInfo_.add, qi::_1, qi::_val)];
-			integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableInfo_.add, qi::_1, qi::_val)];
-			variableDefinition = (booleanVariableDefinition | integerVariableDefinition);
+			// This block defines the general root of all expressions. Most of the time, however, you may want to start with a more specialized rule.
+			expression %= (booleanExpression | integerExpression | constantDoubleExpression);
 
-			definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") >> booleanLiteralExpression >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
-			definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") >> integerLiteralExpression >> qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
-			definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") >> doubleLiteralExpression >> qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
-			undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>(phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), phoenix::bind(booleanConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
-			undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>(phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), phoenix::bind(integerConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
-			undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>(phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), phoenix::bind(doubleConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
-			definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
-			// undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
-			// constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition);
+			stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::StateReward>(qi::_1, qi::_2)];
+			transitionRewardDefinition = (qi::lit("[") > commandName > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::TransitionReward>(qi::_1, qi::_2, qi::_3)];
+			rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) > qi::lit("endrewards"))[qi::_r1[qi::_1] = phoenix::construct<storm::ir::RewardModel>(qi::_1, qi::_a, qi::_b)];
+			rewardDefinitionList = *rewardDefinition(qi::_r1);
 
+			// This block defines auxiliary entities that are used to check whether a certain variable exist.
 			integerVariableName %= integerVariableNames_;
 			booleanVariableName %= booleanVariableNames_;
+			commandName %= commandNames_;
 
-			assignmentDefinition = (qi::lit("(") >> integerVariableName >> qi::lit("'") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)] | (qi::lit("(") >> booleanVariableName >> qi::lit("'") >> booleanExpression >> qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)];
+			// This block defines all entities that are needed for parsing a single command.
+			assignmentDefinition = (qi::lit("(") >> integerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)] | (qi::lit("(") > booleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)];
 			assignmentDefinitionList %= assignmentDefinition % "&";
-			updateDefinition = (doubleConstantExpression >> qi::lit(":") >> assignmentDefinitionList)[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_2)];
-			updateListDefinition = +updateDefinition;
-			commandDefinition = (qi::lit("[") >> freeIdentifierName >> qi::lit("]") >> booleanExpression >> qi::lit("->") >> updateListDefinition >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::Command>(qi::_1, qi::_2, qi::_3)];
+			updateDefinition = (constantDoubleExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_2)];
+			updateListDefinition = +updateDefinition % "+";
+			commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::Command>(qi::_a, qi::_2, qi::_3)];
 
-			moduleDefinition = (qi::lit("module") >> freeIdentifierName >> *(booleanVariableDefinition[phoenix::push_back(qi::_a, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> *commandDefinition >> qi::lit("endmodule"))[qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_a, qi::_b, qi::_3)];
+			// This block defines all entities that are neede for parsing variable definitions.
+			booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::BooleanVariable>(qi::_1, qi::_b), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableInfo_.add, qi::_1, qi::_val)];
+			integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3, qi::_b), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableInfo_.add, qi::_1, qi::_val)];
+			variableDefinition = (booleanVariableDefinition | integerVariableDefinition);
 
-			moduleDefinitionList = +moduleDefinition;
+			// This block defines all entities that are needed for parsing a module.
+			moduleDefinition = (qi::lit("module") > freeIdentifierName > *(booleanVariableDefinition[phoenix::push_back(qi::_a, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_b, qi::_1)]) > +commandDefinition > qi::lit("endmodule"))[qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_a, qi::_b, qi::_3)];
+			moduleDefinitionList %= +moduleDefinition;
+
+			// This block defines all entities that are needed for parsing constant definitions.
+			definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
+			definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
+			definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
+			undefinedBooleanConstantDefinition = (qi::lit("const") > qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>(phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), qi::_r1[qi::_1] = qi::_a, phoenix::bind(booleanConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
+			undefinedIntegerConstantDefinition = (qi::lit("const") > qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>(phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), qi::_r1[qi::_1] = qi::_a, phoenix::bind(integerConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
+			undefinedDoubleConstantDefinition = (qi::lit("const") > qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>(phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), qi::_r1[qi::_1] = qi::_a, phoenix::bind(doubleConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
+			definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
+			undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
+			constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
 
-			start = (*(definedConstantDefinition | (undefinedBooleanConstantDefinition[phoenix::push_back(qi::_a, qi::_1)] | undefinedIntegerConstantDefinition[phoenix::push_back(qi::_b, qi::_1)] | undefinedDoubleConstantDefinition[phoenix::push_back(qi::_c, qi::_1)])) >> moduleDefinitionList)[qi::_val = phoenix::construct<storm::ir::Program>(storm::ir::Program::ModelType::DTMC, qi::_a, qi::_b, qi::_c, qi::_1)];
+			// This block defines all entities that are needed for parsing a program.
+			modelTypeDefinition = modelType_;
+			start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d))[qi::_val = phoenix::construct<storm::ir::Program>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d)];
 		}
 
 		// The starting point of the grammar.
-		qi::rule<Iterator, storm::ir::Program(), qi::locals<std::vector<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>,std::vector<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>,std::vector<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>>, ascii::space_type> start;
-		qi::rule<Iterator, qi::unused_type(), ascii::space_type> constantDefinitionList;
-		qi::rule<Iterator, std::vector<storm::ir::Module>(), ascii::space_type> moduleDefinitionList;
+		qi::rule<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>>, Skipper> start;
+		qi::rule<Iterator, storm::ir::Program::ModelType(), Skipper> modelTypeDefinition;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), Skipper> constantDefinitionList;
+		qi::rule<Iterator, std::vector<storm::ir::Module>(), Skipper> moduleDefinitionList;
 
-		qi::rule<Iterator, storm::ir::Module(), qi::locals<std::vector<storm::ir::BooleanVariable>, std::vector<storm::ir::IntegerVariable>>, ascii::space_type> moduleDefinition;
+		qi::rule<Iterator, storm::ir::Module(), qi::locals<std::vector<storm::ir::BooleanVariable>, std::vector<storm::ir::IntegerVariable>>, Skipper> moduleDefinition;
 
-		qi::rule<Iterator, qi::unused_type(), ascii::space_type> variableDefinition;
-		qi::rule<Iterator, storm::ir::BooleanVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>>, ascii::space_type> booleanVariableDefinition;
-		qi::rule<Iterator, storm::ir::IntegerVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>>, ascii::space_type> integerVariableDefinition;
+		qi::rule<Iterator, qi::unused_type(), Skipper> variableDefinition;
+		qi::rule<Iterator, storm::ir::BooleanVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> booleanVariableDefinition;
+		qi::rule<Iterator, storm::ir::IntegerVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> integerVariableDefinition;
 
-		qi::rule<Iterator, storm::ir::Command(), ascii::space_type> commandDefinition;
+		qi::rule<Iterator, storm::ir::Command(), qi::locals<std::string>, Skipper> commandDefinition;
 
-		qi::rule<Iterator, std::vector<storm::ir::Update>(), ascii::space_type> updateListDefinition;
-		qi::rule<Iterator, storm::ir::Update(), ascii::space_type> updateDefinition;
-		qi::rule<Iterator, std::vector<storm::ir::Assignment>(), ascii::space_type> assignmentDefinitionList;
-		qi::rule<Iterator, storm::ir::Assignment(), ascii::space_type> assignmentDefinition;
+		qi::rule<Iterator, std::vector<storm::ir::Update>(), Skipper> updateListDefinition;
+		qi::rule<Iterator, storm::ir::Update(), Skipper> updateDefinition;
+		qi::rule<Iterator, std::vector<storm::ir::Assignment>(), Skipper> assignmentDefinitionList;
+		qi::rule<Iterator, storm::ir::Assignment(), Skipper> assignmentDefinition;
 
-		qi::rule<Iterator, std::string(), ascii::space_type> integerVariableName;
-		qi::rule<Iterator, std::string(), ascii::space_type> booleanVariableName;
+		qi::rule<Iterator, std::string(), Skipper> integerVariableName;
+		qi::rule<Iterator, std::string(), Skipper> booleanVariableName;
+		qi::rule<Iterator, std::string(), Skipper> commandName;
 
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> constantDefinition;
-		qi::rule<Iterator, qi::unused_type(), ascii::space_type> undefinedConstantDefinition;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedConstantDefinition;
-		qi::rule<Iterator, qi::unused_type(), qi::locals<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, ascii::space_type> undefinedBooleanConstantDefinition;
-		qi::rule<Iterator, qi::unused_type(), qi::locals<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, ascii::space_type> undefinedIntegerConstantDefinition;
-		qi::rule<Iterator, qi::unused_type(), qi::locals<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, ascii::space_type> undefinedDoubleConstantDefinition;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedBooleanConstantDefinition;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedIntegerConstantDefinition;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedDoubleConstantDefinition;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::RewardModel>&), Skipper> rewardDefinitionList;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::RewardModel>&), qi::locals<std::vector<storm::ir::StateReward>, std::vector<storm::ir::TransitionReward>>, Skipper> rewardDefinition;
+		qi::rule<Iterator, storm::ir::StateReward(), Skipper> stateRewardDefinition;
+		qi::rule<Iterator, storm::ir::TransitionReward(), Skipper> transitionRewardDefinition;
 
-		qi::rule<Iterator, std::string(), ascii::space_type> freeIdentifierName;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantDefinition;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedConstantDefinition;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&), qi::locals<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&), qi::locals<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
+		qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), qi::locals<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedBooleanConstantDefinition;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedIntegerConstantDefinition;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedDoubleConstantDefinition;
+
+		qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
 
 		// The starting point for arbitrary expressions.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> expression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> expression;
 
 		// Rules with boolean result type.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> orExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> andExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> atomicBooleanExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> relativeExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> booleanExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> orExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> andExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> notExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> atomicBooleanExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> relativeExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantBooleanExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantOrExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantAndExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantNotExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantAtomicBooleanExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantRelativeExpression;
 
 		// Rules with integer result type.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerPlusExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerMultExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> atomicIntegerExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerPlusExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerMultExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> atomicIntegerExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantIntegerExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantIntegerPlusExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantIntegerMultExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantAtomicIntegerExpression;
 
 		// Rules with double result type.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doublePlusExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleMultExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> atomicDoubleExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantDoubleExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantDoublePlusExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantDoubleMultExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantAtomicDoubleExpression;
 
 		// Rules for variable recognition.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> variableExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanVariableExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerVariableExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> variableExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> booleanVariableExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerVariableExpression;
 
 		// Rules for constant recognition.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> constantExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanConstantExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerConstantExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleConstantExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> booleanConstantExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerConstantExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> doubleConstantExpression;
 
 		// Rules for literal recognition.
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> literalExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanLiteralExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerLiteralExpression;
-		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleLiteralExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> literalExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> booleanLiteralExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerLiteralExpression;
+		qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> doubleLiteralExpression;
 
 		struct keywordsStruct : qi::symbols<char, unsigned> {
 			keywordsStruct() {
@@ -219,10 +273,21 @@ private:
 			}
 		} keywords_;
 
+		struct modelTypeStruct : qi::symbols<char, storm::ir::Program::ModelType> {
+			modelTypeStruct() {
+				add
+					("dtmc", storm::ir::Program::ModelType::DTMC)
+					("ctmc", storm::ir::Program::ModelType::CTMC)
+					("mdp", storm::ir::Program::ModelType::MDP)
+					("ctmdp", storm::ir::Program::ModelType::CTMDP)
+				;
+			}
+		} modelType_;
+
 		struct relationalOperatorStruct : qi::symbols<char, storm::ir::expressions::BinaryRelationExpression::RelationType> {
 			relationalOperatorStruct() {
 				add
-					("==", storm::ir::expressions::BinaryRelationExpression::EQUAL)
+					("=", storm::ir::expressions::BinaryRelationExpression::EQUAL)
 					("<", storm::ir::expressions::BinaryRelationExpression::LESS)
 					("<=", storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL)
 					(">", storm::ir::expressions::BinaryRelationExpression::GREATER)
@@ -235,9 +300,9 @@ private:
 			// Intentionally left empty. This map is filled during parsing.
 		} integerVariables_, booleanVariables_, allVariables_;
 
-		struct variableNamesStruct : qi::symbols<char, std::string> {
+		struct entityNamesStruct : qi::symbols<char, std::string> {
 			// Intentionally left empty. This map is filled during parsing.
-		} integerVariableNames_, booleanVariableNames_;
+		} integerVariableNames_, booleanVariableNames_, commandNames_;
 
 		struct booleanVariableTypesStruct : qi::symbols<char, storm::ir::BooleanVariable> {
 			// Intentionally left empty. This map is filled during parsing.
@@ -266,8 +331,6 @@ private:
 		struct modulesStruct : qi::symbols<char, unsigned> {
 			// Intentionally left empty. This map is filled during parsing.
 		} modules_;
-
-		storm::ir::Program& program;
 	};
 };
 

src/storm.cpp

@@ -241,7 +241,7 @@ int main(const int argc, const char* argv[]) {
 	// testChecking();
 
 	storm::parser::PrismParser parser;
-	parser.test();
+	parser.test("test.input");
 
 	cleanUp();
 	return 0;

test.input

@@ -0,0 +1,19 @@
+dtmc
+
+module die
+
+// local state
+s : [0..7] init 0;
+// value of the dice
+d : [0..6] init 0;
+	
+[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+[] s==7 -> 1 : (s'=7);
+	
+endmodule