sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added a couple of settings that replace hardcoded switches 

Former-commit-id: 3d399c9bf3
tempestpy_adaptions
TimQu 9 years ago
parent
1a0bf89671
commit
511284cd5b
5 changed files with 244 additions and 104 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/modelchecker/region/SamplingModel.cpp
  2. 197
      src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  3. 22
      src/modelchecker/region/SparseDtmcRegionModelChecker.h
  4. 86
      src/settings/modules/RegionSettings.cpp
  5. 41
      src/settings/modules/RegionSettings.h

2
src/modelchecker/region/SamplingModel.cpp
View File

@ -91,7 +91,7 @@ namespace storm {
storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr);
storm::modelchecker::SparseDtmcPrctlModelChecker<ConstantType> modelChecker(*this->model); storm::modelchecker::SparseDtmcPrctlModelChecker<ConstantType> modelChecker(*this->model);
//perform model checking on the mdp
//perform model checking on the dtmc
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula); std::unique_ptr<storm::modelchecker::CheckResult> resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula);
return resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector(); return resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
} }

197
src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
View File

@ -16,6 +16,8 @@
#include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidPropertyException.h"
#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/UnexpectedException.h" #include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm { namespace storm {
@ -29,6 +31,11 @@ namespace storm {
//intentionally left empty //intentionally left empty
} }
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::~SparseDtmcRegionModelChecker(){
//intentionally left empty
}
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::canHandle(storm::logic::Formula const& formula) const { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::canHandle(storm::logic::Formula const& formula) const {
//for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ])
@ -65,6 +72,8 @@ namespace storm {
this->isReachProbFunctionComputed=false; this->isReachProbFunctionComputed=false;
this->isResultConstant=false; this->isResultConstant=false;
this->smtSolver=nullptr; this->smtSolver=nullptr;
this->approximationModel=nullptr;
this->samplingModel=nullptr;
//Get subformula, target states //Get subformula, target states
//Note: canHandle already ensures that the formula has the right shape and that the model has a single initial state. //Note: canHandle already ensures that the formula has the right shape and that the model has a single initial state.
@ -75,18 +84,31 @@ namespace storm {
// get a more simple model with a single target state, a single sink state and where states with constant outgoing transitions have been removed // get a more simple model with a single target state, a single sink state and where states with constant outgoing transitions have been removed
// Note: also checks for linear functions and a constant result // Note: also checks for linear functions and a constant result
std::chrono::high_resolution_clock::time_point timeComputeSimplifiedModelStart = std::chrono::high_resolution_clock::now();
computeSimplifiedModel(targetStates); computeSimplifiedModel(targetStates);
//now create the models used for sampling and approximation
this->samplingModel=std::make_shared<SamplingModel>(*this->simplifiedModel);
this->approximationModel=std::make_shared<ApproximationModel>(*this->simplifiedModel);
std::chrono::high_resolution_clock::time_point timeComputeSimplifiedModelEnd = std::chrono::high_resolution_clock::now();
//now create the model used for Approximation
std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now();
if(storm::settings::regionSettings().doApprox()){
this->approximationModel=std::make_shared<ApproximationModel>(*this->simplifiedModel);
}
std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now();
//now create the model used for Sampling
std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now();
if(storm::settings::regionSettings().doSample() || (storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
this->samplingModel=std::make_shared<SamplingModel>(*this->simplifiedModel);
}
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now();
//some information for statistics... //some information for statistics...
std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart; this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart;
this->timeComputeSimplifiedModel = timeComputeSimplifiedModelEnd - timeComputeSimplifiedModelStart;
this->timeInitSamplingModel = timeInitSamplingModelEnd - timeInitSamplingModelStart;
this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart;
this->numOfCheckedRegions=0; this->numOfCheckedRegions=0;
this->numOfRegionsSolvedThroughSampling=0; this->numOfRegionsSolvedThroughSampling=0;
this->numOfRegionsSolvedThroughApproximation=0; this->numOfRegionsSolvedThroughApproximation=0;
this->numOfRegionsSolvedThroughSubsystemSmt=0;
this->numOfRegionsSolvedThroughFullSmt=0; this->numOfRegionsSolvedThroughFullSmt=0;
this->numOfRegionsExistsBoth=0; this->numOfRegionsExistsBoth=0;
this->numOfRegionsAllSat=0; this->numOfRegionsAllSat=0;
@ -95,7 +117,6 @@ namespace storm {
this->timeSampling=std::chrono::high_resolution_clock::duration::zero(); this->timeSampling=std::chrono::high_resolution_clock::duration::zero();
this->timeApproximation=std::chrono::high_resolution_clock::duration::zero(); this->timeApproximation=std::chrono::high_resolution_clock::duration::zero();
this->timeMDPBuild=std::chrono::high_resolution_clock::duration::zero(); this->timeMDPBuild=std::chrono::high_resolution_clock::duration::zero();
this->timeSubsystemSmt=std::chrono::high_resolution_clock::duration::zero();
this->timeFullSmt=std::chrono::high_resolution_clock::duration::zero(); this->timeFullSmt=std::chrono::high_resolution_clock::duration::zero();
} }
@ -128,7 +149,6 @@ namespace storm {
// eliminate all states with only constant outgoing transitions // eliminate all states with only constant outgoing transitions
//TODO: maybe also states with constant incoming tranistions. THEN the ordering of the eliminated states does matter. //TODO: maybe also states with constant incoming tranistions. THEN the ordering of the eliminated states does matter.
std::chrono::high_resolution_clock::time_point timeInitialStateEliminationStart = std::chrono::high_resolution_clock::now();
// Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
auto flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix); auto flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix);
auto flexibleBackwardTransitions= this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix.transpose(), true); auto flexibleBackwardTransitions= this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix.transpose(), true);
@ -159,8 +179,6 @@ namespace storm {
} }
} }
subsystem.set(initialState, true); subsystem.set(initialState, true);
std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now();
this->timeInitialStateElimination = timeInitialStateEliminationEnd-timeInitialStateEliminationStart;
STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl); STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl);
std::cout << "Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl; std::cout << "Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl;
@ -240,10 +258,10 @@ namespace storm {
//switches for the different steps. //switches for the different steps.
bool done=false; bool done=false;
bool doApproximation=this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions
bool doSampling=true;
bool doSubsystemSmt=false; //this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions
bool doFullSmt=true;
STORM_LOG_WARN_COND( (!storm::settings::regionSettings().doApprox() || this->hasOnlyLinearFunctions), "the approximation is only correct if the model has only linear functions. As this is not the case, approximation is deactivated");
bool doApproximation=storm::settings::regionSettings().doApprox() && this->hasOnlyLinearFunctions;
bool doSampling=storm::settings::regionSettings().doSample();
bool doFullSmt=storm::settings::regionSettings().doSmt();
if(!done && this->isResultConstant){ 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_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none.");
@ -262,10 +280,6 @@ namespace storm {
std::vector<ConstantType> upperBounds; std::vector<ConstantType> upperBounds;
if(!done && doApproximation){ if(!done && doApproximation){
STORM_LOG_DEBUG("Checking approximative probabilities..."); STORM_LOG_DEBUG("Checking approximative probabilities...");
if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
//Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED
checkPoint(region,region.getLowerBounds(), false);
}
if(checkApproximativeProbabilities(region, lowerBounds, upperBounds)){ if(checkApproximativeProbabilities(region, lowerBounds, upperBounds)){
++this->numOfRegionsSolvedThroughApproximation; ++this->numOfRegionsSolvedThroughApproximation;
STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through approximation."); STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through approximation.");
@ -285,12 +299,6 @@ namespace storm {
} }
std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point timeSubsystemSmtStart = std::chrono::high_resolution_clock::now();
if(!done && doSubsystemSmt){
STORM_LOG_WARN("SubsystemSmt approach not yet implemented");
}
std::chrono::high_resolution_clock::time_point timeSubsystemSmtEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point timeFullSmtStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeFullSmtStart = std::chrono::high_resolution_clock::now();
if(!done && doFullSmt){ if(!done && doFullSmt){
STORM_LOG_DEBUG("Checking with Smt Solving..."); STORM_LOG_DEBUG("Checking with Smt Solving...");
@ -307,7 +315,6 @@ namespace storm {
this->timeCheckRegion += timeCheckRegionEnd-timeCheckRegionStart; this->timeCheckRegion += timeCheckRegionEnd-timeCheckRegionStart;
this->timeSampling += timeSamplingEnd - timeSamplingStart; this->timeSampling += timeSamplingEnd - timeSamplingStart;
this->timeApproximation += timeApproximationEnd - timeApproximationStart; this->timeApproximation += timeApproximationEnd - timeApproximationStart;
this->timeSubsystemSmt += timeSubsystemSmtEnd - timeSubsystemSmtStart;
this->timeFullSmt += timeFullSmtEnd - timeFullSmtStart; this->timeFullSmt += timeFullSmtEnd - timeFullSmtStart;
switch(region.getCheckResult()){ switch(region.getCheckResult()){
case RegionCheckResult::EXISTSBOTH: case RegionCheckResult::EXISTSBOTH:
@ -346,81 +353,95 @@ namespace storm {
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkApproximativeProbabilities(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkApproximativeProbabilities(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) {
STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions."); STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions.");
std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now();
STORM_LOG_THROW(this->approximationModel!=nullptr, storm::exceptions::UnexpectedException, "Approximation model not initialized");
this->approximationModel->instantiate(region); this->approximationModel->instantiate(region);
std::chrono::high_resolution_clock::time_point timeMDPBuildEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeMDPBuildEnd = std::chrono::high_resolution_clock::now();
this->timeMDPBuild += timeMDPBuildEnd-timeMDPBuildStart; this->timeMDPBuild += timeMDPBuildEnd-timeMDPBuildStart;
// Decide whether we should minimize or maximize and whether to prove allsat or allviolated. (Hence, there are 4 cases)
// Decide whether the formula has an upper or a lower bond ({<, <=} or {>, >=}) and whether to prove allsat or allviolated. (Hence, there are 4 cases)
bool formulaHasUpperBound = this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::Less || this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::LessEqual; bool formulaHasUpperBound = this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::Less || this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::LessEqual;
STORM_LOG_THROW((formulaHasUpperBound != (this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::Greater || this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::GreaterEqual)), STORM_LOG_THROW((formulaHasUpperBound != (this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::Greater || this->probabilityOperatorFormula->getComparisonType()==storm::logic::ComparisonType::GreaterEqual)),
storm::exceptions::UnexpectedException, "Unexpected comparison Type of formula"); storm::exceptions::UnexpectedException, "Unexpected comparison Type of formula");
bool proveAllSat;
switch (region.getCheckResult()){ switch (region.getCheckResult()){
case RegionCheckResult::EXISTSSAT:
case RegionCheckResult::UNKNOWN: case RegionCheckResult::UNKNOWN:
//Try to prove ALLSAT
if(formulaHasUpperBound){
upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize);
lowerBounds=std::vector<ConstantType>();
if(valueIsInBoundOfFormula(upperBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLSAT);
return true;
}
}
else{
lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize);
upperBounds=std::vector<ConstantType>();
if(valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLSAT);
return true;
}
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);
proveAllSat= (region.getCheckResult()==RegionCheckResult::EXISTSSAT);
break;
case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLSAT:
proveAllSat=true;
break;
case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLVIOLATED:
proveAllSat=false;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The specified approxmode is not supported");
} }
break; break;
case RegionCheckResult::ALLSAT:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)");
//Intentionally no break;
case RegionCheckResult::EXISTSSAT:
proveAllSat=true;
break;
case RegionCheckResult::ALLVIOLATED:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)");
//Intentionally no break;
case RegionCheckResult::EXISTSVIOLATED: case RegionCheckResult::EXISTSVIOLATED:
//Try to prove ALLVIOLATED
if(formulaHasUpperBound){
lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize);
upperBounds=std::vector<ConstantType>();
if(!valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
return true;
}
}
else{
upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize);
lowerBounds=std::vector<ConstantType>();
if(!valueIsInBoundOfFormula(upperBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
return true;
}
}
proveAllSat=false;
break; break;
default: default:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative probabilities"); STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative probabilities");
} }
bool formulaSatisfied;
if((formulaHasUpperBound && proveAllSat) || (!formulaHasUpperBound && !proveAllSat)){
//these are the cases in which we need to compute upper bounds
upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize);
lowerBounds = std::vector<ConstantType>();
formulaSatisfied = valueIsInBoundOfFormula(upperBounds[*this->approximationModel->getModel()->getInitialStates().begin()]);
}
else{
//for the remaining cases we compute lower bounds
lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize);
upperBounds = std::vector<ConstantType>();
formulaSatisfied = valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()]);
}
//check if approximation was conclusive
if(proveAllSat && formulaSatisfied){
region.setCheckResult(RegionCheckResult::ALLSAT);
return true;
}
if(!proveAllSat && !formulaSatisfied){
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
return true;
}
if(region.getCheckResult()==RegionCheckResult::UNKNOWN){ if(region.getCheckResult()==RegionCheckResult::UNKNOWN){
//In this case, it makes sense to try the other optimality Type. Again, 4 cases (Although the ALLSAT cases should not be reachable, since we already tried to prove this above).
//In this case, it makes sense to try to prove the contrary statement
proveAllSat=!proveAllSat;
if(lowerBounds.empty()){ if(lowerBounds.empty()){
lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize); lowerBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Minimize);
if(!formulaHasUpperBound && valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLSAT);
return true;
}
if(formulaHasUpperBound && !valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
return true;
}
formulaSatisfied=valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()]);
} }
if(upperBounds.empty()){
else{
upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize); upperBounds = this->approximationModel->computeReachabilityProbabilities(storm::logic::OptimalityType::Maximize);
if(formulaHasUpperBound && valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLSAT);
return true;
}
if(!formulaHasUpperBound && !valueIsInBoundOfFormula(lowerBounds[*this->approximationModel->getModel()->getInitialStates().begin()])){
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
return true;
}
formulaSatisfied=valueIsInBoundOfFormula(upperBounds[*this->approximationModel->getModel()->getInitialStates().begin()]);
}
//check if approximation was conclusive
if(proveAllSat && formulaSatisfied){
region.setCheckResult(RegionCheckResult::ALLSAT);
return true;
}
if(!proveAllSat && !formulaSatisfied){
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
return true;
} }
} }
//if we reach this point than the result is still inconclusive. //if we reach this point than the result is still inconclusive.
@ -431,7 +452,7 @@ namespace storm {
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkSamplePoints(ParameterRegion& region) { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkSamplePoints(ParameterRegion& region) {
auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points
for (auto const& point : samplingPoints){ for (auto const& point : samplingPoints){
if(checkPoint(region, point, false)){
if(checkPoint(region, point)){
return true; return true;
} }
} }
@ -441,10 +462,12 @@ namespace storm {
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool viaReachProbFunction) { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool viaReachProbFunction) {
bool valueInBoundOfFormula; bool valueInBoundOfFormula;
if(viaReachProbFunction){
if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) ||
(!storm::settings::regionSettings().doSample() && viaReachProbFunction)){
valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(getReachProbFunction(), point)); valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(getReachProbFunction(), point));
} }
else{ else{
STORM_LOG_THROW(this->samplingModel!=nullptr, storm::exceptions::UnexpectedException, "Sampling model not initialized");
this->samplingModel->instantiate(point); this->samplingModel->instantiate(point);
valueInBoundOfFormula=this->valueIsInBoundOfFormula(this->samplingModel->computeReachabilityProbabilities()[*this->samplingModel->getModel()->getInitialStates().begin()]); valueInBoundOfFormula=this->valueIsInBoundOfFormula(this->samplingModel->computeReachabilityProbabilities()[*this->samplingModel->getModel()->getInitialStates().begin()]);
} }
@ -509,6 +532,7 @@ namespace storm {
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkFullSmt(ParameterRegion& region) { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::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){ if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
//Sampling needs to be done (on a single point) //Sampling needs to be done (on a single point)
checkPoint(region,region.getLowerBounds(), true); checkPoint(region,region.getLowerBounds(), true);
@ -680,7 +704,9 @@ namespace storm {
} }
std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timePreprocessing); std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timePreprocessing);
std::chrono::milliseconds timeInitialStateEliminationInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeInitialStateElimination);
std::chrono::milliseconds timeComputeSimplifiedModelInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeComputeSimplifiedModel);
std::chrono::milliseconds timeInitSamplingModelInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeInitSamplingModel);
std::chrono::milliseconds timeInitApproxModelInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeInitApproxModel);
std::chrono::milliseconds timeComputeReachProbFunctionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeComputeReachProbFunction); std::chrono::milliseconds timeComputeReachProbFunctionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeComputeReachProbFunction);
std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeCheckRegion); std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeCheckRegion);
std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSampling); std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSampling);
@ -706,21 +732,22 @@ namespace storm {
outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl; outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSubsystemSmt << " regions solved through SubsystemSmt" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl;
outstream << std::endl; outstream << std::endl;
outstream << "Running times:" << std::endl; outstream << "Running times:" << std::endl;
outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing)" << std::endl; outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing)" << std::endl;
outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl; outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl;
outstream << " " << timeInitialStateEliminationInMilliseconds.count() << "ms Initial state elimination of const transitions" << std::endl;
outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function" << std::endl;
outstream << " " << timeComputeSimplifiedModelInMilliseconds.count() << "ms to obtain a simplified model (state elimination of const transitions)" << std::endl;
outstream << " " << timeInitApproxModelInMilliseconds.count() << "ms to initialize the Approximation Model" << std::endl;
outstream << " " << timeInitSamplingModelInMilliseconds.count() << "ms to initialize the Sampling Model" << std::endl;
outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl;
outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl;
outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl;
outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl;
outstream << " " << timeMDPBuildInMilliseconds.count() << "ms to build the MDP" << std::endl; outstream << " " << timeMDPBuildInMilliseconds.count() << "ms to build the MDP" << std::endl;
outstream << " " << timeFullSmtInMilliseconds.count() << "ms Full Smt solving" << std::endl;
outstream << " " << timeFullSmtInMilliseconds.count() << "ms Smt solving" << std::endl;
outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function (already included in one of the above)" << std::endl;
outstream << "-----------------------------------------------" << std::endl; outstream << "-----------------------------------------------" << std::endl;
} }

