Added Validating Parameter Lifting region model checker

8 years ago · 1dd8cc2d3f
6 changed files with 317 additions and 0 deletions
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
+++ 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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::ValidatingSparseDtmcParameterLiftingModelChecker() {
+            // Intentionally left empty
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+            STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
+        
+            auto dtmc = parametricModel->template as<SparseModelType>();
+            auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getImpreciseChecker() {
+            return impreciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType> const& ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getImpreciseChecker() const {
+            return impreciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, PreciseType>& ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getPreciseChecker() {
+            return preciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, PreciseType> const& ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getPreciseChecker() const {
+            return preciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::applyHintsToPreciseChecker() {
+        
+            if (impreciseChecker.getCurrentMaxScheduler()) {
+                preciseChecker.getCurrentMaxScheduler() = impreciseChecker.getCurrentMaxScheduler()->template toValueType<PreciseType>();
+            }
+            if (impreciseChecker.getCurrentMinScheduler()) {
+                preciseChecker.getCurrentMinScheduler() = impreciseChecker.getCurrentMinScheduler()->template toValueType<PreciseType>();
+            }
+        }
+        
+        template class ValidatingSparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber>;
+    }
+}
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
+++ 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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        class ValidatingSparseDtmcParameterLiftingModelChecker : public ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType> {
+        public:
+            ValidatingSparseDtmcParameterLiftingModelChecker();
+            virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default;
+            
+            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+
+        protected:
+            virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType> const& getImpreciseChecker() const override;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, PreciseType>& getPreciseChecker() override;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, PreciseType> const& getPreciseChecker() const override;
+            
+            virtual void applyHintsToPreciseChecker() override ;
+
+        private:
+            SparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType> impreciseChecker;
+            SparseDtmcParameterLiftingModelChecker<SparseModelType, PreciseType> preciseChecker;
+            
+        };
+    }
+}
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
+++ 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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::ValidatingSparseMdpParameterLiftingModelChecker() {
+            // Intentionally left empty
+        }
+        
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+            STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
+        
+            auto mdp = parametricModel->template as<SparseModelType>();
+            auto simplifier = storm::transformer::SparseParametricMdpSimplifier<SparseModelType>(*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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getImpreciseChecker() {
+            return impreciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType> const& ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getImpreciseChecker() const {
+            return impreciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, PreciseType>& ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getPreciseChecker() {
+            return preciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        SparseParameterLiftingModelChecker<SparseModelType, PreciseType> const& ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::getPreciseChecker() const {
+            return preciseChecker;
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::applyHintsToPreciseChecker() {
+        
+            if (impreciseChecker.getCurrentMaxScheduler()) {
+                preciseChecker.getCurrentMaxScheduler() = impreciseChecker.getCurrentMaxScheduler()->template toValueType<PreciseType>();
+            }
+            if (impreciseChecker.getCurrentMinScheduler()) {
+                preciseChecker.getCurrentMinScheduler() = impreciseChecker.getCurrentMinScheduler()->template toValueType<PreciseType>();
+            }
+            if (impreciseChecker.getCurrentPlayer1Scheduler()) {
+                preciseChecker.getCurrentPlayer1Scheduler() = impreciseChecker.getCurrentPlayer1Scheduler()->template toValueType<PreciseType>();
+            }
+        }
+            
+        template class ValidatingSparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber>;
+    }
+}
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
+++ 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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        class ValidatingSparseMdpParameterLiftingModelChecker : public ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType> {
+        public:
+            ValidatingSparseMdpParameterLiftingModelChecker();
+            virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default;
+            
+            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+
+        protected:
+            virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType> const& getImpreciseChecker() const override;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, PreciseType>& getPreciseChecker() override;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, PreciseType> const& getPreciseChecker() const override;
+            
+            virtual void applyHintsToPreciseChecker() override ;
+
+        private:
+            SparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType> impreciseChecker;
+            SparseMdpParameterLiftingModelChecker<SparseModelType, PreciseType> preciseChecker;
+            
+        };
+    }
+}
--- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
+++ 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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::ValidatingSparseParameterLiftingModelChecker() : numOfWrongRegions(0) {
+            // Intentionally left empty
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::~ValidatingSparseParameterLiftingModelChecker() {
+            if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                STORM_PRINT_AND_LOG("Validating Parameter Lifting Model Checker detected " << numOfWrongRegions << " regions where the imprecise method was wrong.");
+            }
+        }
+        
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        bool ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
+            return getImpreciseChecker().canHandle(parametricModel, checkTask) && getPreciseChecker().canHandle(parametricModel, checkTask);
+        };
+ 
+        template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        RegionResult ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> 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<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber>;
+        template class ValidatingSparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber>;
+
+    }
+}
--- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h
+++ 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 <typename SparseModelType, typename ImpreciseType, typename PreciseType>
+        class ValidatingSparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
+            static_assert(storm::NumberTraits<PreciseType>::IsExact, "Specified type for exact computations is not exact.");
+
+        public:
+            ValidatingSparseParameterLiftingModelChecker();
+            virtual ~ValidatingSparseParameterLiftingModelChecker();
+            
+            virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> 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<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
+
+        protected:
+            
+            virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() = 0;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType> const& getImpreciseChecker() const = 0;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, PreciseType>& getPreciseChecker() = 0;
+            virtual SparseParameterLiftingModelChecker<SparseModelType, PreciseType> const& getPreciseChecker() const = 0;
+            
+            virtual void applyHintsToPreciseChecker() = 0;
+
+        private:
+            
+            // Information for statistics
+            uint_fast64_t numOfWrongRegions;
+            
+        };
+    }
+}