No - I won't wait for those parsers no more. Part one of some compiliation speed up stuff.

Former-commit-id: 20f6996581 [formerly 680bcd1cbb]
Former-commit-id: 2c60f08dd3

src/adapters/CarlAdapter.h

@@ -51,12 +51,10 @@ namespace cln {
     }
 }
 
+
+#include "NumberAdapter.h"
+
 namespace storm {
-#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS
-    typedef cln::cl_RA RationalNumber;
-#else
-    typedef mpq_class RationalNumber;
-#endif
     typedef carl::Variable RationalFunctionVariable;
     typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial;
     typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;

src/adapters/NumberAdapter.h

@@ -0,0 +1,17 @@
+#pragma once
+
+#include "storm-config.h"
+
+#include <boost/multiprecision/gmp.hpp>
+
+#ifdef STORM_HAVE_CARL
+
+#include <carl/numbers/numbers.h>
+namespace storm {
+#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS
+    typedef cln::cl_RA RationalNumber;
+#else
+    typedef mpq_class RationalNumber;
+#endif
+}
+#endif

src/parser/ExpressionCreator.cpp

@@ -0,0 +1,265 @@
+#include "ExpressionCreator.h"
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/WrongFormatException.h"
+
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace parser {
+        
+        ExpressionCreator::ExpressionCreator(storm::expressions::ExpressionManager const& manager) : manager(manager) {
+            // Intenetionally left empty.
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createIteExpression(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2, storm::expressions::Expression const& e3, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    return storm::expressions::ite(e1, e2, e3);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+
+        storm::expressions::Expression ExpressionCreator::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Or: return e1 || e2; break;
+                        case storm::expressions::OperatorType::Implies: return storm::expressions::implies(e1, e2); break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                storm::expressions::Expression result;
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::And: result = e1 && e2; break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+                return result;
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::GreaterOrEqual: return e1 >= e2; break;
+                        case storm::expressions::OperatorType::Greater: return e1 > e2; break;
+                        case storm::expressions::OperatorType::LessOrEqual: return e1 <= e2; break;
+                        case storm::expressions::OperatorType::Less: return e1 < e2; break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Equal: return e1.hasBooleanType() && e2.hasBooleanType() ? storm::expressions::iff(e1, e2) : e1 == e2; break;
+                        case storm::expressions::OperatorType::NotEqual: return e1 != e2; break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Plus: return e1 + e2; break;
+                        case storm::expressions::OperatorType::Minus: return e1 - e2; break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Times: return e1 * e2; break;
+                        case storm::expressions::OperatorType::Divide: return e1 / e2; break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Power: return e1 ^ e2; break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    if (operatorType) {
+                        switch (operatorType.get()) {
+                            case storm::expressions::OperatorType::Not: return !e1; break;
+                            case storm::expressions::OperatorType::Minus: return -e1; break;
+                            default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                        }
+                    } else {
+                        return e1;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createRationalLiteralExpression(storm::RationalNumber const& 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 manager.rational(value);
+            } else {
+                return manager.boolean(false);
+            }
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createIntegerLiteralExpression(int value, bool& pass) const {
+            if (this->createExpressions) {
+                return manager.integer(value);
+            } else {
+                return manager.boolean(false);
+            }
+        }
+        
+        
+        storm::expressions::Expression ExpressionCreator::createBooleanLiteralExpression(bool value, bool& pass) const {
+            if (this->createExpressions) {
+                return manager.boolean(value);
+            } else {
+                return manager.boolean(false);
+            }
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Min: return storm::expressions::minimum(e1, e2); break;
+                        case storm::expressions::OperatorType::Max: return storm::expressions::maximum(e1, e2); break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const {
+            if (this->createExpressions) {
+                try {
+                    switch (operatorType) {
+                        case storm::expressions::OperatorType::Floor: return storm::expressions::floor(e1); break;
+                        case storm::expressions::OperatorType::Ceil: return storm::expressions::ceil(e1); break;
+                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    pass = false;
+                }
+            }
+            return manager.boolean(false);
+        }
+        
+        storm::expressions::Expression ExpressionCreator::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const {
+            if (this->createExpressions) {
+                STORM_LOG_THROW(this->identifiers != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
+                storm::expressions::Expression const* expression = this->identifiers->find(identifier);
+                if (expression == nullptr) {
+                    pass = false;
+                    return manager.boolean(false);
+                }
+                return *expression;
+            } else {
+                return manager.boolean(false);
+            }
+        }
+        
+        void ExpressionCreator::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
+            
+            if (identifiers_ != nullptr) {
+                createExpressions = true;
+                identifiers = identifiers_;
+            } else {
+                createExpressions = false;
+                identifiers = nullptr;
+            }
+        }
+        
+        void ExpressionCreator::setIdentifierMapping(std::unordered_map<std::string, storm::expressions::Expression> const& identifierMapping) {
+            unsetIdentifierMapping();
+            
+            createExpressions =true;
+            identifiers = new qi::symbols<char, storm::expressions::Expression>();
+            for (auto const& identifierExpressionPair : identifierMapping) {
+                identifiers->add(identifierExpressionPair.first, identifierExpressionPair.second);
+            }
+            deleteIdentifierMapping = true;
+        }
+        
+        void ExpressionCreator::unsetIdentifierMapping() {
+            createExpressions = false;
+            if (deleteIdentifierMapping) {
+                delete this->identifiers;
+                deleteIdentifierMapping = false;
+            }
+            this->identifiers = nullptr;
+        }
+        
+
+
+        
+    }
+}

src/parser/ExpressionCreator.h

@@ -0,0 +1,93 @@
+#pragma once
+#include <memory>
+// Very ugly, but currently we would like to have the symbol table here.
+#include "src/parser/SpiritParserDefinitions.h"
+
+#include <boost/optional.hpp>
+#include "src/adapters/NumberAdapter.h"
+
+namespace storm {
+    
+    namespace expressions {
+        class Expression;
+        class ExpressionManager;
+        enum struct OperatorType;
+    }
+    
+    namespace parser {
+        class ExpressionCreator {
+        public:
+            ExpressionCreator(storm::expressions::ExpressionManager const& manager);
+            
+            virtual ~ExpressionCreator() {
+                if (deleteIdentifierMapping) {
+                    delete this->identifiers;
+                }
+            }
+            
+            /*!
+             * 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_);
+            
+            /*!
+             * 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 identifierMapping A mapping from identifiers to expressions.
+             */
+            void setIdentifierMapping(std::unordered_map<std::string, storm::expressions::Expression> const& identifierMapping);
+            
+            /*!
+             * 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();
+
+            bool getAcceptDoubleLiterals() const {
+                return acceptDoubleLiterals;
+            }
+            
+            void setAcceptDoubleLiterals(bool set = true) {
+                acceptDoubleLiterals = set;
+            }
+            
+                        
+            
+            storm::expressions::Expression createIteExpression(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2, storm::expressions::Expression const& e3, bool& pass) const;
+            
+            storm::expressions::Expression createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
+            storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const;
+            storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const;
+            storm::expressions::Expression createBooleanLiteralExpression(bool value, bool& pass) const;
+            storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
+            storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
+            storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const;
+            
+            
+        private:
+            // The manager responsible for the expressions.
+            storm::expressions::ExpressionManager const& manager;
+            qi::symbols<char, storm::expressions::Expression> const* identifiers = nullptr;
+            
+            bool createExpressions = false;
+            
+            bool acceptDoubleLiterals = true;
+            
+            bool deleteIdentifierMapping = false;
+        
+        };
+    }
+}

src/parser/ExpressionParser.cpp

@@ -4,6 +4,9 @@
 #include "src/exceptions/WrongFormatException.h"
 
 #include "src/utility/constants.h"
+#include "src/parser/ExpressionCreator.h"
+#include "src/storage/expressions/Expression.h"
+
 
 namespace boost {
     namespace spirit {
@@ -33,85 +36,91 @@ namespace boost {
 
 namespace storm {
     namespace parser {
-        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
+        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), invalidIdentifiers_(invalidIdentifiers_) {
+            
+            expressionCreator = new ExpressionCreator(manager);
+            
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
             identifier.name("identifier");
             
             if (allowBacktracking) {
-                floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2, qi::_pass)];
+                floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
             } else {
-                floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2, qi::_pass)];
+                floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
             }
             floorCeilExpression.name("floor/ceil expression");
             
             if (allowBacktracking) {
-                minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> expression[qi::_val = qi::_1] >> +(qi::lit(",") >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1, qi::_pass)]) >> qi::lit(")");
+                minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> expression[qi::_val = qi::_1] >> +(qi::lit(",") >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_a, qi::_1, qi::_pass)]) >> qi::lit(")");
             } else {
-                minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) > expression[qi::_val = qi::_1] > +(qi::lit(",") > expression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1, qi::_pass)]) > qi::lit(")");
+                minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) > expression[qi::_val = qi::_1] > +(qi::lit(",") > expression)[qi::_val = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_a, qi::_1, qi::_pass)]) > qi::lit(")");
             }
             minMaxExpression.name("min/max expression");
             
             if (allowBacktracking) {
-                prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3, qi::_pass)];
+                prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)];
             } else {
-                prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3, qi::_pass)];
+                prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)];
             }
             prefixPowerExpression.name("pow expression");
             
-			identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)];
+			identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionCreator::getIdentifierExpression, phoenix::ref(*expressionCreator), qi::_1, allowBacktracking, qi::_pass)];
             identifierExpression.name("identifier expression");
             
-            literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createRationalLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)];
+            literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&ExpressionCreator::createBooleanLiteralExpression, phoenix::ref(*expressionCreator), true, qi::_pass)]
+                | qi::lit("false")[qi::_val = phoenix::bind(&ExpressionCreator::createBooleanLiteralExpression, phoenix::ref(*expressionCreator), false, qi::_pass)]
+                | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionCreator::createRationalLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)]
+                | qi::int_[qi::_val = phoenix::bind(&ExpressionCreator::createIntegerLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
             literalExpression.name("literal expression");
             
             atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression;
             atomicExpression.name("atomic expression");
             
-            unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createUnaryExpression, phoenix::ref(*this), qi::_1, qi::_2, qi::_pass)];
+            unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
             unaryExpression.name("unary expression");
             
             if (allowBacktracking) {
-                infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             } else {
-                infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             }
             infixPowerExpression.name("power expression");
             
             if (allowBacktracking) {
-                multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             } else {
-                multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             }
             multiplicationExpression.name("multiplication expression");
             
-            plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             plusExpression.name("plus expression");
             
             if (allowBacktracking) {
-                relativeExpression = plusExpression[qi::_val = qi::_1] >> -(relationalOperator_ >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                relativeExpression = plusExpression[qi::_val = qi::_1] >> -(relationalOperator_ >> plusExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createRelationalExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             } else {
-                relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createRelationalExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             }
             relativeExpression.name("relative expression");
                         
-            equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             equalityExpression.name("equality expression");
             
             if (allowBacktracking) {
-                andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createAndExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             } else {
-                andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createAndExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             }
             andExpression.name("and expression");
             
             if (allowBacktracking) {
-                orExpression = andExpression[qi::_val = qi::_1] >> *(orOperator_ >> andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                orExpression = andExpression[qi::_val = qi::_1] >> *(orOperator_ >> andExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createOrExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             } else {
-                orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)];
+                orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createOrExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             }
             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, qi::_pass)];
+            iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
             iteExpression.name("if-then-else expression");
             
             expression %= iteExpression;
@@ -154,240 +163,22 @@ namespace storm {
         }
         
         void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
-            if (identifiers_ != nullptr) {
-                this->createExpressions = true;
-                this->identifiers_ = identifiers_;
-            } else {
-                this->createExpressions = false;
-                this->identifiers_ = nullptr;
-            }
+            expressionCreator->setIdentifierMapping(identifiers_);
         }
 
         void ExpressionParser::setIdentifierMapping(std::unordered_map<std::string, storm::expressions::Expression> const& identifierMapping) {
-            unsetIdentifierMapping();
-            this->createExpressions = true;
-            this->identifiers_ = new qi::symbols<char, storm::expressions::Expression>();
-            for (auto const& identifierExpressionPair : identifierMapping) {
-                this->identifiers_->add(identifierExpressionPair.first, identifierExpressionPair.second);
-            }
-            deleteIdentifierMapping = true;
+            expressionCreator->setIdentifierMapping(identifierMapping);
         }
 
         void ExpressionParser::unsetIdentifierMapping() {
-            this->createExpressions = false;
-            if (deleteIdentifierMapping) {
-                delete this->identifiers_;
-                deleteIdentifierMapping = false;
-            }
-            this->identifiers_ = nullptr;
+            expressionCreator->unsetIdentifierMapping();
         }
         
         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, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    return storm::expressions::ite(e1, e2, e3);
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-                
-        storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Or: return e1 || e2; break;
-                        case storm::expressions::OperatorType::Implies: return storm::expressions::implies(e1, e2); break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                storm::expressions::Expression result;
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::And: result = e1 && e2; break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-                return result;
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::GreaterOrEqual: return e1 >= e2; break;
-                        case storm::expressions::OperatorType::Greater: return e1 > e2; break;
-                        case storm::expressions::OperatorType::LessOrEqual: return e1 <= e2; break;
-                        case storm::expressions::OperatorType::Less: return e1 < e2; break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Equal: return e1.hasBooleanType() && e2.hasBooleanType() ? storm::expressions::iff(e1, e2) : e1 == e2; break;
-                        case storm::expressions::OperatorType::NotEqual: return e1 != e2; break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Plus: return e1 + e2; break;
-                        case storm::expressions::OperatorType::Minus: return e1 - e2; break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Times: return e1 * e2; break;
-                        case storm::expressions::OperatorType::Divide: return e1 / e2; break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Power: return e1 ^ e2; break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-                
-        storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    if (operatorType) {
-                        switch (operatorType.get()) {
-                            case storm::expressions::OperatorType::Not: return !e1; break;
-                            case storm::expressions::OperatorType::Minus: return -e1; break;
-                            default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                        }
-                    } else {
-                        return e1;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
+            expressionCreator->setAcceptDoubleLiterals(flag);
         }
+                        
                 
-        storm::expressions::Expression ExpressionParser::createRationalLiteralExpression(storm::RationalNumber const& 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 manager->rational(value);
-            } else {
-                return manager->boolean(false);
-            }
-        }
-        
-        storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value, bool& pass) const {
-            if (this->createExpressions) {
-                return manager->integer(value);
-            } else {
-                return manager->boolean(false);
-            }
-        }
-        
-        storm::expressions::Expression ExpressionParser::createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Min: return storm::expressions::minimum(e1, e2); break;
-                        case storm::expressions::OperatorType::Max: return storm::expressions::maximum(e1, e2); break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-
-        storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const {
-            if (this->createExpressions) {
-                try {
-                    switch (operatorType) {
-                        case storm::expressions::OperatorType::Floor: return storm::expressions::floor(e1); break;
-                        case storm::expressions::OperatorType::Ceil: return storm::expressions::ceil(e1); break;
-                        default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
-                    }
-                } catch (storm::exceptions::InvalidTypeException const& e) {
-                    pass = false;
-                }
-            }
-            return manager->boolean(false);
-        }
-        
-        storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const {
-            if (this->createExpressions) {
-                STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
-                storm::expressions::Expression const* expression = this->identifiers_->find(identifier);
-                if (expression == nullptr) {
-                    pass = false;
-                    return manager->boolean(false);
-                }
-                return *expression;
-            } else {
-                return manager->boolean(false);
-            }
-        }
-        
         bool ExpressionParser::isValidIdentifier(std::string const& identifier) {
             if (this->invalidIdentifiers_.find(identifier) != nullptr) {
                 return false;

src/parser/ExpressionParser.h

@@ -1,16 +1,19 @@
-#ifndef STORM_PARSER_EXPRESSIONPARSER_H_
-#define	STORM_PARSER_EXPRESSIONPARSER_H_
+#pragma once
 
 #include <sstream>
 
 #include "src/parser/SpiritParserDefinitions.h"
 #include "src/parser/SpiritErrorHandler.h"
-#include "src/storage/expressions/Expression.h"
-#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/expressions/OperatorType.h"
 
-#include "src/adapters/CarlAdapter.h"
+#include "src/adapters/NumberAdapter.h"
 
 namespace storm {
+    namespace expressions {
+        class Expression;
+        class ExpressionManager;
+    }
+    
     namespace parser {
         template<typename NumberType>
         struct RationalPolicies : boost::spirit::qi::strict_real_policies<NumberType> {
@@ -22,6 +25,8 @@ namespace storm {
             static bool parse_inf(It&, It const&, Attr&) { return false; }
         };
         
+        class ExpressionCreator;
+        
         class ExpressionParser : public qi::grammar<Iterator, storm::expressions::Expression(), Skipper> {
         public:
             /*!
@@ -197,33 +202,9 @@ namespace storm {
             // A parser used for recognizing the operators at the "power" precedence level.
             prefixPowerOperatorStruct prefixPowerOperator_;
             
-            struct trueFalseOperatorStruct : qi::symbols<char, storm::expressions::Expression> {
-                trueFalseOperatorStruct(storm::expressions::ExpressionManager const& manager) {
-                    add
-                    ("true", manager.boolean(true))
-                    ("false", manager.boolean(false));
-                }
-            };
-            
-            // A parser used for recognizing the literals true and false.
-            trueFalseOperatorStruct trueFalse_;
-            
-            // The manager responsible for the expressions.
-            std::shared_ptr<storm::expressions::ExpressionManager const> manager;
-            
-            // 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;
             
-            // A flag that indicates whether the mapping must be deleted on unsetting.
-            bool deleteIdentifierMapping;
+            ExpressionCreator* expressionCreator;
             
-            // 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> invalidIdentifiers_;
@@ -250,21 +231,6 @@ namespace storm {
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
             boost::spirit::qi::real_parser<storm::RationalNumber, RationalPolicies<storm::RationalNumber>> rationalLiteral_;
             
-            // Helper functions to create expressions.
-            storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3, bool& pass) const;
-            storm::expressions::Expression createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
-            storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const;
-            storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const;
-            storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
-            storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const;
             
             bool isValidIdentifier(std::string const& identifier);
             
@@ -274,4 +240,3 @@ namespace storm {
     } // namespace parser
 } // namespace storm
 
-#endif /* STORM_PARSER_EXPRESSIONPARSER_H_ */

src/parser/FormulaParser.cpp

@@ -11,174 +11,12 @@
 #include "src/exceptions/WrongFormatException.h"
 
 #include "src/storage/expressions/ExpressionEvaluator.h"
+#include "FormulaParserGrammar.h"
+#include "src/storage/expressions/ExpressionManager.h"
 
 namespace storm {
     namespace parser {
         
-        class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<std::shared_ptr<storm::logic::Formula const>>(), Skipper> {
-        public:
-            FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
-            
-            FormulaParserGrammar(FormulaParserGrammar const& other) = default;
-            FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default;
-            
-            /*!
-             * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used
-             * to substitute special identifiers in the formula by expressions.
-             *
-             * @param identifier The identifier that is supposed to be substituted.
-             * @param expression The expression it is to be substituted with.
-             */
-            void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
-            
-        private:
-            struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
-                keywordsStruct() {
-                    add
-                    ("true", 1)
-                    ("false", 2)
-                    ("min", 3)
-                    ("max", 4)
-                    ("F", 5)
-                    ("G", 6)
-                    ("X", 7);
-                }
-            };
-            
-            // A parser used for recognizing the keywords.
-            keywordsStruct keywords_;
-            
-            struct relationalOperatorStruct : qi::symbols<char, storm::logic::ComparisonType> {
-                relationalOperatorStruct() {
-                    add
-                    (">=", storm::logic::ComparisonType::GreaterEqual)
-                    (">", storm::logic::ComparisonType::Greater)
-                    ("<=", storm::logic::ComparisonType::LessEqual)
-                    ("<", storm::logic::ComparisonType::Less);
-                }
-            };
-            
-            // A parser used for recognizing the operators at the "relational" precedence level.
-            relationalOperatorStruct relationalOperator_;
-            
-            struct binaryBooleanOperatorStruct : qi::symbols<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
-                binaryBooleanOperatorStruct() {
-                    add
-                    ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And)
-                    ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or);
-                }
-            };
-            
-            // A parser used for recognizing the operators at the "binary" precedence level.
-            binaryBooleanOperatorStruct binaryBooleanOperator_;
-            
-            struct unaryBooleanOperatorStruct : qi::symbols<char, storm::logic::UnaryBooleanStateFormula::OperatorType> {
-                unaryBooleanOperatorStruct() {
-                    add
-                    ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
-                }
-            };
-            
-            // A parser used for recognizing the operators at the "unary" precedence level.
-            unaryBooleanOperatorStruct unaryBooleanOperator_;
-            
-            struct optimalityOperatorStruct : qi::symbols<char, storm::OptimizationDirection> {
-                optimalityOperatorStruct() {
-                    add
-                    ("min", storm::OptimizationDirection::Minimize)
-                    ("max", storm::OptimizationDirection::Maximize);
-                }
-            };
-            
-            // A parser used for recognizing the optimality operators.
-            optimalityOperatorStruct optimalityOperator_;
-            
-            struct rewardMeasureTypeStruct : qi::symbols<char, storm::logic::RewardMeasureType> {
-                rewardMeasureTypeStruct() {
-                    add
-                    ("exp", storm::logic::RewardMeasureType::Expectation)
-                    ("var", storm::logic::RewardMeasureType::Variance);
-                }
-            };
-
-            // A parser used for recognizing the reward measure types.
-            rewardMeasureTypeStruct rewardMeasureType_;
-            
-            // The manager used to parse expressions.
-            std::shared_ptr<storm::expressions::ExpressionManager const> manager;
-            
-            // Parser and manager used for recognizing expressions.
-            storm::parser::ExpressionParser expressionParser;
-            
-            // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions
-            // they are to be replaced with.
-            qi::symbols<char, storm::expressions::Expression> identifiers_;
-            
-            qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula const>>(), Skipper> start;
-            
-            qi::rule<Iterator, storm::logic::OperatorInformation(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<storm::expressions::Expression>>, Skipper> operatorInformation;
-            qi::rule<Iterator, storm::logic::RewardMeasureType(), Skipper> rewardMeasureType;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> probabilityOperator;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardOperator;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> timeOperator;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageOperator;
-            
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simplePathFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> operatorFormula;
-            qi::rule<Iterator, std::string(), Skipper> label;
-            qi::rule<Iterator, std::string(), Skipper> rewardModelName;
-            
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> andStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> orStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> notStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> labelFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> expressionFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
-            
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> conditionalFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> eventuallyFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> nextFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> globallyFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> untilFormula;
-            qi::rule<Iterator, boost::variant<std::pair<double, double>, uint_fast64_t>(), Skipper> timeBound;
-            
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> cumulativeRewardFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
-            
-            // 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;
-            
-            // Methods that actually create the expression objects.
-            std::shared_ptr<storm::logic::Formula const> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
-            std::shared_ptr<storm::logic::Formula const> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
-            std::shared_ptr<storm::logic::Formula const> createLongRunAverageRewardFormula() const;
-            std::shared_ptr<storm::logic::Formula const> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
-            std::shared_ptr<storm::logic::Formula const> createBooleanLiteralFormula(bool literal) const;
-            std::shared_ptr<storm::logic::Formula const> createAtomicLabelFormula(std::string const& label) const;
-            std::shared_ptr<storm::logic::Formula const> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula);
-            std::shared_ptr<storm::logic::Formula const> createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const;
-            storm::logic::OperatorInformation createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const;
-            std::shared_ptr<storm::logic::Formula const> createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
-            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
-            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
-            
-            // An error handler function.
-            phoenix::function<SpiritErrorHandler> handler;
-        };
-        
         FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : manager(manager), grammar(new FormulaParserGrammar(manager)) {
             // Intentionally left empty.
         }
@@ -256,278 +94,5 @@ namespace storm {
             grammar->addIdentifierExpression(identifier, expression);
         }
                 
-        FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), manager(manager), expressionParser(*manager, keywords_, true, true) {
-            // Register all variables so we can parse them in the expressions.
-            for (auto variableTypePair : *manager) {
-                identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);
-            }
-            // Set the identifier mapping to actually generate expressions.
-            expressionParser.setIdentifierMapping(&identifiers_);
-            
-            longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))];
-            longRunAverageRewardFormula.name("long run average reward formula");
-            
-            instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
-            instantaneousRewardFormula.name("instantaneous reward formula");
-            
-            cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
-            cumulativeRewardFormula.name("cumulative reward formula");
-            
-            rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula;
-            rewardPathFormula.name("reward path formula");
-            
-            expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
-            expressionFormula.name("expression formula");
-            
-            label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]];
-            label.name("label");
-            
-            labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)];
-            labelFormula.name("label formula");
-            
-            booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
-            booleanLiteralFormula.name("boolean literal formula");
-            
-            operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator;
-            operatorFormula.name("operator formulas");
-            
-            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
-            atomicStateFormula.name("atomic state formula");
-
-            notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
-            notStateFormula.name("negation formula");
-            
-            eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
-            eventuallyFormula.name("eventually formula");
-            
-            globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
-            globallyFormula.name("globally formula");
-            
-            nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
-            nextFormula.name("next formula");
-            
-            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula;
-            pathFormulaWithoutUntil.name("path formula");
-            
-            untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
-            untilFormula.name("until formula");
-            
-            conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
-            conditionalFormula.name("conditional formula");
-            
-            timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") >  qi::uint_)[qi::_val = qi::_1];
-            timeBound.name("time bound");
-            
-            pathFormula = conditionalFormula(qi::_r1);
-            pathFormula.name("path formula");
-            
-            rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]");
-            rewardMeasureType.name("reward measure type");
-            
-            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
-            operatorInformation.name("operator information");
-            
-            longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
-            longRunAverageOperator.name("long-run average operator");
-            
-            rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
-            rewardModelName.name("reward model name");
-            
-            rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)];
-            rewardOperator.name("reward operator");
-            
-            timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
-            timeOperator.name("time operator");
-            
-            probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
-            probabilityOperator.name("probability operator");
-            
-            andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
-            andStateFormula.name("and state formula");
-            
-            orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
-            orStateFormula.name("or state formula");
-            
-            stateFormula = (orStateFormula);
-            stateFormula.name("state formula");
-            
-            start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
-            start.name("start");
-            
-            //Enable the following lines to print debug output for most the rules.
-            /*
-            debug(start);
-            debug(stateFormula);
-            debug(orStateFormula);
-            debug(andStateFormula);
-            debug(probabilityOperator);
-            debug(rewardOperator);
-            debug(longRunAverageOperator);
-            debug(timeOperator);
-            debug(pathFormulaWithoutUntil);
-            debug(pathFormula);
-//            debug(conditionalFormula);
-            debug(nextFormula);
-            debug(globallyFormula);
-//            debug(eventuallyFormula);
-            debug(atomicStateFormula);
-            debug(booleanLiteralFormula);
-            debug(labelFormula);
-            debug(expressionFormula);
-            debug(rewardPathFormula);
-            debug(cumulativeRewardFormula);
-            debug(instantaneousRewardFormula);
-            */
-
-            // Enable error reporting.
-            qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(timeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-        }
-        
-        void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
-            this->identifiers_.add(identifier, expression);
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
-            if (timeBound.which() == 0) {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
-            } else {
-                double timeBoundAsDouble = boost::get<double>(timeBound);
-                STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Instantaneous reward property must have non-negative bound.");
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(timeBoundAsDouble));
-            }
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
-            if (timeBound.which() == 0) {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
-            } else {
-                double timeBoundAsDouble = boost::get<double>(timeBound);
-                STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
-            }
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageRewardFormula());
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
-            STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type.");
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicExpressionFormula(expression));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BooleanLiteralFormula(literal));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicLabelFormula(label));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            if (timeBound) {
-                if (timeBound.get().which() == 0) {
-                    std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
-                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second));
-                } else {
-                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
-                }
-            } else {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::EventuallyFormula(subformula, context));
-            }
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
-            if (timeBound) {
-                if (timeBound.get().which() == 0) {
-                    std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
-                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second));
-                } else {
-                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
-                }
-            } else {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
-            }
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
-        }
-        
-        storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const {
-            if (comparisonType && threshold) {
-                storm::expressions::ExpressionEvaluator<storm::RationalNumber> evaluator(*manager);
-                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<RationalNumber>(comparisonType.get(), evaluator.asRational(threshold.get())));
-            } else {
-                return storm::logic::OperatorInformation(optimizationDirection, boost::none);
-            }
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
-            if (rewardMeasureType) {
-                measureType = rewardMeasureType.get();
-            }
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
-            storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
-            if (rewardMeasureType) {
-                measureType = rewardMeasureType.get();
-            }
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
-        }
-        
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
-            if (operatorType) {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
-            } else {
-                return subformula;
-            }
-        }
-
     } // namespace parser
 } // namespace storm

