From 4322d00034f9579eef946aaed7982adad24cbc3b Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 29 Apr 2019 07:24:09 +0200
Subject: [PATCH] FilteredRewardModel: added create method that works without a
 checkout.

---
 src/storm/utility/FilteredRewardModel.h | 26 ++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/storm/utility/FilteredRewardModel.h b/src/storm/utility/FilteredRewardModel.h
index 32dc13521..5280cfd98 100644
--- a/src/storm/utility/FilteredRewardModel.h
+++ b/src/storm/utility/FilteredRewardModel.h
@@ -8,9 +8,8 @@
 namespace storm {
     namespace utility {
         
-        
         /*
-         * This class wraps around a
+         * This class wraps around a Reward model where certain reward types are disabled.
          */
         template <typename RewardModelType>
         class FilteredRewardModel {
@@ -45,20 +44,25 @@ namespace storm {
                 RewardModelType const* rewardModel;
         };
         
-        template <typename ModelType, typename CheckTaskType>
-        FilteredRewardModel<typename ModelType::RewardModelType> createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) {
-            auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel();
-            if (checkTask.getFormula().hasRewardAccumulation()) {
-                auto const& acc = checkTask.getFormula().getRewardAccumulation();
-                STORM_LOG_THROW(model.isDiscreteTimeModel() || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported.");
+        template <typename RewardModelType, typename FormulaType>
+        FilteredRewardModel<RewardModelType> createFilteredRewardModel(RewardModelType const& baseRewardModel, bool isDiscreteTimeModel, FormulaType const& formula) {
+            if (formula.hasRewardAccumulation()) {
+                auto const& acc = formula.getRewardAccumulation();
+                STORM_LOG_THROW(isDiscreteTimeModel || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported.");
                 // Check which of the available reward types are allowed.
-                bool hasStateRewards = model.isDiscreteTimeModel() ? acc.isExitSet() : acc.isTimeSet();
+                bool hasStateRewards = isDiscreteTimeModel ? acc.isExitSet() : acc.isTimeSet();
                 bool hasStateActionRewards = acc.isStepsSet();
                 bool hasTransitionRewards = acc.isStepsSet();
-                return FilteredRewardModel<typename ModelType::RewardModelType>(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards);
+                return FilteredRewardModel<RewardModelType>(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards);
             } else {
-                return FilteredRewardModel<typename ModelType::RewardModelType>(baseRewardModel, true, true, true);
+                return FilteredRewardModel<RewardModelType>(baseRewardModel, true, true, true);
             }
         }
+        
+        template <typename ModelType, typename CheckTaskType>
+        FilteredRewardModel<typename ModelType::RewardModelType> createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) {
+            auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel();
+            return createFilteredRewardModel(baseRewardModel, model.isDiscreteTimeModel(), checkTask.getFormula());
+        }
     }
 }
\ No newline at end of file