From b5bd7aa0c277599f61c2953f2d3ce36656115b90 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 3 Aug 2020 14:57:12 +0200
Subject: [PATCH] Introduced a utility function that sets information from a
 CheckTask to a helper.

---
 .../utility/SetInformationFromCheckTask.h     | 31 +++++++++++++++++++
 .../prctl/SparseMdpPrctlModelChecker.cpp      | 11 ++++---
 2 files changed, 37 insertions(+), 5 deletions(-)
 create mode 100644 src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h

diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h
new file mode 100644
index 000000000..e1348cd03
--- /dev/null
+++ b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h
@@ -0,0 +1,31 @@
+#pragma once
+
+#include "storm/modelchecker/CheckTask.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            
+            /*!
+             * Forwards relevant information stored in the given CheckTask to the given helper
+             */
+            template <typename HelperType, typename FormulaType, typename ModelType>
+            void setInformationFromCheckTaskNondeterministic(HelperType& helper, storm::modelchecker::CheckTask<FormulaType, typename ModelType::ValueType> const& checkTask, ModelType const& model) {
+                // Relevancy of initial states.
+			    if (checkTask.isOnlyInitialStatesRelevantSet()) {
+			        helper.setRelevantStates(model.getInitialStates());
+			    }
+                // Value threshold to which the result will be compared
+			    if (checkTask.isBoundSet()) {
+			        helper.setValueThreshold(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
+			    }
+			    // Optimization direction
+                if (checkTask.isOptimizationDirectionSet()) {
+                    helper.setOptimizationDirection(checkTask.getOptimizationDirection());
+                }
+                // Scheduler Production
+			    helper.setProduceScheduler(checkTask.isProduceSchedulersSet());
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 46a2357c1..bc0321317 100644
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -16,6 +16,7 @@
 
 #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
 #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h"
+#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h"
 
 #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h"
 #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
@@ -221,14 +222,15 @@ namespace storm {
 
 		template<typename SparseMdpModelType>
 		std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
-            storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
+		    storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
 			STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
 			std::unique_ptr<CheckResult> subResultPointer = this->check(env, stateFormula);
 			ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+			
 			storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions());
-			helper.setOptimizationDirection(checkTask.getOptimizationDirection());
-			helper.setProduceScheduler(checkTask.isProduceSchedulersSet());
+            storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
 			auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector());
+			
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
             if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
@@ -241,8 +243,7 @@ namespace storm {
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
             storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions());
-			helper.setOptimizationDirection(checkTask.getOptimizationDirection());
-			helper.setProduceScheduler(checkTask.isProduceSchedulersSet());
+            storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
 			auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
             if (checkTask.isProduceSchedulersSet()) {