parser for predicates

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
 -------------

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<storm::expressions::Expression> 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) {

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<storm::expressions::Expression> const& operands, bool& pass) const;
             
             
         private:

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)];

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<char, storm::expressions::OperatorType> {
+                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> expressionCreator;
             
@@ -237,6 +249,7 @@ namespace storm {
             qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::OperatorType>, Skipper> minMaxExpression;
             qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::OperatorType>, Skipper> floorCeilExpression;
             qi::rule<Iterator, storm::expressions::Expression(), Skipper> roundExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> predicateExpression;
             qi::rule<Iterator, std::string(), Skipper> identifier;
             
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).

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);
                 }
             };
             

src/storm/storage/expressions/Expression.cpp

@@ -438,6 +438,33 @@ namespace storm {
             return ite(first < 0, floor(first), ceil(first));
         }
 
+        Expression atLeastOneOf(std::vector<Expression> const& expressions) {
+            STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "AtLeastOneOf requires arguments");
+            std::vector<std::shared_ptr<BaseExpression const>> baseexpressions;
+            for(auto const& expr : expressions) {
+                baseexpressions.push_back(expr.getBaseExpressionPointer());
+            }
+            return Expression(std::shared_ptr<BaseExpression>(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(), baseexpressions, PredicateExpression::PredicateType::AtLeastOneOf)));
+        }
+
+        Expression atMostOneOf(std::vector<Expression> const& expressions) {
+            STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "AtMostOneOf requires arguments");
+            std::vector<std::shared_ptr<BaseExpression const>> baseexpressions;
+            for(auto const& expr : expressions) {
+                baseexpressions.push_back(expr.getBaseExpressionPointer());
+            }
+            return Expression(std::shared_ptr<BaseExpression>(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(), baseexpressions, PredicateExpression::PredicateType::AtMostOneOf)));
+        }
+
+        Expression exactlyOneOf(std::vector<Expression> const& expressions) {
+            STORM_LOG_THROW(expressions.size() > 0, storm::exceptions::InvalidArgumentException, "ExactlyOneOf requires arguments");
+            std::vector<std::shared_ptr<BaseExpression const>> baseexpressions;
+            for(auto const& expr : expressions) {
+                baseexpressions.push_back(expr.getBaseExpressionPointer());
+            }
+            return Expression(std::shared_ptr<BaseExpression>(new PredicateExpression(expressions.front().getManager(), expressions.front().getManager().getBooleanType(), baseexpressions, PredicateExpression::PredicateType::ExactlyOneOf)));
+        }
+
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions) {
             return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; });
         }

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<storm::expressions::Expression> const& expressions);
+        Expression atMostOneOf(std::vector<storm::expressions::Expression> const& expressions);
+        Expression exactlyOneOf(std::vector<storm::expressions::Expression> const& expressions);
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions);
         Expression conjunction(std::vector<storm::expressions::Expression> const& expressions);
         Expression sum(std::vector<storm::expressions::Expression> const& expressions);

src/storm/storage/expressions/SubstitutionVisitor.cpp

@@ -104,6 +104,26 @@ namespace storm {
 				return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
             }
         }
+
+        template<typename MapType>
+        boost::any SubstitutionVisitor<MapType>::visit(PredicateExpression const& expression, boost::any const& data) {
+            bool changed = false;
+            std::vector<std::shared_ptr<BaseExpression const>> newExpressions;
+            for (uint64_t i = 0; i < expression.getArity(); ++i) {
+                newExpressions.push_back(boost::any_cast<std::shared_ptr<BaseExpression const>>(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<BaseExpression const>(std::shared_ptr<BaseExpression>(new PredicateExpression(expression.getManager(), expression.getType(), newExpressions, expression.getPredicateType())));
+            }
+        }
+
         
 		template<typename MapType>
         boost::any SubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const& expression, boost::any const&) {

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;