From 959e035153f1543c44cfa174fb4cc206fbbbcedf Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 11 Aug 2020 16:56:01 +0200 Subject: [PATCH] Use the new infinite horizon helper for sparse ctmc and dtmc. --- .../csl/SparseCtmcCslModelChecker.cpp | 17 +++++++++++---- .../utility/SetInformationFromCheckTask.h | 15 +++++++++++++ .../prctl/SparseDtmcPrctlModelChecker.cpp | 21 +++++++++++++------ 3 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 10f1600bc..11530673b 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -2,6 +2,8 @@ #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -127,15 +129,22 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), &this->getModel().getExitRateVector()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(probabilisticTransitions, this->getModel().getExitRateVector()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } template std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), &this->getModel().getExitRateVector()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(probabilisticTransitions, this->getModel().getExitRateVector()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } template diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h index e1348cd03..49b46db26 100644 --- a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h +++ b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h @@ -26,6 +26,21 @@ namespace storm { // Scheduler Production helper.setProduceScheduler(checkTask.isProduceSchedulersSet()); } + + /*! + * Forwards relevant information stored in the given CheckTask to the given helper + */ + template + void setInformationFromCheckTaskDeterministic(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()); + } + } } } } \ No newline at end of file diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 541c51502..ad0f95ef6 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -13,6 +13,8 @@ #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" @@ -166,18 +168,25 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(env, stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + std::unique_ptr subResultPointer = this->check(env, stateFormula); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), nullptr); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } template