From d377e6b289419cd4ffb902b6add6e27f94dd6782 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 6 Sep 2015 21:29:22 +0200 Subject: [PATCH] Minor improvements everywhere. Also implemented some tests Former-commit-id: be74e5f4594b3f40614c78e34faea60fc2aeb35d --- examples/pdtmc/brp_rewards/brp256-5.sh | 7 + examples/pdtmc/brp_rewards/brp_16_2.pm | 150 ++++++ .../region/ApproximationModel.cpp | 8 +- src/modelchecker/region/ParameterRegion.cpp | 45 +- src/modelchecker/region/ParameterRegion.h | 14 +- src/modelchecker/region/SamplingModel.cpp | 8 +- .../region/SparseDtmcRegionModelChecker.cpp | 78 +-- .../region/SparseDtmcRegionModelChecker.h | 35 +- src/settings/SettingsManager.cpp | 4 + src/settings/SettingsManager.h | 8 + src/settings/modules/RegionSettings.cpp | 32 +- src/settings/modules/RegionSettings.h | 20 +- src/utility/regions.cpp | 25 +- src/utility/regions.h | 9 +- .../SparseDtmcRegionModelCheckerTest.cpp | 468 ++++++++++++++++++ test/functional/storm-functional-tests.cpp | 3 + 16 files changed, 832 insertions(+), 82 deletions(-) create mode 100755 examples/pdtmc/brp_rewards/brp256-5.sh create mode 100644 examples/pdtmc/brp_rewards/brp_16_2.pm create mode 100644 test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp diff --git a/examples/pdtmc/brp_rewards/brp256-5.sh b/examples/pdtmc/brp_rewards/brp256-5.sh new file mode 100755 index 000000000..c3c52ba6a --- /dev/null +++ b/examples/pdtmc/brp_rewards/brp256-5.sh @@ -0,0 +1,7 @@ +#!/bin/bash + +smtcommand=$(cat smtcommand.txt) + +/home/tim/git/storm/build/storm -s "/home/tim/git/paramagic/benchmarkfiles/pdtmc/brp/brp_256-5.pm" --prop 'P<0.5 [F "target"]' --parametric --parametricRegion --smt2:exportscript "/home/tim/Desktop/smtlibcommand.smt2" --smt2:solvercommand "$smtcommand" --region:regionfile /home/tim/Desktop/brpRegions.txt $1 + + diff --git a/examples/pdtmc/brp_rewards/brp_16_2.pm b/examples/pdtmc/brp_rewards/brp_16_2.pm new file mode 100644 index 000000000..f28a124c1 --- /dev/null +++ b/examples/pdtmc/brp_rewards/brp_16_2.pm @@ -0,0 +1,150 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 + +dtmc + +// number of chunks +const int N = 16; +// maximum number of retransmissions +const int MAX = 2; + +// reliability of channels +const double pL; +const double pK; + +// timeouts +const double TOMsg; +const double TOAck; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +// prevents more than one file being sent +module tester + + T : bool; + + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + +rewards + [TO_Msg] true : TOMsg; + [TO_Ack] true : TOAck; +endrewards + +label "error" = s=5; +label "success" = (s=0) & (srep=3); +label "target" = (s=5) | (s=0 & srep=3); + + diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index c6945ab30..9b5a22300 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -56,7 +56,7 @@ namespace storm { auto approxModelEntry = this->model->getTransitionMatrix().getRow(matrixRow).begin(); for(auto const& parEntry : parametricModel.getTransitionMatrix().getRow(row)){ if(*tableIndex == constantEntryIndex){ - approxModelEntry->setValue(storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parEntry.getValue()))); + approxModelEntry->setValue(storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parEntry.getValue()))); } else { this->probabilityMapping.emplace_back(std::make_pair(&(std::get<2>(this->probabilityEvaluationTable[*tableIndex])), approxModelEntry)); } @@ -178,7 +178,7 @@ namespace storm { std::set occurringProbVariables; bool makeStateReward=true; if(this->parametricTypeComparator.isConstant(parametricModel.getStateRewardVector()[state])){ - stateRewardsAsVector[state]=storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state])); + stateRewardsAsVector[state]=storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state])); stateRewardEntryToEvalTableMapping.emplace_back(constantEntryIndex); } else { //reward depends on parameters. Lets find out if probability parameters occur here. @@ -269,7 +269,7 @@ namespace storm { } //write entries into evaluation table for(auto& tableEntry : this->probabilityEvaluationTable){ - std::get<2>(tableEntry)=storm::utility::regions::convertNumber( + std::get<2>(tableEntry)=storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction( std::get<1>(tableEntry), instantiatedSubs[std::get<0>(tableEntry)] @@ -313,7 +313,7 @@ namespace storm { for(auto const& sub : vertex){ instantiatedRewardSubs[std::get<0>(tableEntry)][sub.first]=sub.second; } - ConstantType currValue = storm::utility::regions::convertNumber( + ConstantType currValue = storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction( std::get<1>(tableEntry), instantiatedRewardSubs[std::get<0>(tableEntry)] diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index c788da9bc..3216493c2 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -20,13 +20,25 @@ namespace storm { namespace modelchecker { template - SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map lowerBounds, std::map upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { - //check whether both mappings map the same variables and precompute the set of variables - for (auto const& variableWithBound : lowerBounds) { - STORM_LOG_THROW((upperBounds.find(variableWithBound.first) != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithBound.first); - this->variables.insert(variableWithBound.first); + SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map const& lowerBounds, std::map const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { + init(); + } + + template + SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map&& lowerBounds, std::map&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) { + init(); + } + + template + void SparseDtmcRegionModelChecker::ParameterRegion::init() { + //check whether both mappings map the same variables, check that lowerbound <= upper bound, and pre-compute the set of variables + for (auto const& variableWithLowerBound : this->lowerBounds) { + auto variableWithUpperBound = this->upperBounds.find(variableWithLowerBound.first); + STORM_LOG_THROW((variableWithUpperBound != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithLowerBound.first); + STORM_LOG_THROW((variableWithLowerBound.second<=variableWithUpperBound->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower bound for " << variableWithLowerBound.first << " is larger then the upper bound"); + this->variables.insert(variableWithLowerBound.first); } - for (auto const& variableWithBound : upperBounds) { + for (auto const& variableWithBound : this->upperBounds) { STORM_LOG_THROW((this->variables.find(variableWithBound.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No lower bound specified for Variable " << variableWithBound.first); } } @@ -92,6 +104,11 @@ namespace storm { return resultingVector; } + template + std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSomePoint() const { + return this->getLowerBounds(); + } + template typename SparseDtmcRegionModelChecker::RegionCheckResult SparseDtmcRegionModelChecker::ParameterRegion::getCheckResult() const { return checkResult; @@ -156,11 +173,11 @@ namespace storm { std::string SparseDtmcRegionModelChecker::ParameterRegion::toString() const { std::stringstream regionstringstream; for (auto var : this->getVariables()) { - regionstringstream << storm::utility::regions::convertNumber::CoefficientType, double>(this->getLowerBound(var)); + regionstringstream << storm::utility::regions::convertNumber(this->getLowerBound(var)); regionstringstream << "<="; regionstringstream << storm::utility::regions::getVariableName(var); regionstringstream << "<="; - regionstringstream << storm::utility::regions::convertNumber::CoefficientType, double>(this->getUpperBound(var)); + regionstringstream << storm::utility::regions::convertNumber(this->getUpperBound(var)); regionstringstream << ","; } std::string regionstring = regionstringstream.str(); @@ -188,8 +205,8 @@ namespace storm { STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a parameter"); VariableType var = storm::utility::regions::getVariableFromString(parameter); - CoefficientType lb = storm::utility::regions::convertNumber(parameterBoundsString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::regions::convertNumber(parameterBoundsString.substr(positionOfSecondRelation+2)); + CoefficientType lb = storm::utility::regions::convertNumber(parameterBoundsString.substr(0,positionOfFirstRelation)); + CoefficientType ub = storm::utility::regions::convertNumber(parameterBoundsString.substr(positionOfSecondRelation+2)); lowerBounds.emplace(std::make_pair(var, lb)); upperBounds.emplace(std::make_pair(var, ub)); } @@ -202,9 +219,11 @@ namespace storm { std::vector parameterBounds; boost::split(parameterBounds, regionString, boost::is_any_of(",")); for(auto const& parameterBound : parameterBounds){ - parseParameterBounds(lowerBounds, upperBounds, parameterBound); + if(!std::all_of(parameterBound.begin(),parameterBound.end(), ::isspace)){ //skip this string if it only consists of space + parseParameterBounds(lowerBounds, upperBounds, parameterBound); + } } - return ParameterRegion(lowerBounds, upperBounds); + return ParameterRegion(std::move(lowerBounds), std::move(upperBounds)); } template @@ -215,7 +234,7 @@ namespace storm { boost::split(regionsStrVec, regionsString, boost::is_any_of(";")); for(auto const& regionStr : regionsStrVec){ if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space - result.emplace_back(parseRegion(regionStr)); + result.emplace_back(parseRegion(regionStr)); } } return result; diff --git a/src/modelchecker/region/ParameterRegion.h b/src/modelchecker/region/ParameterRegion.h index a7b0dd7e6..0f035b15b 100644 --- a/src/modelchecker/region/ParameterRegion.h +++ b/src/modelchecker/region/ParameterRegion.h @@ -22,7 +22,8 @@ namespace storm { typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - ParameterRegion(std::map lowerBounds, std::map upperBounds); + ParameterRegion(std::map const& lowerBounds, std::map const& upperBounds); + ParameterRegion(std::map&& lowerBounds, std::map&& upperBounds); virtual ~ParameterRegion(); std::set getVariables() const; @@ -31,7 +32,7 @@ namespace storm { const std::map getUpperBounds() const; const std::map getLowerBounds() const; - /* + /*! * Returns a vector of all possible combinations of lower and upper bounds of the given variables. * The first entry of the returned vector will map every variable to its lower bound * The second entry will map every variable to its lower bound, except the first one (i.e. *getVariables.begin()) @@ -41,6 +42,11 @@ namespace storm { * If the given set of variables is empty, the returned vector will contain an empty map */ std::vector> getVerticesOfRegion(std::set const& consideredVariables) const; + + /*! + * Returns some point that lies within this region + */ + std::map getSomePoint() const; RegionCheckResult getCheckResult() const; void setCheckResult(RegionCheckResult checkResult); @@ -110,7 +116,9 @@ namespace storm { static std::vector getRegionsFromSettings(); private: - + + void init(); + std::map const lowerBounds; std::map const upperBounds; std::set variables; diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index b34ab459b..ef7dd1aac 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -53,7 +53,7 @@ namespace storm { for(std::size_t const& tableIndex : matrixEntryToEvalTableMapping){ STORM_LOG_THROW(sampleModelEntry->getColumn()==parModelEntry->getColumn(), storm::exceptions::UnexpectedException, "The entries of the given parametric model and the constructed sampling model do not match"); if(tableIndex == constantEntryIndex){ - sampleModelEntry->setValue(storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parModelEntry->getValue()))); + sampleModelEntry->setValue(storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parModelEntry->getValue()))); } else { this->probabilityMapping.emplace_back(std::make_pair(&(this->probabilityEvaluationTable[tableIndex].second), sampleModelEntry)); } @@ -110,7 +110,7 @@ namespace storm { std::size_t numOfNonConstEntries=0; for(std::size_t state=0; stateparametricTypeComparator.isConstant(parametricModel.getStateRewardVector()[state])){ - stateRewardsAsVector[state] = storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state])); + stateRewardsAsVector[state] = storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state])); rewardEntryToEvalTableMapping.emplace_back(constantEntryIndex); } else { ++numOfNonConstEntries; @@ -137,11 +137,11 @@ namespace storm { void SparseDtmcRegionModelChecker::SamplingModel::instantiate(std::mapconst& point) { //write entries into evaluation tables for(auto& tableEntry : this->probabilityEvaluationTable){ - tableEntry.second=storm::utility::regions::convertNumber( + tableEntry.second=storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction(tableEntry.first, point)); } for(auto& tableEntry : this->rewardEvaluationTable){ - tableEntry.second=storm::utility::regions::convertNumber( + tableEntry.second=storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction(tableEntry.first, point)); } diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 9182cb4ef..007a5149c 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -86,11 +86,11 @@ namespace storm { // set some information regarding the formula and model. Also computes a more simple version of the model preprocess(); if(!this->isResultConstant){ - //now create the model used for Approximation + //now create the model used for Approximation (if required) if(storm::settings::regionSettings().doApprox()){ initializeApproximationModel(*this->simpleModel, this->simpleFormula); } - //now create the model used for Sampling + //now create the model used for Sampling (if required) if(storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || (!storm::settings::regionSettings().doSample() && storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ initializeSamplingModel(*this->simpleModel, this->simpleFormula); @@ -100,6 +100,11 @@ namespace storm { (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ computeReachabilityFunction(*this->simpleModel); } + } else { + //for a constant result we just compute the reachability function + if(this->reachabilityFunction==nullptr){ + computeReachabilityFunction(*this->simpleModel); + } } //some information for statistics... std::chrono::high_resolution_clock::time_point timeSpecifyFormulaEnd = std::chrono::high_resolution_clock::now(); @@ -474,7 +479,25 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionEnd = std::chrono::high_resolution_clock::now(); this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart; } + + template + void SparseDtmcRegionModelChecker::checkRegions(std::vector& regions) { + STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); + std::cout << "Checking " << regions.size() << " regions. Progress: "; + std::cout.flush(); + uint_fast64_t progress=0; + uint_fast64_t checkedRegions=0; + for(auto& region : regions){ + checkRegion(region); + if((checkedRegions++)*10/regions.size()==progress){ + std::cout << progress++; + std::cout.flush(); + } + } + std::cout << " done!" << std::endl; + } + template void SparseDtmcRegionModelChecker::checkRegion(ParameterRegion& region) { std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now(); @@ -494,7 +517,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(this->parametricTypeComparator.isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); - if(valueIsInBoundOfFormula(storm::utility::regions::getConstantPart(*getReachabilityFunction()))){ + if(valueIsInBoundOfFormula(this->getReachabilityValue(region.getSomePoint(), true))){ region.setCheckResult(RegionCheckResult::ALLSAT); } else{ @@ -558,24 +581,6 @@ namespace storm { break; } } - - template - void SparseDtmcRegionModelChecker::checkRegions(std::vector& regions) { - STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); - std::cout << "Checking " << regions.size() << " regions. Progress: "; - std::cout.flush(); - - uint_fast64_t progress=0; - uint_fast64_t checkedRegions=0; - for(auto& region : regions){ - checkRegion(region); - if((checkedRegions++)*10/regions.size()==progress){ - std::cout << progress++; - std::cout.flush(); - } - } - std::cout << " done!" << std::endl; - } template bool SparseDtmcRegionModelChecker::checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { @@ -595,7 +600,7 @@ namespace storm { switch(storm::settings::regionSettings().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.getLowerBounds(), false); + checkPoint(region,region.getSomePoint(), false); proveAllSat= (region.getCheckResult()==RegionCheckResult::EXISTSSAT); break; case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLSAT: @@ -701,11 +706,12 @@ namespace storm { bool valueInBoundOfFormula; if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || (!storm::settings::regionSettings().doSample() && favorViaFunction)){ - valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point)); + //evaluate the reachability function + valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue(point, true)); } else{ - getSamplingModel()->instantiate(point); - valueInBoundOfFormula=this->valueIsInBoundOfFormula(getSamplingModel()->computeValues()[*getSamplingModel()->getModel()->getInitialStates().begin()]); + //instantiate the sampling model + valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue(point, false)); } if(valueInBoundOfFormula){ @@ -748,13 +754,25 @@ namespace storm { } return this->reachabilityFunction; } + + template + template + ValueType SparseDtmcRegionModelChecker::getReachabilityValue(std::map const& point, bool evaluateFunction) { + if(evaluateFunction || this->isResultConstant){ + return storm::utility::regions::convertNumber(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point)); + } else { + getSamplingModel()->instantiate(point); + return storm::utility::regions::convertNumber(getSamplingModel()->computeValues()[*getSamplingModel()->getModel()->getInitialStates().begin()]); + } + } + template bool SparseDtmcRegionModelChecker::checkFullSmt(ParameterRegion& region) { STORM_LOG_THROW((storm::settings::regionSettings().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.getLowerBounds(), true); + checkPoint(region,region.getSomePoint(), true); } if(this->smtSolver==nullptr){ @@ -851,7 +869,7 @@ namespace storm { storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions.. this->smtSolver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); - ParametricType bound= storm::utility::regions::convertNumber(this->specifiedFormulaBound); + ParametricType bound= storm::utility::regions::convertNumber(this->specifiedFormulaBound); // To prove that the property is satisfied in the initial state for all parameters, // we ask the solver whether the negation of the property is satisfiable and invert the answer. @@ -897,9 +915,9 @@ namespace storm { template template - bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType value){ + bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType const& value){ STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified."); - double valueAsDouble = storm::utility::regions::convertNumber(value); + double valueAsDouble = storm::utility::regions::convertNumber(value); switch (this->specifiedFormulaCompType) { case storm::logic::ComparisonType::Greater: return (valueAsDouble > this->specifiedFormulaBound); @@ -913,7 +931,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); } } - + template void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index d07845113..1c9523292 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -54,25 +54,42 @@ namespace storm { void specifyFormula(std::shared_ptr formula); /*! - * Checks whether the given formula holds for all parameters that lie in the given region. + * Checks for every given region whether the specified formula holds for all parameters that lie in that region. * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.violatedPoint will be set. * * @note A formula has to be specified first. * * @param region The considered region - * */ - void checkRegion(ParameterRegion& region); + void checkRegions(std::vector& regions); /*! - * Checks for every given region whether the specified formula holds for all parameters that lie in that region. + * Checks whether the given formula holds for all parameters that lie in the given region. * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.violatedPoint will be set. * * @note A formula has to be specified first. * * @param region The considered region + * */ - void checkRegions(std::vector& regions); + void checkRegion(ParameterRegion& region); + + /*! + * Returns the reachability function. + * If it is not yet available, it is computed. + */ + std::shared_ptr const& getReachabilityFunction(); + + /*! + * Returns the reachability Value at the specified point. + * The given flag decides whether to initialize a sampling model or to evaluate a reachability function. + * Might invoke sampling model initialization or the computation of the reachability function (if these are not available yet) + * + * @param point The point (i.e. parameter evaluation) at which to compute the reachability value. + * @param evaluateFunction If set, the reachability function is evaluated. Otherwise, the sampling model is instantiated. + */ + template + ValueType getReachabilityValue(std::mapconst& point, bool evaluateFunction=false); /*! * Prints statistical information to the given stream. @@ -192,12 +209,6 @@ namespace storm { */ std::shared_ptr const& getSamplingModel(); - /*! - * Returns the reachability function. - * If it is not yet available, it is computed. - */ - std::shared_ptr const& getReachabilityFunction(); - /*! * Starts the SMTSolver to get the result. * The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED. @@ -215,7 +226,7 @@ namespace storm { * Returns true iff the given value satisfies the bound given by the specified property */ template - bool valueIsInBoundOfFormula(ValueType value); + bool valueIsInBoundOfFormula(ValueType const& value); // The model this model checker is supposed to analyze. storm::models::sparse::Dtmc const& model; diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 131edcfb5..c3fc777b8 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -545,6 +545,10 @@ namespace storm { storm::settings::modules::RegionSettings const& regionSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::RegionSettings::moduleName)); } + + storm::settings::modules::RegionSettings& mutableRegionSettings() { + return dynamic_cast(storm::settings::SettingsManager::manager().getModule(storm::settings::modules::RegionSettings::moduleName)); + } storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName)); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 7751b890e..703fa0110 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -331,6 +331,14 @@ namespace storm { * @return An object that allows accessing the settings for parametric region model checking. */ storm::settings::modules::RegionSettings const& regionSettings(); + + /*! + * Retrieves the settings for parametric region model checking. + * + * @return An object that allows accessing and writing the settings for parametric region model checking. + */ + storm::settings::modules::RegionSettings& mutableRegionSettings(); + /* Retrieves the settings of the elimination-based DTMC model checker. * diff --git a/src/settings/modules/RegionSettings.cpp b/src/settings/modules/RegionSettings.cpp index 633754132..2f15e15c1 100644 --- a/src/settings/modules/RegionSettings.cpp +++ b/src/settings/modules/RegionSettings.cpp @@ -18,23 +18,23 @@ namespace storm { const std::string RegionSettings::samplemodeOptionName = "samplemode"; const std::string RegionSettings::smtmodeOptionName = "smtmode"; - RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName), modesModified(false) { 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()); this->addOption(storm::settings::OptionBuilder(moduleName, regionsOptionName, true, "Specifies the regions via command line. 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("regions", "The considered regions.").build()).build()); - std::vector approxModes = {"off", "guessallsat", "guessallviolated", "testfirst"}; + std::vector approxModes = {"off", "testfirst", "guessallsat", "guessallviolated"}; this->addOption(storm::settings::OptionBuilder(moduleName, approxmodeOptionName, true, "Sets whether approximation should be done and whether lower or upper bounds are computed first.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, guessallsat, guessallviolated, testfirst). E.g. guessallsat will first try to prove ALLSAT") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, testfirst (default), guessallsat, guessallviolated). E.g. guessallsat will first try to prove ALLSAT") .addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(approxModes)).setDefaultValueString("testfirst").build()).build()); std::vector sampleModes = {"off", "instantiate", "evaluate"}; this->addOption(storm::settings::OptionBuilder(moduleName, samplemodeOptionName, true, "Sets whether sampling should be done and whether to instantiate a model or compute+evaluate a function.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, instantiate, evaluate)") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, instantiate (default), evaluate)") .addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(sampleModes)).setDefaultValueString("instantiate").build()).build()); std::vector smtModes = {"off", "function", "model"}; this->addOption(storm::settings::OptionBuilder(moduleName, smtmodeOptionName, true, "Sets whether SMT solving should be done and whether to encode it via a function or the model.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function, model)") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function (default), model)") .addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtModes)).setDefaultValueString("off").build()).build()); } @@ -55,6 +55,9 @@ 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; @@ -78,6 +81,9 @@ namespace storm { } 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; @@ -98,6 +104,9 @@ namespace storm { } 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; @@ -112,10 +121,21 @@ 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::check() const{ if(isRegionsSet() && isRegionFileSet()){ diff --git a/src/settings/modules/RegionSettings.h b/src/settings/modules/RegionSettings.h index 863794370..98368585c 100644 --- a/src/settings/modules/RegionSettings.h +++ b/src/settings/modules/RegionSettings.h @@ -13,7 +13,7 @@ namespace storm { class RegionSettings : public ModuleSettings { public: - enum class ApproxMode {OFF, GUESSALLSAT, GUESSALLVIOLATED, TESTFIRST }; + enum class ApproxMode {OFF, TESTFIRST, GUESSALLSAT, GUESSALLVIOLATED }; enum class SampleMode {OFF, INSTANTIATE, EVALUATE }; enum class SmtMode {OFF, FUNCTION, MODEL }; @@ -76,6 +76,19 @@ namespace storm { */ 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 check() const override; const static std::string moduleName; @@ -86,6 +99,11 @@ namespace storm { const static std::string approxmodeOptionName; const static std::string samplemodeOptionName; const static std::string smtmodeOptionName; + + bool modesModified; + ApproxMode approxMode; + SampleMode sampleMode; + SmtMode smtMode; }; } // namespace modules diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index 92a072ad3..868e62b8f 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -29,23 +29,28 @@ namespace storm { } template<> - double convertNumber(std::string const& number){ + double&& convertNumber(double&& number){ + return std::move(number); + } + + template<> + double convertNumber(std::string const& number){ return std::stod(number); } #ifdef STORM_HAVE_CARL template<> - storm::RationalNumber convertNumber(double const& number){ + storm::RationalNumber convertNumber(double const& number){ return carl::rationalize(number); } template<> - storm::RationalFunction convertNumber(double const& number){ - return storm::RationalFunction(convertNumber(number)); + storm::RationalFunction convertNumber(double const& number){ + return storm::RationalFunction(convertNumber(number)); } template<> - double convertNumber(storm::RationalNumber const& number){ + double convertNumber(storm::RationalNumber const& number){ return carl::toDouble(number); } @@ -55,11 +60,15 @@ namespace storm { } template<> - storm::RationalNumber convertNumber(std::string const& number){ + storm::RationalNumber&& convertNumber(storm::RationalNumber&& number){ + return std::move(number); + } + + template<> + storm::RationalNumber convertNumber(std::string const& number){ //We parse the number as double and then convert it to a a rational number. - return convertNumber(convertNumber(number)); + return convertNumber(convertNumber(number)); } - template<> storm::Variable getVariableFromString(std::string variableString){ diff --git a/src/utility/regions.h b/src/utility/regions.h index 33713aaa3..7547f47b6 100644 --- a/src/utility/regions.h +++ b/src/utility/regions.h @@ -52,9 +52,16 @@ namespace storm { * Converts a number from one type to a number from the other. * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings. */ - template + template TargetType convertNumber(SourceType const& number); + /* + * Converts a number from one type to a number from the other. + * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings. + */ + template + ValueType&& convertNumber(ValueType&& number); + /* * retrieves the variable object from the given string * Throws an exception if variable not found diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp new file mode 100644 index 000000000..74ccef2d1 --- /dev/null +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -0,0 +1,468 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_CARL + +#include "src/adapters/CarlAdapter.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/RegionSettings.h" + +#include "src/models/sparse/Dtmc.h" +#include "src/parser/PrismParser.h" +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/models/ModelBase.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/Dtmc.h" +#include "builder/ExplicitPrismModelBuilder.h" +#include "modelchecker/region/SparseDtmcRegionModelChecker.h" +#include "modelchecker/region/ParameterRegion.h" + +TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp/brp_16_2.pm"; + std::string const& formulaAsString = "P<=0.85 [F \"target\" ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + bool const buildRewards = false; + std::string const& rewardModelName = ""; + + //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()); + boost::optional> formula = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.buildRewards = buildRewards; + if (buildRewards) options.rewardModelName = rewardModelName; + 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(*formula.get())); + modelchecker.specifyFormula(formula.get()); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); + auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); + auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + + EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + + //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()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.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("0.7<=pL<=0.9,0.75<=pK<=0.95"); + auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); + auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::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::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()); + modelchecker.checkRegion(exBothRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); + modelchecker.checkRegion(allVioRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + +TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_16_2.pm"; + std::string const& formulaAsString = "R>2.5 [F \"target\" ]"; + std::string const& constantsAsString = "pL=0.9,TOAck=0.5"; + bool const buildRewards = true; + std::string const& rewardModelName = ""; + + //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()); + boost::optional> formula = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.buildRewards = buildRewards; + if (buildRewards) options.rewardModelName = rewardModelName; + 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(*formula.get())); + modelchecker.specifyFormula(formula.get()); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); + auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95"); + auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); + + EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue(exBothHardRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue(exBothHardRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue(exBothHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue(exBothHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + + //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()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(exBothHardRegion); + //At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can) + EXPECT_TRUE( + (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH)) || + (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSVIOLATED)) + ); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.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("0.7<=pK<=0.9,0.75<=TOMsg<=0.95"); + auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75"); + auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); + 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()); + modelchecker.checkRegion(exBothRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); + modelchecker.checkRegion(exBothHardRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult()); + modelchecker.checkRegion(allVioRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); + + //test smt + approx + auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); + ASSERT_TRUE(storm::settings::regionSettings().doApprox()); + ASSERT_TRUE(storm::settings::regionSettings().doSample()); + ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + modelchecker.checkRegion(exBothHardRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.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"; + std::string const& formulaAsString = "R>2.5 [F \"target\" ]"; + std::string const& constantsAsString = ""; //!! this model will have 4 parameters + bool const buildRewards = true; + std::string const& rewardModelName = ""; + + //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()); + boost::optional> formula = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.buildRewards = buildRewards; + if (buildRewards) options.rewardModelName = rewardModelName; + 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(*formula.get())); + modelchecker.specifyFormula(formula.get()); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9"); + auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); + auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); + + EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + + //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()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.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("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9"); + auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); + auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); + 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()); + modelchecker.checkRegion(exBothRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); + modelchecker.checkRegion(allVioRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + +TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/crowds/crowds_3-5.pm"; + std::string const& formulaAsString = "P<0.5 [F \"observe0Greater1\" ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + bool const buildRewards = false; + std::string const& rewardModelName = ""; + + //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()); + boost::optional> formula = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.buildRewards = buildRewards; + if (buildRewards) options.rewardModelName = rewardModelName; + 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(*formula.get())); + modelchecker.specifyFormula(formula.get()); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); + auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); + auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); + auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + + EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue(allVioHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue(allVioHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + + //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()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + modelchecker.checkRegion(allVioHardRegion); + //At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can) + EXPECT_TRUE( + (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED)) || + (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSVIOLATED)) + ); + + //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("0.1<=PF<=0.75,0.15<=badC<=0.2"); + auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); + auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); + auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + 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()); + modelchecker.checkRegion(exBothRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); + modelchecker.checkRegion(allVioRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); + modelchecker.checkRegion(allVioHardRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult()); + + //test smt + approx + auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); + ASSERT_TRUE(storm::settings::regionSettings().doApprox()); + ASSERT_TRUE(storm::settings::regionSettings().doSample()); + ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + modelchecker.checkRegion(allVioHardRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + +TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/crowds/crowds_3-5.pm"; + std::string const& formulaAsString = "P>0.75 [F \"observe0Greater1\" ]"; + std::string const& constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5 + bool const buildRewards = false; + std::string const& rewardModelName = ""; + + //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()); + boost::optional> formula = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.buildRewards = buildRewards; + if (buildRewards) options.rewardModelName = rewardModelName; + 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(*formula.get())); + modelchecker.specifyFormula(formula.get()); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.9<=PF<=0.99"); + auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.9"); + auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.01<=PF<=0.8"); + + EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model + EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + + //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()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.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("0.9<=PF<=0.99"); + auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.9"); + auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.01<=PF<=0.8"); + 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()); + modelchecker.checkRegion(exBothRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); + modelchecker.checkRegion(allVioRegionSmt); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + +TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/crowds/crowds_3-5.pm"; + std::string const& formulaAsString = "P>0.6 [F \"observe0Greater1\" ]"; + std::string const& constantsAsString = "PF=0.9,badC=0.2"; + bool const buildRewards = false; + std::string const& rewardModelName = ""; + + //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()); + boost::optional> formula = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.buildRewards = buildRewards; + if (buildRewards) options.rewardModelName = rewardModelName; + 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(*formula.get())); + modelchecker.specifyFormula(formula.get()); + + //start testing + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + + EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function + EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + + //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(); +} + +#endif \ No newline at end of file diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp index 5051bb659..660a8ad7d 100644 --- a/test/functional/storm-functional-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -61,6 +61,9 @@ int main(int argc, char* argv[]) { #ifndef STORM_HAVE_INTELTBB untestedModules.push_back("Intel TBB"); #endif +#ifndef STORM_HAVE_CARL + untestedModules.push_back("Carl"); +#endif if (result == 0) { if (untestedModules.empty()) {