src/parser/FormulaParser.h

@@ -21,7 +21,7 @@ namespace storm {
         
         class FormulaParser {
         public:
-            FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
+            FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
             FormulaParser(storm::prism::Program const& program);
             
             FormulaParser(FormulaParser const& other);

src/parser/FormulaParserGrammar.cpp

@@ -0,0 +1,281 @@
+#include "FormulaParserGrammar.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+    namespace parser {
+        
+        FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), manager(manager), expressionParser(*manager, keywords_, true, true) {
+            // Register all variables so we can parse them in the expressions.
+            for (auto variableTypePair : *manager) {
+                identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);
+            }
+            // Set the identifier mapping to actually generate expressions.
+            expressionParser.setIdentifierMapping(&identifiers_);
+            
+            longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))];
+            longRunAverageRewardFormula.name("long run average reward formula");
+            
+            instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
+            instantaneousRewardFormula.name("instantaneous reward formula");
+            
+            cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
+            cumulativeRewardFormula.name("cumulative reward formula");
+            
+            rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula;
+            rewardPathFormula.name("reward path formula");
+            
+            expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
+            expressionFormula.name("expression formula");
+            
+            label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]];
+            label.name("label");
+            
+            labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)];
+            labelFormula.name("label formula");
+            
+            booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
+            booleanLiteralFormula.name("boolean literal formula");
+            
+            operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator;
+            operatorFormula.name("operator formulas");
+            
+            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
+            atomicStateFormula.name("atomic state formula");
+            
+            notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
+            notStateFormula.name("negation formula");
+            
+            eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
+            eventuallyFormula.name("eventually formula");
+            
+            globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
+            globallyFormula.name("globally formula");
+            
+            nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
+            nextFormula.name("next formula");
+            
+            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula;
+            pathFormulaWithoutUntil.name("path formula");
+            
+            untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            untilFormula.name("until formula");
+            
+            conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
+            conditionalFormula.name("conditional formula");
+            
+            timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") >  qi::uint_)[qi::_val = qi::_1];
+            timeBound.name("time bound");
+            
+            pathFormula = conditionalFormula(qi::_r1);
+            pathFormula.name("path formula");
+            
+            rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]");
+            rewardMeasureType.name("reward measure type");
+            
+            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
+            operatorInformation.name("operator information");
+            
+            longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            longRunAverageOperator.name("long-run average operator");
+            
+            rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
+            rewardModelName.name("reward model name");
+            
+            rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)];
+            rewardOperator.name("reward operator");
+            
+            timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+            timeOperator.name("time operator");
+            
+            probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            probabilityOperator.name("probability operator");
+            
+            andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
+            andStateFormula.name("and state formula");
+            
+            orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
+            orStateFormula.name("or state formula");
+            
+            stateFormula = (orStateFormula);
+            stateFormula.name("state formula");
+            
+            start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
+            start.name("start");
+            
+            //Enable the following lines to print debug output for most the rules.
+            /*
+             debug(start);
+             debug(stateFormula);
+             debug(orStateFormula);
+             debug(andStateFormula);
+             debug(probabilityOperator);
+             debug(rewardOperator);
+             debug(longRunAverageOperator);
+             debug(timeOperator);
+             debug(pathFormulaWithoutUntil);
+             debug(pathFormula);
+             //            debug(conditionalFormula);
+             debug(nextFormula);
+             debug(globallyFormula);
+             //            debug(eventuallyFormula);
+             debug(atomicStateFormula);
+             debug(booleanLiteralFormula);
+             debug(labelFormula);
+             debug(expressionFormula);
+             debug(rewardPathFormula);
+             debug(cumulativeRewardFormula);
+             debug(instantaneousRewardFormula);
+             */
+            
+            // Enable error reporting.
+            qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(timeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+        }
+        
+        void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
+            this->identifiers_.add(identifier, expression);
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
+            if (timeBound.which() == 0) {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
+            } else {
+                double timeBoundAsDouble = boost::get<double>(timeBound);
+                STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Instantaneous reward property must have non-negative bound.");
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(timeBoundAsDouble));
+            }
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
+            if (timeBound.which() == 0) {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
+            } else {
+                double timeBoundAsDouble = boost::get<double>(timeBound);
+                STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
+            }
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageRewardFormula());
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
+            STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type.");
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicExpressionFormula(expression));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BooleanLiteralFormula(literal));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicLabelFormula(label));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            if (timeBound) {
+                if (timeBound.get().which() == 0) {
+                    std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
+                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second));
+                } else {
+                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
+                }
+            } else {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::EventuallyFormula(subformula, context));
+            }
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
+            if (timeBound) {
+                if (timeBound.get().which() == 0) {
+                    std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
+                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second));
+                } else {
+                    return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
+                }
+            } else {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
+            }
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
+        }
+        
+        storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const {
+            if (comparisonType && threshold) {
+                storm::expressions::ExpressionEvaluator<storm::RationalNumber> evaluator(*manager);
+                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<RationalNumber>(comparisonType.get(), evaluator.asRational(threshold.get())));
+            } else {
+                return storm::logic::OperatorInformation(optimizationDirection, boost::none);
+            }
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
+            if (rewardMeasureType) {
+                measureType = rewardMeasureType.get();
+            }
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
+            if (rewardMeasureType) {
+                measureType = rewardMeasureType.get();
+            }
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
+            if (operatorType) {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
+            } else {
+                return subformula;
+            }
+        }
+
+    }
+}

