added mod as binary operation in expressions and slightly extended JANI support for filters

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

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

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<storm::expressions::OperatorType> 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;

src/storm/parser/ExpressionParser.cpp

@@ -36,7 +36,7 @@ namespace boost {
 
 namespace storm {
     namespace parser {
-        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> 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<char, uint_fast64_t> 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");
             

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<char, storm::expressions::OperatorType> {
-                infixPowerOperatorStruct() {
+            struct infixPowerModuloOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+                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<char, storm::expressions::OperatorType> {
                 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<char, storm::expressions::OperatorType> {
-                prefixPowerOperatorStruct() {
+            struct prefixPowerModuloOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
+                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<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
             qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
             qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> prefixPowerExpression;
-            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> infixPowerExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> prefixPowerModuloExpression;
+            qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> infixPowerModuloExpression;
             qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
             qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
             qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;

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<storm::logic::BinaryBooleanStateFormula const>(oper, args[0], args[1]);
+                } else if (opString == "⇒") {
+                    assert(bound == boost::none);
+                    std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, globalVars, constants, "");
+                    assert(args.size() == 2);
+                    std::shared_ptr<storm::logic::UnaryBooleanStateFormula const> tmp = std::make_shared<storm::logic::UnaryBooleanStateFormula const>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]);
+                    return std::make_shared<storm::logic::BinaryBooleanStateFormula const>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, tmp, args[1]);
                 } else if (opString == "¬") {
                     assert(bound == boost::none);
                     std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::logic::Formula const> 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<storm::logic::AtomicLabelFormula>("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<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> 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();

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<BaseExpression const> const& firstOperand, std::shared_ptr<BaseExpression const> 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<int_fast64_t>(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<int_fast64_t> 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<int_fast64_t>(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<BaseExpression>(new IntegerLiteralExpression(this->getManager(), newValue.get()));
                     }
-                    return std::shared_ptr<BaseExpression>(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<storm::RationalNumber> 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<carl::uint>(secondOperandEvaluation);
-                            newValue = carl::pow(firstOperandEvaluation, exponent);
+                            if (carl::isInteger(secondOperandEvaluation)) {
+                                std::size_t exponent = carl::toInt<carl::uint>(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<BaseExpression>(new RationalLiteralExpression(this->getManager(), newValue.get()));
                     }
-                    return std::shared_ptr<BaseExpression>(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 << ")";
         }

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.

src/storm/storage/expressions/Expression.cpp

@@ -277,6 +277,11 @@ namespace storm {
             return Expression(std::shared_ptr<BaseExpression>(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<BaseExpression>(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;

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

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

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;

src/storm/storage/expressions/OperatorType.h

@@ -19,6 +19,7 @@ namespace storm {
             Min,
             Max,
             Power,
+            Modulo,
             Equal,
             NotEqual,
             Less,

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

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

src/storm/storage/expressions/ToRationalNumberVisitor.cpp

@@ -48,6 +48,7 @@ namespace storm {
             RationalNumberType firstOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getFirstOperand()->accept(*this, data));
             RationalNumberType secondOperandAsRationalNumber = boost::any_cast<RationalNumberType>(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<carl::uint>(secondOperandAsRationalNumber);
+                    exponentAsInteger = storm::utility::convertNumber<carl::uint>(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.

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: