From e22f69933986cbd9988f093c9a3416a49d99cfa5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 12 Sep 2020 13:12:14 -0700 Subject: [PATCH] parser for predicates --- CHANGELOG.md | 6 +++++ .../parser/ExpressionCreator.cpp | 15 +++++++++++ src/storm-parsers/parser/ExpressionCreator.h | 1 + src/storm-parsers/parser/ExpressionParser.cpp | 11 ++++++-- src/storm-parsers/parser/ExpressionParser.h | 15 ++++++++++- src/storm-parsers/parser/PrismParser.h | 11 +++++--- src/storm/storage/expressions/Expression.cpp | 27 +++++++++++++++++++ src/storm/storage/expressions/Expression.h | 4 +++ .../expressions/SubstitutionVisitor.cpp | 20 ++++++++++++++ .../storage/expressions/SubstitutionVisitor.h | 3 ++- 10 files changed, 105 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 43b7c547a..8d21bab33 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,12 @@ Changelog This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. The releases of major and minor versions contain an overview of changes since the last major/minor update. +Branch Changes +-------------- + +- n-ary predicates like atMostOneOf, ExactlyOneOf added +- export to Dice expressions added + Version 1.6.x ------------- diff --git a/src/storm-parsers/parser/ExpressionCreator.cpp b/src/storm-parsers/parser/ExpressionCreator.cpp index f9a8ad0c2..7979156a1 100644 --- a/src/storm-parsers/parser/ExpressionCreator.cpp +++ b/src/storm-parsers/parser/ExpressionCreator.cpp @@ -230,6 +230,21 @@ namespace storm { } return manager.boolean(false); } + + storm::expressions::Expression ExpressionCreator::createPredicateExpression(storm::expressions::OperatorType const& opTyp, std::vector const&operands, bool &pass) const { + if (this->createExpressions) { + try { + switch (opTyp) { + case storm::expressions::OperatorType::AtLeastOneOf: return storm::expressions::atLeastOneOf(operands); + case storm::expressions::OperatorType::AtMostOneOf: return storm::expressions::atMostOneOf(operands); + case storm::expressions::OperatorType::ExactlyOneOf: return storm::expressions::exactlyOneOf(operands); + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } storm::expressions::Expression ExpressionCreator::getIdentifierExpression(std::string const& identifier, bool& pass) const { if (this->createExpressions) { diff --git a/src/storm-parsers/parser/ExpressionCreator.h b/src/storm-parsers/parser/ExpressionCreator.h index fb034c95e..f0f615c40 100644 --- a/src/storm-parsers/parser/ExpressionCreator.h +++ b/src/storm-parsers/parser/ExpressionCreator.h @@ -72,6 +72,7 @@ namespace storm { storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; storm::expressions::Expression createRoundExpression(storm::expressions::Expression const& e1, bool& pass) const; storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool& pass) const; + storm::expressions::Expression createPredicateExpression(storm::expressions::OperatorType const& opTyp, std::vector const& operands, bool& pass) const; private: diff --git a/src/storm-parsers/parser/ExpressionParser.cpp b/src/storm-parsers/parser/ExpressionParser.cpp index 9c371e4ac..1e18dafe1 100644 --- a/src/storm-parsers/parser/ExpressionParser.cpp +++ b/src/storm-parsers/parser/ExpressionParser.cpp @@ -44,7 +44,14 @@ namespace storm { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); - + + if (allowBacktracking) { + predicateExpression = ((predicateOperator_ >> qi::lit("(")) >> (expression % qi::lit(",") ) >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPredicateExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; + } else { + predicateExpression = ((predicateOperator_ >> qi::lit("(")) > (expression % qi::lit(",") ) > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPredicateExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; + } + predicateExpression.name("predicate expression"); + if (allowBacktracking) { floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; } else { @@ -84,7 +91,7 @@ namespace storm { | qi::long_long[qi::_val = phoenix::bind(&ExpressionCreator::createIntegerLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)]; literalExpression.name("literal expression"); - atomicExpression = floorCeilExpression | roundExpression | prefixPowerModuloExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression; + atomicExpression = predicateExpression | floorCeilExpression | roundExpression | prefixPowerModuloExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression; atomicExpression.name("atomic expression"); unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; diff --git a/src/storm-parsers/parser/ExpressionParser.h b/src/storm-parsers/parser/ExpressionParser.h index ff0bb69ed..4fe673d8b 100644 --- a/src/storm-parsers/parser/ExpressionParser.h +++ b/src/storm-parsers/parser/ExpressionParser.h @@ -211,7 +211,19 @@ namespace storm { // A parser used for recognizing the operators at the "power" precedence level. prefixPowerModuloOperatorStruct prefixPowerModuloOperator_; - + + struct predicateOperatorStruct : qi::symbols { + predicateOperatorStruct() { + add + ("atLeastOneOf", storm::expressions::OperatorType::AtLeastOneOf) + ("atMostOneOf", storm::expressions::OperatorType::AtMostOneOf) + ("exactlyOneOf", storm::expressions::OperatorType::ExactlyOneOf); + } + }; + + // A parser used for recognizing the operators at the "min/max" precedence level. + predicateOperatorStruct predicateOperator_; + std::unique_ptr expressionCreator; @@ -237,6 +249,7 @@ namespace storm { qi::rule, Skipper> minMaxExpression; qi::rule, Skipper> floorCeilExpression; qi::rule roundExpression; + qi::rule predicateExpression; qi::rule identifier; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index 2668dcb68..72611b0dc 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -128,10 +128,13 @@ namespace storm { ("max", 18) ("floor", 19) ("ceil", 20) - ("init", 21) - ("endinit", 22) - ("invariant", 23) - ("endinvariant", 24); + ("atLeastOneOf", 21) + ("atMostOneOf", 22) + ("exactlyOneOf", 23) + ("init", 24) + ("endinit", 25) + ("invariant", 26) + ("endinvariant", 27); } }; diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 873e21fc2..17eb4d30c 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -438,6 +438,33 @@ namespace storm { return ite(first < 0, floor(first), ceil(first)); } + Expression atLeastOneOf(std::vector const& expressions) { + STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "AtLeastOneOf requires arguments"); + std::vector> baseexpressions; + for(auto const& expr : expressions) { + baseexpressions.push_back(expr.getBaseExpressionPointer()); + } + return Expression(std::shared_ptr(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(), baseexpressions, PredicateExpression::PredicateType::AtLeastOneOf))); + } + + Expression atMostOneOf(std::vector const& expressions) { + STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "AtMostOneOf requires arguments"); + std::vector> baseexpressions; + for(auto const& expr : expressions) { + baseexpressions.push_back(expr.getBaseExpressionPointer()); + } + return Expression(std::shared_ptr(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(), baseexpressions, PredicateExpression::PredicateType::AtMostOneOf))); + } + + Expression exactlyOneOf(std::vector const& expressions) { + STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "ExactlyOneOf requires arguments"); + std::vector> baseexpressions; + for(auto const& expr : expressions) { + baseexpressions.push_back(expr.getBaseExpressionPointer()); + } + return Expression(std::shared_ptr(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(), baseexpressions, PredicateExpression::PredicateType::ExactlyOneOf))); + } + Expression disjunction(std::vector const& expressions) { return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; }); } diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index 22b07734e..f82439a36 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -60,6 +60,7 @@ namespace storm { friend Expression minimum(Expression const& first, Expression const& second); friend Expression maximum(Expression const& first, Expression const& second); + Expression() = default; ~Expression(); @@ -439,6 +440,9 @@ namespace storm { Expression modulo(Expression const& first, Expression const& second); Expression minimum(Expression const& first, Expression const& second); Expression maximum(Expression const& first, Expression const& second); + Expression atLeastOneOf(std::vector const& expressions); + Expression atMostOneOf(std::vector const& expressions); + Expression exactlyOneOf(std::vector const& expressions); Expression disjunction(std::vector const& expressions); Expression conjunction(std::vector const& expressions); Expression sum(std::vector const& expressions); diff --git a/src/storm/storage/expressions/SubstitutionVisitor.cpp b/src/storm/storage/expressions/SubstitutionVisitor.cpp index e835806c6..47f3f7139 100644 --- a/src/storm/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storm/storage/expressions/SubstitutionVisitor.cpp @@ -104,6 +104,26 @@ namespace storm { return std::const_pointer_cast(std::shared_ptr(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType()))); } } + + template + boost::any SubstitutionVisitor::visit(PredicateExpression const& expression, boost::any const& data) { + bool changed = false; + std::vector> newExpressions; + for (uint64_t i = 0; i < expression.getArity(); ++i) { + newExpressions.push_back(boost::any_cast>(expression.getOperand(i)->accept(*this, data))); + if (!changed && newExpressions.back() == expression.getOperand(i)) { + changed = true; + } + } + + // If the arguments did not change, we simply push the expression itself. + if (!changed) { + return expression.getSharedPointer(); + } else { + return std::const_pointer_cast(std::shared_ptr(new PredicateExpression(expression.getManager(), expression.getType(), newExpressions, expression.getPredicateType()))); + } + } + template boost::any SubstitutionVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) { diff --git a/src/storm/storage/expressions/SubstitutionVisitor.h b/src/storm/storage/expressions/SubstitutionVisitor.h index 99f0c2c18..fc2028858 100644 --- a/src/storm/storage/expressions/SubstitutionVisitor.h +++ b/src/storm/storage/expressions/SubstitutionVisitor.h @@ -38,7 +38,8 @@ namespace storm { virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; - + virtual boost::any visit(PredicateExpression const& expression, boost::any const& data) override; + protected: // A mapping of variables to expressions with which they shall be replaced. MapType const& variableToExpressionMapping;