src/parser/FormulaParserGrammar.h

@@ -0,0 +1,185 @@
+#pragma once
+
+#include <memory>
+#include <fstream>
+
+#include "src/parser/SpiritErrorHandler.h"
+#include "src/exceptions/WrongFormatException.h"
+#include "src/logic/Formulas.h"
+#include "src/parser/ExpressionParser.h"
+
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+namespace storm {
+    namespace logic {
+        class Formula;
+    }
+    
+    namespace parser {
+        
+        class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<std::shared_ptr<storm::logic::Formula const>>(), Skipper> {
+        public:
+            FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
+            
+            FormulaParserGrammar(FormulaParserGrammar const& other) = default;
+            FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default;
+            
+            /*!
+             * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used
+             * to substitute special identifiers in the formula by expressions.
+             *
+             * @param identifier The identifier that is supposed to be substituted.
+             * @param expression The expression it is to be substituted with.
+             */
+            void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
+            
+        private:
+            struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
+                keywordsStruct() {
+                    add
+                    ("true", 1)
+                    ("false", 2)
+                    ("min", 3)
+                    ("max", 4)
+                    ("F", 5)
+                    ("G", 6)
+                    ("X", 7);
+                }
+            };
+            
+            // A parser used for recognizing the keywords.
+            keywordsStruct keywords_;
+            
+            struct relationalOperatorStruct : qi::symbols<char, storm::logic::ComparisonType> {
+                relationalOperatorStruct() {
+                    add
+                    (">=", storm::logic::ComparisonType::GreaterEqual)
+                    (">", storm::logic::ComparisonType::Greater)
+                    ("<=", storm::logic::ComparisonType::LessEqual)
+                    ("<", storm::logic::ComparisonType::Less);
+                }
+            };
+            
+            // A parser used for recognizing the operators at the "relational" precedence level.
+            relationalOperatorStruct relationalOperator_;
+            
+            struct binaryBooleanOperatorStruct : qi::symbols<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
+                binaryBooleanOperatorStruct() {
+                    add
+                    ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And)
+                    ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or);
+                }
+            };
+            
+            // A parser used for recognizing the operators at the "binary" precedence level.
+            binaryBooleanOperatorStruct binaryBooleanOperator_;
+            
+            struct unaryBooleanOperatorStruct : qi::symbols<char, storm::logic::UnaryBooleanStateFormula::OperatorType> {
+                unaryBooleanOperatorStruct() {
+                    add
+                    ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
+                }
+            };
+            
+            // A parser used for recognizing the operators at the "unary" precedence level.
+            unaryBooleanOperatorStruct unaryBooleanOperator_;
+            
+            struct optimalityOperatorStruct : qi::symbols<char, storm::OptimizationDirection> {
+                optimalityOperatorStruct() {
+                    add
+                    ("min", storm::OptimizationDirection::Minimize)
+                    ("max", storm::OptimizationDirection::Maximize);
+                }
+            };
+            
+            // A parser used for recognizing the optimality operators.
+            optimalityOperatorStruct optimalityOperator_;
+            
+            struct rewardMeasureTypeStruct : qi::symbols<char, storm::logic::RewardMeasureType> {
+                rewardMeasureTypeStruct() {
+                    add
+                    ("exp", storm::logic::RewardMeasureType::Expectation)
+                    ("var", storm::logic::RewardMeasureType::Variance);
+                }
+            };
+            
+            // A parser used for recognizing the reward measure types.
+            rewardMeasureTypeStruct rewardMeasureType_;
+            
+            // The manager used to parse expressions.
+            std::shared_ptr<storm::expressions::ExpressionManager const> manager;
+            
+            // Parser and manager used for recognizing expressions.
+            storm::parser::ExpressionParser expressionParser;
+            
+            // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions
+            // they are to be replaced with.
+            qi::symbols<char, storm::expressions::Expression> identifiers_;
+            
+            qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula const>>(), Skipper> start;
+            
+            qi::rule<Iterator, storm::logic::OperatorInformation(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<storm::expressions::Expression>>, Skipper> operatorInformation;
+            qi::rule<Iterator, storm::logic::RewardMeasureType(), Skipper> rewardMeasureType;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> probabilityOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> timeOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageOperator;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simplePathFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> operatorFormula;
+            qi::rule<Iterator, std::string(), Skipper> label;
+            qi::rule<Iterator, std::string(), Skipper> rewardModelName;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> andStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> orStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> notStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> labelFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> expressionFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> conditionalFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> eventuallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> nextFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> globallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> untilFormula;
+            qi::rule<Iterator, boost::variant<std::pair<double, double>, uint_fast64_t>(), Skipper> timeBound;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> cumulativeRewardFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
+            
+            // 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;
+            
+            // Methods that actually create the expression objects.
+            std::shared_ptr<storm::logic::Formula const> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
+            std::shared_ptr<storm::logic::Formula const> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
+            std::shared_ptr<storm::logic::Formula const> createLongRunAverageRewardFormula() const;
+            std::shared_ptr<storm::logic::Formula const> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
+            std::shared_ptr<storm::logic::Formula const> createBooleanLiteralFormula(bool literal) const;
+            std::shared_ptr<storm::logic::Formula const> createAtomicLabelFormula(std::string const& label) const;
+            std::shared_ptr<storm::logic::Formula const> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula);
+            std::shared_ptr<storm::logic::Formula const> createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const;
+            storm::logic::OperatorInformation createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const;
+            std::shared_ptr<storm::logic::Formula const> createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
+            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
+            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
+            
+            // An error handler function.
+            phoenix::function<SpiritErrorHandler> handler;
+        };
+
+    }
+}

