From 1dd8cc2d3f68cdac72f334f30295e1287dfd7658 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 27 Jun 2017 12:40:12 +0200 Subject: [PATCH] Added Validating Parameter Lifting region model checker --- ...SparseDtmcParameterLiftingModelChecker.cpp | 67 +++++++++++++++++ ...ngSparseDtmcParameterLiftingModelChecker.h | 31 ++++++++ ...gSparseMdpParameterLiftingModelChecker.cpp | 71 ++++++++++++++++++ ...ingSparseMdpParameterLiftingModelChecker.h | 31 ++++++++ ...tingSparseParameterLiftingModelChecker.cpp | 73 +++++++++++++++++++ ...datingSparseParameterLiftingModelChecker.h | 44 +++++++++++ 6 files changed, 317 insertions(+) create mode 100644 src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp create mode 100644 src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h create mode 100644 src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp create mode 100644 src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h create mode 100644 src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp create mode 100644 src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp new file mode 100644 index 000000000..2ab8c3103 --- /dev/null +++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp @@ -0,0 +1,67 @@ +#include "storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm/models/sparse/Dtmc.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + + template + ValidatingSparseDtmcParameterLiftingModelChecker::ValidatingSparseDtmcParameterLiftingModelChecker() { + // Intentionally left empty + } + + template + void ValidatingSparseDtmcParameterLiftingModelChecker::specify(std::shared_ptr parametricModel, CheckTask const& checkTask) { + STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); + + auto dtmc = parametricModel->template as(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier(*dtmc); + + if (!simplifier.simplify(checkTask.getFormula())) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + } + + auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); + + impreciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true); + preciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true); + } + + template + SparseParameterLiftingModelChecker& ValidatingSparseDtmcParameterLiftingModelChecker::getImpreciseChecker() { + return impreciseChecker; + } + + template + SparseParameterLiftingModelChecker const& ValidatingSparseDtmcParameterLiftingModelChecker::getImpreciseChecker() const { + return impreciseChecker; + } + + template + SparseParameterLiftingModelChecker& ValidatingSparseDtmcParameterLiftingModelChecker::getPreciseChecker() { + return preciseChecker; + } + + template + SparseParameterLiftingModelChecker const& ValidatingSparseDtmcParameterLiftingModelChecker::getPreciseChecker() const { + return preciseChecker; + } + + template + void ValidatingSparseDtmcParameterLiftingModelChecker::applyHintsToPreciseChecker() { + + if (impreciseChecker.getCurrentMaxScheduler()) { + preciseChecker.getCurrentMaxScheduler() = impreciseChecker.getCurrentMaxScheduler()->template toValueType(); + } + if (impreciseChecker.getCurrentMinScheduler()) { + preciseChecker.getCurrentMinScheduler() = impreciseChecker.getCurrentMinScheduler()->template toValueType(); + } + } + + template class ValidatingSparseDtmcParameterLiftingModelChecker, double, storm::RationalNumber>; + } +} diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h new file mode 100644 index 000000000..9fd696be2 --- /dev/null +++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h @@ -0,0 +1,31 @@ +#pragma once + +#include "storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h" + +namespace storm { + namespace modelchecker { + + template + class ValidatingSparseDtmcParameterLiftingModelChecker : public ValidatingSparseParameterLiftingModelChecker { + public: + ValidatingSparseDtmcParameterLiftingModelChecker(); + virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default; + + virtual void specify(std::shared_ptr parametricModel, CheckTask const& checkTask) override; + + protected: + virtual SparseParameterLiftingModelChecker& getImpreciseChecker() override; + virtual SparseParameterLiftingModelChecker const& getImpreciseChecker() const override; + virtual SparseParameterLiftingModelChecker& getPreciseChecker() override; + virtual SparseParameterLiftingModelChecker const& getPreciseChecker() const override; + + virtual void applyHintsToPreciseChecker() override ; + + private: + SparseDtmcParameterLiftingModelChecker impreciseChecker; + SparseDtmcParameterLiftingModelChecker preciseChecker; + + }; + } +} diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp new file mode 100644 index 000000000..014cf6267 --- /dev/null +++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp @@ -0,0 +1,71 @@ +#include "storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h" +#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" + +#include "storm/models/sparse/Mdp.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + + template + ValidatingSparseMdpParameterLiftingModelChecker::ValidatingSparseMdpParameterLiftingModelChecker() { + // Intentionally left empty + } + + + template + void ValidatingSparseMdpParameterLiftingModelChecker::specify(std::shared_ptr parametricModel, CheckTask const& checkTask) { + STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); + + auto mdp = parametricModel->template as(); + auto simplifier = storm::transformer::SparseParametricMdpSimplifier(*mdp); + + if (!simplifier.simplify(checkTask.getFormula())) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + } + + auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); + + impreciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true); + preciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true); + } + + template + SparseParameterLiftingModelChecker& ValidatingSparseMdpParameterLiftingModelChecker::getImpreciseChecker() { + return impreciseChecker; + } + + template + SparseParameterLiftingModelChecker const& ValidatingSparseMdpParameterLiftingModelChecker::getImpreciseChecker() const { + return impreciseChecker; + } + + template + SparseParameterLiftingModelChecker& ValidatingSparseMdpParameterLiftingModelChecker::getPreciseChecker() { + return preciseChecker; + } + + template + SparseParameterLiftingModelChecker const& ValidatingSparseMdpParameterLiftingModelChecker::getPreciseChecker() const { + return preciseChecker; + } + + template + void ValidatingSparseMdpParameterLiftingModelChecker::applyHintsToPreciseChecker() { + + if (impreciseChecker.getCurrentMaxScheduler()) { + preciseChecker.getCurrentMaxScheduler() = impreciseChecker.getCurrentMaxScheduler()->template toValueType(); + } + if (impreciseChecker.getCurrentMinScheduler()) { + preciseChecker.getCurrentMinScheduler() = impreciseChecker.getCurrentMinScheduler()->template toValueType(); + } + if (impreciseChecker.getCurrentPlayer1Scheduler()) { + preciseChecker.getCurrentPlayer1Scheduler() = impreciseChecker.getCurrentPlayer1Scheduler()->template toValueType(); + } + } + + template class ValidatingSparseMdpParameterLiftingModelChecker, double, storm::RationalNumber>; + } +} diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h new file mode 100644 index 000000000..1f56818c6 --- /dev/null +++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h @@ -0,0 +1,31 @@ +#pragma once + +#include "storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h" + +namespace storm { + namespace modelchecker { + + template + class ValidatingSparseMdpParameterLiftingModelChecker : public ValidatingSparseParameterLiftingModelChecker { + public: + ValidatingSparseMdpParameterLiftingModelChecker(); + virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default; + + virtual void specify(std::shared_ptr parametricModel, CheckTask const& checkTask) override; + + protected: + virtual SparseParameterLiftingModelChecker& getImpreciseChecker() override; + virtual SparseParameterLiftingModelChecker const& getImpreciseChecker() const override; + virtual SparseParameterLiftingModelChecker& getPreciseChecker() override; + virtual SparseParameterLiftingModelChecker const& getPreciseChecker() const override; + + virtual void applyHintsToPreciseChecker() override ; + + private: + SparseMdpParameterLiftingModelChecker impreciseChecker; + SparseMdpParameterLiftingModelChecker preciseChecker; + + }; + } +} diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp new file mode 100644 index 000000000..447bcd27e --- /dev/null +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp @@ -0,0 +1,73 @@ +#include "storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h" + +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" + +namespace storm { + namespace modelchecker { + + template + ValidatingSparseParameterLiftingModelChecker::ValidatingSparseParameterLiftingModelChecker() : numOfWrongRegions(0) { + // Intentionally left empty + } + + template + ValidatingSparseParameterLiftingModelChecker::~ValidatingSparseParameterLiftingModelChecker() { + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Validating Parameter Lifting Model Checker detected " << numOfWrongRegions << " regions where the imprecise method was wrong."); + } + } + + template + bool ValidatingSparseParameterLiftingModelChecker::canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const { + return getImpreciseChecker().canHandle(parametricModel, checkTask) && getPreciseChecker().canHandle(parametricModel, checkTask); + }; + + template + RegionResult ValidatingSparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + + RegionResult currentResult = getImpreciseChecker().analyzeRegion(region, initialResult); + + if (currentResult == RegionResult::AllSat || currentResult == RegionResult::AllViolated) { + applyHintsToPreciseChecker(); + + storm::solver::OptimizationDirection parameterOptDir = getPreciseChecker().getCurrentCheckTask().getOptimizationDirection(); + if (currentResult == RegionResult::AllViolated) { + parameterOptDir = storm::solver::invert(parameterOptDir); + } + + bool preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()]; + bool preciseResultAgrees = preciseResult == (currentResult == RegionResult::AllSat); + + if (!preciseResultAgrees) { + // Imprecise result is wrong! + currentResult = RegionResult::Unknown; + ++numOfWrongRegions; + + // Check the other direction + parameterOptDir = storm::solver::invert(parameterOptDir); + preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()]; + if (preciseResult && parameterOptDir == getPreciseChecker().getCurrentCheckTask().getOptimizationDirection()) { + currentResult = RegionResult::AllSat; + } else if (!preciseResult && parameterOptDir == storm::solver::invert(getPreciseChecker().getCurrentCheckTask().getOptimizationDirection())) { + currentResult = RegionResult::AllViolated; + } + } + } + + if (sampleVerticesOfRegion && currentResult != RegionResult::AllSat && currentResult != RegionResult::AllViolated) { + currentResult = getPreciseChecker().sampleVertices(region, currentResult); + } + + return currentResult; + } + + template class ValidatingSparseParameterLiftingModelChecker, double, storm::RationalNumber>; + template class ValidatingSparseParameterLiftingModelChecker, double, storm::RationalNumber>; + + } +} diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h new file mode 100644 index 000000000..7f9789ebf --- /dev/null +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h @@ -0,0 +1,44 @@ +#pragma once + +#include "storm-pars/modelchecker/region/RegionModelChecker.h" +#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h" +#include "storm-pars/storage/ParameterRegion.h" +#include "storm/utility/NumberTraits.h" + +namespace storm { + namespace modelchecker { + + template + class ValidatingSparseParameterLiftingModelChecker : public RegionModelChecker { + static_assert(storm::NumberTraits::IsExact, "Specified type for exact computations is not exact."); + + public: + ValidatingSparseParameterLiftingModelChecker(); + virtual ~ValidatingSparseParameterLiftingModelChecker(); + + virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const override; + + /*! + * Analyzes the given region by means of parameter lifting. + * We first apply unsound solution methods (standard value iteratio with doubles) and then validate the obtained result + * by means of exact and soud methods. + */ + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; + + protected: + + virtual SparseParameterLiftingModelChecker& getImpreciseChecker() = 0; + virtual SparseParameterLiftingModelChecker const& getImpreciseChecker() const = 0; + virtual SparseParameterLiftingModelChecker& getPreciseChecker() = 0; + virtual SparseParameterLiftingModelChecker const& getPreciseChecker() const = 0; + + virtual void applyHintsToPreciseChecker() = 0; + + private: + + // Information for statistics + uint_fast64_t numOfWrongRegions; + + }; + } +}