diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 6f84aa89c..6afddd246 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -34,31 +34,38 @@ namespace parser { template struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> { PrctlGrammar() : PrctlGrammar::base_type(start) { - freeIdentifierName = qi::lexeme[(qi::alpha | qi::char_('_'))]; + freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; //This block defines rules for parsing state formulas stateFormula %= orFormula; + stateFormula.name("state formula"); - andFormula = notFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notFormula)[qi::_val = + andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]; - orFormula = andFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andFormula)[qi::_val = + andFormula.name("state formula"); + orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]; - notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") >> atomicStateFormula)[qi::_val = + orFormula.name("state formula"); + notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = phoenix::new_>(qi::_1)]; + notFormula.name("state formula"); atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")"); + atomicStateFormula.name("state formula"); atomicProposition = (freeIdentifierName)[qi::_val = phoenix::new_>(qi::_1)]; + atomicProposition.name("state formula"); probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); + probabilisticBoundOperator.name("state formula"); rewardBoundOperator = ( (qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | @@ -69,29 +76,39 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); + rewardBoundOperator.name("state formula"); //This block defines rules for parsing formulas with noBoundOperators noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); + noBoundOperator.name("no bound operator"); probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1)]; + probabilisticNoBoundOperator.name("no bound operator"); rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1)]; + rewardNoBoundOperator.name("no bound operator"); //This block defines rules for parsing path formulas - pathFormula = (eventually | boundedEventually | globally | boundedUntil | until); - eventually = (qi::lit("F") >> stateFormula)[qi::_val = - phoenix::new_ >(qi::_1)]; - boundedEventually = (qi::lit("F") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val = + pathFormula = (boundedEventually | eventually | globally | boundedUntil | until); + pathFormula.name("path formula"); + boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; - globally = (qi::lit("G") >> stateFormula)[qi::_val = + boundedEventually.name("path formula"); + eventually = (qi::lit("F") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + eventually.name("path formula"); + globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - until = (stateFormula >> qi::lit("U") >> stateFormula)[qi::_val = - phoenix::new_>(qi::_1, qi::_2)]; - boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val = + globally.name("path formula"); + boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_3, qi::_2)]; + boundedUntil.name("path formula"); + until = (stateFormula >> qi::lit("U") > stateFormula)[qi::_val = + phoenix::new_>(qi::_1, qi::_2)]; + until.name("path formula"); start = (noBoundOperator | stateFormula); - + start.name("PRCTL formula"); } qi::rule*(), Skipper> start; @@ -136,7 +153,37 @@ void storm::parser::PrctlParser::parse(std::string formulaString) { PrctlGrammar grammar; - qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); + try { + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << e.first.get_currentline() << std::endl << "\t"; + int i = 0; + for (i = 0; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + + std::cerr << msg.str(); + + // Now propagate exception. + throw storm::exceptions::WrongFileFormatException() << msg.str(); + } + if (result_pointer == nullptr) { + throw storm::exceptions::WrongFileFormatException() << "Syntax error in formula"; + } formula = result_pointer; } diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index 163a9265e..02d9ddc43 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -12,7 +12,7 @@ #include "src/parser/PrctlFileParser.h" TEST(PrctlParserTest, parseApOnlyTest) { - std::string ap = "P"; + std::string ap = "ap"; storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( prctlParser = new storm::parser::PrctlParser(ap); @@ -129,3 +129,31 @@ TEST(PrctlParserTest, parseComplexFormulaTest) { delete prctlFileParser; } + +TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_THROW( + prctlParser = new storm::parser::PrctlParser("P > 0.5 [ a ]"), + storm::exceptions::WrongFileFormatException + ); + + delete prctlParser; +} + +TEST(PrctlParserTest, wrongFormulaTest) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_THROW( + prctlParser = new storm::parser::PrctlFileParser("& a"), + storm::exceptions::WrongFileFormatException + ); + delete prctlParser; +} + +TEST(PrctlParserTest, wrongFormulaTest2) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_THROW( + prctlParser = new storm::parser::PrctlFileParser("P>0 [ F & a ]"), + storm::exceptions::WrongFileFormatException + ); + delete prctlParser; +}