Fixed reduction to state-based rewards for CTMCs in Dd engine. When action rewards are reduced to state rewards, they have to be multiplied with the exit rate.

src/storm/models/symbolic/Ctmc.cpp

@@ -84,6 +84,17 @@ namespace storm {
                 return exitRates.get();
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            void Ctmc<Type, ValueType>::reduceToStateBasedRewards() {
+                for (auto& rewardModel : this->getRewardModels()) {
+                    if (rewardModel.second.hasStateActionRewards()) {
+                        rewardModel.second.getStateActionRewardVector() *= getExitRateVector();
+                    }
+                    rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), true);
+                }
+            }
+            
+            
             template<storm::dd::DdType Type, typename ValueType>
             template<typename NewValueType>
             std::shared_ptr<Ctmc<Type, NewValueType>> Ctmc<Type, ValueType>::toValueType() const {

src/storm/models/symbolic/Ctmc.h

@@ -141,6 +141,8 @@ namespace storm {
                  */
                 storm::dd::Add<Type, ValueType> const& getExitRateVector() const;
                 
+                virtual void reduceToStateBasedRewards() override;
+
                 template<typename NewValueType>
                 std::shared_ptr<Ctmc<Type, NewValueType>> toValueType() const;
                 

src/storm/models/symbolic/DeterministicModel.cpp

@@ -45,13 +45,6 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            template<storm::dd::DdType Type, typename ValueType>
-            void DeterministicModel<Type, ValueType>::reduceToStateBasedRewards() {
-                for (auto& rewardModel : this->getRewardModels()) {
-                    rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), true);
-                }
-            }
-            
             // Explicitly instantiate the template class.
             template class DeterministicModel<storm::dd::DdType::CUDD>;
             template class DeterministicModel<storm::dd::DdType::Sylvan>;

src/storm/models/symbolic/DeterministicModel.h

@@ -81,7 +81,6 @@ namespace storm {
                                    std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
                                    std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
                 
-                virtual void reduceToStateBasedRewards() override;
             };
             
         } // namespace symbolic

src/storm/models/symbolic/Dtmc.cpp

@@ -43,6 +43,13 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            void Dtmc<Type, ValueType>::reduceToStateBasedRewards() {
+                for (auto& rewardModel : this->getRewardModels()) {
+                    rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), true);
+                }
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             template<typename NewValueType>
             std::shared_ptr<Dtmc<Type, NewValueType>> Dtmc<Type, ValueType>::toValueType() const {

src/storm/models/symbolic/Dtmc.h

@@ -77,6 +77,8 @@ namespace storm {
                      std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
                      std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
                 
+                virtual void reduceToStateBasedRewards() override;
+
                 template<typename NewValueType>
                 std::shared_ptr<Dtmc<Type, NewValueType>> toValueType() const;