From c18340b76a5435e424e5ef935fc2bf6cafb3619c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 9 Apr 2018 22:08:04 +0200 Subject: [PATCH] added mod as binary operation in expressions and slightly extended JANI support for filters --- src/storm/adapters/AddExpressionAdapter.cpp | 3 ++ src/storm/parser/ExpressionCreator.cpp | 3 +- src/storm/parser/ExpressionCreator.h | 2 +- src/storm/parser/ExpressionParser.cpp | 22 ++++++----- src/storm/parser/ExpressionParser.h | 22 ++++++----- src/storm/parser/JaniParser.cpp | 35 +++++++++++++---- .../BinaryNumericalFunctionExpression.cpp | 38 ++++++++++++++----- .../BinaryNumericalFunctionExpression.h | 2 +- src/storm/storage/expressions/Expression.cpp | 5 +++ src/storm/storage/expressions/Expression.h | 1 + .../expressions/LinearityCheckVisitor.cpp | 1 + .../storage/expressions/OperatorType.cpp | 1 + src/storm/storage/expressions/OperatorType.h | 1 + .../storage/expressions/ToCppVisitor.cpp | 7 ++++ .../expressions/ToExprtkStringVisitor.cpp | 7 ++++ .../expressions/ToRationalNumberVisitor.cpp | 5 ++- src/storm/storage/jani/JSONExporter.cpp | 2 + 17 files changed, 116 insertions(+), 41 deletions(-) diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index f792584a8..c713cae38 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -111,6 +111,9 @@ namespace storm { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power: result = leftResult.pow(rightResult); break; + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Modulo: + result = leftResult.mod(rightResult); + break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate expression containing power operator."); } diff --git a/src/storm/parser/ExpressionCreator.cpp b/src/storm/parser/ExpressionCreator.cpp index 6266206ef..b96dd5080 100644 --- a/src/storm/parser/ExpressionCreator.cpp +++ b/src/storm/parser/ExpressionCreator.cpp @@ -120,11 +120,12 @@ namespace storm { return manager.boolean(false); } - storm::expressions::Expression ExpressionCreator::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + storm::expressions::Expression ExpressionCreator::createPowerModuloExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { if (this->createExpressions) { try { switch (operatorType) { case storm::expressions::OperatorType::Power: return e1 ^ e2; break; + case storm::expressions::OperatorType::Modulo: return e1 % e2; break; default: STORM_LOG_ASSERT(false, "Invalid operation."); break; } } catch (storm::exceptions::InvalidTypeException const& e) { diff --git a/src/storm/parser/ExpressionCreator.h b/src/storm/parser/ExpressionCreator.h index bf454c552..20bcc5854 100644 --- a/src/storm/parser/ExpressionCreator.h +++ b/src/storm/parser/ExpressionCreator.h @@ -67,7 +67,7 @@ namespace storm { storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createPowerModuloExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const; storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const; diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp index 492fb337d..64e185b54 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm/parser/ExpressionParser.cpp @@ -36,7 +36,7 @@ namespace boost { namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerModuloOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerModuloOperator_(), invalidIdentifiers_(invalidIdentifiers_) { expressionCreator = new ExpressionCreator(manager); @@ -58,11 +58,13 @@ namespace storm { minMaxExpression.name("min/max expression"); if (allowBacktracking) { - prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; + prefixPowerModuloExpression = ((prefixPowerModuloOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)] + | (qi::lit("func") >> qi::lit("(") >> prefixPowerModuloOperator_ >> qi::lit(",") >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; } else { - prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; + prefixPowerModuloExpression = ((prefixPowerModuloOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)] + | ((qi::lit("func") >> qi::lit("(")) > prefixPowerModuloOperator_ > qi::lit(",") > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; } - prefixPowerExpression.name("pow expression"); + prefixPowerModuloExpression.name("power/modulo expression"); identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionCreator::getIdentifierExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)]; identifierExpression.name("identifier expression"); @@ -73,23 +75,23 @@ namespace storm { | qi::int_[qi::_val = phoenix::bind(&ExpressionCreator::createIntegerLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)]; literalExpression.name("literal expression"); - atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression; + atomicExpression = floorCeilExpression | 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)]; unaryExpression.name("unary expression"); if (allowBacktracking) { - infixPowerExpression = unaryExpression[qi::_val = qi::_1] >> -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; + infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] >> -(infixPowerModuloOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; + infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerModuloOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } - infixPowerExpression.name("power expression"); + infixPowerModuloExpression.name("power/modulo expression"); if (allowBacktracking) { - multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; + multiplicationExpression = infixPowerModuloExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerModuloExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; + multiplicationExpression = infixPowerModuloExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerModuloExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } multiplicationExpression.name("multiplication expression"); diff --git a/src/storm/parser/ExpressionParser.h b/src/storm/parser/ExpressionParser.h index da3282b1b..3c5b093fd 100644 --- a/src/storm/parser/ExpressionParser.h +++ b/src/storm/parser/ExpressionParser.h @@ -149,15 +149,16 @@ namespace storm { // A parser used for recognizing the operators at the "multiplication" precedence level. multiplicationOperatorStruct multiplicationOperator_; - struct infixPowerOperatorStruct : qi::symbols { - infixPowerOperatorStruct() { + struct infixPowerModuloOperatorStruct : qi::symbols { + infixPowerModuloOperatorStruct() { add - ("^", storm::expressions::OperatorType::Power); + ("^", storm::expressions::OperatorType::Power) + ("%", storm::expressions::OperatorType::Modulo); } }; // A parser used for recognizing the operators at the "power" precedence level. - infixPowerOperatorStruct infixPowerOperator_; + infixPowerModuloOperatorStruct infixPowerModuloOperator_; struct unaryOperatorStruct : qi::symbols { unaryOperatorStruct() { @@ -192,15 +193,16 @@ namespace storm { // A parser used for recognizing the operators at the "min/max" precedence level. minMaxOperatorStruct minMaxOperator_; - struct prefixPowerOperatorStruct : qi::symbols { - prefixPowerOperatorStruct() { + struct prefixPowerModuloOperatorStruct : qi::symbols { + prefixPowerModuloOperatorStruct() { add - ("pow", storm::expressions::OperatorType::Power); + ("pow", storm::expressions::OperatorType::Power) + ("mod", storm::expressions::OperatorType::Modulo); } }; // A parser used for recognizing the operators at the "power" precedence level. - prefixPowerOperatorStruct prefixPowerOperator_; + prefixPowerModuloOperatorStruct prefixPowerModuloOperator_; ExpressionCreator* expressionCreator; @@ -218,8 +220,8 @@ namespace storm { qi::rule, Skipper> equalityExpression; qi::rule, Skipper> plusExpression; qi::rule, Skipper> multiplicationExpression; - qi::rule, Skipper> prefixPowerExpression; - qi::rule, Skipper> infixPowerExpression; + qi::rule, Skipper> prefixPowerModuloExpression; + qi::rule, Skipper> infixPowerModuloExpression; qi::rule unaryExpression; qi::rule atomicExpression; qi::rule literalExpression; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 3de6bb2cc..a428ce4fa 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -140,9 +140,9 @@ namespace storm { auto prop = this->parseProperty(propertyEntry, globalVars, constants); properties.emplace(prop.getName(), prop); } catch (storm::exceptions::NotSupportedException const& ex) { - STORM_LOG_WARN("Cannot handle property " << ex.what()); + STORM_LOG_WARN("Cannot handle property: " << ex.what()); } catch (storm::exceptions::NotImplementedException const& ex) { - STORM_LOG_WARN("Cannot handle property " << ex.what()); + STORM_LOG_WARN("Cannot handle property: " << ex.what()); } } } @@ -433,6 +433,12 @@ namespace storm { assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared(oper, args[0], args[1]); + } else if (opString == "⇒") { + assert(bound == boost::none); + std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, globalVars, constants, ""); + assert(args.size() == 2); + std::shared_ptr tmp = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + return std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, tmp, args[1]); } else if (opString == "¬") { assert(bound == boost::none); std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, globalVars, constants, ""); @@ -514,12 +520,27 @@ namespace storm { } STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); - STORM_LOG_THROW(expressionStructure.at("states").count("op") > 0, storm::exceptions::NotImplementedException, "We only support properties where the filter has initial states"); - std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); - STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); + std::shared_ptr statesFormula; + if (expressionStructure.at("states").count("op") > 0) { + std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); + if (statesDescr == "initial") { + statesFormula = std::make_shared("init"); + } + } + if (!statesFormula) { + try { + // Try to parse the states as formula. + statesFormula = parseFormula(expressionStructure.at("states"), storm::logic::FormulaContext::Undefined, globalVars, constants, "Values of property " + name); + } catch (storm::exceptions::NotSupportedException const& ex) { + throw ex; + } catch (storm::exceptions::NotImplementedException const& ex) { + throw ex; + } + } + STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, globalVars, constants, "Values of property " + name); - return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), comment); } std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::unordered_map> const& constants, std::string const& scopeDescription) { @@ -805,7 +826,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 2cd3c2f61..92ed03c5c 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -6,11 +6,13 @@ #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" #include "storm/storage/expressions/ExpressionVisitor.h" + #include "storm/utility/macros.h" +#include "storm/utility/constants.h" +#include "storm/utility/NumberTraits.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidStateException.h" - namespace storm { namespace expressions { BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType) : BinaryExpression(manager, type, firstOperand, secondOperand), operatorType(operatorType) { @@ -31,6 +33,7 @@ namespace storm { case OperatorType::Min: result = storm::expressions::OperatorType::Min; break; case OperatorType::Max: result = storm::expressions::OperatorType::Max; break; case OperatorType::Power: result = storm::expressions::OperatorType::Power; break; + case OperatorType::Modulo: result = storm::expressions::OperatorType::Modulo; break; } return result; } @@ -49,6 +52,7 @@ namespace storm { case OperatorType::Min: result = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: result = std::max(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Power: result = static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; + case OperatorType::Modulo: result = firstOperandEvaluation % secondOperandEvaluation; break; } return result; } @@ -67,6 +71,7 @@ namespace storm { case OperatorType::Min: result = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: result = std::max(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Power: result = std::pow(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Modulo: result = std::fmod(firstOperandEvaluation, secondOperandEvaluation); break; } return result; } @@ -79,7 +84,7 @@ namespace storm { if (this->hasIntegerType()) { int_fast64_t firstOperandEvaluation = firstOperandSimplified->evaluateAsInt(); int_fast64_t secondOperandEvaluation = secondOperandSimplified->evaluateAsInt(); - int_fast64_t newValue = 0; + boost::optional newValue; switch (this->getOperatorType()) { case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break; case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break; @@ -87,28 +92,40 @@ namespace storm { case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Power: newValue = static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; - case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; + case OperatorType::Modulo: newValue = firstOperandEvaluation % secondOperandEvaluation; break; + case OperatorType::Divide: break; // do not simplify division. + } + if (newValue) { + return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), newValue.get())); } - return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), newValue)); } else if (this->hasRationalType()) { storm::RationalNumber firstOperandEvaluation = firstOperandSimplified->evaluateAsRational(); storm::RationalNumber secondOperandEvaluation = secondOperandSimplified->evaluateAsRational(); - storm::RationalNumber newValue = 0; + boost::optional newValue; switch (this->getOperatorType()) { case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break; case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break; case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break; case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break; case OperatorType::Power: { - STORM_LOG_THROW(carl::isInteger(secondOperandEvaluation), storm::exceptions::InvalidStateException, "Can not simplify pow() with fractional exponent."); - std::size_t exponent = carl::toInt(secondOperandEvaluation); - newValue = carl::pow(firstOperandEvaluation, exponent); + if (carl::isInteger(secondOperandEvaluation)) { + std::size_t exponent = carl::toInt(secondOperandEvaluation); + newValue = carl::pow(firstOperandEvaluation, exponent); + } break; } - case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; + case OperatorType::Modulo: { + if (carl::isInteger(firstOperandEvaluation) && carl::isInteger(secondOperandEvaluation)) { + newValue = storm::utility::mod(storm::utility::numerator(firstOperandEvaluation), storm::utility::numerator(secondOperandEvaluation)); + } + break; + } + } + if (newValue) { + return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue.get())); } - return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); } } @@ -137,6 +154,7 @@ namespace storm { case OperatorType::Min: stream << "min(" << *this->getFirstOperand() << ", " << *this->getSecondOperand() << ")"; break; case OperatorType::Max: stream << "max(" << *this->getFirstOperand() << ", " << *this->getSecondOperand() << ")"; break; case OperatorType::Power: stream << *this->getFirstOperand() << " ^ " << *this->getSecondOperand(); break; + case OperatorType::Modulo: stream << *this->getFirstOperand() << " % " << *this->getSecondOperand(); break; } stream << ")"; } diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h index 1e9adb028..1879b141d 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h @@ -11,7 +11,7 @@ namespace storm { /*! * An enum type specifying the different operators applicable. */ - enum class OperatorType {Plus, Minus, Times, Divide, Min, Max, Power}; + enum class OperatorType {Plus, Minus, Times, Divide, Min, Max, Power, Modulo}; /*! * Constructs a binary numerical function expression with the given return type, operands and operator. diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 1537e633e..2ec1604a7 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -277,6 +277,11 @@ namespace storm { return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power))); } + Expression operator%(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo))); + } + Expression operator&&(Expression const& first, Expression const& second) { if (!first.isInitialized()) { return second; diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index 98a2e6417..99d409e2e 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -33,6 +33,7 @@ namespace storm { friend Expression operator*(Expression const& first, Expression const& second); friend Expression operator/(Expression const& first, Expression const& second); friend Expression operator^(Expression const& first, Expression const& second); + friend Expression operator%(Expression const& first, Expression const& second); friend Expression operator&&(Expression const& first, Expression const& second); friend Expression operator||(Expression const& first, Expression const& second); friend Expression operator!(Expression const& first); diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.cpp b/src/storm/storage/expressions/LinearityCheckVisitor.cpp index 9eeb3ea56..86650acea 100644 --- a/src/storm/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storm/storage/expressions/LinearityCheckVisitor.cpp @@ -77,6 +77,7 @@ namespace storm { case BinaryNumericalFunctionExpression::OperatorType::Min: return LinearityStatus::NonLinear; break; case BinaryNumericalFunctionExpression::OperatorType::Max: return LinearityStatus::NonLinear; break; case BinaryNumericalFunctionExpression::OperatorType::Power: return LinearityStatus::NonLinear; break; + case BinaryNumericalFunctionExpression::OperatorType::Modulo: return LinearityStatus::NonLinear; break; } STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal binary numerical expression operator."); } diff --git a/src/storm/storage/expressions/OperatorType.cpp b/src/storm/storage/expressions/OperatorType.cpp index 1036869bc..bba61a653 100644 --- a/src/storm/storage/expressions/OperatorType.cpp +++ b/src/storm/storage/expressions/OperatorType.cpp @@ -16,6 +16,7 @@ namespace storm { case OperatorType::Min: stream << "min"; break; case OperatorType::Max: stream << "max"; break; case OperatorType::Power: stream << "^"; break; + case OperatorType::Modulo: stream << "%"; break; case OperatorType::Equal: stream << "="; break; case OperatorType::NotEqual: stream << "!="; break; case OperatorType::Less: stream << "<"; break; diff --git a/src/storm/storage/expressions/OperatorType.h b/src/storm/storage/expressions/OperatorType.h index f056f494a..e334b8104 100644 --- a/src/storm/storage/expressions/OperatorType.h +++ b/src/storm/storage/expressions/OperatorType.h @@ -19,6 +19,7 @@ namespace storm { Min, Max, Power, + Modulo, Equal, NotEqual, Less, diff --git a/src/storm/storage/expressions/ToCppVisitor.cpp b/src/storm/storage/expressions/ToCppVisitor.cpp index b68de7132..70b76a467 100644 --- a/src/storm/storage/expressions/ToCppVisitor.cpp +++ b/src/storm/storage/expressions/ToCppVisitor.cpp @@ -142,6 +142,13 @@ namespace storm { expression.getSecondOperand()->accept(*this, data); stream << ")"; break; + case BinaryNumericalFunctionExpression::OperatorType::Modulo: + stream << "("; + expression.getFirstOperand()->accept(*this, data); + stream << " % "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; } return boost::none; } diff --git a/src/storm/storage/expressions/ToExprtkStringVisitor.cpp b/src/storm/storage/expressions/ToExprtkStringVisitor.cpp index d9098af2b..b7e9c39f2 100644 --- a/src/storm/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storm/storage/expressions/ToExprtkStringVisitor.cpp @@ -100,6 +100,13 @@ namespace storm { expression.getSecondOperand()->accept(*this, data); stream << ")"; break; + case BinaryNumericalFunctionExpression::OperatorType::Modulo: + stream << "("; + expression.getFirstOperand()->accept(*this, data); + stream << "%"; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; case BinaryNumericalFunctionExpression::OperatorType::Max: stream << "max("; expression.getFirstOperand()->accept(*this, data); diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 15a8d61eb..89408f9d3 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -48,6 +48,7 @@ namespace storm { RationalNumberType firstOperandAsRationalNumber = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); RationalNumberType secondOperandAsRationalNumber = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); RationalNumberType result; + uint_fast64_t exponentAsInteger; switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: result = firstOperandAsRationalNumber + secondOperandAsRationalNumber; @@ -75,10 +76,12 @@ namespace storm { break; case BinaryNumericalFunctionExpression::OperatorType::Power: STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); - uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); + exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); return result; break; + default: + STORM_LOG_ASSERT(false, "Illegal operator type."); } // Return a dummy. This point must, however, never be reached. diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 5fde8267a..0c0c212a0 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -455,6 +455,8 @@ namespace storm { return "max"; case OpType::Power: return "pow"; + case OpType::Modulo: + return "mod"; case OpType::Equal: return "="; case OpType::NotEqual: