Formula parser works again. Tests adapted.

Former-commit-id: 78ce54d69f

src/logic/AtomicExpressionFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool AtomicExpressionFormula::isPropositionalFormula() const {
+            return true;
+        }
+        
         storm::expressions::Expression const& AtomicExpressionFormula::getExpression() const {
             return expression;
         }

src/logic/AtomicExpressionFormula.h

@@ -15,7 +15,8 @@ namespace storm {
             }
             
             virtual bool isAtomicExpressionFormula() const override;
-            
+            virtual bool isPropositionalFormula() const override;
+
             storm::expressions::Expression const& getExpression() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/AtomicLabelFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool AtomicLabelFormula::isPropositionalFormula() const {
+            return true;
+        }
+        
         std::string const& AtomicLabelFormula::getLabel() const {
             return label;
         }

src/logic/AtomicLabelFormula.h

@@ -16,6 +16,7 @@ namespace storm {
             }
             
             virtual bool isAtomicLabelFormula() const override;
+            virtual bool isPropositionalFormula() const override;
 
             std::string const& getLabel() const;
             

src/logic/BinaryBooleanStateFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool BinaryBooleanStateFormula::isPropositionalFormula() const {
+            return this->getLeftSubformula().isPropositionalFormula() && this->getRightSubformula().isPropositionalFormula();
+        }
+        
         std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const {
             out << "(";
             this->getLeftSubformula().writeToStream(out);

src/logic/BinaryBooleanStateFormula.h

@@ -16,7 +16,8 @@ namespace storm {
             };
             
             virtual bool isBinaryBooleanStateFormula() const override;
-            
+            virtual bool isPropositionalFormula() const override;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/BooleanLiteralFormula.cpp

@@ -14,6 +14,10 @@ namespace storm {
             return !value;
         }
         
+        bool BooleanLiteralFormula::isPropositionalFormula() const {
+            return true;
+        }
+        
         std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out) const {
             if (value) {
                 out << "true";

src/logic/BooleanLiteralFormula.h

@@ -13,9 +13,10 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            virtual bool isTrue() const;
-            virtual bool isFalse() const;
-            
+            virtual bool isTrue() const override;
+            virtual bool isFalse() const override;
+            virtual bool isPropositionalFormula() const override;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/Formula.cpp

@@ -118,6 +118,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isPropositionalFormula() const {
+            return false;
+        }
+        
         PathFormula& Formula::asPathFormula() {
             return dynamic_cast<PathFormula&>(*this);
         }

src/logic/Formula.h

@@ -77,6 +77,7 @@ namespace storm {
             virtual bool isPctlPathFormula() const;
             virtual bool isPctlStateFormula() const;
             virtual bool isPltlFormula() const;
+            virtual bool isPropositionalFormula() const;
             
             PathFormula& asPathFormula();
             PathFormula const& asPathFormula() const;

src/logic/UnaryBooleanStateFormula.cpp

@@ -2,8 +2,21 @@
 
 namespace storm {
     namespace logic {
+        UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula> const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) {
+            // Intentionally left empty.
+        }
+        
         bool UnaryBooleanStateFormula::isUnaryBooleanStateFormula() const {
             return true;
         }
+        
+        std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out) const {
+            switch (operatorType) {
+                case OperatorType::Not: out << "!("; break;
+            }
+            this->getSubformula().writeToStream(out);
+            out << ")";
+            return out;
+        }
     }
 }

src/logic/UnaryBooleanStateFormula.h

@@ -7,11 +7,20 @@ namespace storm {
     namespace logic {
         class UnaryBooleanStateFormula : public UnaryStateFormula {
         public:
+            enum class OperatorType { Not };
+
+            UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula> const& subformula);
+            
             virtual ~UnaryBooleanStateFormula() {
                 // Intentionally left empty.
             };
             
             virtual bool isUnaryBooleanStateFormula() const override;
+
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+        private:
+            OperatorType operatorType;
         };
     }
 }

src/logic/UnaryStateFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool UnaryStateFormula::isPropositionalFormula() const {
+            return this->getSubformula().isPropositionalFormula();
+        }
+        
         Formula& UnaryStateFormula::getSubformula() {
             return *subformula;
         }

src/logic/UnaryStateFormula.h

@@ -14,7 +14,8 @@ namespace storm {
             }
             
             virtual bool isUnaryStateFormula() const override;
