From 38af6357d74de9c37ba6d8ecb3404b3484ec97a6 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 12 Aug 2020 10:43:49 +0200 Subject: [PATCH] Using the new hybrid infinite horizon helper in the model checkers --- .../modelchecker/csl/HybridCtmcCslModelChecker.cpp | 12 ++++++++++-- .../csl/HybridMarkovAutomatonCslModelChecker.cpp | 6 +++--- .../prctl/HybridDtmcPrctlModelChecker.cpp | 12 +++++++++--- 3 files changed, 22 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index c4102efab..78ec476a4 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -4,6 +4,8 @@ #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "storm/modelchecker/csl/helper/HybridCtmcCslHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -123,13 +125,19 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(env, this->getModel(), checkTask.isOnlyInitialStatesRelevantSet(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + storm::modelchecker::helper::HybridInfiniteHorizonHelper helper(this->getModel(), probabilisticTransitions, this->getModel().getExitRateVector()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + return helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); } template std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageRewards(env, this->getModel(), checkTask.isOnlyInitialStatesRelevantSet(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModel.get()); + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + storm::modelchecker::helper::HybridInfiniteHorizonHelper helper(this->getModel(), probabilisticTransitions, this->getModel().getExitRateVector()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + return helper.computeLongRunAverageRewards(env, rewardModel.get()); } // Explicitly instantiate the model checker. diff --git a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp index b2833ee78..c8dff0c8f 100644 --- a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp @@ -5,7 +5,7 @@ #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" #include "storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h" #include "storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h" -#include "storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -107,7 +107,7 @@ namespace storm { SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - storm::modelchecker::helper::HybridNondeterministicInfiniteHorizonHelper helper(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector()); + storm::modelchecker::helper::HybridInfiniteHorizonHelper helper(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); return helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); } @@ -116,7 +116,7 @@ namespace storm { std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { 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::HybridNondeterministicInfiniteHorizonHelper helper(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector()); + storm::modelchecker::helper::HybridInfiniteHorizonHelper helper(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); return helper.computeLongRunAverageRewards(env, rewardModel.get()); } diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 266363662..c861d0ea9 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -2,6 +2,8 @@ #include "storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/storage/dd/Odd.h" #include "storm/storage/dd/DdManager.h" @@ -113,20 +115,24 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityTimes(env, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } - template std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeLongRunAverageProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + storm::modelchecker::helper::HybridInfiniteHorizonHelper helper(this->getModel(), this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + return helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get()); + + storm::modelchecker::helper::HybridInfiniteHorizonHelper helper(this->getModel(), this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + return helper.computeLongRunAverageRewards(env, rewardModel.get()); } template class HybridDtmcPrctlModelChecker>;