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 + void setInformationFromCheckTaskNondeterministic(HelperType& helper, storm::modelchecker::CheckTask 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 std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask 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 subResultPointer = this->check(env, stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper 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 result(new ExplicitQuantitativeCheckResult(std::move(values))); if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(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 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 result(new ExplicitQuantitativeCheckResult(std::move(values))); if (checkTask.isProduceSchedulersSet()) {