diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 659c9b3d4..e7b6accad 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -140,13 +140,13 @@ namespace storm { result << std::endl; for (auto const& element : booleanUndefinedConstantExpressions) { - result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + result << "const bool " << element.second->toString() << ";" << std::endl; } for (auto const& element : integerUndefinedConstantExpressions) { - result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + result << "const int " << element.second->toString() << ";" << std::endl; } for (auto const& element : doubleUndefinedConstantExpressions) { - result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + result << "const double " << element.second->toString() << ";" << std::endl; } result << std::endl; @@ -163,7 +163,7 @@ namespace storm { } for (auto const& rewardModel : rewards) { - result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl; + result << rewardModel.second.toString() << std::endl; } for (auto const& label : labels) { diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp index 51878942f..452fb278a 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp @@ -47,6 +47,8 @@ namespace storm { case MINUS: return resultLeft - resultRight; break; case TIMES: return resultLeft * resultRight; break; case DIVIDE: return resultLeft / resultRight; break; + case MIN: return std::min(resultLeft, resultRight); break; + case MAX: return std::max(resultLeft, resultRight); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Unknown numeric binary operator: '" << functionType << "'."; } @@ -64,6 +66,8 @@ namespace storm { case MINUS: return resultLeft - resultRight; break; case TIMES: return resultLeft * resultRight; break; case DIVIDE: return resultLeft / resultRight; break; + case MIN: return std::min(resultLeft, resultRight); break; + case MAX: return std::max(resultLeft, resultRight); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Unknown numeric binary operator: '" << functionType << "'."; } @@ -75,14 +79,14 @@ namespace storm { std::string BinaryNumericalFunctionExpression::toString() const { std::stringstream result; - result << "(" << this->getLeft()->toString(); switch (functionType) { - case PLUS: result << " + "; break; - case MINUS: result << " - "; break; - case TIMES: result << " * "; break; - case DIVIDE: result << " / "; break; + case PLUS: result << "(" << this->getLeft()->toString() << " + " << this->getRight()->toString() << ")"; break; + case MINUS: result << "(" << this->getLeft()->toString() << " - " << this->getRight()->toString() << ")"; break; + case TIMES: result << "(" << this->getLeft()->toString() << " * " << this->getRight()->toString() << ")"; break; + case DIVIDE: result << "(" << this->getLeft()->toString() << " / " << this->getRight()->toString() << ")"; break; + case MIN: result << "min(" << this->getLeft()->toString() << ", " << this->getRight()->toString() << ")"; break; + case MAX: result << "max(" << this->getLeft()->toString() << ", " << this->getRight()->toString() << ")"; break; } - result << this->getRight()->toString() << ")"; return result.str(); } diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 32b6b45fd..846ceb99a 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -22,7 +22,7 @@ namespace storm { /*! * An enum type specifying the different functions applicable. */ - enum FunctionType {PLUS, MINUS, TIMES, DIVIDE}; + enum FunctionType {PLUS, MINUS, TIMES, DIVIDE, MIN, MAX}; /*! * Creates a binary numerical function expression with the given type, children and function type. diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp index e4ac21e13..6b4b1fbb2 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp @@ -5,6 +5,8 @@ * Author: Christian Dehnert */ +#include + #include "UnaryNumericalFunctionExpression.h" namespace storm { @@ -35,6 +37,8 @@ namespace storm { int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues); switch(functionType) { case MINUS: return -resultChild; break; + case FLOOR: return static_cast(std::floor(resultChild)); break; + case CEIL: return static_cast(std::ceil(resultChild)); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Unknown numerical unary operator: '" << functionType << "'."; } @@ -48,6 +52,8 @@ namespace storm { double resultChild = this->getChild()->getValueAsDouble(variableValues); switch(functionType) { case MINUS: return -resultChild; break; + case FLOOR: return std::floor(resultChild); break; + case CEIL: return std::ceil(resultChild); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Unknown numerical unary operator: '" << functionType << "'."; } @@ -66,6 +72,8 @@ namespace storm { result << "("; switch (functionType) { case MINUS: result << "-"; break; + case FLOOR: result << "floor("; break; + case CEIL: result << "ceil("; break; } result << this->getChild()->toString() << ")"; diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index fbcbb7fe4..bcb942378 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -22,7 +22,7 @@ namespace storm { /*! * An enum type specifying the different functions applicable. */ - enum FunctionType {MINUS}; + enum FunctionType {MINUS, FLOOR, CEIL}; /*! * Creates a unary numerical function expression tree node with the given child and function type. diff --git a/src/parser/prismparser/BaseGrammar.h b/src/parser/prismparser/BaseGrammar.h index 6b0b37a8a..7cac493c3 100644 --- a/src/parser/prismparser/BaseGrammar.h +++ b/src/parser/prismparser/BaseGrammar.h @@ -127,6 +127,7 @@ namespace prism { std::shared_ptr createIntMult(std::shared_ptr const& left, std::shared_ptr const& right) { return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES)); } + /*! * Create a new integer multiplication expression. If multiplication is true, it will be an multiplication, otherwise a division. * @param left Left operand. @@ -141,6 +142,38 @@ namespace prism { return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::DIVIDE)); } } + + /*! + * Creates an integer min/max expression. + * + * @param min Indicates whether the expression is min or max. + * @param left The left operand. + * @param right The right operand. + * @return An integer min/max expression. + */ + std::shared_ptr createIntMinMax(bool min, std::shared_ptr const& left, std::shared_ptr const& right) { + if (min) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MIN)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MAX)); + } + } + + /*! + * Creates an integer floor/ceil expression. + * + * @param floor Indicates whether the expression is a floor expression. + * @param operand The argument of the floor/ceil operation. + * @return An integer floor/ceil expression. + */ + std::shared_ptr createIntFloorCeil(bool floor, std::shared_ptr const& operand) { + if (floor) { + return std::shared_ptr(new UnaryNumericalFunctionExpression(BaseExpression::int_, operand->clone(), UnaryNumericalFunctionExpression::FLOOR)); + } else { + return std::shared_ptr(new UnaryNumericalFunctionExpression(BaseExpression::int_, operand->clone(), UnaryNumericalFunctionExpression::CEIL)); + } + } + /*! * Create a new binary relation expression. * @param left Left operand. diff --git a/src/parser/prismparser/IntegerExpressionGrammar.cpp b/src/parser/prismparser/IntegerExpressionGrammar.cpp index 1c34b0b56..19170455c 100644 --- a/src/parser/prismparser/IntegerExpressionGrammar.cpp +++ b/src/parser/prismparser/IntegerExpressionGrammar.cpp @@ -19,9 +19,15 @@ namespace storm { integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]); integerMultExpression.name("integer expression"); - atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state)); + atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state)); atomicIntegerExpression.name("integer expression"); + integerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(",") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)]; + integerMinMaxExpression.name("integer min/max expression"); + + integerFloorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntFloorCeil, this, qi::_a, qi::_1)]; + integerFloorCeilExpression.name("integer floor/ceil expression"); + integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)]; integerVariableExpression.name("integer variable"); } diff --git a/src/parser/prismparser/IntegerExpressionGrammar.h b/src/parser/prismparser/IntegerExpressionGrammar.h index c04150761..7531ef36e 100644 --- a/src/parser/prismparser/IntegerExpressionGrammar.h +++ b/src/parser/prismparser/IntegerExpressionGrammar.h @@ -38,6 +38,8 @@ namespace storm { qi::rule(), Skipper> integerMultExpression; qi::rule(), Skipper> atomicIntegerExpression; qi::rule(), Skipper> integerVariableExpression; + qi::rule(), qi::locals, Skipper> integerMinMaxExpression; + qi::rule(), qi::locals, Skipper> integerFloorCeilExpression; }; } diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index e1182c751..4ab8fae58 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -179,7 +179,9 @@ namespace storm { assignmentDefinition.name("assignment"); assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = ((ConstDoubleExpressionGrammar::instance(this->state) | qi::attr(phoenix::construct>(phoenix::new_(1)))) >> qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)]; + updateDefinition = (((ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(":")) + | qi::attr(std::shared_ptr(new storm::ir::expressions::DoubleLiteralExpression(1))))[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] + >> assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list");