diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 5666b39db..507753a71 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -23,7 +23,7 @@ namespace storm { } minMaxExpression.name("min/max expression"); - identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)]; + identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, phoenix::ref(qi::_pass))]; identifierExpression.name("identifier expression"); literalExpression = trueFalse_[qi::_val = qi::_1] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)]; @@ -53,7 +53,7 @@ namespace storm { 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)]; + 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)]; } @@ -70,7 +70,7 @@ namespace storm { 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)]; + 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)]; } @@ -82,6 +82,24 @@ namespace storm { expression %= iteExpression; expression.name("expression"); + /*! + * Enable this for debugging purposes. + debug(expression); + debug(iteExpression); + debug(orExpression); + debug(andExpression); + debug(equalityExpression); + debug(relativeExpression); + debug(plusExpression); + debug(multiplicationExpression); + debug(powerExpression); + debug(unaryExpression); + debug(atomicExpression); + debug(literalExpression); + debug(identifierExpression); + */ + + // Enable error reporting. qi::on_error(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -304,11 +322,18 @@ namespace storm { return manager.boolean(false); } - storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const { + 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); - STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'."); + if (expression == nullptr) { + if (allowBacktracking) { + pass = false; + return manager.boolean(false); + } else { + STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'."); + } + } return *expression; } else { return manager.boolean(false); diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 2a67e7df6..55df73e2a 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -223,7 +223,7 @@ namespace storm { storm::expressions::Expression createIntegerLiteralExpression(int value) const; storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const; storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const; - storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const; + storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const; bool isValidIdentifier(std::string const& identifier); diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 218a51734..268865f47 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -38,7 +38,10 @@ namespace storm { booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula.name("boolean literal formula"); - atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")); + operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator; + 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(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; @@ -89,7 +92,7 @@ namespace storm { 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 = (probabilityOperator | rewardOperator | steadyStateOperator | orStateFormula); + stateFormula = (orStateFormula); stateFormula.name("state formula"); start = qi::eps > stateFormula >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index c5735286b..d2de1a73f 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -132,6 +132,7 @@ namespace storm { qi::rule(), Skipper> pathFormulaWithoutUntil; qi::rule(), Skipper> simplePathFormula; qi::rule(), Skipper> atomicStateFormula; + qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule(), Skipper> andStateFormula;