From c40ecae2e61d13e169d3f9456b18bc1811a5d902 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 15 Mar 2019 09:59:29 +0100 Subject: [PATCH] Implemented quantiles for DTMCs. --- .../prctl/SparseDtmcPrctlModelChecker.cpp | 32 ++++++++++++++++++- .../prctl/SparseDtmcPrctlModelChecker.h | 1 + .../prctl/SparseMdpPrctlModelChecker.cpp | 2 +- .../helper/rewardbounded/QuantileHelper.cpp | 16 ++++++++-- 4 files changed, 47 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index f561d3e98..7c11c31b8 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -7,9 +7,11 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" +#include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" #include "storm/logic/FragmentSpecification.h" @@ -31,7 +33,13 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { + return true; + } else if (formula.isInFragment(storm::logic::quantiles())) { + if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + return true; + } + return false; } template @@ -184,6 +192,28 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + + template<> + std::unique_ptr SparseDtmcPrctlModelChecker>::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Quantiles for parametric models are not implemented."); + } + + template + std::unique_ptr SparseDtmcPrctlModelChecker::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for the initial states of a model."); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, "Quantiles not supported on models with multiple initial states."); + uint64_t initialState = *this->getModel().getInitialStates().begin(); + + helper::rewardbounded::QuantileHelper qHelper(this->getModel(), checkTask.getFormula()); + auto res = qHelper.computeQuantile(env); + + if (res.size() == 1 && res.front().size() == 1) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, std::move(res.front().front()))); + } else { + return std::unique_ptr(new ExplicitParetoCurveCheckResult(initialState, std::move(res))); + } + } + template class SparseDtmcPrctlModelChecker>; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 1aafc0efb..1001b5572 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -34,6 +34,7 @@ namespace storm { virtual std::unique_ptr computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 759d7a976..bd2dfd326 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -228,7 +228,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { - STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for models with a single initial states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for the initial states of a model."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, "Quantiles not supported on models with multiple initial states."); uint64_t initialState = *this->getModel().getInitialStates().begin(); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index ea7d5ad06..45512006c 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -8,6 +8,7 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/Expressions.h" @@ -360,7 +361,12 @@ namespace storm { auto lowerBound = rewardUnfolding.getLowerObjectiveBound(); auto upperBound = rewardUnfolding.getUpperObjectiveBound(); std::vector x, b; - std::unique_ptr> minMaxSolver; + std::unique_ptr> minMaxSolver; // Needed for MDP + std::unique_ptr> linEqSolver; // Needed for DTMC + if (!model.isNondeterministicModel()) { + rewardUnfolding.setEquationSystemFormatForEpochModel(storm::solver::GeneralLinearEquationSolverFactory().getEquationProblemFormat(env)); + } + swExploration.start(); bool progress = true; for (CostLimit candidateCostLimitSum(0); progress; ++candidateCostLimitSum.get()) { @@ -395,7 +401,11 @@ namespace storm { ++numCheckedEpochs; swEpochAnalysis.start(); auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); - rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env,boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound)); + if (model.isNondeterministicModel()) { + rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env, boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound)); + } else { + rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env, x, b, linEqSolver, lowerBound, upperBound)); + } swEpochAnalysis.stop(); CostLimits epochAsCostLimits; @@ -431,6 +441,8 @@ namespace storm { template class QuantileHelper>; template class QuantileHelper>; + template class QuantileHelper>; + template class QuantileHelper>; } }