From 39ec9401ef67f7fe96df45b4b7a44c7650c7ee6f Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 Apr 2014 13:23:53 +0200 Subject: [PATCH] Fixed the PrismParser so the exact format of PRISMs boolean expressions can now be parsed. Former-commit-id: bb08ec1646a7890cc768b4b4462c0af613d079b4 --- src/parser/PrismParser.cpp | 36 +++++++++---------- src/parser/PrismParser.h | 5 ++- .../BinaryBooleanFunctionExpression.cpp | 4 +-- test/functional/parser/PrismParserTest.cpp | 2 +- 4 files changed, 21 insertions(+), 26 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 33373782e..ed15050cb 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -88,10 +88,13 @@ namespace storm { plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]]; plusExpression.name("plus expression"); - relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; + relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; relativeExpression.name("relative expression"); - andExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("&")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And] | qi::lit("<=>")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff] | qi::lit("^")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor]) >> relativeExpression)[phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And) [ qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [ phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff) [ qi::_val = phoenix::bind(&PrismParser::createIffExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createXorExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ] ]; + equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ]; + equalityExpression.name("equality expression"); + + andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; andExpression.name("and expression"); orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ]; @@ -204,6 +207,7 @@ namespace storm { qi::on_error(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -327,27 +331,15 @@ namespace storm { } } - storm::expressions::Expression PrismParser::createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { - if (!this->secondRun) { - return storm::expressions::Expression::createFalse(); - } else { - return e1.iff(e2); - } - } - - storm::expressions::Expression PrismParser::createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { - if (!this->secondRun) { - return storm::expressions::Expression::createFalse(); - } else { - return e1 ^ e2; - } - } - storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 == e2; + if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { + return e1.iff(e2); + } else { + return e1 == e2; + } } } @@ -355,7 +347,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 != e2; + if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { + return e1 ^ e2; + } else { + return e1 != e2; + } } } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 15acef30b..4a0eec392 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -246,8 +246,9 @@ namespace storm { qi::rule expression; qi::rule iteExpression; qi::rule, Skipper> orExpression; - qi::rule, Skipper> andExpression; + qi::rule andExpression; qi::rule relativeExpression; + qi::rule, Skipper> equalityExpression; qi::rule, Skipper> plusExpression; qi::rule, Skipper> multiplicationExpression; qi::rule unaryExpression; @@ -277,8 +278,6 @@ namespace storm { storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; - storm::expressions::Expression createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; - storm::expressions::Expression createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index d5d6694ab..02cd9686b 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -90,9 +90,9 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: stream << " & "; break; case OperatorType::Or: stream << " | "; break; - case OperatorType::Xor: stream << " ^ "; break; + case OperatorType::Xor: stream << " != "; break; case OperatorType::Implies: stream << " => "; break; - case OperatorType::Iff: stream << " <=> "; break; + case OperatorType::Iff: stream << " = "; break; } stream << *this->getSecondOperand() << ")"; } diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 381ca3e1b..81731114b 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -47,7 +47,7 @@ TEST(PrismParser, SimpleFullTest) { R"(dtmc module mod1 b : bool; - [a] true -> 1: (b'=true ^ false <=> b => false); + [a] true -> 1: (b'=true != false = b => false); endmodule)"; storm::prism::Program result;