src/parser/PgclParser.cpp

@@ -1,10 +1,3 @@
-/* 
- * File:   PgclParser.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 1. April 2015, 19:12
- */
-
 #include "src/parser/PgclParser.h"
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"
@@ -60,22 +53,24 @@ namespace storm {
         }
         
         PgclParser::PgclParser(std::string const& filename, Iterator first) :
-            PgclParser::base_type(program, "PGCL grammar"),
-            annotate(first),
-            expressionManager(std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager())),
-            expressionParser(*expressionManager, invalidIdentifiers) {
+        PgclParser::base_type(program, "PGCL grammar"),
+        annotate(first),
+        expressionManager(std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager())),
+        expressionParser(*expressionManager, invalidIdentifiers)
+        {
             this->enableExpressions();
             /*
              * PGCL grammar is defined here
              */
             // Rough program structure
-            program               = (qi::lit("function ") >> programName >> qi::lit("(") >> -(doubleDeclaration % qi::lit(",")) >> qi::lit(")") >> qi::lit("{") >>
-                                        variableDeclarations >>
-                                        sequenceOfStatements >>
+            program               = (qi::lit("function ") > programName > qi::lit("(") > -(doubleDeclaration % qi::lit(",")) > qi::lit(")") > qi::lit("{") >
+                                        variableDeclarations >
+                                        sequenceOfStatements >
                                     qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createProgram, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)];
             sequenceOfStatements %= +(statement);
+            sequenceOfStatements.name("sequence of statements");
             
-            variableDeclarations %= qi::lit("var") >> qi::lit("{") >> +(integerDeclaration | booleanDeclaration) >> qi::lit("}");
+            variableDeclarations %= qi::lit("var") > qi::lit("{") > +(integerDeclaration | booleanDeclaration) > qi::lit("}");
             variableDeclarations.name("variable declarations");
                 
             // Statements
@@ -86,32 +81,39 @@ namespace storm {
             // Simple statements
             doubleDeclaration           = (qi::lit("double ") >> variableName)[qi::_val = phoenix::bind(&PgclParser::declareDoubleVariable, phoenix::ref(*this), qi::_1)];
             integerDeclaration = (qi::lit("int ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createIntegerDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)];
+            integerDeclaration.name("integer declaration");
             booleanDeclaration = (qi::lit("bool ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createBooleanDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)];
-
-            assignmentStatement         = (variableName >> qi::lit(":=") >> (expression | uniformExpression) >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createAssignmentStatement, phoenix::ref(*this), qi::_1, qi::_2)];
-            observeStatement            = (qi::lit("observe") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createObserveStatement, phoenix::ref(*this), qi::_1)];
+            booleanDeclaration.name("boolean declaration");
+            
+            assignmentStatement         = (variableName > qi::lit(":=") > (expression | uniformExpression) > qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createAssignmentStatement, phoenix::ref(*this), qi::_1, qi::_2)];
+            observeStatement            = (qi::lit("observe") > qi::lit("(") >> booleanCondition >> qi::lit(")") > qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createObserveStatement, phoenix::ref(*this), qi::_1)];
 
             // Compound statements
-            ifElseStatement        = (qi::lit("if") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >>
+            ifElseStatement        = (qi::lit("if") > qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >>
                                          sequenceOfStatements >>
                                      qi::lit("}") >> -(qi::lit("else") >> qi::lit("{") >>
                                          sequenceOfStatements >>
                                      qi::lit("}")))
                                      [qi::_val = phoenix::bind(&PgclParser::createIfElseStatement, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+            ifElseStatement.name("if/else statement");
             branchStatement        = nondeterministicBranch | probabilisticBranch;
-            loopStatement          = (qi::lit("while") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >>
+            loopStatement          = (qi::lit("while") > qi::lit("(") > booleanCondition > qi::lit(")") > qi::lit("{") >>
                                          sequenceOfStatements >>
                                      qi::lit("}"))
                                      [qi::_val = phoenix::bind(&PgclParser::createLoopStatement, phoenix::ref(*this), qi::_1, qi::_2)];
+            loopStatement.name("loop statement");
             nondeterministicBranch = (qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> qi::lit("[]") >> qi::lit("{") >> sequenceOfStatements>> qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createNondeterministicBranch, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilisticBranch    = (qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> qi::lit("[") >> expression >> qi::lit("]") >> qi::lit("{") >> sequenceOfStatements >> qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createProbabilisticBranch, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)];
 
             // Expression and condition building, and basic identifiers
             expression       %= expressionParser;
+            expression.name("expression");
             booleanCondition  = expressionParser[qi::_val = phoenix::bind(&PgclParser::createBooleanExpression, phoenix::ref(*this), qi::_1)];
             uniformExpression = (qi::lit("unif") >> qi::lit("(") >> qi::int_ >> qi::lit(",") >> qi::int_ >> qi::lit(")"))[qi::_val = phoenix::bind(&PgclParser::createUniformExpression, phoenix::ref(*this), qi::_1, qi::_2)];
-            variableName     %= (+(qi::alnum | qi::lit("_"))) - (qi::lit("int") >> +(qi::alnum | qi::lit("_")));
+            variableName     %= (+(qi::alnum | qi::lit("_"))) - invalidIdentifiers;
+            variableName.name("variable name");
             programName      %= +(qi::alnum | qi::lit("_"));
+            programName.name("program name");
 
             // Enables location tracking for important entities
             auto setLocationInfoFunction = this->annotate(*qi::_val, qi::_1, qi::_3);
@@ -121,8 +123,24 @@ namespace storm {
             qi::on_success(probabilisticBranch, setLocationInfoFunction);
             qi::on_success(loopStatement, setLocationInfoFunction);
             qi::on_success(ifElseStatement, setLocationInfoFunction);
-            qi::on_success(integerDeclaration, setLocationInfoFunction);
-
+                
+            // Enable error reporting.
+            qi::on_error<qi::fail>(program, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(variableDeclarations, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(integerDeclaration, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(booleanDeclaration, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            
+            qi::on_error<qi::fail>(assignmentStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(observeStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(ifElseStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(loopStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(branchStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            
+            
+            qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(booleanCondition, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(uniformExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            
             // Adds dummy to the 0-th location.
             std::shared_ptr<storm::pgcl::AssignmentStatement> dummy(new storm::pgcl::AssignmentStatement());
             this->locationToStatement.insert(this->locationToStatement.begin(), dummy);
@@ -139,15 +157,20 @@ namespace storm {
          * throw excpetions in case something unexpected was parsed, e.g.
          * (x+5) as a boolean expression, or types of assignments don't match.
          */
-        storm::pgcl::PgclProgram PgclParser::createProgram(std::string const& programName, boost::optional<std::vector<storm::expressions::Variable>> parameters, std::vector<std::shared_ptr<storm::pgcl::AssignmentStatement>> const& variableDeclarations, std::vector<std::shared_ptr<storm::pgcl::Statement>> statements) {
+        storm::pgcl::PgclProgram PgclParser::createProgram(std::string const& programName, boost::optional<std::vector<storm::expressions::Variable>> parameters, std::vector<std::shared_ptr<storm::pgcl::VariableDeclaration>> const& variableDeclarations, std::vector<std::shared_ptr<storm::pgcl::Statement>> const&  statements) {
             // Creates an empty paramter list in case no parameters were given.
             std::vector<storm::expressions::Variable> params;
             if(parameters != boost::none) {
                 params = *parameters;
             }
+            std::vector<storm::pgcl::VariableDeclaration> declarations;
+            for (auto const& decl : variableDeclarations) {
+                declarations.push_back(*decl);
+            }
+            
             // Creates the actual program.
             std::shared_ptr<storm::pgcl::PgclProgram> result(
-                    new storm::pgcl::PgclProgram(statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated)
+                    new storm::pgcl::PgclProgram(declarations, statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated)
             );
             result->back()->setLast(true);
             // Sets the current program as a parent to all its direct children statements.
@@ -181,7 +204,7 @@ namespace storm {
             return newAssignment;
         }
 
-        std::shared_ptr<storm::pgcl::AssignmentStatement> PgclParser::createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) {
+        std::shared_ptr<storm::pgcl::VariableDeclaration> PgclParser::createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) {
             storm::expressions::Variable variable;
             if(!(*expressionManager).hasVariable(variableName)) {
                 variable = (*expressionManager).declareIntegerVariable(variableName);
@@ -191,14 +214,11 @@ namespace storm {
                 variable = (*expressionManager).getVariable(variableName);
                 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Declaration of integer variable " << variableName << " which was already declared previously.");
             }
-            std::shared_ptr<storm::pgcl::AssignmentStatement> newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression));
-            newAssignment->setLocationNumber(this->currentLocationNumber);
-            this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment);
-            currentLocationNumber++;
-            return newAssignment;
+            // Todo add some checks
+            return std::make_shared<storm::pgcl::VariableDeclaration>(variable, assignedExpression);
         }
 
-        std::shared_ptr<storm::pgcl::AssignmentStatement> PgclParser::createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) {
+        std::shared_ptr<storm::pgcl::VariableDeclaration> PgclParser::createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) {
             storm::expressions::Variable variable;
             if(!(*expressionManager).hasVariable(variableName)) {
                 variable = (*expressionManager).declareBooleanVariable(variableName);
@@ -208,11 +228,8 @@ namespace storm {
                 variable = (*expressionManager).getVariable(variableName);
                 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Declaration of boolean variable " << variableName << " which was already declared previously.");
             }
-            std::shared_ptr<storm::pgcl::AssignmentStatement> newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression));
-            newAssignment->setLocationNumber(this->currentLocationNumber);
-            this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment);
-            currentLocationNumber++;
-            return newAssignment;
+            // TODO add some checks.
+            return std::make_shared<storm::pgcl::VariableDeclaration>(variable, assignedExpression);
         }
 
         std::shared_ptr<storm::pgcl::ObserveStatement> PgclParser::createObserveStatement(storm::pgcl::BooleanExpression const& condition) {

src/parser/PgclParser.h

@@ -1,12 +1,4 @@
-/* 
- * File:   PgclParser.h
- * Author: Lukas Westhofen
- *
- * Created on 1. April 2015, 19:12
- */
-
-#ifndef PGCLPARSER_H
-#define	PGCLPARSER_H
+#pragma once
 
 // Includes files for file input.
 #include <fstream>
@@ -14,6 +6,7 @@
 #include <iomanip>
 // Includes files for building and parsing the PGCL program
 #include "src/parser/SpiritParserDefinitions.h"
+#include "src/parser/SpiritErrorHandler.h"
 #include "src/parser/ExpressionParser.h"
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/expressions/Expression.h"
@@ -29,6 +22,10 @@
 #include "src/storage/pgcl/Statement.h"
 
 namespace storm {
+    namespace pgcl {
+        class IfStatement;
+    }
+    
     namespace parser {
         
         class PgclParser : public qi::grammar<Iterator, storm::pgcl::PgclProgram(), Skipper> {
@@ -74,11 +71,14 @@ namespace storm {
             qi::rule<Iterator, std::string(), Skipper> variableName;
             qi::rule<Iterator, std::string(), Skipper> programName;
 
-            qi::rule<Iterator, std::vector<std::shared_ptr<storm::pgcl::AssignmentStatement>>(), Skipper> variableDeclarations;
-            qi::rule<Iterator, std::shared_ptr<storm::pgcl::AssignmentStatement>(), Skipper> integerDeclaration;
-            qi::rule<Iterator, std::shared_ptr<storm::pgcl::AssignmentStatement>(), Skipper> booleanDeclaration;
+            qi::rule<Iterator, std::vector<std::shared_ptr<storm::pgcl::VariableDeclaration>>(), Skipper> variableDeclarations;
+            qi::rule<Iterator, std::shared_ptr<storm::pgcl::VariableDeclaration>(), Skipper> integerDeclaration;
+            qi::rule<Iterator, std::shared_ptr<storm::pgcl::VariableDeclaration>(), Skipper> booleanDeclaration;
             qi::rule<Iterator, storm::expressions::Variable(), Skipper> doubleDeclaration;
             
+            // An error handler function.
+            phoenix::function<SpiritErrorHandler> handler;
+            
             /// Denotes the invalid identifiers, which are later passed to the expression parser.
             struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
                 keywordsStruct() {
@@ -87,7 +87,8 @@ namespace storm {
                     ("if", 2)
                     ("observe", 3)
                     ("int", 4)
-                    ("function", 5);
+                    ("bool", 5)
+                    ("function", 6);
                 }
             };
 
@@ -138,11 +139,11 @@ namespace storm {
             void enableExpressions();
 
             // Constructors for the single program parts. They just wrap the statement constructors and throw exceptions in case something unexpected was parsed.
-            storm::pgcl::PgclProgram createProgram(std::string const& programName, boost::optional<std::vector<storm::expressions::Variable> > parameters, std::vector<std::shared_ptr<storm::pgcl::AssignmentStatement>> const& variableDeclarations, std::vector<std::shared_ptr<storm::pgcl::Statement> > statements);
+            storm::pgcl::PgclProgram createProgram(std::string const& programName, boost::optional<std::vector<storm::expressions::Variable> > parameters, std::vector<std::shared_ptr<storm::pgcl::VariableDeclaration>> const& variableDeclarations, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& statements);
             storm::expressions::Variable declareDoubleVariable(std::string const& variableName);
             std::shared_ptr<storm::pgcl::AssignmentStatement> createAssignmentStatement(std::string const& variableName, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& assignedExpression);
-            std::shared_ptr<storm::pgcl::AssignmentStatement> createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
-            std::shared_ptr<storm::pgcl::AssignmentStatement> createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
+            std::shared_ptr<storm::pgcl::VariableDeclaration> createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
+            std::shared_ptr<storm::pgcl::VariableDeclaration> createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
             std::shared_ptr<storm::pgcl::ObserveStatement> createObserveStatement(storm::pgcl::BooleanExpression const& condition);
             std::shared_ptr<storm::pgcl::IfStatement> createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& if_body, boost::optional<std::vector<std::shared_ptr<storm::pgcl::Statement> > > const& else_body);
             std::shared_ptr<storm::pgcl::LoopStatement> createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& body);
@@ -154,5 +155,4 @@ namespace storm {
     } // namespace parser
 } // namespace storm
 
-#endif	/* PGCLPARSER_H */
 

src/parser/PrismParser.cpp

@@ -9,6 +9,10 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
 
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "src/parser/ExpressionParser.h"
+
 namespace storm {
     namespace parser {
         storm::prism::Program PrismParser::parse(std::string const& filename) {
@@ -70,7 +74,9 @@ namespace storm {
             return result;
         }
         
-        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(*manager, keywords_, false, false) {
+        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) {
+            
+            ExpressionParser& expression_ = *expressionParser;
             // 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");
@@ -90,25 +96,25 @@ namespace storm {
             undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
             undefinedConstantDefinition.name("undefined constant definition");
             
-            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 = ((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.name("defined boolean constant declaration");
             
-            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 = ((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.name("defined integer constant declaration");
             
-            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 = ((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.name("defined double constant declaration");
             
             definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
             definedConstantDefinition.name("defined constant definition");
             
-            formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression_ > 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") > expressionParser[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)];
+            booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > -((qi::lit("init") > expression_[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)];
             booleanVariableDefinition.name("boolean variable definition");
             
-            integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser > 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 = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression_ > 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.name("integer variable definition");
             
             variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
@@ -117,13 +123,13 @@ 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 = (expressionParser > qi::lit(":") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
+            stateRewardDefinition = (expression_ > qi::lit(":") > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
             stateRewardDefinition.name("state reward definition");
             
-            stateActionRewardDefinition = (qi::lit("[") >> -identifier >> qi::lit("]") >> expressionParser >> qi::lit(":") >> expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)];
+            stateActionRewardDefinition = (qi::lit("[") >> -identifier >> qi::lit("]") >> expression_ >> qi::lit(":") >> expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)];
             stateActionRewardDefinition.name("state action reward definition");
 
-            transitionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > expressionParser > qi::lit("->") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4, qi::_r1)];
+            transitionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > expression_ > qi::lit("->") > expression_ > qi::lit(":") > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4, qi::_r1)];
             transitionRewardDefinition.name("transition reward definition");
             
             rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\""))
@@ -134,7 +140,7 @@ namespace storm {
                                      >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)];
             rewardModelDefinition.name("reward model definition");
             
-            initialStatesConstruct = (qi::lit("init") > expressionParser > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
+            initialStatesConstruct = (qi::lit("init") > expression_ > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             initialStatesConstruct.name("initial construct");
             
             systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
@@ -176,16 +182,16 @@ namespace storm {
             moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)];
             moduleComposition.name("module composition");
             
-            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 = (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.name("label definition");
             
-            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 = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression_ > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
             assignmentDefinition.name("assignment");
             
             assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
             assignmentDefinitionList.name("assignment list");
             
-            updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
+            updateDefinition = (((expression_ >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
             updateDefinition.name("update");
             
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
@@ -254,17 +260,17 @@ namespace storm {
             commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]"))
                                  |
                                   (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true]))
-                                 > expressionParser
+                                 > *expressionParser
                                  > qi::lit("->")
                                  > updateListDefinition(qi::_r1)
                                  > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)];
             
             this->secondRun = true;
-            this->expressionParser.setIdentifierMapping(&this->identifiers_);
+            this->expressionParser->setIdentifierMapping(&this->identifiers_);
         }
         
         void PrismParser::allowDoubleLiterals(bool flag) {
-            this->expressionParser.setAcceptDoubleLiterals(flag);
+            this->expressionParser->setAcceptDoubleLiterals(flag);
         }
         
         std::string const& PrismParser::getFilename() const {

src/parser/PrismParser.h

@@ -7,7 +7,7 @@
 #include <iomanip>
 
 #include "src/parser/SpiritParserDefinitions.h"
-#include "src/parser/ExpressionParser.h"
+#include "src/parser/SpiritErrorHandler.h"
 #include "src/storage/prism/Program.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/Expressions.h"
@@ -20,6 +20,8 @@ namespace storm {
 
 namespace storm {
     namespace parser {
+        class ExpressionParser;
+        
         // A class that stores information about the parsed program.
         class GlobalProgramInformation {
         public:
@@ -237,7 +239,8 @@ namespace storm {
             
             // Parser and manager used for recognizing expressions.
             std::shared_ptr<storm::expressions::ExpressionManager> manager;
-            storm::parser::ExpressionParser expressionParser;
+            // TODO shared?
+            std::shared_ptr<storm::parser::ExpressionParser> expressionParser;
             
             // Helper methods used in the grammar.
             bool isValidIdentifier(std::string const& identifier);

src/parser/SpiritErrorHandler.h

@@ -1,5 +1,4 @@
-#ifndef STORM_PARSER_SPIRITERRORHANDLER_H_
-#define STORM_PARSER_SPIRITERRORHANDLER_H_
+#pragma once
 
 #include "src/parser/SpiritParserDefinitions.h"
 
@@ -30,5 +29,3 @@ namespace storm {
         };
     }
 }
-
-#endif /* STORM_PARSER_SPIRITERRORHANDLER_H_ */

src/utility/storm.cpp

@@ -37,7 +37,8 @@ namespace storm {
     }
 
     std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString) {
-        storm::parser::FormulaParser formulaParser;
+        auto exprManager = std::make_shared<storm::expressions::ExpressionManager>();
+        storm::parser::FormulaParser formulaParser(exprManager);
         return parseFormulas(formulaParser, inputString);
     }