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