From 478f5ee38c8048d0261f5649930256e309d2a655 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 6 Jun 2014 15:14:14 +0200
Subject: [PATCH] Started separating expression parsing from PRISM model
 parsing.

Former-commit-id: 84d1354f9726b4200a79a0e30d9c05b26e118ab4
---
 src/parser/ExpressionParser.cpp      | 382 ++++++++++++++++++++++++++
 src/parser/ExpressionParser.h        | 126 +++++++++
 src/parser/PrismParser.cpp           | 383 ++-------------------------
 src/parser/PrismParser.h             |  82 +-----
 src/parser/SpiritParserDefinitions.h |  21 ++
 5 files changed, 549 insertions(+), 445 deletions(-)
 create mode 100644 src/parser/ExpressionParser.cpp
 create mode 100644 src/parser/ExpressionParser.h
 create mode 100644 src/parser/SpiritParserDefinitions.h

diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
new file mode 100644
index 000000000..e879994f6
--- /dev/null
+++ b/src/parser/ExpressionParser.cpp
@@ -0,0 +1,382 @@
+#include "src/parser/ExpressionParser.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+    namespace parser {
+        ExpressionParser::ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
+            identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
+            identifier.name("identifier");
+            
+            floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createFloorExpression, phoenix::ref(*this), qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createCeilExpression, phoenix::ref(*this), qi::_1)]];
+            floorCeilExpression.name("floor/ceil expression");
+            
+            minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMinimumExpression, phoenix::ref(*this), qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMaximumExpression, phoenix::ref(*this), qi::_1, qi::_2)]];
+            minMaxExpression.name("min/max expression");
+            
+            identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
+            identifierExpression.name("identifier expression");
+            
+            literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&ExpressionParser::createTrueExpression, phoenix::ref(*this))] | qi::lit("false")[qi::_val = phoenix::bind(&ExpressionParser::createFalseExpression, phoenix::ref(*this))] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)];
+            literalExpression.name("literal expression");
+            
+            atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression;
+            atomicExpression.name("atomic expression");
+            
+            unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_1)];
+            unaryExpression.name("unary expression");
+            
+            multiplicationExpression = unaryExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> unaryExpression[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createDivExpression, phoenix::ref(*this), qi::_val, qi::_1)]]);
+            multiplicationExpression.name("multiplication expression");
+            
+            plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]];
+            plusExpression.name("plus expression");
+            
+            relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
+            relativeExpression.name("relative expression");
+            
+            equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&ExpressionParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ];
+            equalityExpression.name("equality expression");
+            
+            andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)];
+            andExpression.name("and expression");
+            
+            orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
+            orExpression.name("or expression");
+            
+            iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            iteExpression.name("if-then-else expression");
+            
+            expression %= iteExpression;
+            expression.name("expression");
+            
+            // Enable error reporting.
+            qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+        }
+        
+        void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
+            this->createExpressions = true;
+            this->identifiers_ = identifiers_;
+        }
+        
+        void ExpressionParser::unsetIdentifierMapping() {
+            this->createExpressions = false;
+        }
+        
+        void ExpressionParser::setAcceptDoubleLiterals(bool flag) {
+            this->acceptDoubleLiterals = flag;
+        }
+        
+        storm::expressions::Expression ExpressionParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const {
+            if (this->createExpressions) {
+                try {
+                    return e1.ite(e2, e3);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1.implies(e2);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 || e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try{
+                    return e1 && e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 > e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 >= e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 < e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 <= e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
+                        return e1.iff(e2);
+                    } else {
+                        return e1 == e2;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
+                        return e1 ^ e2;
+                    } else {
+                        return e1 != e2;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 + e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 - e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 * e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return e1 / e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createNotExpression(storm::expressions::Expression e1) const {
+            if (this->createExpressions) {
+                try {
+                    return !e1;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1) const {
+            if (this->createExpressions) {
+                try {
+                    return -e1;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createTrueExpression() const {
+            if (this->createExpressions) {
+                return storm::expressions::Expression::createFalse();
+            } else {
+                return storm::expressions::Expression::createTrue();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createFalseExpression() const {
+            return storm::expressions::Expression::createFalse();
+        }
+        
+        storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const {
+            // If we are not supposed to accept double expressions, we reject it by setting pass to false.
+            if (!this->acceptDoubleLiterals) {
+                pass = false;
+            }
+            
+            if (this->createExpressions) {
+                return storm::expressions::Expression::createDoubleLiteral(value);
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const {
+            if (this->createExpressions) {
+                return storm::expressions::Expression::createFalse();
+            } else {
+                return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value));
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return storm::expressions::Expression::minimum(e1, e2);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
+            if (this->createExpressions) {
+                try {
+                    return storm::expressions::Expression::maximum(e1, e2);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createFloorExpression(storm::expressions::Expression e1) const {
+            if (this->createExpressions) {
+                try {
+                    return e1.floor();
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::createCeilExpression(storm::expressions::Expression e1) const {
+            if (this->createExpressions) {
+                try {
+                    return e1.ceil();
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
+            } else {
+                return storm::expressions::Expression::createFalse();
+            }
+        }
+        
+        storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const {
+            if (this->createExpressions) {
+                return storm::expressions::Expression::createFalse();
+            } else {
+                storm::expressions::Expression const* expression = this->identifiers_->find(identifier);
+                LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
+                return *expression;
+            }
+        }
+        
+        bool ExpressionParser::isValidIdentifier(std::string const& identifier) {
+            if (this->invalidIdentifiers_.find(identifier) != nullptr) {
+                return false;
+            }
+            return true;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
new file mode 100644
index 000000000..c340f9c14
--- /dev/null
+++ b/src/parser/ExpressionParser.h
@@ -0,0 +1,126 @@
+#ifndef STORM_PARSER_EXPRESSIONPARSER_H_
+#define	STORM_PARSER_EXPRESSIONPARSER_H_
+
+#include "src/parser/SpiritParserDefinitions.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+    namespace parser {
+        class ExpressionParser : public qi::grammar<Iterator, storm::expressions::Expression(), Skipper> {
+        public:
+            /*!
+             * Creates an expression parser. Initially the parser is set to a mode in which it will not generate the
+             * actual expressions but only perform a syntax check and return the expression "false". To make the parser
+             * generate the actual expressions, a mapping of valid identifiers to their expressions need to be provided
+             * later.
+             *
+             * @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected.
+             */
+            ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
+            
+            /*!
+             * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to
+             * expressions will be substituted wherever the key value appears in the parsed expression. After setting
+             * this, the parser will generate expressions.
+             *
+             * @param identifiers A pointer to a mapping from identifiers to expressions.
+             */
+            void setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_);
+            
+            /*!
+             * Unsets a previously set identifier mapping. This will make the parser not generate expressions any more
+             * but merely check for syntactic correctness of an expression.
+             */
+            void unsetIdentifierMapping();
+            
+            /*!
+             * Sets whether double literals are to be accepted or not.
+             *
+             * @param flag If set to true, double literals are accepted.
+             */
+            void setAcceptDoubleLiterals(bool flag);
+            
+        private:
+            // A flag that indicates whether expressions should actually be generated or just a syntax check shall be
+            // performed.
+            bool createExpressions;
+            
+            // A flag that indicates whether double literals are accepted.
+            bool acceptDoubleLiterals;
+            
+            // The currently used mapping of identifiers to expressions. This is used if the parser is set to create
+            // expressions.
+            qi::symbols<char, storm::expressions::Expression> const* identifiers_;
+            
+            // The symbol table of invalid identifiers.
+            qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_;
+            
+            // Rules for parsing a composed expression.
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
+            qi::rule<Iterator, std::string(), Skipper> identifier;
+            
+            // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
+            boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
+            
+            // Helper functions to create expressions.
+            storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
+            storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createNotExpression(storm::expressions::Expression e1) const;
+            storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1) const;
+            storm::expressions::Expression createTrueExpression() const;
+            storm::expressions::Expression createFalseExpression() const;
+            storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const;
+            storm::expressions::Expression createIntegerLiteralExpression(int value) const;
+            storm::expressions::Expression createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
+            storm::expressions::Expression createFloorExpression(storm::expressions::Expression e1) const;
+            storm::expressions::Expression createCeilExpression(storm::expressions::Expression e1) const;
+            storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const;
+            
+            bool isValidIdentifier(std::string const& identifier);
+            
+            // Functor used for displaying error information.
+            struct ErrorHandler {
+                typedef qi::error_handler_result result_type;
+                
+                template<typename T1, typename T2, typename T3, typename T4>
+                qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << ".");
+                    return qi::fail;
+                }
+            };
+            
+            // An error handler function.
+            phoenix::function<ErrorHandler> handler;
+        };
+    } // namespace parser
+} // namespace storm
+
+#endif /* STORM_PARSER_EXPRESSIONPARSER_H_ */
\ No newline at end of file
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index d4686bcff..5e64ca8eb 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -60,53 +60,11 @@ namespace storm {
             return result;
         }
         
-        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), allowDoubleLiteralsFlag(true), filename(filename), annotate(first) {
+        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), expressionParser(keywords_) {
             // Parse simple identifier.
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
             identifier.name("identifier");
             
-            floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createFloorExpression, phoenix::ref(*this), qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createCeilExpression, phoenix::ref(*this), qi::_1)]];
-            floorCeilExpression.name("floor/ceil expression");
-            
-            minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createMinimumExpression, phoenix::ref(*this), qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMaximumExpression, phoenix::ref(*this), qi::_1, qi::_2)]];
-            minMaxExpression.name("min/max expression");
-            
-            identifierExpression = identifier[qi::_val = phoenix::bind(&PrismParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
-            identifierExpression.name("identifier expression");
-            
-            literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&PrismParser::createTrueExpression, phoenix::ref(*this))] | qi::lit("false")[qi::_val = phoenix::bind(&PrismParser::createFalseExpression, phoenix::ref(*this))] | strict_double[qi::_val = phoenix::bind(&PrismParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&PrismParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)];
-            literalExpression.name("literal expression");
-            
-            atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression;
-            atomicExpression.name("atomic expression");
-            
-            unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = phoenix::bind(&PrismParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_1)];
-            unaryExpression.name("unary expression");
-            
-            multiplicationExpression = unaryExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> unaryExpression[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createDivExpression, phoenix::ref(*this), qi::_val, qi::_1)]]);
-            multiplicationExpression.name("multiplication expression");
-            
-            plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]];
-            plusExpression.name("plus expression");
-            
-            relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
-            relativeExpression.name("relative expression");
-            
-            equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ];
-            equalityExpression.name("equality expression");
-            
-            andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)];
-            andExpression.name("and expression");
-            
-            orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
-            orExpression.name("or expression");
-            
-            iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
-            iteExpression.name("if-then-else expression");
-            
-            expression %= iteExpression;
-            expression.name("expression");
-            
             modelTypeDefinition %= modelType_;
             modelTypeDefinition.name("model type");
             