-            
+            virtual bool isPropositionalFormula() const override;
+
             Formula& getSubformula();
             Formula const& getSubformula() const;
             

src/parser/ExpressionParser.cpp

@@ -5,14 +5,22 @@
 
 namespace storm {
     namespace parser {
-        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
+        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
             identifier.name("identifier");
             
-            floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > plusExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)];
+            if (allowBacktracking) {
+                floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)];
+            } else {
+                floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > plusExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)];
+            }
             floorCeilExpression.name("floor/ceil expression");
             
-            minMaxExpression = ((minMaxOperator_ >> qi::lit("(")) > plusExpression > qi::lit(",") > plusExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)];
+            if (allowBacktracking) {
+                minMaxExpression = ((minMaxOperator_ >> qi::lit("(")) >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)];
+            } else {
+                minMaxExpression = ((minMaxOperator_ >> qi::lit("(")) > plusExpression > qi::lit(",") > plusExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)];
+            }
             minMaxExpression.name("min/max expression");
             
             identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
@@ -27,25 +35,45 @@ namespace storm {
             unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createUnaryExpression, phoenix::ref(*this), qi::_1, qi::_2)];
             unaryExpression.name("unary expression");
             
-            powerExpression = unaryExpression[qi::_val = qi::_1] > -(powerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            if (allowBacktracking) {
+                powerExpression = unaryExpression[qi::_val = qi::_1] > -(powerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            } else {
+                powerExpression = unaryExpression[qi::_val = qi::_1] > -(powerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            }
             powerExpression.name("power expression");
             
-            multiplicationExpression = powerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > powerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            if (allowBacktracking) {
+                multiplicationExpression = powerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> powerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            } else {
+                multiplicationExpression = powerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > powerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            }
             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)];
             plusExpression.name("plus expression");
             
-            relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            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)];
+            } else {
+                relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            }
             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)];
             equalityExpression.name("equality expression");
             
-            andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            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)];
+            } else {
+                andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            }
             andExpression.name("and expression");
             
-            orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            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)];
+            } else {
+                orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+            }
             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)];

src/parser/ExpressionParser.h

