From 96539f41a500f518ec32d5c64cb416fcbdacd87d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 17 Mar 2015 12:40:59 +0100
Subject: [PATCH] Fixed simplification of division: division expressions must
not be simplified, because it is not (yet) clear whether integer division or
floating point division is to be used.
Former-commit-id: 506798c1cdc40d8311525661cd090888f724558b
---
src/builder/ExplicitPrismModelBuilder.cpp | 13 +++++++++++--
.../BinaryNumericalFunctionExpression.cpp | 7 ++++---
.../UnaryNumericalFunctionExpression.cpp | 2 +-
src/storage/prism/BooleanVariable.cpp | 2 +-
4 files changed, 17 insertions(+), 7 deletions(-)
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 5ac83af33..082cdb457 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -127,6 +127,7 @@ namespace storm {
// all expressions in the program so we can then evaluate them without having to store the values of the
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
+
storm::prism::RewardModel rewardModel = storm::prism::RewardModel();
// Select the appropriate reward model.
@@ -564,7 +565,11 @@ namespace storm {
}
for (auto const& stateProbabilityPair : choice) {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
+ if (discreteTimeModel) {
+ globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
+ } else {
+ globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
+ }
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
@@ -580,7 +585,11 @@ namespace storm {
}
for (auto const& stateProbabilityPair : choice) {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
+ if (discreteTimeModel) {
+ globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
+ } else {
+ globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
+ }
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
index be0f30dc0..4e95ea551 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -6,6 +6,7 @@
#include "src/storage/expressions/DoubleLiteralExpression.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/InvalidStateException.h"
namespace storm {
namespace expressions {
@@ -65,7 +66,7 @@ namespace storm {
std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
- if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
+ if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral() && this->getOperatorType() != OperatorType::Divide) {
if (this->hasIntegerType()) {
int_fast64_t firstOperandEvaluation = firstOperandSimplified->evaluateAsInt();
int_fast64_t secondOperandEvaluation = secondOperandSimplified->evaluateAsInt();
@@ -74,10 +75,10 @@ namespace storm {
case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
- case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break;
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;
}
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), newValue));
} else if (this->hasRationalType()) {
@@ -88,10 +89,10 @@ namespace storm {
case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
- case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break;
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;
}
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), newValue));
}
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 6e2a13ae0..edfb22702 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -76,7 +76,7 @@ namespace storm {
case OperatorType::Floor: value = std::floor(boost::get<double>(operandEvaluation)); break;
case OperatorType::Ceil: value = std::ceil(boost::get<double>(operandEvaluation)); break;
}
- return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), boost::get<double>(result)));
+ return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), value));
}
}
diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp
index 35df52356..c38812ec6 100644
--- a/src/storage/prism/BooleanVariable.cpp
+++ b/src/storage/prism/BooleanVariable.cpp
@@ -11,7 +11,7 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
- stream << variable.getName() << ": bool init" << variable.getInitialValueExpression() << ";";
+ stream << variable.getName() << ": bool init " << variable.getInitialValueExpression() << ";";
return stream;
}