From 34e23f94fcbc473a4d3b662a8806706192a5af80 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 21 Aug 2017 19:47:02 +0200
Subject: [PATCH] started on reward model preservation in DD bisimulation

---
 src/storm/models/symbolic/Model.cpp           |  6 ++++
 src/storm/models/symbolic/Model.h             |  7 ++++
 .../bisimulation/PreservationInformation.cpp  | 33 ++++++++++++++-----
 .../dd/bisimulation/PreservationInformation.h |  3 ++
 4 files changed, 41 insertions(+), 8 deletions(-)

diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 505241dbc..f468cc377 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -239,6 +239,12 @@ namespace storm {
                 return this->rewardModels.cbegin()->second;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            std::string const& Model<Type, ValueType>::getUniqueRewardModelName() const {
+                STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve name of unique reward model, because there is no unique one.");
+                return this->rewardModels.cbegin()->first;
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             typename Model<Type, ValueType>::RewardModelType& Model<Type, ValueType>::getUniqueRewardModel() {
                 STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve unique reward model, because there is no unique one.");
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index 89e447640..1bebd7fe5 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -277,6 +277,13 @@ namespace storm {
                  */
                 RewardModelType const& getUniqueRewardModel() const;
 
+                /*!
+                 * Retrieves the name of the unique reward model, if there exists exactly one. Otherwise, an exception is thrown.
+                 *
+                 * @return The name of the unique reward model.
+                 */
+                std::string const& getUniqueRewardModelName() const;
+
                 /*!
                  * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown.
                  *
diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp
index 5009fa371..0569df104 100644
--- a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp
+++ b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp
@@ -39,10 +39,10 @@ namespace storm {
                         this->addLabel(label);
                         this->addExpression(model.getExpression(label));
                     }
+                    for (auto const& rewardModel : model.getRewardModels()) {
+                        this->addRewardModel(rewardModel.first);
+                    }
                 } else {
-                    std::set<std::string> labels;
-                    std::set<storm::expressions::Expression> expressions;
-                    
                     for (auto const& formula : formulas) {
                         for (auto const& expressionFormula : formula->getAtomicExpressionFormulas()) {
                             this->addExpression(expressionFormula->getExpression());
@@ -53,11 +53,18 @@ namespace storm {
                             STORM_LOG_THROW(model.hasLabel(label), storm::exceptions::InvalidPropertyException, "Property refers to illegal label '" << label << "'.");
                             this->addExpression(model.getExpression(label));
                         }
-                    }
-                    
-                    std::vector<storm::expressions::Expression> expressionVector;
-                    for (auto const& expression : expressions) {
-                        expressionVector.emplace_back(expression);
+                        for (auto const& rewardModel : formula->getReferencedRewardModels()) {
+                            if (rewardModel == "") {
+                                if (model.hasRewardModel("")) {
+                                    this->addRewardModel(rewardModel);
+                                } else {
+                                    STORM_LOG_THROW(model.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "Property refers to the default reward model, but it does not exist or is not unique.");
+                                    this->addRewardModel(model.getUniqueRewardModelName());
+                                }
+                            } else {
+                                this->addRewardModel(rewardModel);
+                            }
+                        }
                     }
                 }
             }
@@ -72,6 +79,11 @@ namespace storm {
                 expressions.insert(expression);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PreservationInformation<DdType, ValueType>::addRewardModel(std::string const& name) {
+                rewardModelNames.insert(name);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::set<std::string> const& PreservationInformation<DdType, ValueType>::getLabels() const {
                 return labels;
@@ -82,6 +94,11 @@ namespace storm {
                 return expressions;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::set<std::string> const& PreservationInformation<DdType, ValueType>::getRewardModelNames() const {
+                return rewardModelNames;
+            }
+            
             template class PreservationInformation<storm::dd::DdType::CUDD, double>;
             
             template class PreservationInformation<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.h b/src/storm/storage/dd/bisimulation/PreservationInformation.h
index a5bfbc3d1..2286e9bc6 100644
--- a/src/storm/storage/dd/bisimulation/PreservationInformation.h
+++ b/src/storm/storage/dd/bisimulation/PreservationInformation.h
@@ -28,13 +28,16 @@ namespace storm {
                 
                 void addLabel(std::string const& label);
                 void addExpression(storm::expressions::Expression const& expression);
+                void addRewardModel(std::string const& name);
                 
                 std::set<std::string> const& getLabels() const;
                 std::set<storm::expressions::Expression> const& getExpressions() const;
+                std::set<std::string> const& getRewardModelNames() const;
                 
             private:
                 std::set<std::string> labels;
                 std::set<storm::expressions::Expression> expressions;
+                std::set<std::string> rewardModelNames;
             };
             
         }