@@ -21,8 +21,11 @@ namespace storm {
              *
              * @param manager The manager responsible for the expressions.
              * @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected.
+             * @param allowBacktracking A flag that indicates whether or not the parser is supposed to backtrack beyond
+             * points it would typically allow. This can, for example, be used to prevent errors if the outer grammar
+             * also parses boolean conjuncts that are erroneously consumed by the expression parser.
              */
-            ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
+            ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool allowBacktracking = false);
             
             /*!
              * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to

src/parser/FormulaParser.cpp

@@ -6,7 +6,14 @@
 namespace storm {
     namespace parser {
         
-        FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParser::base_type(start), expressionParser(*manager, keywords_) {
+        FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParser::base_type(start), expressionParser(*manager, keywords_, 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_);
+            
             instantaneousRewardFormula = (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
             instantaneousRewardFormula.name("instantaneous reward formula");
             
@@ -33,28 +40,37 @@ namespace storm {
             
             atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | qi::lit("(") > stateFormula > qi::lit(")");
             atomicStateFormula.name("atomic state formula");
+
+            notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
+            notStateFormula.name("negation formula");
             
-            eventuallyFormula = (qi::lit("F") > formula)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1)];
+            eventuallyFormula = (qi::lit("F") >> simpleFormula)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1)];
             eventuallyFormula.name("eventually formula");
             
-            globallyFormula = (qi::lit("G") > formula)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)];
+            globallyFormula = (qi::lit("G") >> simpleFormula)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)];
             globallyFormula.name("globally formula");
             
-            nextFormula = (qi::lit("X") > formula)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)];
+            nextFormula = (qi::lit("X") >> simpleFormula)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)];
             nextFormula.name("next formula");
             
-            boundedUntilFormula = (formula > (qi::lit("U<=") > qi::uint_ > formula))[qi::_val = phoenix::bind(&FormulaParser::createBoundedUntilFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+            boundedUntilFormula = (simpleFormula >> (qi::lit("U<=") >> qi::uint_ >> simpleFormula))[qi::_val = phoenix::bind(&FormulaParser::createBoundedUntilFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
             boundedUntilFormula.name("bounded until formula");
             
-            untilFormula = (formula >> (qi::lit("U") > formula))[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            untilFormula = (simpleFormula >> (qi::lit("U") >> simpleFormula))[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             untilFormula.name("until formula");
             
-            conditionalFormula = (formula >> (qi::lit("||") > formula))[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            simplePathFormula = eventuallyFormula | globallyFormula | nextFormula | boundedUntilFormula | untilFormula;
+            simplePathFormula.name("simple path formula");
+            
+            conditionalFormula = (simplePathFormula >> (qi::lit("||") > simplePathFormula))[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             conditionalFormula.name("conditional formula");
             
-            pathFormula = eventuallyFormula | globallyFormula | nextFormula | conditionalFormula | boundedUntilFormula | untilFormula;
+            pathFormula = conditionalFormula | simplePathFormula;
             pathFormula.name("path formula");
             
+            simpleFormula = stateFormula | simplePathFormula;
+            simpleFormula.name("simple formula");
+            
             formula = stateFormula | pathFormula;
             formula.name("formula");
             
@@ -70,26 +86,31 @@ namespace storm {
             probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilityOperator.name("probability operator");
             
-            andStateFormula = (stateFormula >> (qi::lit("&") > stateFormula))[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_1, qi::_2, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
+            andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
             andStateFormula.name("and state formula");
             
-            orStateFormula = (andStateFormula >> (qi::lit("|") > andStateFormula))[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_1, qi::_2, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
+            orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
             orStateFormula.name("or state formula");
             
-            stateFormula = (atomicStateFormula | probabilityOperator | rewardOperator | steadyStateOperator | orStateFormula);
+            stateFormula = (probabilityOperator | rewardOperator | steadyStateOperator | orStateFormula);
             stateFormula.name("state formula");
             
-            start = qi::eps > stateFormula > qi::eoi;
+            comments = qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps];
+            comments.name("comment");
+            
+            start = qi::eps > stateFormula >> comments >> qi::eoi;
             start.name("start");
             
+            /*!
+             * Enable the following lines to print debug output for most the rules.
             debug(start);
+            debug(comments);
             debug(stateFormula);
             debug(orStateFormula);
             debug(andStateFormula);
             debug(probabilityOperator);
             debug(rewardOperator);
             debug(steadyStateOperator);
-            // debug(operatorInformation);
             debug(formula);
             debug(pathFormula);
             debug(conditionalFormula);
@@ -104,6 +125,7 @@ namespace storm {
             debug(reachabilityRewardFormula);
             debug(cumulativeRewardFormula);
             debug(instantaneousRewardFormula);
+             */
 
             // Enable error reporting.
             qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@@ -131,7 +153,11 @@ namespace storm {
             qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParser::parseFromString(std::string const& formulaString, std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) {
+        void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
+            this->identifiers_.add(identifier, expression);
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::parseFromString(std::string const& formulaString) {
             PositionIteratorType first(formulaString.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(formulaString.end());
@@ -140,10 +166,9 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> result;
             
             // Create grammar.
-            storm::parser::FormulaParser grammar(manager);
             try {
                 // Start parsing.
-                bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
+                bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
                 STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula.");
                 STORM_LOG_DEBUG("Parsed formula successfully.");
             } catch (qi::expectation_failure<PositionIteratorType> const& e) {
@@ -166,6 +191,7 @@ namespace storm {
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParser::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>(new storm::logic::AtomicExpressionFormula(expression));
         }
         
@@ -174,7 +200,6 @@ namespace storm {
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParser::createAtomicLabelFormula(std::string const& label) const {
-            std::cout << "creating atomic label formula" << std::endl;
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label));
         }
         
@@ -217,5 +242,14 @@ namespace storm {
         std::shared_ptr<storm::logic::Formula> FormulaParser::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
         }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
+            if (operatorType) {
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
+            } else {
+                return subformula;
+            }
+        }
+
     } // namespace parser
 } // namespace storm

src/parser/FormulaParser.h

@@ -14,25 +14,36 @@ namespace storm {
         
         class FormulaParser : public qi::grammar<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> {
         public:
-            
+            FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
+
             /*!
              * Parses the formula given by the provided string.
              *
              * @param formulaString The formula as a string.
              * @return The resulting formula representation.
              */
-            static std::shared_ptr<storm::logic::Formula> parseFromString(std::string const& formulaString, std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
+            std::shared_ptr<storm::logic::Formula> parseFromString(std::string const& formulaString);
             
-        private:
-            FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
+            /*!
+             * 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);
+                    ("max", 4)
+                    ("F", 5)
+                    ("G", 6)
+                    ("X", 7);
                 }
             };
             
@@ -52,16 +63,26 @@ namespace storm {
             // A parser used for recognizing the operators at the "relational" precedence level.
             relationalOperatorStruct relationalOperator_;
             
-            struct booleanOperatorStruct : qi::symbols<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
-                booleanOperatorStruct() {
+            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 "boolean" precedence level.
-            booleanOperatorStruct booleanOperator_;
+            // 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::logic::OptimalityType> {
                 optimalityOperatorStruct() {
@@ -93,7 +114,12 @@ namespace storm {
             // An error handler function.
             phoenix::function<ErrorHandler> handler;
             
+            // 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::shared_ptr<storm::logic::Formula>(), Skipper> start;
+            qi::rule<Iterator, qi::unused_type(), Skipper> comments;
             
             qi::rule<Iterator, std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
@@ -101,9 +127,10 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> steadyStateOperator;
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> formula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simpleFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> stateFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormula;
-            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simplePathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> atomicStateFormula;
             qi::rule<Iterator, std::string(), Skipper> label;
             
@@ -143,7 +170,7 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
             std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
-            
+            std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
         };
         
     } // namespace parser

src/parser/PrismParser.cpp

@@ -39,7 +39,7 @@ namespace storm {
             storm::parser::PrismParser grammar(filename, first);
             try {
                 // Start first run.
-                bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
+                bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
                 STORM_LOG_THROW(succeeded,  storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
                 STORM_LOG_DEBUG("First pass of parsing PRISM input finished.");
                 
@@ -48,7 +48,7 @@ namespace storm {
                 iter = first;
                 last = PositionIteratorType(input.end());
                 grammar.moveToSecondRun();
-                succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
+                succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
                 STORM_LOG_THROW(succeeded,  storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
             } catch (qi::expectation_failure<PositionIteratorType> const& e) {
                 // If the parser expected content different than the one provided, display information about the location of the error.

src/parser/SpiritParserDefinitions.h

@@ -16,6 +16,6 @@ typedef std::string::const_iterator BaseIteratorType;
 typedef boost::spirit::line_pos_iterator<BaseIteratorType> PositionIteratorType;
 typedef PositionIteratorType Iterator;
 
-typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
+typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi)) Skipper;
 
 #endif /* STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ */

test/functional/parser/FormulaParserTest.cpp

@@ -3,233 +3,147 @@
 #include "src/parser/FormulaParser.h"
 #include "src/exceptions/WrongFormatException.h"
 
-TEST(FormulaParserTest, parseLabelTest) {
-	std::string input = "\"label\"";
+TEST(FormulaParserTest, LabelTest) {
+    storm::parser::FormulaParser parser;
+
+    std::string input = "\"label\"";
     std::shared_ptr<storm::logic::Formula> formula(nullptr);
-	ASSERT_NO_THROW(formula = storm::parser::FormulaParser::parseFromString(input));
+	ASSERT_NO_THROW(formula = parser.parseFromString(input));
 
     EXPECT_TRUE(formula->isAtomicLabelFormula());
 }
 
-//TEST(PrctlParserTest, parsePropositionalFormulaTest) {
-//	std::string input =  "!(a & b) | a & ! c";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	ASSERT_TRUE(formula->getChild()->isPropositional());
-//	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
-//
-//	// The input was parsed correctly.
-//	ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parsePathFormulaTest) {
-//	std::string input = "X( P<0.9 (a U b))";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	// The input was parsed correctly.
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild()).get(), nullptr);
-//	auto nextFormula = std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild());
-//	ASSERT_FALSE(nextFormula->isPropositional());
-//	ASSERT_FALSE(nextFormula->isProbEventuallyAP());
-//
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
-//	auto probBoundFormula = std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild());
-//	ASSERT_EQ(0.9, probBoundFormula->getBound());
-//	ASSERT_EQ(storm::properties::LESS, probBoundFormula->getComparisonOperator());
-//	ASSERT_FALSE(probBoundFormula->isPropositional());
-//	ASSERT_TRUE(probBoundFormula->isProbEventuallyAP());
-//
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
-//	auto untilFormula = std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild());
-//	ASSERT_FALSE(untilFormula->isPropositional());
-//	ASSERT_FALSE(untilFormula->isProbEventuallyAP());
-//
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
-//	ASSERT_EQ("a", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft())->getAp());
-//	ASSERT_EQ("b", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight())->getAp());
-//
-//	// The string representation is also correct.
-//	ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
-//	std::string input =  "P > 0.5 [ F a ]";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(formula->getChild()).get(), nullptr);
-//	std::shared_ptr<prctl::ProbabilisticBoundOperator<double>> op = std::static_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(formula->getChild());
-//
-//	ASSERT_EQ(storm::properties::GREATER, op->getComparisonOperator());
-//	ASSERT_EQ(0.5, op->getBound());
-//	ASSERT_FALSE(op->isPropositional());
-//	ASSERT_TRUE(op->isProbEventuallyAP());
-//
-//	// Test the string representation for the parsed formula.
-//	ASSERT_EQ("P > 0.500000 (F a)", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parseRewardFormulaTest) {
-//	std::string input =  "R >= 15 [ I=5 ]";
-//	std::shared_ptr<prctl::PrctlFilter<double>>formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input);
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	ASSERT_NE(std::dynamic_pointer_cast<prctl::RewardBoundOperator<double>>(formula->getChild()).get(), nullptr);
-//	std::shared_ptr<prctl::RewardBoundOperator<double>> op = std::static_pointer_cast<prctl::RewardBoundOperator<double>>(formula->getChild());
-//
-//	ASSERT_EQ(storm::properties::GREATER_EQUAL, op->getComparisonOperator());
-//	ASSERT_EQ(15.0, op->getBound());
-//	ASSERT_FALSE(op->isPropositional());
-//	ASSERT_FALSE(op->isProbEventuallyAP());
-//
-//	// Test the string representation for the parsed formula.
-//	ASSERT_EQ("R >= 15.000000 (I=5)", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
-//	std::string input =  "R = ? [ F a ]";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	ASSERT_FALSE(formula->getChild()->isPropositional());
-//	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
-//
-//	// The input was parsed correctly.
-//	ASSERT_EQ("R = ? (F a)", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
-//	std::string input =  "P = ? [ a U <= 4 b & (!c) ]";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	ASSERT_FALSE(formula->getChild()->isPropositional());
-//	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
-//
-//	// The input was parsed correctly.
-//	ASSERT_EQ("P = ? (a U<=4 (b & !c))", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parseComplexFormulaTest) {
-//	std::string input =  "R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	ASSERT_FALSE(formula->getChild()->isPropositional());
-//	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
-//
-//	// The input was parsed correctly.
-//	ASSERT_EQ("(R <= 0.500000 (S) & (R > 15.000000 (C <= 0.500000) | !P < 0.400000 (G P > 0.900000 (F<=7 (a & b)))))", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, parsePrctlFilterTest) {
-//	std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser did not falsely recognize the input as a comment.
-//	ASSERT_NE(formula.get(), nullptr);
-//
-//	ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator());
-//
-//	ASSERT_EQ(5, formula->getActionCount());
-//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::FormulaAction<double>>(formula->getAction(0)).get(), nullptr);
-//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
-//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::BoundAction<double>>(formula->getAction(2)).get(), nullptr);
-//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
-//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr);
-//
-//	ASSERT_FALSE(formula->getChild()->isPropositional());
-//	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
-//
-//	// The input was parsed correctly.
-//	ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
-//}
-//
-//TEST(PrctlParserTest, commentTest) {
-//	std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]";
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	// The parser recognized the input as a comment.
-//	ASSERT_NE(nullptr, formula.get());
-//
-//	// Test if the parser recognizes the comment at the end of a line.
-//	input = "P<=0.5 [ X a ] // This is a comment.";
-//	ASSERT_NO_THROW(
-//				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
-//	);
-//
-//	ASSERT_FALSE(formula->getChild()->isPropositional());
-//	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
-//
-//	ASSERT_EQ("P <= 0.500000 (X a)", formula->toString());
-//}
-//
-//
-//TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_THROW(
-//			formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"),
-//			storm::exceptions::WrongFormatException
-//	);
-//}
-//
-//TEST(PrctlParserTest, wrongFormulaTest) {
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_THROW(
-//			formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"),
-//			storm::exceptions::WrongFormatException
-//	);
-//}
-//
-//TEST(PrctlParserTest, wrongFormulaTest2) {
-//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-//	ASSERT_THROW(
-//			formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"),
-//			storm::exceptions::WrongFormatException
-//	);
-//}
+TEST(FormulaParserTest, ComplexLabelTest) {
+    storm::parser::FormulaParser parser;
+
+    std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\"";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+	ASSERT_NO_THROW(formula = parser.parseFromString(input));
+
+    EXPECT_TRUE(formula->isPropositionalFormula());
+    EXPECT_TRUE(formula->isBinaryBooleanStateFormula());
+}
+
+TEST(FormulaParserTest, ExpressionTest) {
+    std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
+    manager->declareBooleanVariable("x");
+    manager->declareIntegerVariable("y");
+    
+    storm::parser::FormulaParser parser(manager);
+    
+    std::string input = "!(x | y > 3)";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    
+    EXPECT_TRUE(formula->isPropositionalFormula());
+    EXPECT_TRUE(formula->isUnaryBooleanStateFormula());
+}
+
+TEST(FormulaParserTest, LabelAndExpressionTest) {
+    std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
+    manager->declareBooleanVariable("x");
+    manager->declareIntegerVariable("y");
+    
+    storm::parser::FormulaParser parser(manager);
+    
+    std::string input = "!\"a\" | x | y > 3";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    
+    EXPECT_TRUE(formula->isPropositionalFormula());
+    
+    input = "x | y > 3 | !\"a\"";
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    EXPECT_TRUE(formula->isPropositionalFormula());
+}
+
+TEST(FormulaParserTest, ProbabilityOperatorTest) {
+    storm::parser::FormulaParser parser;
+
+    std::string input = "P<0.9 [\"a\" U \"b\"]";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+	ASSERT_NO_THROW(formula = parser.parseFromString(input));
+
+    EXPECT_TRUE(formula->isProbabilityOperator());
+    EXPECT_TRUE(formula->asProbabilityOperatorFormula().hasBound());
+    EXPECT_FALSE(formula->asProbabilityOperatorFormula().hasOptimalityType());
+}
+
+TEST(FormulaParserTest, RewardOperatorTest) {
+    storm::parser::FormulaParser parser;
+    
+    std::string input = "Rmin<0.9 [F \"a\"]";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    
+    EXPECT_TRUE(formula->isRewardOperator());
+    EXPECT_TRUE(formula->asRewardOperatorFormula().hasBound());
+    EXPECT_TRUE(formula->asRewardOperatorFormula().hasOptimalityType());
+    
+    input = "R=? [I=10]";
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    
+    EXPECT_TRUE(formula->isRewardOperator());
+    EXPECT_FALSE(formula->asRewardOperatorFormula().hasBound());
+    EXPECT_FALSE(formula->asRewardOperatorFormula().hasOptimalityType());
+    EXPECT_TRUE(formula->asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula());
+}
+
+TEST(FormulaParserTest, ConditionalProbabilityTest) {
+    storm::parser::FormulaParser parser;
+    
+    std::string input = "P<0.9 [F \"a\" || F \"b\"]";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    
+    EXPECT_TRUE(formula->isProbabilityOperator());
+    storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asProbabilityOperatorFormula();
+    EXPECT_TRUE(probFormula.getSubformula().isConditionalPathFormula());
+}
+
+TEST(FormulaParserTest, NestedPathFormulaTest) {
+    storm::parser::FormulaParser parser;
+    
+    std::string input = "P<0.9 [F X \"a\"]";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+    ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    
+    EXPECT_TRUE(formula->isProbabilityOperator());
+    ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
+    ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula());
+}
+
+TEST(FormulaParserTest, CommentTest) {
+    storm::parser::FormulaParser parser;
+
+    std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment.";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+	ASSERT_NO_THROW(formula = parser.parseFromString(input));
+    EXPECT_TRUE(formula->isProbabilityOperator());
+    ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula());
+    ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
+}
+
+
+TEST(FormulaParserTest, WrongFormatTest) {
+    std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
+    manager->declareBooleanVariable("x");
+    manager->declareIntegerVariable("y");
+    
+    storm::parser::FormulaParser parser(manager);
+    std::string input = "P>0.5 [ a ]";
+    std::shared_ptr<storm::logic::Formula> formula(nullptr);
+	EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
+    
+    input = "P=0.5 [F \"a\"]";
+    EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
+
+    input = "P>0.5 [F !(x = 0)]";
+    EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
+
+    input = "P>0.5 [F !y]";
+    EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
+
+    input = "P>0.5 [F y!=0)]";
+    EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
+}