@@ -122,25 +80,25 @@ namespace storm {
             undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
             undefinedConstantDefinition.name("undefined constant definition");
             
-            definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
+            definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
             definedBooleanConstantDefinition.name("defined boolean constant declaration");
             
-            definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
+            definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
             definedIntegerConstantDefinition.name("defined integer constant declaration");
             
-            definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
+            definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
             definedDoubleConstantDefinition.name("defined double constant declaration");
             
             definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
             definedConstantDefinition.name("defined constant definition");
             
-            formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             formulaDefinition.name("formula definition");
             
-            booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
+            booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
             booleanVariableDefinition.name("boolean variable definition");
             
-            integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression[qi::_a = qi::_1] > qi::lit("..") > expression > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
+            integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
             integerVariableDefinition.name("integer variable definition");
             
             variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
@@ -149,10 +107,10 @@ namespace storm {
             globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
             globalVariableDefinition.name("global variable declaration list");
                         
-            stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
+            stateRewardDefinition = (expressionParser > qi::lit(":") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
             stateRewardDefinition.name("state reward definition");
             
-            transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit(":") > plusExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)];
+            transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)];
             transitionRewardDefinition.name("transition reward definition");
             
             rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\""))
@@ -162,25 +120,25 @@ namespace storm {
                                      >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
             rewardModelDefinition.name("reward model definition");
             
-            initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
+            initialStatesConstruct = (qi::lit("init") > expressionParser > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             initialStatesConstruct.name("initial construct");
             
-            labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
+            labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
             labelDefinition.name("label definition");
             
-            assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
+            assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expressionParser > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
             assignmentDefinition.name("assignment");
             
             assignmentDefinitionList %= +assignmentDefinition % "&";
             assignmentDefinitionList.name("assignment list");
             
-            updateDefinition = (((plusExpression > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
+            updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
             updateDefinition.name("update");
             
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
             updateListDefinition.name("update list");
             
-            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
+            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
             commandDefinition.name("command definition");
             
             moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
@@ -209,22 +167,6 @@ namespace storm {
                      > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
             start.name("probabilistic program");
             
-            // Enable error reporting.
-            qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            
             // Enable location tracking for important entities.
             auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
             qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction);
@@ -250,7 +192,7 @@ namespace storm {
         }
         
         void PrismParser::allowDoubleLiterals(bool flag) {
-            this->allowDoubleLiteralsFlag = flag;
+            this->expressionParser.setAcceptDoubleLiterals(flag);
         }
         
         std::string const& PrismParser::getFilename() const {
@@ -274,301 +216,6 @@ namespace storm {
             return true;
         }
         
-        storm::expressions::Expression PrismParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1.ite(e2, e3);
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1.implies(e2);
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 || e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try{
-                    return e1 && e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 > e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 >= e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 < e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 <= e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
-                        return e1.iff(e2);
-                    } else {
-                        return e1 == e2;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
-                        return e1 ^ e2;
-                    } else {
-                        return e1 != e2;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 + e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 - e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 * e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1 / e2;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createNotExpression(storm::expressions::Expression e1) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return !e1;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createMinusExpression(storm::expressions::Expression e1) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return -e1;
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createTrueExpression() const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                return storm::expressions::Expression::createTrue();
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createFalseExpression() const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                return storm::expressions::Expression::createFalse();
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createDoubleLiteralExpression(double value, bool& pass) const {
-            // If we are not supposed to accept double expressions, we reject it by setting pass to false.
-            if (!this->allowDoubleLiteralsFlag) {
-                pass = false;
-            }
-            
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                return storm::expressions::Expression::createDoubleLiteral(value);
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createIntegerLiteralExpression(int value) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value));
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return storm::expressions::Expression::minimum(e1, e2);
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return storm::expressions::Expression::maximum(e1, e2);
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createFloorExpression(storm::expressions::Expression e1) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1.floor();
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::createCeilExpression(storm::expressions::Expression e1) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                try {
-                    return e1.ceil();
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
-                }
-            }
-        }
-        
-        storm::expressions::Expression PrismParser::getIdentifierExpression(std::string const& identifier) const {
-            if (!this->secondRun) {
-                return storm::expressions::Expression::createFalse();
-            } else {
-                storm::expressions::Expression const* expression = this->identifiers_.find(identifier);
-                LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
-                return *expression;
-            }
-        }
-        
         storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index e1a9136ba..bdf84af24 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -6,23 +6,8 @@
 #include <memory>
 #include <iomanip>
 
-// Include boost spirit.
-#define BOOST_SPIRIT_USE_PHOENIX_V3
-#include <boost/typeof/typeof.hpp>
-#include <boost/spirit/include/qi.hpp>
-#include <boost/spirit/include/phoenix.hpp>
-#include <boost/spirit/include/support_line_pos_iterator.hpp>
-#include <boost/spirit/home/classic/iterator/position_iterator.hpp>
-
-namespace qi = boost::spirit::qi;
-namespace phoenix = boost::phoenix;
-
-typedef std::string::const_iterator BaseIteratorType;
-typedef boost::spirit::line_pos_iterator<BaseIteratorType> PositionIteratorType;
-typedef PositionIteratorType Iterator;
-typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
-typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
-
+#include "src/parser/SpiritParserDefinitions.h"
+#include "src/parser/ExpressionParser.h"
 #include "src/storage/prism/Program.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/Expressions.h"
@@ -113,17 +98,6 @@ namespace storm {
                 }
             };
             
-            // Functor used for displaying error information.
-            struct ErrorHandler {
-                typedef qi::error_handler_result result_type;
-                
-                template<typename T1, typename T2, typename T3, typename T4>
-                qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
-                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << ".");
-                    return qi::fail;
-                }
-            };
-            
             // Functor used for annotating entities with line number information.
             class PositionAnnotation {
             public:
@@ -165,9 +139,6 @@ namespace storm {
              */
             void allowDoubleLiterals(bool flag);
             
-            // A flag that stores wether to allow or forbid double literals in parsed expressions.
-            bool allowDoubleLiteralsFlag;
-            
             // The name of the file being parsed.
             std::string filename;
             
@@ -179,7 +150,6 @@ namespace storm {
             std::string const& getFilename() const;
             
             // A function used for annotating the entities with their position.
-            phoenix::function<ErrorHandler> handler;
             phoenix::function<PositionAnnotation> annotate;
             
             // The starting point of the grammar.
@@ -237,60 +207,18 @@ namespace storm {
             // Rules for identifier parsing.
             qi::rule<Iterator, std::string(), Skipper> identifier;
             
-            // Rules for parsing a composed expression.
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
-            
-            // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
-            boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
-            
             // Parsers that recognize special keywords and model types.
             storm::parser::PrismParser::keywordsStruct keywords_;
             storm::parser::PrismParser::modelTypeStruct modelType_;
             qi::symbols<char, storm::expressions::Expression> identifiers_;
             
+            // Parser used for recognizing expressions.
+            storm::parser::ExpressionParser expressionParser;
+            
             // Helper methods used in the grammar.
             bool isValidIdentifier(std::string const& identifier);
             bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
             
-            storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
-            storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createNotExpression(storm::expressions::Expression e1) const;
-            storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1) const;
-            storm::expressions::Expression createTrueExpression() const;
-            storm::expressions::Expression createFalseExpression() const;
-            storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const;
-            storm::expressions::Expression createIntegerLiteralExpression(int value) const;
-            storm::expressions::Expression createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
-            storm::expressions::Expression createFloorExpression(storm::expressions::Expression e1) const;
-            storm::expressions::Expression createCeilExpression(storm::expressions::Expression e1) const;
-            storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const;
-            
             storm::prism::Constant createUndefinedBooleanConstant(std::string const& newConstant) const;
             storm::prism::Constant createUndefinedIntegerConstant(std::string const& newConstant) const;
             storm::prism::Constant createUndefinedDoubleConstant(std::string const& newConstant) const;
diff --git a/src/parser/SpiritParserDefinitions.h b/src/parser/SpiritParserDefinitions.h
new file mode 100644
index 000000000..feb78f77d
--- /dev/null
+++ b/src/parser/SpiritParserDefinitions.h
@@ -0,0 +1,21 @@
+#ifndef STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
+#define	STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
+
+// Include boost spirit.
+#define BOOST_SPIRIT_USE_PHOENIX_V3
+#include <boost/typeof/typeof.hpp>
+#include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/phoenix.hpp>
+#include <boost/spirit/include/support_line_pos_iterator.hpp>
+#include <boost/spirit/home/classic/iterator/position_iterator.hpp>
+
+namespace qi = boost::spirit::qi;
+namespace phoenix = boost::phoenix;
+
+typedef std::string::const_iterator BaseIteratorType;
+typedef boost::spirit::line_pos_iterator<BaseIteratorType> PositionIteratorType;
+typedef PositionIteratorType Iterator;
+
+typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
+
+#endif /* STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ */
\ No newline at end of file