diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index a246aacaf..8538c8d3f 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -40,7 +40,15 @@ namespace parser { template struct CslParser::CslGrammar : qi::grammar*(), Skipper > { CslGrammar() : CslGrammar::base_type(start) { - freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; + //This block contains helper rules that may be used several times + freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; + comparisonType = ( + (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | + (qi::lit(">"))[qi::_val = storm::property::GREATER] | + (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | + (qi::lit("<"))[qi::_val = storm::property::LESS]); + //Comment: Empty line or line starting with "//" + comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; //This block defines rules for parsing state formulas stateFormula %= orFormula; @@ -63,25 +71,13 @@ struct CslParser::CslGrammar : qi::grammar>(qi::_1)]; atomicProposition.name("state formula"); probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] + (qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); probabilisticBoundOperator.name("state formula"); steadyStateBoundOperator = ( - (qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] + (qi::lit("S") >> comparisonType > qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); steadyStateBoundOperator.name("state formula"); @@ -126,11 +122,18 @@ struct CslParser::CslGrammar : qi::grammar>(phoenix::bind(&storm::property::csl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; until.name("path formula (for probabilistic operator)"); - start = (noBoundOperator | stateFormula); + formula = (noBoundOperator | stateFormula); + formula.name("CSL formula"); + + start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] | + comment + ) > qi::eoi; start.name("CSL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> formula; + qi::rule*(), Skipper> comment; qi::rule*(), Skipper> stateFormula; qi::rule*(), Skipper> atomicStateFormula; @@ -155,6 +158,7 @@ struct CslParser::CslGrammar : qi::grammar freeIdentifierName; + qi::rule comparisonType; }; diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 060ad5e21..6060adedc 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -43,6 +43,11 @@ namespace parser { template struct LtlParser::LtlGrammar : qi::grammar*(), Skipper > { LtlGrammar() : LtlGrammar::base_type(start) { + //This block contains helper rules that may be used several times + freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; + //Comment: Empty line or line starting with "//" + comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; + freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; //This block defines rules for parsing state formulas @@ -68,27 +73,9 @@ struct LtlParser::LtlGrammar : qi::grammar>(qi::_1)]; atomicProposition.name("LTL formula"); - /*probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] - ); - probabilisticBoundOperator.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("[") >> LtlFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1)]; - probabilisticNoBoundOperator.name("no bound operator");*/ //This block defines rules for parsing probabilistic path formulas - pathFormula = (boundedEventually | eventually | globally);//(boundedEventually | eventually | globally | boundedUntil | until); + pathFormula = (boundedEventually | eventually | globally); pathFormula.name("LTL formula"); boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; @@ -100,11 +87,14 @@ struct LtlParser::LtlGrammar : qi::grammar >(qi::_1)]; globally.name("LTL formula"); - start = ltlFormula; + start = (((ltlFormula) > (comment | qi::eps))[qi::_val = qi::_1] | + comment + ) > qi::eoi; start.name("LTL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> comment; qi::rule*(), Skipper> ltlFormula; qi::rule*(), Skipper> atomicLtlFormula; diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 446a6feb5..88098561d 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -35,7 +35,6 @@ namespace parser { template struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper > { PrctlGrammar() : PrctlGrammar::base_type(start) { - //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; comparisonType = ( diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index ebf7250a9..f6657289c 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -116,7 +116,7 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { TEST(CslParserTest, parseComplexFormulaTest) { storm::parser::CslParser* cslParser = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ])") + cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment") ); ASSERT_NE(cslParser->getFormula(), nullptr); diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index 1a50ddb28..c88885372 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -132,7 +132,7 @@ TEST(LtlParserTest, parseComplexUntilTest) { TEST(LtlParserTest, parseComplexFormulaTest) { storm::parser::LtlParser* ltlParser = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b") + ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b //and a comment :P") ); ASSERT_NE(ltlParser->getFormula(), nullptr); @@ -145,7 +145,7 @@ TEST(LtlParserTest, parseComplexFormulaTest) { TEST(LtlParserTest, wrongFormulaTest) { storm::parser::LtlParser* ltlParser = nullptr; ASSERT_THROW( - ltlParser = new storm::parser::LtlParser("(a | b) & +"), + ltlParser = new storm::parser::LtlParser("(a | c) & +"), storm::exceptions::WrongFormatException ); delete ltlParser;