From 5b1494b9a92a51bb4241db730b99be9bad4df96f Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 7 Sep 2015 20:28:20 +0200 Subject: [PATCH] Made use of this new cool rewardModel thing Former-commit-id: d670d09278d035def65a31ae2ed508471f213a29 --- src/builder/ExplicitPrismModelBuilder.cpp | 6 +- .../region/ApproximationModel.cpp | 122 ++++++------------ src/modelchecker/region/ApproximationModel.h | 5 +- .../region/SparseDtmcRegionModelChecker.cpp | 36 ++++-- .../region/SparseDtmcRegionModelChecker.h | 2 + src/utility/constants.cpp | 10 ++ .../SparseDtmcRegionModelCheckerTest.cpp | 47 +++++++ 7 files changed, 132 insertions(+), 96 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index cf02700eb..7fa0043e9 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -460,7 +460,8 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + //STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + STORM_LOG_ERROR_COND(!discreteTimeModel || comparator.isOne(probabilitySum), "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); } } @@ -536,7 +537,8 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + //STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + STORM_LOG_ERROR_COND(!discreteTimeModel || comparator.isOne(probabilitySum), "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); // Dispose of the temporary maps. delete currentTargetStates; diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 2514abb78..1e11a5c8d 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -39,14 +39,12 @@ namespace storm { //Now consider rewards std::unordered_map> rewardModels; - std::vector stateRewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping + std::vector rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping std::vector transitionRewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping if(this->computeRewards){ - boost::optional> stateRewards; boost::optional> stateActionRewards; - boost::optional> transitionRewards; - initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateRewards, transitionRewards, stateRewardEntryToEvalTableMapping, transitionRewardEntryToEvalTableMapping, constantEntryIndex); - rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); + initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, transitionRewardEntryToEvalTableMapping, constantEntryIndex); + rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(boost::optional>(), std::move(stateActionRewards)))); } //Obtain other model ingredients and the approximation model itself storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling()); @@ -71,18 +69,13 @@ namespace storm { } } if(this->computeRewards){ - //the same for state and transition rewards - auto approxModelStateRewardEntry = this->model->getUniqueRewardModel()->second.getStateRewardVector().begin(); - for (std::size_t const& tableIndex : stateRewardEntryToEvalTableMapping){ + //the same for rewards + auto approxModelRewardEntry = this->model->getUniqueRewardModel()->second.getStateActionRewardVector().begin(); + for (std::size_t const& tableIndex : rewardEntryToEvalTableMapping){ if(tableIndex != constantEntryIndex){ - this->stateRewardMapping.emplace_back(std::make_tuple(&(std::get<2>(this->rewardEvaluationTable[tableIndex])), &(std::get<3>(this->rewardEvaluationTable[tableIndex])), approxModelStateRewardEntry)); + this->rewardMapping.emplace_back(std::make_tuple(&(std::get<2>(this->rewardEvaluationTable[tableIndex])), &(std::get<3>(this->rewardEvaluationTable[tableIndex])), approxModelRewardEntry)); } - ++approxModelStateRewardEntry; - } - auto approxModelTransitionRewardEntry = this->model->getUniqueRewardModel()->second.getTransitionRewardMatrix().begin(); - for (std::size_t const& tableIndex : transitionRewardEntryToEvalTableMapping){ - this->transitionRewardMapping.emplace_back(std::make_tuple(&(std::get<2>(this->rewardEvaluationTable[tableIndex])), &(std::get<3>(this->rewardEvaluationTable[tableIndex])), approxModelTransitionRewardEntry)); - ++approxModelTransitionRewardEntry; + ++approxModelRewardEntry; } //Get the sets of reward parameters that map to "CHOSEOPTIMAL". this->choseOptimalRewardPars = std::vector>(this->rewardSubstitutions.size()); @@ -158,61 +151,41 @@ namespace storm { void SparseDtmcRegionModelChecker::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, - boost::optional >& stateRewards, - boost::optional >& transitionRewards, - std::vector& stateRewardEntryToEvalTableMapping, + boost::optional>& stateActionRewardVector, + std::vector& rewardEntryToEvalTableMapping, std::vector& transitionRewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex) { // run through the state reward vector of the parametric model. // Constant entries can be set directly. - // For Parametric entries we have two cases: - // (1) make state rewards if the reward is independent of parameters that occur in probability functions. - // (2) make transition rewards otherwise. - - //stateRewards - std::vector stateRewardsAsVector(parametricModel.getNumberOfStates()); - std::size_t numOfNonConstStateRewEntries=0; - //TransitionRewards - storm::storage::SparseMatrixBuilder matrixBuilder(probabilityMatrix.getRowCount(), probabilityMatrix.getColumnCount(), 0, true, true, probabilityMatrix.getRowGroupCount()); - std::size_t numOfNonConstTransitonRewEntries=0; + // For Parametric entries we set a dummy value and add one entry to the rewardEntryEvalTableMapping + std::vector stateActionRewardsAsVector; + stateActionRewardsAsVector.reserve(probabilityMatrix.getRowCount()); + rewardEntryToEvalTableMapping.reserve(probabilityMatrix.getRowCount()); + std::size_t numOfNonConstRewEntries=0; this->rewardSubstitutions.emplace_back(std::map()); //we want that the empty substitution is always the first one - + for(std::size_t state=0; state occurringRewVariables; std::set occurringProbVariables; - bool makeStateReward=true; + std::size_t evalTableIndex; if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){ - stateRewardsAsVector[state]=storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])); - stateRewardEntryToEvalTableMapping.emplace_back(constantEntryIndex); + ConstantType reward = storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])); + //Add one of these entries for every row in the row group of state + for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRowsecond.getStateRewardVector()[state], occurringRewVariables); - for(auto const& entry : parametricModel.getTransitionMatrix().getRow(state)){ - storm::utility::regions::gatherOccurringVariables(entry.getValue(), occurringProbVariables); - } - for( auto const& rewVar : occurringRewVariables){ - if(occurringProbVariables.find(rewVar)!=occurringProbVariables.end()){ - makeStateReward=false; - break; - } - } - if(makeStateReward){ - //Get the corresponding substitution and substitutionIndex - std::map rewardSubstitution; - for(auto const& rewardVar : occurringRewVariables){ - rewardSubstitution.insert(std::make_pair(rewardVar, TypeOfBound::CHOSEOPTIMAL)); - } - std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution)); - //insert table entry and dummy data in the stateRewardVector - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(substitutionIndex, parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero(), storm::utility::zero())); - stateRewardEntryToEvalTableMapping.emplace_back(tableIndex); - stateRewardsAsVector[state]=storm::utility::zero(); - ++numOfNonConstStateRewEntries; - } else { - for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow rewardSubstitution; for(auto const& rewardVar : occurringRewVariables){ typename std::map::iterator const substitutionIt=this->probabilitySubstitutions[rowSubstitutions[matrixRow]].find(rewardVar); @@ -220,26 +193,21 @@ namespace storm { rewardSubstitution.insert(std::make_pair(rewardVar, TypeOfBound::CHOSEOPTIMAL)); } else { rewardSubstitution.insert(*substitutionIt); + rewardDependsOnProbVars=true; } } std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution)); - //insert table entries and dummy data - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(substitutionIndex, parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero(), storm::utility::zero())); - for(auto const& matrixEntry : probabilityMatrix.getRow(matrixRow)){ - transitionRewardEntryToEvalTableMapping.emplace_back(tableIndex); - matrixBuilder.addNextValue(matrixRow, matrixEntry.getColumn(), storm::utility::zero()); - ++numOfNonConstTransitonRewEntries; - } + tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(substitutionIndex, parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero(), storm::utility::zero())); } - stateRewardsAsVector[state]=storm::utility::zero(); - stateRewardEntryToEvalTableMapping.emplace_back(constantEntryIndex); + //insert table entries and dummy data + stateActionRewardsAsVector.emplace_back(storm::utility::zero()); + rewardEntryToEvalTableMapping.emplace_back(tableIndex); + ++numOfNonConstRewEntries; } } } - stateRewards=std::move(stateRewardsAsVector); - this->stateRewardMapping.reserve(numOfNonConstStateRewEntries); - transitionRewards=matrixBuilder.build(); - this->transitionRewardMapping.reserve(numOfNonConstTransitonRewEntries); + stateActionRewardVector=std::move(stateActionRewardsAsVector); + this->rewardMapping.reserve(numOfNonConstRewEntries); } @@ -343,20 +311,14 @@ namespace storm { //write the reward values into the model switch(optDir){ case storm::solver::OptimizationDirection::Minimize: - for(auto& mappingTriple : this->stateRewardMapping){ + for(auto& mappingTriple : this->rewardMapping){ *std::get<2>(mappingTriple)=*std::get<0>(mappingTriple); } - for(auto& mappingTriple : this->transitionRewardMapping){ - std::get<2>(mappingTriple)->setValue(*(std::get<0>(mappingTriple))); - } break; case storm::solver::OptimizationDirection::Maximize: - for(auto& mappingTriple : this->stateRewardMapping){ + for(auto& mappingTriple : this->rewardMapping){ *std::get<2>(mappingTriple)=*std::get<1>(mappingTriple); } - for(auto& mappingTriple : this->transitionRewardMapping){ - std::get<2>(mappingTriple)->setValue(*(std::get<1>(mappingTriple))); - } break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given optimality Type is not supported."); diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index fbdd14861..c101a2ac4 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -59,7 +59,7 @@ namespace storm { }; void initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& rowSubstitutions, std::vector& matrixEntryToEvalTableMapping, std::size_t const& constantEntryIndex); - void initializeRewards(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, boost::optional>& stateRewards, boost::optional>& transitionRewards, std::vector& stateRewardEntryToEvalTableMapping, std::vector& transitionRewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex); + void initializeRewards(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, boost::optional>& stateActionRewardVector, std::vector& stateRewardEntryToEvalTableMapping, std::vector& transitionRewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex); //Vector has one entry for every (non-constant) matrix entry. //pair.first points to an entry in the evaluation table, @@ -67,8 +67,7 @@ namespace storm { std::vector::iterator>> probabilityMapping; //similar for the rewards. But now the first entry points to a minimal and the second one to a maximal value. //The third entry points to the state reward vector and the transitionRewardMatrix, respectively. - std::vector::iterator>> stateRewardMapping; - std::vector::iterator>> transitionRewardMapping; + std::vector::iterator>> rewardMapping; //Vector has one (unique) entry for every occurring pair of a non-constant function and // a substitution, i.e., a mapping of variables to a TypeOfBound diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index afe825b2d..3331c290c 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -76,15 +76,17 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now(); STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled."); + //Note: canHandle already ensures that the formula has the right shape. + this->specifiedFormula = formula; this->isResultConstant=false; + this->isResultInfinity=false; + this->simpleFormula=nullptr; this->isApproximationApplicable=false; this->smtSolver=nullptr; this->approximationModel=nullptr; this->samplingModel=nullptr; this->reachabilityFunction=nullptr; - //Note: canHandle already ensures that the formula has the right shape. - this->specifiedFormula = formula; // set some information regarding the formula and model. Also computes a more simple version of the model preprocess(); if(!this->isResultConstant){ @@ -154,7 +156,6 @@ namespace storm { storm::storage::sparse::state_type initialState = *(this->model.getInitialStates() % maybeStates).begin(); // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = this->model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - // Eliminate all states with only constant outgoing transitions // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. auto flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix); @@ -355,11 +356,20 @@ namespace storm { //maybeStates: Compute the subset of states that has a reachability reward less than infinity. storm::storage::BitVector statesWithProbability1 = storm::utility::graph::performProb1(this->model.getBackwardTransitions(), storm::storage::BitVector(this->model.getNumberOfStates(), true), targetStates); maybeStates = ~targetStates & statesWithProbability1; - // If the initial state is known to have 0 reward or an infinite reward value, we can directly set the reachRewardFunction. + + //Compute the new state reward vector + stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->model.getTransitionMatrix(), maybeStates); + + // If the initial state is known to have 0 reward or an infinite reachability reward value, we can directly set the reachRewardFunction. storm::storage::sparse::state_type initialState = *this->model.getInitialStates().begin(); if (!maybeStates.get(initialState)) { STORM_LOG_WARN("The expected reward of the initial state is constant (infinity or zero)"); - this->reachabilityFunction = std::make_shared(statesWithProbability1.get(initialState) ? storm::utility::zero() : storm::utility::infinity()); + if(statesWithProbability1.get(initialState)){ + this->reachabilityFunction = std::make_shared(storm::utility::zero()); + } else { + this->reachabilityFunction = std::make_shared(storm::utility::one()); + this->isResultInfinity=true; + } this->isResultConstant=true; return; //nothing else to do... } @@ -414,9 +424,6 @@ namespace storm { } } STORM_LOG_WARN_COND(!this->isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); - - //Everything is fine, so we can now compute the new state reward vector - stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->model.getTransitionMatrix(), maybeStates); } @@ -508,8 +515,7 @@ namespace storm { if(!done && this->isResultConstant){ STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none."); - STORM_LOG_THROW(storm::utility::isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); - if(valueIsInBoundOfFormula(this->getReachabilityValue(region.getSomePoint(), true))){ + if(valueIsInBoundOfFormula(this->getReachabilityValue(region.getSomePoint(), true))){ region.setCheckResult(RegionCheckResult::ALLSAT); } else{ @@ -750,7 +756,15 @@ namespace storm { template template ValueType SparseDtmcRegionModelChecker::getReachabilityValue(std::map const& point, bool evaluateFunction) { - if(evaluateFunction || this->isResultConstant){ + if(this->isResultConstant){ + //Todo: remove workaround (infinityisResultInfinity){ + return storm::utility::infinity(); + } + STORM_LOG_THROW(storm::utility::isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); + return storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(*getReachabilityFunction())); + } + if(evaluateFunction){ return storm::utility::regions::convertNumber(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point)); } else { getSamplingModel()->instantiate(point); diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index b75549fe9..f54954332 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -257,6 +257,8 @@ namespace storm { bool isApproximationApplicable; // a flag that is true iff the resulting reachability function is constant bool isResultConstant; + // workaround to represent that the result is infinity (utility::infinity() does not work at this moment) + bool isResultInfinity; // the smt solver that is used to prove properties with the help of the reachabilityFunction std::shared_ptr smtSolver; diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 4ba26ea99..4ff8be6fd 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -4,6 +4,7 @@ #include "src/storage/sparse/StateType.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/utility/macros.h" #include "src/adapters/CarlAdapter.h" @@ -74,8 +75,16 @@ namespace storm { template<> storm::RationalFunction infinity() { // FIXME: this does not work. + STORM_LOG_ERROR("Tried to get infinity as a rational function, which does not seem to work"); return storm::RationalFunction(carl::rationalize(std::numeric_limits::infinity())); } + + template<> + storm::RationalNumber infinity() { + // FIXME: this does not work. + STORM_LOG_ERROR("Tried to get infinity as a rational number, which does not seem to work"); + return carl::rationalize(std::numeric_limits::infinity()); + } #endif template @@ -221,6 +230,7 @@ namespace storm { template RationalNumber one(); template RationalNumber zero(); + template RationalNumber infinity(); template bool isOne(Interval const& value); template bool isZero(Interval const& value); diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 2019e5d67..00061d570 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -182,6 +182,53 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { storm::settings::mutableRegionSettings().resetModes(); } +TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_16_2.pm"; + std::string const& formulaAsString = "R>2.5 [F \"success\" ]"; + std::string const& constantsAsString = ""; + + //Build model, formula, region model checker + boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); + program->checkValidity(); + storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); + std::vector> formulas = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); + ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); + ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); + modelchecker.specifyFormula(formulas[0]); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + + EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false)); //instantiation of sampling model + EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true)); //instantiation of sampling model + + //test approximative method + storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); + ASSERT_TRUE(storm::settings::regionSettings().doApprox()); + ASSERT_TRUE(storm::settings::regionSettings().doSample()); + ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + modelchecker.checkRegion(allSatRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + + //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) + auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + 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::regionSettings().doApprox()); + ASSERT_TRUE(storm::settings::regionSettings().doSample()); + ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + modelchecker.checkRegion(allSatRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_16_2.pm";