From a9a1c4feed77238a88c133dbe70f18da1997957c Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 11 Oct 2017 18:50:53 +0200 Subject: [PATCH] Region model checker can now also return a (quantitative) upper/lower bound for a given region --- .../modelchecker/region/RegionModelChecker.cpp | 7 +++++++ .../modelchecker/region/RegionModelChecker.h | 2 ++ .../region/SparseParameterLiftingModelChecker.cpp | 13 +++++++++++++ .../region/SparseParameterLiftingModelChecker.h | 3 +++ 4 files changed, 25 insertions(+) diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index 23ba29489..ab0142d0b 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -17,6 +17,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/exceptions/NotImplementedException.h" namespace storm { @@ -43,6 +44,12 @@ namespace storm { return std::make_unique>(std::move(result)); } + template + ParametricType RegionModelChecker::getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The selected region model checker does not support this functionality."); + return storm::utility::zero(); + } + template std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold, RegionResultHypothesis const& hypothesis) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index c1a558800..595d1e8f0 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -42,6 +42,8 @@ namespace storm { */ std::unique_ptr> analyzeRegions(std::vector> const& regions, std::vector const& hypotheses, bool sampleVerticesOfRegion = false) ; + virtual ParametricType getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + /*! * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated). * @param region the considered region diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index d0b2af22b..1accd68cc 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -4,6 +4,7 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/utility/vector.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -130,6 +131,18 @@ namespace storm { } } + template + std::unique_ptr> SparseParameterLiftingModelChecker::getBound(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(), "Computing quantitative bounds for a qualitative formula..."); + return std::make_unique>(std::move(computeQuantitativeValues(region, dirForParameters)->template asExplicitQuantitativeCheckResult())); + } + + template + typename SparseModelType::ValueType SparseParameterLiftingModelChecker::getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting a bound at the initial state requires a model with a single initial state."); + return storm::utility::convertNumber(getBound(region, dirForParameters)->template asExplicitQuantitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]); + } + template SparseModelType const& SparseParameterLiftingModelChecker::getConsideredParametricModel() const { return *parametricModel; diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h index e0cabd5f0..cb993ad4f 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h @@ -45,6 +45,9 @@ namespace storm { */ std::unique_ptr check(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + std::unique_ptr> getBound(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + virtual typename SparseModelType::ValueType getBoundAtInitState(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; + SparseModelType const& getConsideredParametricModel() const; CheckTask const& getCurrentCheckTask() const;