diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index bd75a73b2..30ad5eaec 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -47,27 +47,27 @@ struct LtlParser::LtlGrammar : qi::grammar *(qi::lit("|") > andFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]; - orFormula.name("state formula"); + orFormula.name("LTL formula"); andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]; - andFormula.name("state formula"); + andFormula.name("LTL formula"); untilFormula = notFormula[qi::_val = qi::_1] > *((qi::lit("U") >> qi::lit("<=") > qi::int_ > notFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_2, qi::_1)] | (qi::lit("U") > notFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]); notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val = phoenix::new_>(qi::_1)]; - notFormula.name("state formula"); + notFormula.name("LTL formula"); //This block defines rules for "atomic" state formulas //(Propositions, probabilistic/reward formulas, and state formulas in brackets) atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> ltlFormula >> qi::lit(")"); - atomicLtlFormula.name("state formula"); + atomicLtlFormula.name("LTL formula"); atomicProposition = (freeIdentifierName)[qi::_val = phoenix::new_>(qi::_1)]; - atomicProposition.name("state formula"); + atomicProposition.name("LTL formula"); /*probabilisticBoundOperator = ( (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::GREATER, qi::_1, qi::_2)] | @@ -89,16 +89,16 @@ struct LtlParser::LtlGrammar : qi::grammar> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; - boundedEventually.name("ltl formula"); - eventually = (qi::lit("F") > ltlFormula)[qi::_val = + boundedEventually.name("LTL formula"); + eventually = (qi::lit("F") >> ltlFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - eventually.name("ltl formula"); - globally = (qi::lit("G") > ltlFormula)[qi::_val = + eventually.name("LTL formula"); + globally = (qi::lit("G") >> ltlFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - globally.name("ltl formula"); + globally.name("LTL formula"); start = ltlFormula; start.name("LTL formula"); diff --git a/test/parser/LtlParserTest.cpp b/test/parser/LtlParserTest.cpp index cd2a842d6..27d00f01b 100644 --- a/test/parser/LtlParserTest.cpp +++ b/test/parser/LtlParserTest.cpp @@ -40,6 +40,44 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) { delete ltlParser; } +/*! + * The following test checks whether in the formula "F & b", F is correctly interpreted as proposition instead of the + * "Eventually" operator. + */ +TEST(LtlParserTest, parseAmbiguousFormulaTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("F & b") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + + ASSERT_EQ(ltlParser->getFormula()->toString(), "(F & b)"); + + delete ltlParser->getFormula(); + delete ltlParser; +} + +/*! + * The following test checks whether in the formula "F F", F is interpreted as "eventually" operator or atomic proposition, + * depending where it occurs. + */ +TEST(LtlParserTest, parseAmbiguousFormulaTest2) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("F F") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + + ASSERT_EQ(ltlParser->getFormula()->toString(), "F F"); + + delete ltlParser->getFormula(); + delete ltlParser; +} + TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { storm::parser::LtlParser* ltlParser = nullptr; ASSERT_NO_THROW( @@ -102,6 +140,13 @@ TEST(LtlParserTest, parseComplexFormulaTest) { ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlParser->getFormula()->toString()); delete ltlParser->getFormula(); delete ltlParser; - } +TEST(LtlParserTest, wrongFormulaTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_THROW( + ltlParser = new storm::parser::LtlParser("(a | b) & +"), + storm::exceptions::WrongFormatException + ); + delete ltlParser; +}