Fixed a bug that sometimes prevented transition rewards from being built.

Former-commit-id: afd56375ab

src/builder/ExplicitPrismModelBuilder.cpp

@@ -220,7 +220,7 @@ namespace storm {
                 int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
                 STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
-                STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) == assignedValue, "Writing to the bit vector bucket failed.");
+                STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed.");
             }
             
             // Check that we processed all assignments.

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -642,7 +642,7 @@ namespace storm {
                     measureDrivenInitialPartition = true;
                 }
             } else if (newFormula->isReachabilityRewardFormula()) {
-                rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
+                rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer();
                 if (rightSubformula->isPropositionalFormula()) {
                     measureDrivenInitialPartition = true;
                 }

src/storage/prism/TransitionReward.cpp

@@ -2,7 +2,7 @@
 
 namespace storm {
     namespace prism {
-        TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
+        TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
             // Nothing to do here.
         }