diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp index d02a43a88..116c63b34 100644 --- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -3,6 +3,7 @@ #include #include #include +#include #include "storm/adapters/CarlAdapter.h" #include "storm/logic/Formulas.h" @@ -33,6 +34,7 @@ #include "storm/transformer/SparseParametricDtmcSimplifier.h" #include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h" +#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h" namespace storm { namespace modelchecker { @@ -427,6 +429,23 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Initialized Sampling Model"); } + + template + void SparseDtmcRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + STORM_LOG_DEBUG("Initializing the Approx Model...."); + std::chrono::high_resolution_clock::time_point timeInitApproximationModelStart = std::chrono::high_resolution_clock::now(); + this->approximationModel = std::make_shared>(model); + // replace bounds by optimization direction to obtain a quantitative formula + if(formula->isProbabilityOperatorFormula()) { + auto quantitativeFormula = std::make_shared(formula->getSubformula().asSharedPointer(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize)); + this->approximationModel->specifyFormula(*quantitativeFormula); + } else { + auto quantitativeFormula = std::make_shared(formula->getSubformula().asSharedPointer(), formula->asRewardOperatorFormula().getOptionalRewardModelName(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize)); + this->approximationModel->specifyFormula(*quantitativeFormula); + } + std::chrono::high_resolution_clock::time_point timeInitApproximationModelEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Initialized Approximation Model"); + } template void SparseDtmcRegionModelChecker::computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel){ diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h index ecdad8c5b..01ba478b3 100644 --- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -62,6 +62,13 @@ namespace storm { */ virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; + + /*! + * initializes the Approx Model + */ + virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; + + private: /*! * Does some sanity checks and preprocessing steps on the currently specified model and diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp index 350604ba1..f5b6d97a0 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -316,6 +316,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkSmt invoked but smt solving has not been implemented for MDPs."); } + + + template + void SparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + std::cout << "approx model for mdps not implemented" << std::endl; + } + #ifdef STORM_HAVE_CARL template class SparseMdpRegionModelChecker, double>; #endif diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h index accebefe2..d849df6c3 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h @@ -85,6 +85,10 @@ namespace storm { * initializes the Sampling Model */ virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; + /*! + * initializes the Approx Model + */ + virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; }; } //namespace region diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp index 3f7dbde59..8baa6ab02 100644 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp @@ -19,6 +19,9 @@ #include "storm/exceptions/UnexpectedException.h" #include "modelchecker/results/CheckResult.h" #include "modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/parametric/ParameterRegion.h" + namespace storm { namespace modelchecker { @@ -191,17 +194,6 @@ namespace storm { this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart; } - template - void SparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { - std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Initializing the Approximation Model..."); - STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Approximation model requested but approximation is not applicable"); - this->approximationModel=std::make_shared>(model, formula); - std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now(); - this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart; - STORM_LOG_DEBUG("Initialized Approximation Model"); - } - template void SparseRegionModelChecker::checkRegions(std::vector>& regions) { STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); @@ -408,12 +400,12 @@ namespace storm { return (proveAllSat==this->checkFormulaOnSamplingPoint(region.getSomePoint())); } bool computeLowerBounds = (this->specifiedFormulaHasLowerBound() && proveAllSat) || (!this->specifiedFormulaHasLowerBound() && !proveAllSat); - bool formulaSatisfied = this->getApproximationModel()->checkFormulaOnRegion(region, computeLowerBounds); + bool formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximationModel()->check(storm::modelchecker::parametric::ParameterRegion(region.getLowerBoundaries(), region.getUpperBoundaries()), computeLowerBounds ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult()[*this->simpleModel->getInitialStates().begin()]); return (proveAllSat==formulaSatisfied); } template - std::shared_ptr> const& SparseRegionModelChecker::getApproximationModel() { + std::shared_ptr> const& SparseRegionModelChecker::getApproximationModel() { if(this->approximationModel==nullptr){ STORM_LOG_WARN("Approximation model requested but it has not been initialized when specifying the formula. Will initialize it now."); initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula()); diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.h b/src/storm/modelchecker/region/SparseRegionModelChecker.h index 992317055..ab90cbfac 100644 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseRegionModelChecker.h @@ -2,12 +2,15 @@ #include #include +#include #include "storm/utility/region.h" #include "storm/modelchecker/region/AbstractSparseRegionModelChecker.h" #include "storm/modelchecker/region/ParameterRegion.h" #include "storm/modelchecker/region/ApproximationModel.h" #include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h" +#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h" + #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Model.h" @@ -39,7 +42,7 @@ namespace storm { storm::settings::modules::RegionSettings::ApproxMode approxMode; storm::settings::modules::RegionSettings::SmtMode smtMode; }; - + template class SparseRegionModelChecker : public AbstractSparseRegionModelChecker { public: @@ -191,7 +194,7 @@ namespace storm { * Returns the approximation model. * If it is not yet available, it is computed. */ - std::shared_ptr> const& getApproximationModel(); + std::shared_ptr> const& getApproximationModel(); /*! * Checks the value of the function at some sampling points within the given region. @@ -240,13 +243,18 @@ namespace storm { // the model that can be instantiated to check the value at a certain point std::shared_ptr> samplingModel; - private: - /*! + /*! * initializes the Approximation Model - * + * * @note does not check whether approximation can be applied */ - void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula); + virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) = 0; + + // the model that is used to approximate the reachability values + std::shared_ptr> approximationModel; + + private: + // The model this model checker is supposed to analyze. @@ -261,8 +269,6 @@ namespace storm { std::shared_ptr simpleFormula; // a flag that is true if approximation is applicable, i.e., there are only linear functions at transitions of the model bool isApproximationApplicable; - // the model that is used to approximate the reachability values - std::shared_ptr> approximationModel; // a flag that is true iff the resulting reachability function is constant boost::optional constantResult;