From 419013025bb44467a741260da7e6726e868ac348 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 5 Dec 2019 12:28:58 +0100
Subject: [PATCH] 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               | 11 +++++++++++
 src/storm/models/symbolic/Ctmc.h                 |  2 ++
 src/storm/models/symbolic/DeterministicModel.cpp |  7 -------
 src/storm/models/symbolic/DeterministicModel.h   |  1 -
 src/storm/models/symbolic/Dtmc.cpp               |  7 +++++++
 src/storm/models/symbolic/Dtmc.h                 |  2 ++
 6 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/storm/models/symbolic/Ctmc.cpp b/src/storm/models/symbolic/Ctmc.cpp
index 4b05372be..d54b3156d 100644
--- a/src/storm/models/symbolic/Ctmc.cpp
+++ b/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 {
diff --git a/src/storm/models/symbolic/Ctmc.h b/src/storm/models/symbolic/Ctmc.h
index 0035e3ffb..c73340946 100644
--- a/src/storm/models/symbolic/Ctmc.h
+++ b/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;
                 
diff --git a/src/storm/models/symbolic/DeterministicModel.cpp b/src/storm/models/symbolic/DeterministicModel.cpp
index 5eba1bbc9..3555dcaff 100644
--- a/src/storm/models/symbolic/DeterministicModel.cpp
+++ b/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>;
diff --git a/src/storm/models/symbolic/DeterministicModel.h b/src/storm/models/symbolic/DeterministicModel.h
index a8fde85b4..4612354b7 100644
--- a/src/storm/models/symbolic/DeterministicModel.h
+++ b/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
diff --git a/src/storm/models/symbolic/Dtmc.cpp b/src/storm/models/symbolic/Dtmc.cpp
index 2b4adb149..a4b422360 100644
--- a/src/storm/models/symbolic/Dtmc.cpp
+++ b/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 {
diff --git a/src/storm/models/symbolic/Dtmc.h b/src/storm/models/symbolic/Dtmc.h
index 76a3e81ca..be98cf34d 100644
--- a/src/storm/models/symbolic/Dtmc.h
+++ b/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;