From 8cd3f1bc1a02ee13ecbfdde613886d720a82f497 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 13 Jan 2018 14:19:39 +0100 Subject: [PATCH] added a switch to disable simplifications within PLA --- src/storm-pars/api/region.h | 8 ++++---- src/storm-pars/modelchecker/region/RegionModelChecker.h | 5 +++-- .../region/SparseDtmcParameterLiftingModelChecker.cpp | 7 +++---- .../region/SparseDtmcParameterLiftingModelChecker.h | 7 ++++--- .../region/SparseMdpParameterLiftingModelChecker.cpp | 5 +++-- .../region/SparseMdpParameterLiftingModelChecker.h | 4 ++-- .../ValidatingSparseDtmcParameterLiftingModelChecker.cpp | 2 +- .../ValidatingSparseDtmcParameterLiftingModelChecker.h | 2 +- .../ValidatingSparseMdpParameterLiftingModelChecker.cpp | 2 +- .../ValidatingSparseMdpParameterLiftingModelChecker.h | 2 +- 10 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 27d35d526..56aba0cf3 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -81,7 +81,7 @@ namespace storm { } template - std::shared_ptr> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -105,13 +105,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - checker->specify(env, consideredModel, task); + checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification); return checker; } template - std::shared_ptr> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -135,7 +135,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - checker->specify(env, consideredModel, task); + checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification); return checker; } diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index 72f56bf73..11cf160e4 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -28,7 +28,8 @@ namespace storm { virtual ~RegionModelChecker() = default; virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const = 0; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false) = 0; + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications = true) = 0; + /*! * Analyzes the given region. @@ -45,7 +46,7 @@ namespace storm { * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown. */ std::unique_ptr> analyzeRegions(Environment const& env, std::vector> const& regions, std::vector const& hypotheses, bool sampleVerticesOfRegion = false) ; - + virtual ParametricType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); /*! diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 9c009ccee..8d290ed2c 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -48,14 +48,13 @@ namespace storm { } template - void SparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates) { + void SparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplification) { auto dtmc = parametricModel->template as(); - specify(env, dtmc, checkTask, generateRegionSplitEstimates, false); + specify_internal(env, dtmc, checkTask, generateRegionSplitEstimates, !allowModelSimplification); } template - void SparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) { - + void SparseDtmcParameterLiftingModelChecker::specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) { STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); reset(); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h index 88231e76c..03dc1747a 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h @@ -23,9 +23,10 @@ namespace storm { virtual ~SparseDtmcParameterLiftingModelChecker() = default; virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const override; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false) override; - void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification); - + + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplification = true) override; + void specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification); + boost::optional> getCurrentMinScheduler(); boost::optional> getCurrentMaxScheduler(); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 55a1b65a7..1e28787b2 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -45,13 +45,14 @@ namespace storm { } template - void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates) { + void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates,bool allowModelSimplifications) { auto mdp = parametricModel->template as(); specify(env, mdp, checkTask, generateRegionSplitEstimates, false); } template - void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) { + void SparseMdpParameterLiftingModelChecker::specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) { + STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h index cffab74ed..d29525e2e 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h @@ -25,8 +25,8 @@ namespace storm { virtual ~SparseMdpParameterLiftingModelChecker() = default; virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const override; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false) override; - void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification); + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplification = true) override; + void specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification); boost::optional> getCurrentMinScheduler(); boost::optional> getCurrentMaxScheduler(); diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp index e84f6c9d0..2e9bf221b 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp @@ -15,7 +15,7 @@ namespace storm { } template - void ValidatingSparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates) { + void ValidatingSparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) { STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); auto dtmc = parametricModel->template as(); diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h index 5aed6b5d3..e99792eed 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h @@ -12,7 +12,7 @@ namespace storm { ValidatingSparseDtmcParameterLiftingModelChecker(); virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false) override; + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplifications = true) override; protected: virtual SparseParameterLiftingModelChecker& getImpreciseChecker() override; diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp index a3c01b4bd..444dd334c 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp @@ -16,7 +16,7 @@ namespace storm { template - void ValidatingSparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates) { + void ValidatingSparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) { STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); auto mdp = parametricModel->template as(); diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h index d6ef0ba74..9147e574e 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h @@ -12,7 +12,7 @@ namespace storm { ValidatingSparseMdpParameterLiftingModelChecker(); virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false) override; + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplifications = true) override; protected: virtual SparseParameterLiftingModelChecker& getImpreciseChecker() override;