Introduced a utility function that sets information from a CheckTask to a helper.

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());
+            }
+        }
+    }
+}

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"
@@ -225,10 +226,11 @@ 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.");
 			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()) {