diff --git a/src/logic/AtomicExpressionFormula.cpp b/src/logic/AtomicExpressionFormula.cpp index 2be59262d..811364fe3 100644 --- a/src/logic/AtomicExpressionFormula.cpp +++ b/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; } diff --git a/src/logic/AtomicExpressionFormula.h b/src/logic/AtomicExpressionFormula.h index 7ba5bbdcb..1ec39c2e5 100644 --- a/src/logic/AtomicExpressionFormula.h +++ b/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; diff --git a/src/logic/AtomicLabelFormula.cpp b/src/logic/AtomicLabelFormula.cpp index 44f742f19..a53c2762e 100644 --- a/src/logic/AtomicLabelFormula.cpp +++ b/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; } diff --git a/src/logic/AtomicLabelFormula.h b/src/logic/AtomicLabelFormula.h index 62a001ab2..12ea764ff 100644 --- a/src/logic/AtomicLabelFormula.h +++ b/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; diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp index 199cfda39..7bd49f109 100644 --- a/src/logic/BinaryBooleanStateFormula.cpp +++ b/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); diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h index 3f7d12b0d..bb4688ccd 100644 --- a/src/logic/BinaryBooleanStateFormula.h +++ b/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: diff --git a/src/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp index 1c7adf5bd..06d8cd464 100644 --- a/src/logic/BooleanLiteralFormula.cpp +++ b/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"; diff --git a/src/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h index bc2f0d95c..0451aa5a7 100644 --- a/src/logic/BooleanLiteralFormula.h +++ b/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: diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 0514dff6b..d2f4d2527 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -118,6 +118,10 @@ namespace storm { return false; } + bool Formula::isPropositionalFormula() const { + return false; + } + PathFormula& Formula::asPathFormula() { return dynamic_cast(*this); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index ee7be3779..e3ab2063d 100644 --- a/src/logic/Formula.h +++ b/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; diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp index 4becf8a43..a54b3a16c 100644 --- a/src/logic/UnaryBooleanStateFormula.cpp +++ b/src/logic/UnaryBooleanStateFormula.cpp @@ -2,8 +2,21 @@ namespace storm { namespace logic { + UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr 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; + } } } \ No newline at end of file diff --git a/src/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h index a7ae644ba..2e9fd5793 100644 --- a/src/logic/UnaryBooleanStateFormula.h +++ b/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 const& subformula); + virtual ~UnaryBooleanStateFormula() { // Intentionally left empty. }; virtual bool isUnaryBooleanStateFormula() const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + private: + OperatorType operatorType; }; } } diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index 90b112ee2..ee6a5a8c0 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/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; } diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index 381348184..0f6791a20 100644 --- a/src/logic/UnaryStateFormula.h +++ b/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; diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 826722618..5666b39db 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,14 +5,22 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols 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 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)]; diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 30807d6c5..2a67e7df6 100644 --- a/src/parser/ExpressionParser.h +++ b/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 const& invalidIdentifiers_); + ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking = false); /*! * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 89f869504..b8ec3e9a4 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -6,7 +6,14 @@ namespace storm { namespace parser { - FormulaParser::FormulaParser(std::shared_ptr const& manager) : FormulaParser::base_type(start), expressionParser(*manager, keywords_) { + FormulaParser::FormulaParser(std::shared_ptr 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(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -131,7 +153,11 @@ namespace storm { qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } - std::shared_ptr FormulaParser::parseFromString(std::string const& formulaString, std::shared_ptr const& manager) { + void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { + this->identifiers_.add(identifier, expression); + } + + std::shared_ptr 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 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 const& e) { @@ -166,6 +191,7 @@ namespace storm { } std::shared_ptr 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(new storm::logic::AtomicExpressionFormula(expression)); } @@ -174,7 +200,6 @@ namespace storm { } std::shared_ptr FormulaParser::createAtomicLabelFormula(std::string const& label) const { - std::cout << "creating atomic label formula" << std::endl; return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } @@ -217,5 +242,14 @@ namespace storm { std::shared_ptr FormulaParser::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); } + + std::shared_ptr FormulaParser::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + if (operatorType) { + return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); + } else { + return subformula; + } + } + } // namespace parser } // namespace storm diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index 3c13f65a7..d89dae967 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -14,25 +14,36 @@ namespace storm { class FormulaParser : public qi::grammar(), Skipper> { public: - + FormulaParser(std::shared_ptr const& manager = std::shared_ptr(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 parseFromString(std::string const& formulaString, std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); + std::shared_ptr parseFromString(std::string const& formulaString); - private: - FormulaParser(std::shared_ptr 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 { 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 { - booleanOperatorStruct() { + struct binaryBooleanOperatorStruct : qi::symbols { + 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 { + 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 { optimalityOperatorStruct() { @@ -93,7 +114,12 @@ namespace storm { // An error handler function. phoenix::function 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 identifiers_; + qi::rule(), Skipper> start; + qi::rule comments; qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule(), Skipper> probabilityOperator; @@ -101,9 +127,10 @@ namespace storm { qi::rule(), Skipper> steadyStateOperator; qi::rule(), Skipper> formula; + qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; qi::rule(), Skipper> pathFormula; - + qi::rule(), Skipper> simplePathFormula; qi::rule(), Skipper> atomicStateFormula; qi::rule label; @@ -143,7 +170,7 @@ namespace storm { std::shared_ptr createRewardOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); - + std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); }; } // namespace parser diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index b46684786..6426f0e16 100644 --- a/src/parser/PrismParser.cpp +++ b/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 const& e) { // If the parser expected content different than the one provided, display information about the location of the error. diff --git a/src/parser/SpiritParserDefinitions.h b/src/parser/SpiritParserDefinitions.h index feb78f77d..20c922863 100644 --- a/src/parser/SpiritParserDefinitions.h +++ b/src/parser/SpiritParserDefinitions.h @@ -16,6 +16,6 @@ typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::line_pos_iterator 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_ */ \ No newline at end of file diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp index 828a34f74..c1fd6c152 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/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 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> 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> 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>(formula->getChild()).get(), nullptr); -// auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); -// ASSERT_FALSE(nextFormula->isPropositional()); -// ASSERT_FALSE(nextFormula->isProbEventuallyAP()); -// -// ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); -// auto probBoundFormula = std::dynamic_pointer_cast>(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>(probBoundFormula->getChild()).get(), nullptr); -// auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); -// ASSERT_FALSE(untilFormula->isPropositional()); -// ASSERT_FALSE(untilFormula->isProbEventuallyAP()); -// -// ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); -// ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); -// ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); -// ASSERT_EQ("b", std::dynamic_pointer_cast>(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> 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>(formula->getChild()).get(), nullptr); -// std::shared_ptr> op = std::static_pointer_cast>(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>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>(formula->getChild()).get(), nullptr); -// std::shared_ptr> op = std::static_pointer_cast>(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> 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> 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> 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> 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>(formula->getAction(0)).get(), nullptr); -// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); -// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); -// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); -// ASSERT_NE(std::dynamic_pointer_cast>(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> 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> formula(nullptr); -// ASSERT_THROW( -// formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"), -// storm::exceptions::WrongFormatException -// ); -//} -// -//TEST(PrctlParserTest, wrongFormulaTest) { -// std::shared_ptr> formula(nullptr); -// ASSERT_THROW( -// formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"), -// storm::exceptions::WrongFormatException -// ); -//} -// -//TEST(PrctlParserTest, wrongFormulaTest2) { -// std::shared_ptr> 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 formula(nullptr); + ASSERT_NO_THROW(formula = parser.parseFromString(input)); + + EXPECT_TRUE(formula->isPropositionalFormula()); + EXPECT_TRUE(formula->isBinaryBooleanStateFormula()); +} + +TEST(FormulaParserTest, ExpressionTest) { + std::shared_ptr 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 formula(nullptr); + ASSERT_NO_THROW(formula = parser.parseFromString(input)); + + EXPECT_TRUE(formula->isPropositionalFormula()); + EXPECT_TRUE(formula->isUnaryBooleanStateFormula()); +} + +TEST(FormulaParserTest, LabelAndExpressionTest) { + std::shared_ptr 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 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 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 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 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 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 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 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 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); +}