diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 6039c2c11..f46b3f691 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -91,10 +91,10 @@ namespace storm { 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.name("relative expression"); - andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + 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) ] ] ]; andExpression.name("and expression"); - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + 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)] ]; orExpression.name("or expression"); iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; @@ -271,6 +271,14 @@ namespace storm { } } + storm::expressions::Expression PrismParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.implies(e2); + } + } + storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); @@ -319,6 +327,22 @@ 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(); diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 3f8f17b65..de3effa32 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -25,6 +25,7 @@ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost: #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Expressions.h" #include "src/exceptions/ExceptionMacros.h" namespace storm { @@ -244,8 +245,8 @@ namespace storm { // Rules for parsing a composed expression. qi::rule expression; qi::rule iteExpression; - qi::rule orExpression; - qi::rule andExpression; + qi::rule, Skipper> orExpression; + qi::rule, Skipper> andExpression; qi::rule relativeExpression; qi::rule, Skipper> plusExpression; qi::rule, Skipper> multiplicationExpression; @@ -269,12 +270,15 @@ namespace storm { bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; + storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; 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 9f5e5edeb..d5d6694ab 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -23,6 +23,7 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break; case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break; + case OperatorType::Xor: result = firstOperandEvaluation ^ secondOperandEvaluation; break; case OperatorType::Implies: result = !firstOperandEvaluation || secondOperandEvaluation; break; case OperatorType::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break; } @@ -55,6 +56,7 @@ namespace storm { return firstOperandSimplified; } break; + case OperatorType::Xor: break; case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { return secondOperandSimplified; } else if (firstOperandSimplified->isFalse()) { @@ -88,6 +90,7 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: stream << " & "; break; case OperatorType::Or: stream << " | "; break; + case OperatorType::Xor: stream << " ^ "; break; case OperatorType::Implies: stream << " => "; break; case OperatorType::Iff: stream << " <=> "; break; } diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index 7a05a1ab5..8b1bb7437 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -11,7 +11,7 @@ namespace storm { /*! * An enum type specifying the different operators applicable. */ - enum class OperatorType {And, Or, Implies, Iff}; + enum class OperatorType {And, Or, Xor, Implies, Iff}; /*! * Creates a binary boolean function expression with the given return type, operands and operator. diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 7eb94966b..5b5a2bfb6 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -166,6 +166,11 @@ namespace storm { return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide))); } + Expression Expression::operator^(Expression const& other) const { + LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '^' requires boolean operands."); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); + } + Expression Expression::operator&&(Expression const& other) const { LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index ea7d99572..d751dfbb9 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -47,6 +47,7 @@ namespace storm { Expression operator-() const; Expression operator*(Expression const& other) const; Expression operator/(Expression const& other) const; + Expression operator^(Expression const& other) const; Expression operator&&(Expression const& other) const; Expression operator||(Expression const& other) const; Expression operator!() const; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 739d9ca5b..381ca3e1b 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); + [a] true -> 1: (b'=true ^ false <=> b => false); endmodule)"; storm::prism::Program result; diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 0c19c5bfb..6ce9f50c5 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -264,6 +264,12 @@ TEST(Expression, OperatorTest) { ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = trueExpression ^ falseExpression); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolConstExpression); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression.floor()); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);