22
src/modelchecker/region/SparseDtmcRegionModelChecker.h
View File

@ -33,6 +33,8 @@ namespace storm {
class ParameterRegion; class ParameterRegion;
explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model); explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model);
virtual ~SparseDtmcRegionModelChecker();
/*! /*!
* Checks if the given formula can be handled by This region model checker * Checks if the given formula can be handled by This region model checker
@ -117,12 +119,14 @@ namespace storm {
* May set the satPoint and violatedPoint of the regions if thy are not yet specified and such point is given. * May set the satPoint and violatedPoint of the regions if thy are not yet specified and such point is given.
* Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH * Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH
* *
* @param viaReachProbFunction if set, the sampling will be done via the reachProbFunction.
* Otherwise, the model will be instantiated and checked
* @param favorViaFunction if not stated otherwise (e.g. in the settings), the sampling will be done via the
* reachProbFunction if this flag is true. If the flag is false, sampling will be
* done via instantiation of the samplingmodel. Note that this argument is ignored,
* unless sampling has been turned of in the settings
* *
* @return true if an violated point as well as a sat point has been found, i.e., the check result is changed to EXISTSOTH * @return true if an violated point as well as a sat point has been found, i.e., the check result is changed to EXISTSOTH
*/ */
bool checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool viaReachProbFunction=false);
bool checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction=false);
/*! /*!
* Returns the reachability probability function. * Returns the reachability probability function.
@ -165,10 +169,10 @@ namespace storm {
std::unique_ptr<storm::logic::ProbabilityOperatorFormula> probabilityOperatorFormula; std::unique_ptr<storm::logic::ProbabilityOperatorFormula> probabilityOperatorFormula;
// the original model after states with constant transitions have been eliminated // the original model after states with constant transitions have been eliminated
std::shared_ptr<storm::models::sparse::Dtmc<ParametricType>> simplifiedModel; std::shared_ptr<storm::models::sparse::Dtmc<ParametricType>> simplifiedModel;
// the model that can be instantiated to check the value at a certain point
std::shared_ptr<SamplingModel> samplingModel;
// the model that is used to approximate the probability values // the model that is used to approximate the probability values
std::shared_ptr<ApproximationModel> approximationModel; std::shared_ptr<ApproximationModel> approximationModel;
// the model that can be instantiated to check the value at a certain point
std::shared_ptr<SamplingModel> samplingModel;
// The function for the reachability probability in the initial state // The function for the reachability probability in the initial state
ParametricType reachProbFunction; ParametricType reachProbFunction;
// a flag that is true if there are only linear functions at transitions of the model // a flag that is true if there are only linear functions at transitions of the model
@ -182,22 +186,22 @@ namespace storm {
// runtimes and other information for statistics. // runtimes and other information for statistics.
uint_fast64_t numOfCheckedRegions; uint_fast64_t numOfCheckedRegions;
uint_fast64_t numOfRegionsSolvedThroughSampling;
uint_fast64_t numOfRegionsSolvedThroughApproximation; uint_fast64_t numOfRegionsSolvedThroughApproximation;
uint_fast64_t numOfRegionsSolvedThroughSubsystemSmt;
uint_fast64_t numOfRegionsSolvedThroughSampling;
uint_fast64_t numOfRegionsSolvedThroughFullSmt; uint_fast64_t numOfRegionsSolvedThroughFullSmt;
uint_fast64_t numOfRegionsExistsBoth; uint_fast64_t numOfRegionsExistsBoth;
uint_fast64_t numOfRegionsAllSat; uint_fast64_t numOfRegionsAllSat;
uint_fast64_t numOfRegionsAllViolated; uint_fast64_t numOfRegionsAllViolated;
std::chrono::high_resolution_clock::duration timePreprocessing; std::chrono::high_resolution_clock::duration timePreprocessing;
std::chrono::high_resolution_clock::duration timeInitialStateElimination;
std::chrono::high_resolution_clock::duration timeComputeSimplifiedModel;
std::chrono::high_resolution_clock::duration timeInitApproxModel;
std::chrono::high_resolution_clock::duration timeInitSamplingModel;
std::chrono::high_resolution_clock::duration timeComputeReachProbFunction; std::chrono::high_resolution_clock::duration timeComputeReachProbFunction;
std::chrono::high_resolution_clock::duration timeCheckRegion; std::chrono::high_resolution_clock::duration timeCheckRegion;
std::chrono::high_resolution_clock::duration timeSampling; std::chrono::high_resolution_clock::duration timeSampling;
std::chrono::high_resolution_clock::duration timeApproximation; std::chrono::high_resolution_clock::duration timeApproximation;
std::chrono::high_resolution_clock::duration timeMDPBuild; std::chrono::high_resolution_clock::duration timeMDPBuild;
std::chrono::high_resolution_clock::duration timeSubsystemSmt;
std::chrono::high_resolution_clock::duration timeFullSmt; std::chrono::high_resolution_clock::duration timeFullSmt;
}; };

86
src/settings/modules/RegionSettings.cpp
View File

@ -1,6 +1,7 @@
#include "src/settings/modules/RegionSettings.h" #include "src/settings/modules/RegionSettings.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "exceptions/InvalidSettingsException.h"
namespace storm { namespace storm {
namespace settings { namespace settings {
@ -9,16 +10,30 @@ namespace storm {
const std::string RegionSettings::moduleName = "region"; const std::string RegionSettings::moduleName = "region";
const std::string RegionSettings::regionfileOptionName = "regionfile"; const std::string RegionSettings::regionfileOptionName = "regionfile";
const std::string RegionSettings::regionsOptionName = "regions"; const std::string RegionSettings::regionsOptionName = "regions";
const std::string RegionSettings::approxmodeOptionName = "approxmode";
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) {
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") 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.").build()).build());
.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'") 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());
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build());
std::vector<std::string> approxModes = {"off", "guessallsat", "guessallviolated", "testfirst"};
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")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(approxModes)).setDefaultValueString("guessallsat").build()).build());
std::vector<std::string> 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)")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(sampleModes)).setDefaultValueString("instantiate").build()).build());
std::vector<std::string> 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)")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtModes)).setDefaultValueString("off").build()).build());
} }
bool RegionSettings::isRegionFileSet() const{ bool RegionSettings::isRegionFileSet() const{
return this->getOption(regionfileOptionName).getHasOptionBeenSet(); return this->getOption(regionfileOptionName).getHasOptionBeenSet();
} }
@ -35,6 +50,69 @@ namespace storm {
return this->getOption(regionsOptionName).getArgumentByName("regions").getValueAsString(); return this->getOption(regionsOptionName).getArgumentByName("regions").getValueAsString();
} }
RegionSettings::ApproxMode RegionSettings::getApproxMode() const {
std::string modeString= this->getOption(approxmodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return ApproxMode::OFF;
}
if(modeString=="guessallsat"){
return ApproxMode::GUESSALLSAT;
}
if(modeString=="guessallviolated"){
return ApproxMode::GUESSALLVIOLATED;
}
if(modeString=="testfirst"){
return ApproxMode::TESTFIRST;
}
//if we reach this point, something went wrong
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The approx mode '" << modeString << "' is not valid");
return ApproxMode::OFF;
}
bool RegionSettings::doApprox() const {
return getApproxMode()!=ApproxMode::OFF;
}
RegionSettings::SampleMode RegionSettings::getSampleMode() const {
std::string modeString= this->getOption(samplemodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return SampleMode::OFF;
}
if(modeString=="instantiate"){
return SampleMode::INSTANTIATE;
}
if(modeString=="evaluate"){
return SampleMode::EVALUATE;
}
//if we reach this point, something went wrong
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The sample mode '" << modeString << "' is not valid");
return SampleMode::OFF;
}
bool RegionSettings::doSample() const {
return getSampleMode()!=SampleMode::OFF;
}
RegionSettings::SmtMode RegionSettings::getSmtMode() const {
std::string modeString= this->getOption(smtmodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return SmtMode::OFF;
}
if(modeString=="function"){
return SmtMode::FUNCTION;
}
if(modeString=="model"){
return SmtMode::MODEL;
}
//if we reach this point, something went wrong
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;
}
bool RegionSettings::check() const{ bool RegionSettings::check() const{
if(isRegionsSet() && isRegionFileSet()){ if(isRegionsSet() && isRegionFileSet()){
STORM_LOG_ERROR("Regions specified twice: via command line AND via file."); STORM_LOG_ERROR("Regions specified twice: via command line AND via file.");

41
src/settings/modules/RegionSettings.h
View File

@ -12,11 +12,10 @@ namespace storm {
*/ */
class RegionSettings : public ModuleSettings { class RegionSettings : public ModuleSettings {
public: public:
/**
* A type for saving the Solving Strategy.
*
*/
//enum class SolvingStrategy { ... };
enum class ApproxMode {OFF, GUESSALLSAT, GUESSALLVIOLATED, TESTFIRST };
enum class SampleMode {OFF, INSTANTIATE, EVALUATE };
enum class SmtMode {OFF, FUNCTION, MODEL };
/*! /*!
* Creates a new set of parametric region model checking settings that is managed by the given manager. * Creates a new set of parametric region model checking settings that is managed by the given manager.
@ -46,7 +45,36 @@ namespace storm {
* Returns the regions that are specified as cmd line parameter * Returns the regions that are specified as cmd line parameter
*/ */
std::string getRegionsFromCmdLine() const; std::string getRegionsFromCmdLine() const;
/*!
* Returns the mode in which approximation should be used
*/
ApproxMode getApproxMode() const;
/*!
* Returns whether to use approximation
*/
bool doApprox() const;
/*!
* Returns the mode in which Sampling should be used
*/
SampleMode getSampleMode() const;
/*!
* Returns whether to use Sampling
*/
bool doSample() const;
/*!
* Returns the mode in which SMT solving should be used
*/
SmtMode getSmtMode() const;
/*!
* Returns whether to use SMT Solving
*/
bool doSmt() const;
bool check() const override; bool check() const override;
@ -55,6 +83,9 @@ namespace storm {
private: private:
const static std::string regionfileOptionName; const static std::string regionfileOptionName;
const static std::string regionsOptionName; const static std::string regionsOptionName;
const static std::string approxmodeOptionName;
const static std::string samplemodeOptionName;
const static std::string smtmodeOptionName;
}; };
} // namespace modules } // namespace modules

Write Preview
Loading…
Cancel
Save