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: 506798c1cd

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

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

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

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