From 96539f41a500f518ec32d5c64cb416fcbdacd87d Mon Sep 17 00:00:00 2001 From: dehnert 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 firstOperandSimplified = this->getFirstOperand()->simplify(); std::shared_ptr 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(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; + case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } return std::shared_ptr(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(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; + case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } return std::shared_ptr(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(operandEvaluation)); break; case OperatorType::Ceil: value = std::ceil(boost::get(operandEvaluation)); break; } - return std::shared_ptr(new DoubleLiteralExpression(this->getManager(), boost::get(result))); + return std::shared_ptr(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; }