diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 6b4a78c99..6e0132ff8 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -37,14 +37,16 @@ struct PrctlParser::PrctlGrammar : qi::grammar> stateFormula >> qi::lit("&") >> stateFormula >> qi::lit(")"))[ - qi::_val = phoenix::new_>(qi::_1, qi::_2)]; - orFormula = (qi::lit("(") >> stateFormula >> qi::lit("|") >> stateFormula >> qi::lit(")"))[qi::_val = - phoenix::new_>(qi::_1, qi::_2)]; - notFormula = (qi::lit("!") >> stateFormula)[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 = + phoenix::new_>(qi::_val, qi::_1)]; + notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") >> atomicStateFormula)[qi::_val = phoenix::new_>(qi::_1)]; + + atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")"); atomicProposition = (freeIdentifierName)[qi::_val = phoenix::new_>(qi::_1)]; probabilisticBoundOperator = ( @@ -95,10 +97,12 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> start; qi::rule*(), Skipper> stateFormula; - qi::rule*(), Skipper> andFormula; - qi::rule*(), Skipper> atomicProposition; - qi::rule*(), Skipper> orFormula; - qi::rule*(), Skipper> notFormula; + qi::rule*(), Skipper> atomicStateFormula; + + qi::rule*(), Skipper> andFormula; + qi::rule*(), Skipper> atomicProposition; + qi::rule*(), Skipper> orFormula; + qi::rule*(), Skipper> notFormula; qi::rule*(), Skipper> probabilisticBoundOperator; qi::rule*(), Skipper> rewardBoundOperator; diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index 058271207..6d795819c 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -35,7 +35,7 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) { ASSERT_NE(prctlParser->getFormula(), nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "!(a && b)"); + ASSERT_EQ(prctlParser->getFormula()->toString(), "(!(a && b) || (a && !c))"); delete prctlParser->getFormula(); delete prctlParser; diff --git a/test/parser/prctl_files/complexFormula.prctl b/test/parser/prctl_files/complexFormula.prctl index 0cf4504b9..fef75f247 100644 --- a/test/parser/prctl_files/complexFormula.prctl +++ b/test/parser/prctl_files/complexFormula.prctl @@ -1 +1 @@ -(P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 (a & b)] ] | !P < 0.4 [ G !b ])) \ No newline at end of file +(P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ])) \ No newline at end of file diff --git a/test/parser/prctl_files/propositionalFormula.prctl b/test/parser/prctl_files/propositionalFormula.prctl index 62ed48627..25827e9c4 100644 --- a/test/parser/prctl_files/propositionalFormula.prctl +++ b/test/parser/prctl_files/propositionalFormula.prctl @@ -1 +1 @@ -!(a & b) \ No newline at end of file +!(a & b) | a & ! c \ No newline at end of file diff --git a/test/parser/prctl_files/rewardNoBoundFormula.prctl b/test/parser/prctl_files/rewardNoBoundFormula.prctl index c3415980c..09caf07f7 100644 --- a/test/parser/prctl_files/rewardNoBoundFormula.prctl +++ b/test/parser/prctl_files/rewardNoBoundFormula.prctl @@ -1 +1 @@ -R = ? [ a U <= 4 (b & !c) ] \ No newline at end of file +R = ? [ a U <= 4 b & (!c) ] \ No newline at end of file