From 0ef2b55c75f8c2d8e931944c8d9dff19144369ae Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 6 Aug 2016 14:56:46 +0200 Subject: [PATCH] made some region settings attribute to the model checker instead of global Former-commit-id: e53ca967607b5b32690d82ea919f69ffd538acc0 --- src/modelchecker/region/ParameterRegion.cpp | 7 -- .../region/SparseDtmcRegionModelChecker.cpp | 14 ++-- .../region/SparseDtmcRegionModelChecker.h | 2 +- .../region/SparseMdpRegionModelChecker.cpp | 4 +- .../region/SparseMdpRegionModelChecker.h | 2 +- .../region/SparseRegionModelChecker.cpp | 73 ++++++++++++++----- .../region/SparseRegionModelChecker.h | 44 +++++++---- src/settings/modules/RegionSettings.cpp | 37 +--------- src/settings/modules/RegionSettings.h | 33 +-------- src/utility/storm.h | 8 +- .../SparseDtmcRegionModelCheckerTest.cpp | 22 +++--- 11 files changed, 118 insertions(+), 128 deletions(-) diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index b04fda643..0f3fe8a52 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -1,10 +1,3 @@ -/* - * File: ParameterRegion.cpp - * Author: tim - * - * Created on August 10, 2015, 1:51 PM - */ - #include "src/modelchecker/region/ParameterRegion.h" #include "src/utility/region.h" diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 18b373d72..c02ce14cc 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -36,8 +36,8 @@ namespace storm { namespace region { template - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(std::shared_ptr model) : - SparseRegionModelChecker(model){ + SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings) : + SparseRegionModelChecker(model, settings){ //intentionally left empty } @@ -247,8 +247,8 @@ namespace storm { simpleFormula = std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); } //Check if the reachability function needs to be computed - if((storm::settings::getModule().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || - (storm::settings::getModule().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ + if((this->getSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || + (this->getSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ this->computeReachabilityFunction(*(this->getSimpleModel())->template as>()); } } @@ -439,8 +439,8 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { bool valueInBoundOfFormula; - if((storm::settings::getModule().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || - (!storm::settings::getModule().doSample() && favorViaFunction)){ + if((this->getSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || + (!this->getSettings().doSample() && favorViaFunction)){ //evaluate the reachability function valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->evaluateReachabilityFunction(point)); } @@ -496,7 +496,7 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkSmt(ParameterRegion& region) { - STORM_LOG_THROW((storm::settings::getModule().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented."); + STORM_LOG_THROW((this->getSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented."); if (region.getCheckResult()==RegionCheckResult::UNKNOWN){ //Sampling needs to be done (on a single point) checkPoint(region,region.getSomePoint(), true); diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index 6854879d1..868ebe8b7 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -20,7 +20,7 @@ namespace storm { typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit SparseDtmcRegionModelChecker(std::shared_ptr model); + SparseDtmcRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings); virtual ~SparseDtmcRegionModelChecker(); diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index cc913c52c..79d090347 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -36,8 +36,8 @@ namespace storm { namespace region { template - SparseMdpRegionModelChecker::SparseMdpRegionModelChecker(std::shared_ptr model) : - SparseRegionModelChecker(model){ + SparseMdpRegionModelChecker::SparseMdpRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings) : + SparseRegionModelChecker(model, settings){ STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidArgumentException, "Tried to create an mdp region model checker for a model that is not an mdp"); } diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.h b/src/modelchecker/region/SparseMdpRegionModelChecker.h index 244d7411c..3fccb56ea 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.h @@ -19,7 +19,7 @@ namespace storm { typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit SparseMdpRegionModelChecker(std::shared_ptr model); + SparseMdpRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings); virtual ~SparseMdpRegionModelChecker(); diff --git a/src/modelchecker/region/SparseRegionModelChecker.cpp b/src/modelchecker/region/SparseRegionModelChecker.cpp index a9172a204..c4a4979bf 100644 --- a/src/modelchecker/region/SparseRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseRegionModelChecker.cpp @@ -1,10 +1,3 @@ -/* - * File: SparseRegionModelChecker.cpp - * Author: tim - * - * Created on September 9, 2015, 12:34 PM - */ - #include "src/modelchecker/region/SparseRegionModelChecker.h" #include "src/adapters/CarlAdapter.h" @@ -30,11 +23,42 @@ namespace storm { namespace modelchecker { namespace region { - + + SparseRegionModelCheckerSettings::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode const& sampleM, + storm::settings::modules::RegionSettings::ApproxMode const& appM, + storm::settings::modules::RegionSettings::SmtMode const& smtM) : sampleMode(sampleM), approxMode(appM), smtMode(smtM) { + // Intentionally left empty + } + + storm::settings::modules::RegionSettings::ApproxMode SparseRegionModelCheckerSettings::getApproxMode() const { + return this->approxMode; + } + + storm::settings::modules::RegionSettings::SampleMode SparseRegionModelCheckerSettings::getSampleMode() const { + return this->sampleMode; + } + + storm::settings::modules::RegionSettings::SmtMode SparseRegionModelCheckerSettings::getSmtMode() const { + return this->smtMode; + } + + bool SparseRegionModelCheckerSettings::doApprox() const { + return getApproxMode() != storm::settings::modules::RegionSettings::ApproxMode::OFF; + } + + bool SparseRegionModelCheckerSettings::doSample() const { + return getSampleMode() != storm::settings::modules::RegionSettings::SampleMode::OFF; + } + + bool SparseRegionModelCheckerSettings::doSmt() const { + return getSmtMode() != storm::settings::modules::RegionSettings::SmtMode::OFF; + } + template - SparseRegionModelChecker::SparseRegionModelChecker(std::shared_ptr model) : + SparseRegionModelChecker::SparseRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings) : model(model), - specifiedFormula(nullptr){ + specifiedFormula(nullptr), + settings(settings) { STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state."); } @@ -83,6 +107,19 @@ namespace storm { return this->simpleFormula; } +// template +// SparseRegionModelCheckerSettings& SparseRegionModelChecker::getSettings() { +// return this->settings; +// }; + + template + SparseRegionModelCheckerSettings const& SparseRegionModelChecker::getSettings() const { + return this->settings; + }; + + + + template void SparseRegionModelChecker::specifyFormula(std::shared_ptr formula) { std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now(); @@ -133,11 +170,11 @@ namespace storm { //Check if the approximation and the sampling model needs to be computed if(!this->isResultConstant()){ - if(this->isApproximationApplicable && storm::settings::getModule().doApprox()){ + if(this->isApproximationApplicable && settings.doApprox()){ initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula()); } - if(storm::settings::getModule().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || - (!storm::settings::getModule().doSample() && storm::settings::getModule().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ + if(settings.getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || + (!settings.doSample() && settings.getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula()); } } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber(-1.0)){ @@ -240,10 +277,10 @@ namespace storm { //switches for the different steps. bool done=false; - STORM_LOG_WARN_COND( (!storm::settings::getModule().doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions (more precisely: linear in a single parameter, i.e., functions like p*q are okay). As this is not the case, approximation is deactivated"); - bool doApproximation=storm::settings::getModule().doApprox() && this->isApproximationApplicable; - bool doSampling=storm::settings::getModule().doSample(); - bool doSmt=storm::settings::getModule().doSmt(); + STORM_LOG_WARN_COND( (!settings.doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions (more precisely: linear in a single parameter, i.e., functions like p*q are okay). As this is not the case, approximation is deactivated"); + bool doApproximation=settings.doApprox() && this->isApproximationApplicable; + bool doSampling=settings.doSample(); + bool doSmt=settings.doSmt(); if(this->isResultConstant()){ STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none."); @@ -316,7 +353,7 @@ namespace storm { bool proveAllSat; switch (region.getCheckResult()){ case RegionCheckResult::UNKNOWN: - switch(storm::settings::getModule().getApproxMode()){ + switch(this->settings.getApproxMode()){ case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST: //Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED checkPoint(region,region.getSomePoint(), false); diff --git a/src/modelchecker/region/SparseRegionModelChecker.h b/src/modelchecker/region/SparseRegionModelChecker.h index ba45341d4..d73fd49b6 100644 --- a/src/modelchecker/region/SparseRegionModelChecker.h +++ b/src/modelchecker/region/SparseRegionModelChecker.h @@ -1,12 +1,4 @@ -/* - * File: SparseRegionModelChecker.h - * Author: tim - * - * Created on September 9, 2015, 12:34 PM - */ - -#ifndef STORM_MODELCHECKER_REGION_SPARSEREGIONMODELCHECKER_H -#define STORM_MODELCHECKER_REGION_SPARSEREGIONMODELCHECKER_H +#pragma once #include #include @@ -23,9 +15,31 @@ #include "src/models/sparse/Mdp.h" #include "src/logic/Formulas.h" +#include "src/settings/modules/RegionSettings.h" + namespace storm { namespace modelchecker{ namespace region{ + + class SparseRegionModelCheckerSettings { + public: + SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode const& sampleM, + storm::settings::modules::RegionSettings::ApproxMode const& appM, + storm::settings::modules::RegionSettings::SmtMode const& smtM); + + storm::settings::modules::RegionSettings::SampleMode getSampleMode() const; + storm::settings::modules::RegionSettings::ApproxMode getApproxMode() const; + storm::settings::modules::RegionSettings::SmtMode getSmtMode() const; + + bool doApprox() const; + bool doSmt() const; + bool doSample() const; + private: + storm::settings::modules::RegionSettings::SampleMode sampleMode; + storm::settings::modules::RegionSettings::ApproxMode approxMode; + storm::settings::modules::RegionSettings::SmtMode smtMode; + }; + template class SparseRegionModelChecker : public AbstractSparseRegionModelChecker { public: @@ -34,7 +48,7 @@ namespace storm { typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit SparseRegionModelChecker(std::shared_ptr model); + SparseRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings); virtual ~SparseRegionModelChecker(); @@ -138,6 +152,9 @@ namespace storm { */ std::shared_ptr const& getSpecifiedFormula() const; + //SparseRegionModelCheckerSettings& getSettings(); + SparseRegionModelCheckerSettings const& getSettings() const; + protected: /*! @@ -244,6 +261,10 @@ namespace storm { std::shared_ptr> samplingModel; // a flag that is true iff the resulting reachability function is constant boost::optional constantResult; + + SparseRegionModelCheckerSettings settings; + + // runtimes and other information for statistics. uint_fast64_t numOfCheckedRegions; @@ -269,6 +290,3 @@ namespace storm { } //namespace region } //namespace modelchecker } //namespace storm - -#endif /* STORM_MODELCHECKER_REGION_SPARSEREGIONMODELCHECKER_H */ - diff --git a/src/settings/modules/RegionSettings.cpp b/src/settings/modules/RegionSettings.cpp index 9422719ca..2ead32614 100644 --- a/src/settings/modules/RegionSettings.cpp +++ b/src/settings/modules/RegionSettings.cpp @@ -19,7 +19,7 @@ namespace storm { const std::string RegionSettings::smtmodeOptionName = "smtmode"; const std::string RegionSettings::refinementOptionName = "refinement"; - RegionSettings::RegionSettings() : ModuleSettings(moduleName), modesModified(false) { + RegionSettings::RegionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the regions.") .addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); @@ -58,9 +58,6 @@ namespace storm { } RegionSettings::ApproxMode RegionSettings::getApproxMode() const { - if(this->modesModified) { - return this->approxMode; - } std::string modeString= this->getOption(approxmodeOptionName).getArgumentByName("mode").getValueAsString(); if(modeString=="off"){ return ApproxMode::OFF; @@ -79,14 +76,7 @@ namespace storm { return ApproxMode::OFF; } - bool RegionSettings::doApprox() const { - return getApproxMode()!=ApproxMode::OFF; - } - RegionSettings::SampleMode RegionSettings::getSampleMode() const { - if (this->modesModified){ - return this->sampleMode; - } std::string modeString= this->getOption(samplemodeOptionName).getArgumentByName("mode").getValueAsString(); if(modeString=="off"){ return SampleMode::OFF; @@ -101,15 +91,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The sample mode '" << modeString << "' is not valid"); return SampleMode::OFF; } - - bool RegionSettings::doSample() const { - return getSampleMode()!=SampleMode::OFF; - } RegionSettings::SmtMode RegionSettings::getSmtMode() const { - if(this->modesModified){ - return this->smtMode; - } std::string modeString= this->getOption(smtmodeOptionName).getArgumentByName("mode").getValueAsString(); if(modeString=="off"){ return SmtMode::OFF; @@ -124,22 +107,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The smt mode '" << modeString << "' is not valid"); return SmtMode::OFF; } - - bool RegionSettings::doSmt() const { - return getSmtMode()!=SmtMode::OFF; - } - - void RegionSettings::modifyModes(ApproxMode const& approxMode, SampleMode const& sampleMode, SmtMode const& smtMode) { - this->approxMode = approxMode; - this->sampleMode = sampleMode; - this->smtMode = smtMode; - this->modesModified=true; - } - - void RegionSettings::resetModes() { - this->modesModified=false; - } - + + bool RegionSettings::doRefinement() const{ return this->getOption(refinementOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/RegionSettings.h b/src/settings/modules/RegionSettings.h index 1f61c0e42..2ecf6ba5a 100644 --- a/src/settings/modules/RegionSettings.h +++ b/src/settings/modules/RegionSettings.h @@ -51,43 +51,17 @@ namespace storm { */ ApproxMode getApproxMode() const; - /*! - * Returns whether to use approximation - */ - bool doApprox() const; - /*! * Returns the mode in which Sampling should be used */ SampleMode getSampleMode() const; - /*! - * Returns whether to use Sampling - */ - bool doSample() const; - /*! * Returns the mode in which SMT solving should be used */ SmtMode getSmtMode() const; - /*! - * Returns whether to use SMT Solving - */ - bool doSmt() const; - - /*! - * Sets the modes accordingly. Great for debugging purposes. - * Use resetModes() to switch back to the modes specified by the settings - */ - void modifyModes(ApproxMode const& approxMode, SampleMode const& sampleMode, SmtMode const& smtMode); - - /*! - * Resets the modes to the ones specified by the settings. - * This is useful if the modes have been altered by setModes(...) - */ - void resetModes(); - + bool doRefinement() const; double getRefinementThreshold() const; @@ -102,11 +76,6 @@ namespace storm { const static std::string samplemodeOptionName; const static std::string smtmodeOptionName; const static std::string refinementOptionName; - - bool modesModified; - ApproxMode approxMode; - SampleMode sampleMode; - SmtMode smtMode; }; } // namespace modules diff --git a/src/utility/storm.h b/src/utility/storm.h index 0ffbea3f1..ad9cb1de0 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -409,18 +409,20 @@ namespace storm { storm::prism::Program program = parseProgram(programFilePath); program.checkValidity(); std::vector> formulas = parseFormulasForProgram(formulaString, program);; - if(formulas.size()!=1){ + if(formulas.size()!=1) { STORM_LOG_ERROR("The given formulaString does not specify exactly one formula"); return false; } std::shared_ptr> model = buildSparseModel(program, formulas); + auto const& regionSettings = storm::settings::getModule(); + storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); // Preprocessing and ModelChecker if(model->isOfType(storm::models::ModelType::Dtmc)){ preprocessModel>(model,formulas); - regionModelChecker = std::make_shared, double>>(model->as>()); + regionModelChecker = std::make_shared, double>>(model->as>(), settings); } else if (model->isOfType(storm::models::ModelType::Mdp)){ preprocessModel>(model,formulas); - regionModelChecker = std::make_shared, double>>(model->as>()); + regionModelChecker = std::make_shared, double>>(model->as>(), settings); } else { STORM_LOG_ERROR("The type of the given model is not supported (only Dtmcs or Mdps are supported"); return false; diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 0a5424791..1f38f5ca6 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -48,10 +48,11 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method - storm::settings::getModule().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::getModule().doApprox()); - ASSERT_TRUE(storm::settings::getModule().doSample()); - ASSERT_FALSE(storm::settings::getModule().doSmt()); + storm::modelchecker::region::SparseRegionModelCheckerSettings settings(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); + dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker, settings); + ASSERT_TRUE(settings.doApprox()); + ASSERT_TRUE(settings.doSample()); + ASSERT_FALSE(settings.doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegion); @@ -63,18 +64,19 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); - storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::getModule().doApprox()); - ASSERT_TRUE(storm::settings::getModule().doSample()); - ASSERT_TRUE(storm::settings::getModule().doSmt()); + + settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); + dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker, settings); + ASSERT_FALSE(settings.doApprox()); + ASSERT_TRUE(settings.doSample()); + ASSERT_TRUE(settings.doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(allVioRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); - - storm::settings::mutableRegionSettings().resetModes(); + carl::VariablePool::getInstance().clear(); }