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

Splitted region modelchecker in abstract class and dtmc class (to easily add an mdp class soon) 

Former-commit-id: e722c8f2bd
main
TimQu 10 years ago
parent
0043d3ebf5
commit
70dd76c08b
17 changed files with 2579 additions and 2317 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  2. 390
      src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
  3. 239
      src/modelchecker/region/AbstractSparseRegionModelChecker.h
  4. 554
      src/modelchecker/region/ApproximationModel.cpp
  5. 279
      src/modelchecker/region/ApproximationModel.h
  6. 440
      src/modelchecker/region/ParameterRegion.cpp
  7. 229
      src/modelchecker/region/ParameterRegion.h
  8. 42
      src/modelchecker/region/RegionCheckResult.cpp
  9. 34
      src/modelchecker/region/RegionCheckResult.h
  10. 280
      src/modelchecker/region/SamplingModel.cpp
  11. 122
      src/modelchecker/region/SamplingModel.h
  12. 1555
      src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  13. 414
      src/modelchecker/region/SparseDtmcRegionModelChecker.h
  14. 2
      src/utility/region.h
  15. 4
      src/utility/regions.cpp
  16. 6
      src/utility/storm.h
  17. 298
      test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp

8
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -9,8 +9,10 @@
//forward declaration of friend class
namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
class SparseDtmcRegionModelChecker;
namespace region {
template<typename ParametricModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
}
}
}
@ -19,7 +21,7 @@ namespace storm {
template<typename SparseDtmcModelType>
class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker<SparseDtmcModelType> {
template<typename ParametricType, typename ConstantType> friend class storm::modelchecker::SparseDtmcRegionModelChecker;
template<typename ParametricModelType, typename ConstantType> friend class storm::modelchecker::region::SparseDtmcRegionModelChecker;
public:
typedef typename SparseDtmcModelType::ValueType ValueType;
typedef typename SparseDtmcModelType::RewardModelType RewardModelType;

390
src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
View File

@ -0,0 +1,390 @@
/*
* File: AbstractSparseRegionModelChecker.cpp
* Author: tim
*
* Created on September 9, 2015, 12:34 PM
*/
#include "AbstractSparseRegionModelChecker.h"
#include "src/adapters/CarlAdapter.h"
#include "src/modelchecker/region/RegionCheckResult.h"
#include "src/logic/Formulas.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/RegionSettings.h"
#include "src/utility/constants.h"
#include "src/utility/graph.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::AbstractSparseRegionModelChecker(ParametricSparseModelType const& model) :
model(model),
specifiedFormula(nullptr){
STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state.");
}
template<typename ParametricSparseModelType, typename ConstantType>
AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::~AbstractSparseRegionModelChecker() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
ParametricSparseModelType const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getModel() const {
return this->model;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::isResultConstant() const {
return this->resultConstant;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<ParametricSparseModelType> const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSimpleModel() const {
return this->simpleModel;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::isComputeRewards() const {
return computeRewards;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::logic::Formula> const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormula() const {
return specifiedFormula;
}
template<typename ParametricSparseModelType, typename ConstantType>
ConstantType const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaBound() const {
return specifiedFormulaBound;
}
template<typename ParametricSparseModelType, typename ConstantType>
storm::logic::ComparisonType const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaCompType() const {
return specifiedFormulaCompType;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifiedFormulaHasUpperBound() const {
return !storm::logic::isLowerBound(this->getSpecifiedFormulaCompType());
}
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifyFormula(std::shared_ptr<storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now();
STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled.");
//Initialize the context for this formula
this->specifiedFormula = formula;
this->resultConstant=false;
this->simpleFormula=nullptr;
this->isApproximationApplicable=false;
this->approximationModel=nullptr;
this->samplingModel=nullptr;
//stuff for statistics:
this->numOfCheckedRegions=0;
this->numOfRegionsSolvedThroughSampling=0;
this->numOfRegionsSolvedThroughApproximation=0;
this->numOfRegionsSolvedThroughSmt=0;
this->numOfRegionsExistsBoth=0;
this->numOfRegionsAllSat=0;
this->numOfRegionsAllViolated=0;
this->timeCheckRegion=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->timeSmt=std::chrono::high_resolution_clock::duration::zero();
this->timeApproxModelInstantiation=std::chrono::high_resolution_clock::duration::zero();
this->timeComputeReachabilityFunction=std::chrono::high_resolution_clock::duration::zero();
this->timeApproxModelInstantiation=std::chrono::high_resolution_clock::duration::zero();
// set some information regarding the formula.
if (this->getSpecifiedFormula()->isProbabilityOperatorFormula()) {
this->computeRewards = false;
this->specifiedFormulaCompType = this->getSpecifiedFormula()->asProbabilityOperatorFormula().getComparisonType();
this->specifiedFormulaBound = storm::utility::region::convertNumber<ConstantType>(this->getSpecifiedFormula()->asProbabilityOperatorFormula().getBound());
}
else if (this->getSpecifiedFormula()->isRewardOperatorFormula()) {
this->computeRewards=true;
this->specifiedFormulaCompType = this->getSpecifiedFormula()->asRewardOperatorFormula().getComparisonType();
this->specifiedFormulaBound = this->getSpecifiedFormula()->asRewardOperatorFormula().getBound();
}
else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The specified property " << this->getSpecifiedFormula() << "is not supported");
}
std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now();
this->preprocess(this->simpleModel, this->simpleFormula, isApproximationApplicable, resultConstant);
std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
//Check if the approximation and the sampling model needs to be computed
if(!this->isResultConstant()){
if(this->isApproximationApplicable && storm::settings::regionSettings().doApprox()){
initializeApproximationModel(*this->getSimpleModel(), this->simpleFormula);
}
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->getSimpleModel(), this->simpleFormula);
}
}
//some more information for statistics...
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaEnd = std::chrono::high_resolution_clock::now();
this->timeSpecifyFormula= timeSpecifyFormulaEnd - timeSpecifyFormulaStart;
this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart;
}
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now();
STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Approximation model requested but approximation is not applicable");
this->approximationModel=std::make_shared<ApproximationModel<ParametricSparseModelType, ConstantType>>(model, formula);
std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now();
this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart;
STORM_LOG_DEBUG("Initialized Approximation Model");
}
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now();
this->samplingModel=std::make_shared<SamplingModel<ParametricSparseModelType, ConstantType>>(model, formula);
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now();
this->timeInitSamplingModel = timeInitSamplingModelEnd - timeInitSamplingModelStart;
STORM_LOG_DEBUG("Initialized Sampling Model");
}
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegions(std::vector<ParameterRegion<ParametricType>>& 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){
this->checkRegion(region);
if((checkedRegions++)*10/regions.size()==progress){
std::cout << progress++;
std::cout.flush();
}
}
std::cout << " done!" << std::endl;
}
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegion(ParameterRegion<ParametricType>& region) {
std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now();
++this->numOfCheckedRegions;
STORM_LOG_THROW(this->getSpecifiedFormula()!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" );
STORM_LOG_DEBUG("Analyzing the region " << region.toString());
//std::cout << "Analyzing the region " << region.toString() << std::endl;
//switches for the different steps.
bool done=false;
STORM_LOG_WARN_COND( (!storm::settings::regionSettings().doApprox() || this->isApproximationApplicable), "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->isApproximationApplicable;
bool doSampling=storm::settings::regionSettings().doSample();
bool doSmt=storm::settings::regionSettings().doSmt();
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.");
if(this->valueIsInBoundOfFormula(this->getReachabilityValue(region.getSomePoint()))){
region.setCheckResult(RegionCheckResult::ALLSAT);
}
else{
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
}
done=true;
}
std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now();
std::vector<ConstantType> lowerBounds;
std::vector<ConstantType> upperBounds;
if(!done && doApproximation){
STORM_LOG_DEBUG("Checking approximative values...");
if(this->checkApproximativeValues(region, lowerBounds, upperBounds)){
++this->numOfRegionsSolvedThroughApproximation;
STORM_LOG_DEBUG("Result '" << region.getCheckResult() <<"' obtained through approximation.");
done=true;
}
}
std::chrono::high_resolution_clock::time_point timeApproximationEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point timeSamplingStart = std::chrono::high_resolution_clock::now();
if(!done && doSampling){
STORM_LOG_DEBUG("Checking sample points...");
if(this->checkSamplePoints(region)){
++this->numOfRegionsSolvedThroughSampling;
STORM_LOG_DEBUG("Result '" << region.getCheckResult() <<"' obtained through sampling.");
done=true;
}
}
std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point timeSmtStart = std::chrono::high_resolution_clock::now();
if(!done && doSmt){
STORM_LOG_DEBUG("Checking with Smt Solving...");
if(this->checkSmt(region)){
++this->numOfRegionsSolvedThroughSmt;
STORM_LOG_DEBUG("Result '" << region.getCheckResult() <<"' obtained through Smt Solving.");
done=true;
}
}
std::chrono::high_resolution_clock::time_point timeSmtEnd = std::chrono::high_resolution_clock::now();
//some information for statistics...
std::chrono::high_resolution_clock::time_point timeCheckRegionEnd = std::chrono::high_resolution_clock::now();
this->timeCheckRegion += timeCheckRegionEnd-timeCheckRegionStart;
this->timeSampling += timeSamplingEnd - timeSamplingStart;
this->timeApproximation += timeApproximationEnd - timeApproximationStart;
this->timeSmt += timeSmtEnd - timeSmtStart;
switch(region.getCheckResult()){
case RegionCheckResult::EXISTSBOTH:
++this->numOfRegionsExistsBoth;
break;
case RegionCheckResult::ALLSAT:
++this->numOfRegionsAllSat;
break;
case RegionCheckResult::ALLVIOLATED:
++this->numOfRegionsAllViolated;
break;
default:
break;
}
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<ApproximationModel<ParametricSparseModelType, ConstantType>> const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getApproximationModel() {
if(this->approximationModel==nullptr){
STORM_LOG_WARN("Approximation model requested but it has not been initialized when specifying the formula. Will initialize it now.");
initializeApproximationModel(*this->getSimpleModel(), this->simpleFormula);
}
return this->approximationModel;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSamplePoints(ParameterRegion<ParametricType>& region) {
auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points
for (auto const& point : samplingPoints){
if(checkPoint(region, point)){
return true;
}
}
return false;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<SamplingModel<ParametricSparseModelType, ConstantType>> const& AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSamplingModel() {
if(this->samplingModel==nullptr){
STORM_LOG_WARN("Sampling model requested but it has not been initialized when specifying the formula. Will initialize it now.");
initializeSamplingModel(*this->getSimpleModel(), this->simpleFormula);
}
return this->samplingModel;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(ConstantType const& value){
STORM_LOG_THROW(this->getSpecifiedFormula()!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified.");
switch (this->getSpecifiedFormulaCompType()) {
case storm::logic::ComparisonType::Greater:
return (value > this->getSpecifiedFormulaBound());
case storm::logic::ComparisonType::GreaterEqual:
return (value >= this->getSpecifiedFormulaBound());
case storm::logic::ComparisonType::Less:
return (value < this->getSpecifiedFormulaBound());
case storm::logic::ComparisonType::LessEqual:
return (value <= this->getSpecifiedFormulaBound());
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
}
}
template<typename ParametricSparseModelType, typename ConstantType>
bool AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(CoefficientType const& value){
return valueIsInBoundOfFormula(storm::utility::region::convertNumber<ConstantType>(value));
}
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::printStatisticsToStream(std::ostream& outstream) {
if(this->getSpecifiedFormula()==nullptr){
outstream << "Region Model Checker Statistics Error: No formula specified." << std::endl;
return;
}
std::chrono::milliseconds timeSpecifyFormulaInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSpecifyFormula);
std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timePreprocessing);
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 timeComputeReachabilityFunctionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeComputeReachabilityFunction);
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 timeApproximationInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeApproximation);
std::chrono::milliseconds timeApproxModelInstantiationInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeApproxModelInstantiation);
std::chrono::milliseconds timeSmtInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSmt);
std::chrono::high_resolution_clock::duration timeOverall = timeSpecifyFormula + timeCheckRegion; // + ...
std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(timeOverall);
uint_fast64_t numOfSolvedRegions= this->numOfRegionsExistsBoth + this->numOfRegionsAllSat + this->numOfRegionsAllViolated;
outstream << std::endl << "Region Model Checker Statistics:" << std::endl;
outstream << "-----------------------------------------------" << std::endl;
outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl;
outstream << "Formula: " << *this->getSpecifiedFormula() << std::endl;
if(this->isResultConstant()){
outstream << "The requested value is constant (i.e. independent of any parameters)" << std::endl;
}
else{
outstream << "Simple model: " << this->getSimpleModel()->getNumberOfStates() << " states, " << this->getSimpleModel()->getNumberOfTransitions() << " transitions" << std::endl;
}
outstream << "Approximation is " << (this->isApproximationApplicable ? "" : "not ") << "applicable" << std::endl;
outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl;
if(this->numOfCheckedRegions>0){
outstream << " Number of solved regions: " << numOfSolvedRegions << "(" << numOfSolvedRegions*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " AllSat: " << this->numOfRegionsAllSat << "(" << this->numOfRegionsAllSat*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " AllViolated: " << this->numOfRegionsAllViolated << "(" << this->numOfRegionsAllViolated*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 << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSmt << " regions solved through Smt" << std::endl;
outstream << std::endl;
}
outstream << "Running times:" << std::endl;
outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing, bisimulation (if applied))" << std::endl;
outstream << " " << timeSpecifyFormulaInMilliseconds.count() << "ms Initialization for the specified formula, including... " << std::endl;
outstream << " " << timePreprocessingInMilliseconds.count() << "ms for Preprocessing (mainly: state elimination of const transitions), including" << std::endl;
outstream << " " << timeComputeReachabilityFunctionInMilliseconds.count() << "ms to compute the reachability function" << 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 << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl;
outstream << " " << timeApproxModelInstantiationInMilliseconds.count() << "ms for instantiation of the approximation model" << std::endl;
outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl;
outstream << " " << timeSmtInMilliseconds.count() << "ms Smt solving" << std::endl;
outstream << "-----------------------------------------------" << std::endl;
}
#ifdef STORM_HAVE_CARL
template class AbstractSparseRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>, double>;
#endif
} // namespace region
} //namespace modelchecker
} //namespace storm

239
src/modelchecker/region/AbstractSparseRegionModelChecker.h
View File

@ -0,0 +1,239 @@
/*
* File: AbstractSparseRegionModelChecker.h
* Author: tim
*
* Created on September 9, 2015, 12:34 PM
*/
#ifndef STORM_MODELCHECKER_REGION_ABSTRACTSPARSEREGIONMODELCHECKER_H
#define STORM_MODELCHECKER_REGION_ABSTRACTSPARSEREGIONMODELCHECKER_H
#include <ostream>
#include "src/utility/region.h"
#include "src/modelchecker/region/ParameterRegion.h"
#include "src/modelchecker/region/ApproximationModel.h"
#include "src/modelchecker/region/SamplingModel.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/models/sparse/Model.h"
#include "src/models/sparse/Dtmc.h"
#include "src/logic/Formulas.h"
namespace storm {
namespace modelchecker{
namespace region{
template<typename ParametricSparseModelType, typename ConstantType>
class AbstractSparseRegionModelChecker {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
explicit AbstractSparseRegionModelChecker(ParametricSparseModelType const& model);
virtual ~AbstractSparseRegionModelChecker();
/*!
* Checks if the given formula can be handled by This region model checker
* @param formula the formula to be checked
*/
virtual bool canHandle(storm::logic::Formula const& formula) const = 0;
/*!
* Specifies the considered formula.
* A few preprocessing steps are performed.
* If another formula has been specified before, all 'context' regarding the old formula is lost.
*
* @param formula the formula to be considered.
*/
void specifyFormula(std::shared_ptr<storm::logic::Formula> formula);
/*!
* Checks for every given region whether the specified formula holds for all parameters that lie in that region.
* Sets the region checkresult accordingly.
* TODO: set region.satpoint and violated point correctly.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*/
void checkRegions(std::vector<ParameterRegion<ParametricType>>& regions);
/*!
* Checks whether the given formula holds for all parameters that lie in the given region.
* Sets the region checkresult accordingly.
* TODO: set region.satpoint and violated point correctly.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*
*/
void checkRegion(ParameterRegion<ParametricType>& region);
/*!
* Returns the reachability Value at the specified point by instantiating the sampling model.
*
* @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.
*/
virtual ConstantType getReachabilityValue(std::map<VariableType, CoefficientType>const& point, bool evaluateFunction=false) = 0;
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
bool valueIsInBoundOfFormula(ConstantType const& value);
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
bool valueIsInBoundOfFormula(CoefficientType const& value);
/*!
* Prints statistical information to the given stream.
*/
void printStatisticsToStream(std::ostream& outstream);
protected:
/*!
* returns the considered model
*/
ParametricSparseModelType const& getModel() const;
bool const& isResultConstant() const;
std::shared_ptr<ParametricSparseModelType> const& getSimpleModel() const;
bool const& isComputeRewards() const;
std::shared_ptr<storm::logic::Formula> const& getSpecifiedFormula() const;
ConstantType const& getSpecifiedFormulaBound() const;
storm::logic::ComparisonType const& getSpecifiedFormulaCompType() const;
bool specifiedFormulaHasUpperBound() const;
/*!
* Makes the required preprocessing steps for the specified model and formula
* Computes a simplified version of the model and formula that can be analyzed more efficiently.
* Also checks whether the approximation technique is applicable and whether the result is constant.
*
* @note this->specifiedFormula and this->computeRewards has to be set accordingly, before calling this function
*/
virtual void preprocess(std::shared_ptr<ParametricSparseModelType>& simpleModel, std::shared_ptr<storm::logic::Formula>& simpleFormula, bool& isApproximationApplicable, bool& isResultConstant) = 0;
/*!
* Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability (or reachability reward).
* If the current region result is EXISTSSAT (or EXISTSVIOLATED), then this function tries to prove ALLSAT (or ALLVIOLATED).
* If this succeeded, then the region check result is changed accordingly.
* If the current region result is UNKNOWN, then this function first tries to prove ALLSAT and if that failed, it tries to prove ALLVIOLATED.
* In any case, the computed bounds are written to the given lowerBounds/upperBounds.
* However, if only the lowerBounds (or upperBounds) have been computed, the other vector is set to a vector of size 0.
* True is returned iff either ALLSAT or ALLVIOLATED could be proved.
*/
virtual bool checkApproximativeValues(ParameterRegion<ParametricType>& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds)=0;
/*!
* Returns the approximation model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ApproximationModel<ParametricSparseModelType, ConstantType>> const& getApproximationModel();
/*!
* Checks the value of the function at some sampling points within the given region.
* May set the satPoint and violatedPoint of the regions if they are not yet specified and such points are found
* Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH
*
* @return true if an violated point as well as a sat point has been found during the process
*/
bool checkSamplePoints(ParameterRegion<ParametricType>& region);
/*!
* Checks the value of the function at the given sampling point.
* 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
*
* @param favorViaFunction if not stated otherwise (e.g. in the settings), the sampling will be done via the
* reachabilityFunction 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
*/
virtual bool checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction=false) = 0;
/*!
* Returns the sampling model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<SamplingModel<ParametricSparseModelType, ConstantType>> const& getSamplingModel();
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
* Otherwise, a sampingPoint will be computed.
* True is returned iff the solver was successful (i.e., it returned sat or unsat)
* A Sat- or Violated point is set, if the solver has found one (not yet implemented!).
* The region checkResult of the given region is changed accordingly.
*/
virtual bool checkSmt(ParameterRegion<ParametricType>& region)=0;
private:
/*!
* initializes the Approximation Model
*
* @note does not check whether approximation can be applied
*/
void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::Formula> formula);
/*!
* initializes the Sampling Model
*/
void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::Formula> formula);
// The model this model checker is supposed to analyze.
ParametricSparseModelType const& model;
//The currently specified formula
std::shared_ptr<storm::logic::Formula> specifiedFormula;
storm::logic::ComparisonType specifiedFormulaCompType;
ConstantType specifiedFormulaBound;
//A flag that is true iff we are interested in rewards
bool computeRewards;
// the original model after states with constant transitions have been eliminated
std::shared_ptr<ParametricSparseModelType> simpleModel;
// a formula that can be checked on the simplified model
std::shared_ptr<storm::logic::Formula> simpleFormula;
// a flag that is true if approximation is applicable, i.e., there are only linear functions at transitions of the model
bool isApproximationApplicable;
// the model that is used to approximate the reachability values
std::shared_ptr<ApproximationModel<ParametricSparseModelType, ConstantType>> approximationModel;
// the model that can be instantiated to check the value at a certain point
std::shared_ptr<SamplingModel<ParametricSparseModelType, ConstantType>> samplingModel;
// a flag that is true iff the resulting reachability function is constant
bool resultConstant;
// runtimes and other information for statistics.
uint_fast64_t numOfCheckedRegions;
uint_fast64_t numOfRegionsSolvedThroughApproximation;
uint_fast64_t numOfRegionsSolvedThroughSampling;
uint_fast64_t numOfRegionsSolvedThroughSmt;
uint_fast64_t numOfRegionsExistsBoth;
uint_fast64_t numOfRegionsAllSat;
uint_fast64_t numOfRegionsAllViolated;
std::chrono::high_resolution_clock::duration timeSpecifyFormula;
std::chrono::high_resolution_clock::duration timePreprocessing;
std::chrono::high_resolution_clock::duration timeInitApproxModel;
std::chrono::high_resolution_clock::duration timeInitSamplingModel;
std::chrono::high_resolution_clock::duration timeCheckRegion;
std::chrono::high_resolution_clock::duration timeSampling;
std::chrono::high_resolution_clock::duration timeApproximation;
std::chrono::high_resolution_clock::duration timeSmt;
protected:
std::chrono::high_resolution_clock::duration timeComputeReachabilityFunction;
std::chrono::high_resolution_clock::duration timeApproxModelInstantiation;
};
} //namespace region
} //namespace modelchecker
} //namespace storm
#endif /* STORM_MODELCHECKER_REGION_ABSTRACTSPARSEREGIONMODELCHECKER_H */

554
src/modelchecker/region/ApproximationModel.cpp
View File

@ -9,336 +9,338 @@
#include "src/modelchecker/region/ApproximationModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/macros.h"
#include "src/utility/region.h"
#include "src/utility/vector.h"
#include "src/utility/regions.h"
#include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
if(this->formula->isEventuallyFormula()){
this->computeRewards=false;
} else if(this->formula->isReachabilityRewardFormula()){
this->computeRewards=true;
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state rewards only");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Approximation model only supports eventually or reachability reward formulae.");
}
//Start with the probabilities
storm::storage::SparseMatrix<ConstantType> probabilityMatrix;
std::vector<std::size_t> rowSubstitutions;// the substitution used in every row (required if rewards are computed)
std::vector<ProbTableEntry*> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability-matrix entry
//for the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table.
//We can later transform this mapping into the desired mapping with iterators
ProbTableEntry constantProbEntry; //this value is stored in the matrixEntrytoEvalTableMapping for every constant probability matrix entry.
initializeProbabilities(parametricModel, probabilityMatrix, rowSubstitutions, matrixEntryToEvalTableMapping, &constantProbEntry);
//Now consider rewards
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ConstantType>> rewardModels;
std::vector<RewTableEntry*> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
RewTableEntry constantRewEntry; //this value is stored in the rewardEntryToEvalTableMapping for every constant reward vector entry.
if(this->computeRewards){
std::vector<ConstantType> stateActionRewards;
initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, &constantRewEntry);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(boost::optional<std::vector<ConstantType>>(), boost::optional<std::vector<ConstantType>>(std::move(stateActionRewards)))));
}
//Obtain other model ingredients and the approximation model itself
storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling());
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> noChoiceLabeling;
this->model=std::make_shared<storm::models::sparse::Mdp<ConstantType>>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling));
//translate the matrixEntryToEvalTableMapping into the actual probability mapping
typename storm::storage::SparseMatrix<ConstantType>::index_type matrixRow=0;
auto tableEntry=matrixEntryToEvalTableMapping.begin();
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
for (; matrixRow<this->model->getTransitionMatrix().getRowGroupIndices()[row+1]; ++matrixRow){
auto approxModelEntry = this->model->getTransitionMatrix().getRow(matrixRow).begin();
for(auto const& parEntry : parametricModel.getTransitionMatrix().getRow(row)){
if(*tableEntry == &constantProbEntry){
approxModelEntry->setValue(storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parEntry.getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry));
}
++approxModelEntry;
++tableEntry;
}
template<typename ParametricSparseModelType, typename ConstantType>
ApproximationModel<ParametricSparseModelType, ConstantType>::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
if(this->formula->isEventuallyFormula()){
this->computeRewards=false;
} else if(this->formula->isReachabilityRewardFormula()){
this->computeRewards=true;
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state rewards only");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Approximation model only supports eventually or reachability reward formulae.");
}
}
if(this->computeRewards){
//the same for rewards
auto approxModelRewardEntry = this->model->getUniqueRewardModel()->second.getStateActionRewardVector().begin();
for (auto tableEntry : rewardEntryToEvalTableMapping){
if(tableEntry != &constantRewEntry){
//insert pointer to minValue, pointer to maxValue, iterator to reward vector entry
this->rewardMapping.emplace_back(std::make_tuple(&(tableEntry->second.first), &(tableEntry->second.second), approxModelRewardEntry));
}
++approxModelRewardEntry;
//Start with the probabilities
storm::storage::SparseMatrix<ConstantType> probabilityMatrix;
std::vector<std::size_t> rowSubstitutions;// the substitution used in every row (required if rewards are computed)
std::vector<ProbTableEntry*> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability-matrix entry
//for the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table.
//We can later transform this mapping into the desired mapping with iterators
ProbTableEntry constantProbEntry; //this value is stored in the matrixEntrytoEvalTableMapping for every constant probability matrix entry.
initializeProbabilities(parametricModel, probabilityMatrix, rowSubstitutions, matrixEntryToEvalTableMapping, &constantProbEntry);
//Now consider rewards
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ConstantType>> rewardModels;
std::vector<RewTableEntry*> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
RewTableEntry constantRewEntry; //this value is stored in the rewardEntryToEvalTableMapping for every constant reward vector entry.
if(this->computeRewards){
std::vector<ConstantType> stateActionRewards;
initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, &constantRewEntry);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(boost::optional<std::vector<ConstantType>>(), boost::optional<std::vector<ConstantType>>(std::move(stateActionRewards)))));
}
//Get the sets of reward parameters that map to "CHOSEOPTIMAL".
this->choseOptimalRewardPars = std::vector<std::set<VariableType>>(this->rewardSubstitutions.size());
for(std::size_t index = 0; index<this->rewardSubstitutions.size(); ++index){
for(auto const& sub : this->rewardSubstitutions[index]){
if(sub.second==TypeOfBound::CHOSEOPTIMAL){
this->choseOptimalRewardPars[index].insert(sub.first);
//Obtain other model ingredients and the approximation model itself
storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling());
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> noChoiceLabeling;
this->model=std::make_shared<storm::models::sparse::Mdp<ConstantType>>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling));
//translate the matrixEntryToEvalTableMapping into the actual probability mapping
typename storm::storage::SparseMatrix<ConstantType>::index_type matrixRow=0;
auto tableEntry=matrixEntryToEvalTableMapping.begin();
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
for (; matrixRow<this->model->getTransitionMatrix().getRowGroupIndices()[row+1]; ++matrixRow){
auto approxModelEntry = this->model->getTransitionMatrix().getRow(matrixRow).begin();
for(auto const& parEntry : parametricModel.getTransitionMatrix().getRow(row)){
if(*tableEntry == &constantProbEntry){
approxModelEntry->setValue(storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parEntry.getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry));
}
++approxModelEntry;
++tableEntry;
}
}
}
}
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::initializeProbabilities(storm::models::sparse::Dtmc<ParametricType>const& parametricModel,
storm::storage::SparseMatrix<ConstantType>& probabilityMatrix,
std::vector<std::size_t>& rowSubstitutions,
std::vector<ProbTableEntry*>& matrixEntryToEvalTableMapping,
ProbTableEntry* constantEntry) {
// Run through the rows of the original model and obtain the different substitutions, the probability evaluation table,
// an MDP probability matrix with some dummy entries, and the mapping between the two
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(0, parametricModel.getNumberOfStates(), 0, true, true, parametricModel.getNumberOfStates());
this->probabilitySubstitutions.emplace_back(std::map<VariableType, TypeOfBound>()); //we want that the empty substitution is always the first one
std::size_t numOfNonConstEntries=0;
typename storm::storage::SparseMatrix<ConstantType>::index_type matrixRow=0;
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
matrixBuilder.newRowGroup(matrixRow);
// Find the different substitutions, i.e., mappings from Variables that occur in this row to {lower, upper}
std::set<VariableType> occurringVariables;
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
storm::utility::regions::gatherOccurringVariables(entry.getValue(), occurringVariables);
}
std::size_t numOfSubstitutions=1ull<<occurringVariables.size(); //=2^(#variables). Note that there is still 1 substitution when #variables==0 (i.e.,the empty substitution)
for(uint_fast64_t substitutionId=0; substitutionId<numOfSubstitutions; ++substitutionId){
//compute actual substitution from substitutionId by interpreting the Id as a bit sequence.
//the occurringVariables.size() least significant bits of substitutionId will always represent the substitution that we have to consider
//(00...0 = lower bounds for all parameters, 11...1 = upper bounds for all parameters)
std::map<VariableType, TypeOfBound> currSubstitution;
std::size_t parameterIndex=0;
for(auto const& parameter : occurringVariables){
if((substitutionId>>parameterIndex)%2==0){
currSubstitution.insert(std::make_pair(parameter, TypeOfBound::LOWER));
if(this->computeRewards){
//the same for rewards
auto approxModelRewardEntry = this->model->getUniqueRewardModel()->second.getStateActionRewardVector().begin();
for (auto tableEntry : rewardEntryToEvalTableMapping){
if(tableEntry != &constantRewEntry){
//insert pointer to minValue, pointer to maxValue, iterator to reward vector entry
this->rewardMapping.emplace_back(std::make_tuple(&(tableEntry->second.first), &(tableEntry->second.second), approxModelRewardEntry));
}
else{
currSubstitution.insert(std::make_pair(parameter, TypeOfBound::UPPER));
}
++parameterIndex;
++approxModelRewardEntry;
}
std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->probabilitySubstitutions, std::move(currSubstitution));
rowSubstitutions.push_back(substitutionIndex);
//For every substitution, run again through the row and add an entry in matrixEntryToEvalTableMapping as well as dummy entries in the matrix
//Note that this is still executed once, even if no parameters occur.
ConstantType dummyEntry=storm::utility::one<ConstantType>();
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
if(storm::utility::isConstant(entry.getValue())){
matrixEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
auto evalTableIt = this->probabilityEvaluationTable.insert(ProbTableEntry(FunctionSubstitution(entry.getValue(), substitutionIndex), storm::utility::zero<ConstantType>())).first;
matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
//Get the sets of reward parameters that map to "CHOSEOPTIMAL".
this->choseOptimalRewardPars = std::vector<std::set<VariableType>>(this->rewardSubstitutions.size());
for(std::size_t index = 0; index<this->rewardSubstitutions.size(); ++index){
for(auto const& sub : this->rewardSubstitutions[index]){
if(sub.second==TypeOfBound::CHOSEOPTIMAL){
this->choseOptimalRewardPars[index].insert(sub.first);
}
}
matrixBuilder.addNextValue(matrixRow, entry.getColumn(), dummyEntry);
dummyEntry=storm::utility::zero<ConstantType>();
}
++matrixRow;
}
}
this->probabilityMapping.reserve(numOfNonConstEntries);
probabilityMatrix=matrixBuilder.build();
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix,
std::vector<std::size_t> const& rowSubstitutions,
std::vector<ConstantType>& stateActionRewardVector,
std::vector<RewTableEntry*>& rewardEntryToEvalTableMapping,
RewTableEntry* constantEntry){
// run through the state reward vector of the parametric model.
// Constant entries can be set directly.
// For Parametric entries we set a dummy value and insert one entry to the rewardEntryEvalTableMapping
stateActionRewardVector.reserve(probabilityMatrix.getRowCount());
rewardEntryToEvalTableMapping.reserve(probabilityMatrix.getRowCount());
std::size_t numOfNonConstRewEntries=0;
this->rewardSubstitutions.emplace_back(std::map<VariableType, TypeOfBound>()); //we want that the empty substitution is always the first one
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
std::set<VariableType> occurringRewVariables;
std::set<VariableType> occurringProbVariables;
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){
ConstantType reward = storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state]));
//Add one of these entries for every row in the row group of state
for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow<probabilityMatrix.getRowGroupIndices()[state+1]; ++matrixRow){
stateActionRewardVector.emplace_back(reward);
rewardEntryToEvalTableMapping.emplace_back(constantEntry);
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::initializeProbabilities(ParametricSparseModelType const& parametricModel,
storm::storage::SparseMatrix<ConstantType>& probabilityMatrix,
std::vector<std::size_t>& rowSubstitutions,
std::vector<ProbTableEntry*>& matrixEntryToEvalTableMapping,
ProbTableEntry* constantEntry) {
// Run through the rows of the original model and obtain the different substitutions, the probability evaluation table,
// an MDP probability matrix with some dummy entries, and the mapping between the two
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(0, parametricModel.getNumberOfStates(), 0, true, true, parametricModel.getNumberOfStates());
this->probabilitySubstitutions.emplace_back(std::map<VariableType, TypeOfBound>()); //we want that the empty substitution is always the first one
std::size_t numOfNonConstEntries=0;
typename storm::storage::SparseMatrix<ConstantType>::index_type matrixRow=0;
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
matrixBuilder.newRowGroup(matrixRow);
// Find the different substitutions, i.e., mappings from Variables that occur in this row to {lower, upper}
std::set<VariableType> occurringVariables;
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
storm::utility::region::gatherOccurringVariables(entry.getValue(), occurringVariables);
}
} else {
storm::utility::regions::gatherOccurringVariables(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], occurringRewVariables);
//For each row in the row group of state, we get the corresponding substitution and tableIndex
// We might find out that the reward is independent of the probability variables (and will thus be independent of nondeterministic choices)
// In that case, the reward function and the substitution will not change and thus we can use the same table index
bool rewardDependsOnProbVars=true;
RewTableEntry* evalTablePtr;
for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow<probabilityMatrix.getRowGroupIndices()[state+1]; ++matrixRow){
if(rewardDependsOnProbVars){ //always executed in first iteration
rewardDependsOnProbVars=false;
std::map<VariableType, TypeOfBound> rewardSubstitution;
for(auto const& rewardVar : occurringRewVariables){
typename std::map<VariableType, TypeOfBound>::iterator const substitutionIt=this->probabilitySubstitutions[rowSubstitutions[matrixRow]].find(rewardVar);
if(substitutionIt==this->probabilitySubstitutions[rowSubstitutions[matrixRow]].end()){
rewardSubstitution.insert(std::make_pair(rewardVar, TypeOfBound::CHOSEOPTIMAL));
} else {
rewardSubstitution.insert(*substitutionIt);
rewardDependsOnProbVars=true;
}
std::size_t numOfSubstitutions=1ull<<occurringVariables.size(); //=2^(#variables). Note that there is still 1 substitution when #variables==0 (i.e.,the empty substitution)
for(uint_fast64_t substitutionId=0; substitutionId<numOfSubstitutions; ++substitutionId){
//compute actual substitution from substitutionId by interpreting the Id as a bit sequence.
//the occurringVariables.size() least significant bits of substitutionId will always represent the substitution that we have to consider
//(00...0 = lower bounds for all parameters, 11...1 = upper bounds for all parameters)
std::map<VariableType, TypeOfBound> currSubstitution;
std::size_t parameterIndex=0;
for(auto const& parameter : occurringVariables){
if((substitutionId>>parameterIndex)%2==0){
currSubstitution.insert(std::make_pair(parameter, TypeOfBound::LOWER));
}
std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution));
auto evalTableIt = this->rewardEvaluationTable.insert(
RewTableEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], substitutionIndex),
std::pair<ConstantType, ConstantType>(storm::utility::zero<ConstantType>(), storm::utility::zero<ConstantType>()))
).first;
evalTablePtr=&(*evalTableIt);
else{
currSubstitution.insert(std::make_pair(parameter, TypeOfBound::UPPER));
}
++parameterIndex;
}
std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->probabilitySubstitutions, std::move(currSubstitution));
rowSubstitutions.push_back(substitutionIndex);
//For every substitution, run again through the row and add an entry in matrixEntryToEvalTableMapping as well as dummy entries in the matrix
//Note that this is still executed once, even if no parameters occur.
ConstantType dummyEntry=storm::utility::one<ConstantType>();
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
if(storm::utility::isConstant(entry.getValue())){
matrixEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
auto evalTableIt = this->probabilityEvaluationTable.insert(ProbTableEntry(FunctionSubstitution(entry.getValue(), substitutionIndex), storm::utility::zero<ConstantType>())).first;
matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
matrixBuilder.addNextValue(matrixRow, entry.getColumn(), dummyEntry);
dummyEntry=storm::utility::zero<ConstantType>();
}
//insert table entries and dummy data
stateActionRewardVector.emplace_back(storm::utility::zero<ConstantType>());
rewardEntryToEvalTableMapping.emplace_back(evalTablePtr);
++numOfNonConstRewEntries;
++matrixRow;
}
}
this->probabilityMapping.reserve(numOfNonConstEntries);
probabilityMatrix=matrixBuilder.build();
}
this->rewardMapping.reserve(numOfNonConstRewEntries);
}
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::initializeRewards(ParametricSparseModelType const& parametricModel,
storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix,
std::vector<std::size_t> const& rowSubstitutions,
std::vector<ConstantType>& stateActionRewardVector,
std::vector<RewTableEntry*>& rewardEntryToEvalTableMapping,
RewTableEntry* constantEntry){
// run through the state reward vector of the parametric model.
// Constant entries can be set directly.
// For Parametric entries we set a dummy value and insert one entry to the rewardEntryEvalTableMapping
stateActionRewardVector.reserve(probabilityMatrix.getRowCount());
rewardEntryToEvalTableMapping.reserve(probabilityMatrix.getRowCount());
std::size_t numOfNonConstRewEntries=0;
this->rewardSubstitutions.emplace_back(std::map<VariableType, TypeOfBound>()); //we want that the empty substitution is always the first one
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::~ApproximationModel() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::getModel() const {
return this->model;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::instantiate(const ParameterRegion& region) {
//Instantiate the substitutions
std::vector<std::map<VariableType, CoefficientType>> instantiatedSubs(this->probabilitySubstitutions.size());
for(uint_fast64_t substitutionIndex=0; substitutionIndex<this->probabilitySubstitutions.size(); ++substitutionIndex){
for(std::pair<VariableType, TypeOfBound> const& sub : this->probabilitySubstitutions[substitutionIndex]){
switch(sub.second){
case TypeOfBound::LOWER:
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBound(sub.first)));
break;
case TypeOfBound::UPPER:
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBound(sub.first)));
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of Bound");
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
std::set<VariableType> occurringRewVariables;
std::set<VariableType> occurringProbVariables;
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){
ConstantType reward = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state]));
//Add one of these entries for every row in the row group of state
for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow<probabilityMatrix.getRowGroupIndices()[state+1]; ++matrixRow){
stateActionRewardVector.emplace_back(reward);
rewardEntryToEvalTableMapping.emplace_back(constantEntry);
}
} else {
storm::utility::region::gatherOccurringVariables(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], occurringRewVariables);
//For each row in the row group of state, we get the corresponding substitution and tableIndex
// We might find out that the reward is independent of the probability variables (and will thus be independent of nondeterministic choices)
// In that case, the reward function and the substitution will not change and thus we can use the same table index
bool rewardDependsOnProbVars=true;
RewTableEntry* evalTablePtr;
for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow<probabilityMatrix.getRowGroupIndices()[state+1]; ++matrixRow){
if(rewardDependsOnProbVars){ //always executed in first iteration
rewardDependsOnProbVars=false;
std::map<VariableType, TypeOfBound> rewardSubstitution;
for(auto const& rewardVar : occurringRewVariables){
typename std::map<VariableType, TypeOfBound>::iterator const substitutionIt=this->probabilitySubstitutions[rowSubstitutions[matrixRow]].find(rewardVar);
if(substitutionIt==this->probabilitySubstitutions[rowSubstitutions[matrixRow]].end()){
rewardSubstitution.insert(std::make_pair(rewardVar, TypeOfBound::CHOSEOPTIMAL));
} else {
rewardSubstitution.insert(*substitutionIt);
rewardDependsOnProbVars=true;
}
}
std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution));
auto evalTableIt = this->rewardEvaluationTable.insert(
RewTableEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], substitutionIndex),
std::pair<ConstantType, ConstantType>(storm::utility::zero<ConstantType>(), storm::utility::zero<ConstantType>()))
).first;
evalTablePtr=&(*evalTableIt);
}
//insert table entries and dummy data
stateActionRewardVector.emplace_back(storm::utility::zero<ConstantType>());
rewardEntryToEvalTableMapping.emplace_back(evalTablePtr);
++numOfNonConstRewEntries;
}
}
}
this->rewardMapping.reserve(numOfNonConstRewEntries);
}
//write entries into evaluation table
for(auto& tableEntry : this->probabilityEvaluationTable){
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(
tableEntry.first.getFunction(),
instantiatedSubs[tableEntry.first.getSubstitution()]
)
);
template<typename ParametricSparseModelType, typename ConstantType>
ApproximationModel<ParametricSparseModelType, ConstantType>::~ApproximationModel() {
//Intentionally left empty
}
//write the instantiated values to the matrix according to the mapping
for(auto& mappingPair : this->probabilityMapping){
mappingPair.second->setValue(*(mappingPair.first));
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> const& ApproximationModel<ParametricSparseModelType, ConstantType>::getModel() const {
return this->model;
}
if(this->computeRewards){
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::instantiate(const ParameterRegion<ParametricType>& region) {
//Instantiate the substitutions
std::vector<std::map<VariableType, CoefficientType>> instantiatedRewardSubs(this->rewardSubstitutions.size());
for(uint_fast64_t substitutionIndex=0; substitutionIndex<this->rewardSubstitutions.size(); ++substitutionIndex){
for(std::pair<VariableType, TypeOfBound> const& sub : this->rewardSubstitutions[substitutionIndex]){
std::vector<std::map<VariableType, CoefficientType>> instantiatedSubs(this->probabilitySubstitutions.size());
for(uint_fast64_t substitutionIndex=0; substitutionIndex<this->probabilitySubstitutions.size(); ++substitutionIndex){
for(std::pair<VariableType, TypeOfBound> const& sub : this->probabilitySubstitutions[substitutionIndex]){
switch(sub.second){
case TypeOfBound::LOWER:
instantiatedRewardSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBound(sub.first)));
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBound(sub.first)));
break;
case TypeOfBound::UPPER:
instantiatedRewardSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBound(sub.first)));
break;
case TypeOfBound::CHOSEOPTIMAL:
//Insert some dummy value
instantiatedRewardSubs[substitutionIndex].insert(std::make_pair(sub.first, storm::utility::zero<ConstantType>()));
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBound(sub.first)));
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of Bound when instantiating a reward substitution. Index: " << substitutionIndex << " TypeOfBound: "<< ((int)sub.second));
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of Bound");
}
}
}
//write entries into evaluation table
for(auto& tableEntry : this->rewardEvaluationTable){
auto& funcSub = tableEntry.first;
auto& minMax = tableEntry.second;
minMax.first=storm::utility::infinity<ConstantType>();
minMax.second=storm::utility::zero<ConstantType>();
//Iterate over the different combinations of lower and upper bounds and update the min and max values
auto const& vertices=region.getVerticesOfRegion(this->choseOptimalRewardPars[funcSub.getSubstitution()]);
for(auto const& vertex : vertices){
//extend the substitution
for(auto const& vertexSub : vertex){
instantiatedRewardSubs[funcSub.getSubstitution()][vertexSub.first]=vertexSub.second;
}
ConstantType currValue = storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(
funcSub.getFunction(),
instantiatedRewardSubs[funcSub.getSubstitution()]
for(auto& tableEntry : this->probabilityEvaluationTable){
tableEntry.second=storm::utility::region::convertNumber<ConstantType>(
storm::utility::region::evaluateFunction(
tableEntry.first.getFunction(),
instantiatedSubs[tableEntry.first.getSubstitution()]
)
);
minMax.first=std::min(minMax.first, currValue);
minMax.second=std::max(minMax.second, currValue);
}
}
//Note: the rewards are written to the model as soon as the optimality type is known (i.e. in computeValues)
}
}
//write the instantiated values to the matrix according to the mapping
for(auto& mappingPair : this->probabilityMapping){
mappingPair.second->setValue(*(mappingPair.first));
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(*this->model);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr;
if(this->computeRewards){
//write the reward values into the model
switch(optDir){
case storm::solver::OptimizationDirection::Minimize:
for(auto& mappingTriple : this->rewardMapping){
*std::get<2>(mappingTriple)=*std::get<0>(mappingTriple);
if(this->computeRewards){
//Instantiate the substitutions
std::vector<std::map<VariableType, CoefficientType>> instantiatedRewardSubs(this->rewardSubstitutions.size());
for(uint_fast64_t substitutionIndex=0; substitutionIndex<this->rewardSubstitutions.size(); ++substitutionIndex){
for(std::pair<VariableType, TypeOfBound> const& sub : this->rewardSubstitutions[substitutionIndex]){
switch(sub.second){
case TypeOfBound::LOWER:
instantiatedRewardSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBound(sub.first)));
break;
case TypeOfBound::UPPER:
instantiatedRewardSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBound(sub.first)));
break;
case TypeOfBound::CHOSEOPTIMAL:
//Insert some dummy value
instantiatedRewardSubs[substitutionIndex].insert(std::make_pair(sub.first, storm::utility::zero<ConstantType>()));
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of Bound when instantiating a reward substitution. Index: " << substitutionIndex << " TypeOfBound: "<< ((int)sub.second));
}
}
break;
case storm::solver::OptimizationDirection::Maximize:
for(auto& mappingTriple : this->rewardMapping){
*std::get<2>(mappingTriple)=*std::get<1>(mappingTriple);
}
//write entries into evaluation table
for(auto& tableEntry : this->rewardEvaluationTable){
auto& funcSub = tableEntry.first;
auto& minMax = tableEntry.second;
minMax.first=storm::utility::infinity<ConstantType>();
minMax.second=storm::utility::zero<ConstantType>();
//Iterate over the different combinations of lower and upper bounds and update the min and max values
auto const& vertices=region.getVerticesOfRegion(this->choseOptimalRewardPars[funcSub.getSubstitution()]);
for(auto const& vertex : vertices){
//extend the substitution
for(auto const& vertexSub : vertex){
instantiatedRewardSubs[funcSub.getSubstitution()][vertexSub.first]=vertexSub.second;
}
ConstantType currValue = storm::utility::region::convertNumber<ConstantType>(
storm::utility::region::evaluateFunction(
funcSub.getFunction(),
instantiatedRewardSubs[funcSub.getSubstitution()]
)
);
minMax.first=std::min(minMax.first, currValue);
minMax.second=std::max(minMax.second, currValue);
}
break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given optimality Type is not supported.");
}
//Note: the rewards are written to the model as soon as the optimality type is known (i.e. in computeValues)
}
//perform model checking on the mdp
boost::optional<std::string> noRewardModelName; //it should be uniquely given
resultPtr = modelChecker.computeReachabilityRewards(this->formula->asReachabilityRewardFormula(), noRewardModelName, false, optDir);
}
else {
//perform model checking on the mdp
resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asEventuallyFormula(), false, optDir);
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> const& ApproximationModel<ParametricSparseModelType, ConstantType>::computeValues(storm::solver::OptimizationDirection const& optDir) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(*this->model);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr;
if(this->computeRewards){
//write the reward values into the model
switch(optDir){
case storm::solver::OptimizationDirection::Minimize:
for(auto& mappingTriple : this->rewardMapping){
*std::get<2>(mappingTriple)=*std::get<0>(mappingTriple);
}
break;
case storm::solver::OptimizationDirection::Maximize:
for(auto& mappingTriple : this->rewardMapping){
*std::get<2>(mappingTriple)=*std::get<1>(mappingTriple);
}
break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given optimality Type is not supported.");
}
//perform model checking on the mdp
boost::optional<std::string> noRewardModelName; //it should be uniquely given
resultPtr = modelChecker.computeReachabilityRewards(this->formula->asReachabilityRewardFormula(), noRewardModelName, false, optDir);
}
else {
//perform model checking on the mdp
resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asEventuallyFormula(), false, optDir);
}
return resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
return resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class ApproximationModel<storm::models::sparse::Dtmc<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>, double>;
#endif
} //namespace region
}
}

279
src/modelchecker/region/ApproximationModel.h
View File

@ -9,157 +9,156 @@
#define STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H
#include <unordered_map>
#include <memory>
#include "src/utility/region.h"
#include "src/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "src/models/sparse/Mdp.h"
#include "src/logic/Formulas.h"
#include "src/modelchecker/region/ParameterRegion.h"
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Mdp.h"
#include "src/storage/SparseMatrix.h"
namespace storm {
namespace modelchecker {
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel{
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType CoefficientType;
/*!
* @note this will not check whether approximation is applicable
*/
ApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula);
virtual ~ApproximationModel();
/*!
* returns the underlying model
*/
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> const& getModel() const;
/*!
* Instantiates the underlying model according to the given region
*/
void instantiate(ParameterRegion const& region);
/*!
* Returns the approximated reachability probabilities for every state.
* Undefined behavior if model has not been instantiated first!
* @param optimalityType Use MAXIMIZE to get upper bounds or MINIMIZE to get lower bounds
*/
std::vector<ConstantType> const& computeValues(storm::solver::OptimizationDirection const& optDir);
private:
//This enum helps to store how a parameter will be substituted.
enum class TypeOfBound {
LOWER,
UPPER,
CHOSEOPTIMAL
};
//A class that represents a function and how it should be substituted (i.e. which variables should be replaced with lower and which with upper bounds of the region)
//The substitution is given as an index in probability or reward substitutions. (This allows to instantiate the substitutions more easily)
class FunctionSubstitution {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class ApproximationModel{
public:
FunctionSubstitution(ParametricType const& fun, std::size_t const& sub) : hash(computeHash(fun,sub)), function(fun), substitution(sub) {
//intentionally left empty
}
FunctionSubstitution(ParametricType&& fun, std::size_t&& sub) : hash(computeHash(fun,sub)), function(std::move(fun)), substitution(std::move(sub)) {
//intentionally left empty
}
FunctionSubstitution(FunctionSubstitution const& other) : hash(other.hash), function(other.function), substitution(other.substitution){
//intentionally left empty
}
FunctionSubstitution(FunctionSubstitution&& other) : hash(std::move(other.hash)), function(std::move(other.function)), substitution(std::move(other.substitution)){
//intentionally left empty
}
FunctionSubstitution() = default;
~FunctionSubstitution() = default;
bool operator==(FunctionSubstitution const& other) const {
return this->hash==other.hash && this->substitution==other.substitution && this->function==other.function;
}
ParametricType const& getFunction() const{
return this->function;
}
std::size_t const& getSubstitution() const{
return this->substitution;
}
std::size_t const& getHash() const{
return this->hash;
}
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
/*!
* @note this will not check whether approximation is applicable
*/
ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::Formula> formula);
virtual ~ApproximationModel();
/*!
* returns the underlying model
*/
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> const& getModel() const;
/*!
* Instantiates the underlying model according to the given region
*/
void instantiate(ParameterRegion<ParametricType> const& region);
/*!
* Returns the approximated reachability probabilities for every state.
* Undefined behavior if model has not been instantiated first!
* @param optimalityType Use MAXIMIZE to get upper bounds or MINIMIZE to get lower bounds
*/
std::vector<ConstantType> const& computeValues(storm::solver::OptimizationDirection const& optDir);
private:
static std::size_t computeHash(ParametricType const& fun, std::size_t const& sub) {
std::size_t hf = std::hash<ParametricType>()(fun);
std::size_t hs = std::hash<std::size_t>()(sub);
return hf ^(hs << 1);
}
std::size_t hash;
ParametricType function;
std::size_t substitution;
};
class FuncSubHash{
//This enum helps to store how a parameter will be substituted.
enum class TypeOfBound {
LOWER,
UPPER,
CHOSEOPTIMAL
};
//A class that represents a function and how it should be substituted (i.e. which variables should be replaced with lower and which with upper bounds of the region)
//The substitution is given as an index in probability or reward substitutions. (This allows to instantiate the substitutions more easily)
class FunctionSubstitution {
public:
std::size_t operator()(FunctionSubstitution const& fs) const {
return fs.getHash();
FunctionSubstitution(ParametricType const& fun, std::size_t const& sub) : hash(computeHash(fun,sub)), function(fun), substitution(sub) {
//intentionally left empty
}
FunctionSubstitution(ParametricType&& fun, std::size_t&& sub) : hash(computeHash(fun,sub)), function(std::move(fun)), substitution(std::move(sub)) {
//intentionally left empty
}
FunctionSubstitution(FunctionSubstitution const& other) : hash(other.hash), function(other.function), substitution(other.substitution){
//intentionally left empty
}
FunctionSubstitution(FunctionSubstitution&& other) : hash(std::move(other.hash)), function(std::move(other.function)), substitution(std::move(other.substitution)){
//intentionally left empty
}
FunctionSubstitution() = default;
~FunctionSubstitution() = default;
bool operator==(FunctionSubstitution const& other) const {
return this->hash==other.hash && this->substitution==other.substitution && this->function==other.function;
}
ParametricType const& getFunction() const{
return this->function;
}
std::size_t const& getSubstitution() const{
return this->substitution;
}
std::size_t const& getHash() const{
return this->hash;
}
private:
static std::size_t computeHash(ParametricType const& fun, std::size_t const& sub) {
std::size_t hf = std::hash<ParametricType>()(fun);
std::size_t hs = std::hash<std::size_t>()(sub);
return hf ^(hs << 1);
}
std::size_t hash;
ParametricType function;
std::size_t substitution;
};
class FuncSubHash{
public:
std::size_t operator()(FunctionSubstitution const& fs) const {
return fs.getHash();
}
};
typedef typename std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash>::value_type ProbTableEntry;
typedef typename std::unordered_map<FunctionSubstitution, std::pair<ConstantType, ConstantType>, FuncSubHash>::value_type RewTableEntry;
void initializeProbabilities(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<std::size_t>& rowSubstitutions, std::vector<ProbTableEntry*>& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry);
void initializeRewards(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix, std::vector<std::size_t> const& rowSubstitutions, std::vector<ConstantType>& stateActionRewardVector, std::vector<RewTableEntry*>& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry);
//The Model with which we work
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> model;
//The formula for which we will compute the values
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
// We store one (unique) entry for every occurring pair of a non-constant function and substitution.
// Whenever a region is given, we can then evaluate the functions (w.r.t. the corresponding substitutions)
// and store the result to the target value of this map
std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash> probabilityEvaluationTable;
//For rewards, we map to the minimal value and the maximal value (depending on the CHOSEOPTIMAL parameters).
std::unordered_map<FunctionSubstitution, std::pair<ConstantType, ConstantType>, FuncSubHash> rewardEvaluationTable;
//Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region)
std::vector<std::map<VariableType, TypeOfBound>> probabilitySubstitutions;
//Same for the different substitutions for the reward functions.
//In addition, we store the parameters for which the correct substitution
//depends on the region and whether to minimize/maximize (i.e. CHOSEOPTIMAL parameters)
std::vector<std::map<VariableType, TypeOfBound>> rewardSubstitutions;
std::vector<std::set<VariableType>> choseOptimalRewardPars;
//This Vector connects the probability evaluation table with the probability matrix of the model.
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
//Similar for the rewards. But now the first entry points to a minimal and the second one to a maximal value.
//The third entry points to the state reward vector.
std::vector<std::tuple<ConstantType*, ConstantType*, typename std::vector<ConstantType>::iterator>> rewardMapping;
};
typedef typename std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash>::value_type ProbTableEntry;
typedef typename std::unordered_map<FunctionSubstitution, std::pair<ConstantType, ConstantType>, FuncSubHash>::value_type RewTableEntry;
void initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<std::size_t>& rowSubstitutions, std::vector<ProbTableEntry*>& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry);
void initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix, std::vector<std::size_t> const& rowSubstitutions, std::vector<ConstantType>& stateActionRewardVector, std::vector<RewTableEntry*>& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry);
//The Model with which we work
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> model;
//The formula for which we will compute the values
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
// We store one (unique) entry for every occurring pair of a non-constant function and substitution.
// Whenever a region is given, we can then evaluate the functions (w.r.t. the corresponding substitutions)
// and store the result to the target value of this map
std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash> probabilityEvaluationTable;
//For rewards, we map to the minimal value and the maximal value (depending on the CHOSEOPTIMAL parameters).
std::unordered_map<FunctionSubstitution, std::pair<ConstantType, ConstantType>, FuncSubHash> rewardEvaluationTable;
//Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region)
std::vector<std::map<VariableType, TypeOfBound>> probabilitySubstitutions;
//Same for the different substitutions for the reward functions.
//In addition, we store the parameters for which the correct substitution
//depends on the region and whether to minimize/maximize (i.e. CHOSEOPTIMAL parameters)
std::vector<std::map<VariableType, TypeOfBound>> rewardSubstitutions;
std::vector<std::set<VariableType>> choseOptimalRewardPars;
//This Vector connects the probability evaluation table with the probability matrix of the model.
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
//Similar for the rewards. But now the first entry points to a minimal and the second one to a maximal value.
//The third entry points to the state reward vector.
std::vector<std::tuple<ConstantType*, ConstantType*, typename std::vector<ConstantType>::iterator>> rewardMapping;
};
} //namespace region
}
}

440
src/modelchecker/region/ParameterRegion.cpp
View File

@ -7,260 +7,240 @@
#include "src/modelchecker/region/ParameterRegion.h"
#include "src/utility/regions.h"
#include "src/utility/region.h"
#include "src/utility/macros.h"
#include "src/parser/MappedFile.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/RegionSettings.h"
#include "src/exceptions/UnexpectedException.h"
#include "exceptions/InvalidSettingsException.h"
#include "exceptions/InvalidArgumentException.h"
#include "parser/MappedFile.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::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);
template<typename ParametricType>
ParameterRegion<ParametricType>::ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
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);
template<typename ParametricType>
ParameterRegion<ParametricType>::ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
}
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::~ParameterRegion() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
std::set<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getVariables() const {
return this->variables;
}
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getLowerBound(VariableType const& variable) const {
auto const& result = lowerBounds.find(variable);
STORM_LOG_THROW(result != lowerBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower bound of a variable that is not specified by this region");
return (*result).second;
}
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getUpperBound(VariableType const& variable) const {
auto const& result = upperBounds.find(variable);
STORM_LOG_THROW(result != upperBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper bound of a variable that is not specified by this region");
return (*result).second;
}
template<typename ParametricSparseModelType, typename ConstantType>
const std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getUpperBounds() const {
return upperBounds;
}
template<typename ParametricSparseModelType, typename ConstantType>
const std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getLowerBounds() const {
return lowerBounds;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType>> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const {
std::size_t const numOfVariables = consideredVariables.size();
std::size_t const numOfVertices = std::pow(2, numOfVariables);
std::vector<std::map<VariableType, CoefficientType >> resultingVector(numOfVertices, std::map<VariableType, CoefficientType>());
if (numOfVertices == 1) {
//no variables are given, the returned vector should still contain an empty map
return resultingVector;
template<typename ParametricType>
void ParameterRegion<ParametricType>::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 : 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);
}
}
template<typename ParametricType>
ParameterRegion<ParametricType>::~ParameterRegion() {
//Intentionally left empty
}
template<typename ParametricType>
std::set<typename ParameterRegion<ParametricType>::VariableType> ParameterRegion<ParametricType>::getVariables() const {
return this->variables;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getLowerBound(VariableType const& variable) const {
auto const& result = lowerBounds.find(variable);
STORM_LOG_THROW(result != lowerBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower bound of a variable that is not specified by this region");
return (*result).second;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getUpperBound(VariableType const& variable) const {
auto const& result = upperBounds.find(variable);
STORM_LOG_THROW(result != upperBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper bound of a variable that is not specified by this region");
return (*result).second;
}
template<typename ParametricType>
const typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getUpperBounds() const {
return upperBounds;
}
for (uint_fast64_t vertexId = 0; vertexId < numOfVertices; ++vertexId) {
//interprete vertexId as a bit sequence
//the consideredVariables.size() least significant bits of vertex will always represent the next vertex
//(00...0 = lower bounds for all variables, 11...1 = upper bounds for all variables)
std::size_t variableIndex = 0;
for (auto const& variable : consideredVariables) {
if ((vertexId >> variableIndex) % 2 == 0) {
resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getLowerBound(variable)));
} else {
resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getUpperBound(variable)));
template<typename ParametricType>
const typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getLowerBounds() const {
return lowerBounds;
}
template<typename ParametricType>
std::vector<typename ParameterRegion<ParametricType>::VariableSubstitutionType> ParameterRegion<ParametricType>::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const {
std::size_t const numOfVariables = consideredVariables.size();
std::size_t const numOfVertices = std::pow(2, numOfVariables);
std::vector<VariableSubstitutionType> resultingVector(numOfVertices, VariableSubstitutionType());
if (numOfVertices == 1) {
//no variables are given, the returned vector should still contain an empty map
return resultingVector;
}
for (uint_fast64_t vertexId = 0; vertexId < numOfVertices; ++vertexId) {
//interprete vertexId as a bit sequence
//the consideredVariables.size() least significant bits of vertex will always represent the next vertex
//(00...0 = lower bounds for all variables, 11...1 = upper bounds for all variables)
std::size_t variableIndex = 0;
for (auto const& variable : consideredVariables) {
if ((vertexId >> variableIndex) % 2 == 0) {
resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getLowerBound(variable)));
} else {
resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getUpperBound(variable)));
}
++variableIndex;
}
++variableIndex;
}
return resultingVector;
}
return resultingVector;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getSomePoint() const {
return this->getLowerBounds();
}
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::RegionCheckResult SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getCheckResult() const {
return checkResult;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::setCheckResult(RegionCheckResult checkResult) {
//a few sanity checks
STORM_LOG_THROW((this->checkResult == RegionCheckResult::UNKNOWN || checkResult != RegionCheckResult::UNKNOWN), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from something known to UNKNOWN ");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::EXISTSVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to EXISTSVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to ALLVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSVIOLATED || checkResult != RegionCheckResult::EXISTSSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to EXISTSSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSVIOLATED || checkResult != RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to ALLSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSBOTH || checkResult != RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSBOTH || checkResult != RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::ALLSAT || checkResult == RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLSAT to something else");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::ALLVIOLATED || checkResult == RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLVIOLATED to something else");
this->checkResult = checkResult;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getViolatedPoint() const {
return violatedPoint;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::setViolatedPoint(std::map<VariableType, CoefficientType> const& violatedPoint) {
this->violatedPoint = violatedPoint;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getSatPoint() const {
return satPoint;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::setSatPoint(std::map<VariableType, CoefficientType> const& satPoint) {
this->satPoint = satPoint;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::string SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::checkResultToString() const {
switch (this->checkResult) {
case RegionCheckResult::UNKNOWN:
return "unknown";
case RegionCheckResult::EXISTSSAT:
return "ExistsSat";
case RegionCheckResult::EXISTSVIOLATED:
return "ExistsViolated";
case RegionCheckResult::EXISTSBOTH:
return "ExistsBoth";
case RegionCheckResult::ALLSAT:
return "allSat";
case RegionCheckResult::ALLVIOLATED:
return "allViolated";
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getSomePoint() const {
return this->getLowerBounds();
}
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not identify check result")
return "ERROR";
}
template<typename ParametricSparseModelType, typename ConstantType>
std::string SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::toString() const {
std::stringstream regionstringstream;
for (auto var : this->getVariables()) {
regionstringstream << storm::utility::regions::convertNumber<double>(this->getLowerBound(var));
regionstringstream << "<=";
regionstringstream << storm::utility::regions::getVariableName(var);
regionstringstream << "<=";
regionstringstream << storm::utility::regions::convertNumber<double>(this->getUpperBound(var));
regionstringstream << ",";
template<typename ParametricType>
RegionCheckResult ParameterRegion<ParametricType>::getCheckResult() const {
return checkResult;
}
std::string regionstring = regionstringstream.str();
//the last comma should actually be a semicolon
regionstring = regionstring.substr(0, regionstring.length() - 1) + ";";
return regionstring;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::parseParameterBounds(
std::map<VariableType, CoefficientType>& lowerBounds,
std::map<VariableType, CoefficientType>& upperBounds,
std::string const& parameterBoundsString){
std::string::size_type positionOfFirstRelation = parameterBoundsString.find("<=");
STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the first number");
std::string::size_type positionOfSecondRelation = parameterBoundsString.find("<=", positionOfFirstRelation+2);
STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the parameter");
std::string parameter=parameterBoundsString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
//removes all whitespaces from the parameter string:
parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
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<VariableType>(parameter);
CoefficientType lb = storm::utility::regions::convertNumber<CoefficientType>(parameterBoundsString.substr(0,positionOfFirstRelation));
CoefficientType ub = storm::utility::regions::convertNumber<CoefficientType>(parameterBoundsString.substr(positionOfSecondRelation+2));
lowerBounds.emplace(std::make_pair(var, lb));
upperBounds.emplace(std::make_pair(var, ub));
template<typename ParametricType>
void ParameterRegion<ParametricType>::setCheckResult(RegionCheckResult checkResult) {
//a few sanity checks
STORM_LOG_THROW((this->checkResult == RegionCheckResult::UNKNOWN || checkResult != RegionCheckResult::UNKNOWN), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from something known to UNKNOWN ");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::EXISTSVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to EXISTSVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to ALLVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSVIOLATED || checkResult != RegionCheckResult::EXISTSSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to EXISTSSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSVIOLATED || checkResult != RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to ALLSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSBOTH || checkResult != RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSBOTH || checkResult != RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::ALLSAT || checkResult == RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLSAT to something else");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::ALLVIOLATED || checkResult == RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLVIOLATED to something else");
this->checkResult = checkResult;
}
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::parseRegion(
std::string const& regionString){
std::map<VariableType, CoefficientType> lowerBounds;
std::map<VariableType, CoefficientType> upperBounds;
std::vector<std::string> parameterBounds;
boost::split(parameterBounds, regionString, boost::is_any_of(","));
for(auto const& parameterBound : parameterBounds){
if(!std::all_of(parameterBound.begin(),parameterBound.end(), ::isspace)){ //skip this string if it only consists of space
parseParameterBounds(lowerBounds, upperBounds, parameterBound);
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getViolatedPoint() const {
return violatedPoint;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::setViolatedPoint(VariableSubstitutionType const& violatedPoint) {
this->violatedPoint = violatedPoint;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getSatPoint() const {
return satPoint;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::setSatPoint(VariableSubstitutionType const& satPoint) {
this->satPoint = satPoint;
}
template<typename ParametricType>
std::string ParameterRegion<ParametricType>::toString() const {
std::stringstream regionstringstream;
for (auto var : this->getVariables()) {
regionstringstream << storm::utility::region::convertNumber<double>(this->getLowerBound(var));
regionstringstream << "<=";
regionstringstream << storm::utility::region::getVariableName(var);
regionstringstream << "<=";
regionstringstream << storm::utility::region::convertNumber<double>(this->getUpperBound(var));
regionstringstream << ",";
}
return ParameterRegion(std::move(lowerBounds), std::move(upperBounds));
std::string regionstring = regionstringstream.str();
//the last comma should actually be a semicolon
regionstring = regionstring.substr(0, regionstring.length() - 1) + ";";
return regionstring;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::parseMultipleRegions(
std::string const& regionsString){
std::vector<ParameterRegion> result;
std::vector<std::string> regionsStrVec;
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));
template<typename ParametricType>
void ParameterRegion<ParametricType>::parseParameterBounds(
VariableSubstitutionType& lowerBounds,
VariableSubstitutionType& upperBounds,
std::string const& parameterBoundsString){
std::string::size_type positionOfFirstRelation = parameterBoundsString.find("<=");
STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the first number");
std::string::size_type positionOfSecondRelation = parameterBoundsString.find("<=", positionOfFirstRelation+2);
STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the parameter");
std::string parameter=parameterBoundsString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
//removes all whitespaces from the parameter string:
parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a parameter");
VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
CoefficientType lb = storm::utility::region::convertNumber<CoefficientType>(parameterBoundsString.substr(0,positionOfFirstRelation));
CoefficientType ub = storm::utility::region::convertNumber<CoefficientType>(parameterBoundsString.substr(positionOfSecondRelation+2));
lowerBounds.emplace(std::make_pair(var, lb));
upperBounds.emplace(std::make_pair(var, ub));
}
template<typename ParametricType>
ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(
std::string const& regionString){
VariableSubstitutionType lowerBounds;
VariableSubstitutionType upperBounds;
std::vector<std::string> parameterBounds;
boost::split(parameterBounds, regionString, boost::is_any_of(","));
for(auto const& parameterBound : parameterBounds){
if(!std::all_of(parameterBound.begin(),parameterBound.end(), ::isspace)){ //skip this string if it only consists of space
parseParameterBounds(lowerBounds, upperBounds, parameterBound);
}
}
return ParameterRegion(std::move(lowerBounds), std::move(upperBounds));
}
return result;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getRegionsFromSettings(){
STORM_LOG_THROW(storm::settings::regionSettings().isRegionsSet() || storm::settings::regionSettings().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
STORM_LOG_THROW(!(storm::settings::regionSettings().isRegionsSet() && storm::settings::regionSettings().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
std::string regionsString;
if(storm::settings::regionSettings().isRegionsSet()){
regionsString = storm::settings::regionSettings().getRegionsFromCmdLine();
template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(
std::string const& regionsString){
std::vector<ParameterRegion> result;
std::vector<std::string> regionsStrVec;
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));
}
}
return result;
}
else{
//if we reach this point we can assume that the region is given as a file.
STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::regionSettings().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
storm::parser::MappedFile mf(storm::settings::regionSettings().getRegionFilePath().c_str());
regionsString = std::string(mf.getData(),mf.getDataSize());
template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::getRegionsFromSettings(){
STORM_LOG_THROW(storm::settings::regionSettings().isRegionsSet() || storm::settings::regionSettings().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
STORM_LOG_THROW(!(storm::settings::regionSettings().isRegionsSet() && storm::settings::regionSettings().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
std::string regionsString;
if(storm::settings::regionSettings().isRegionsSet()){
regionsString = storm::settings::regionSettings().getRegionsFromCmdLine();
}
else{
//if we reach this point we can assume that the region is given as a file.
STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::regionSettings().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
storm::parser::MappedFile mf(storm::settings::regionSettings().getRegionFilePath().c_str());
regionsString = std::string(mf.getData(),mf.getDataSize());
}
return parseMultipleRegions(regionsString);
}
return parseMultipleRegions(regionsString);
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class ParameterRegion<storm::RationalFunction>;
#endif
} //namespace region
}
}

229
src/modelchecker/region/ParameterRegion.h
View File

@ -8,125 +8,124 @@
#ifndef STORM_MODELCHECKER_REGION_PARAMETERREGION_H
#define STORM_MODELCHECKER_REGION_PARAMETERREGION_H
#include "src/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include <map>
#include "src/modelchecker/region/RegionCheckResult.h"
#include "src/utility/region.h"
namespace storm {
namespace modelchecker{
namespace region {
template<typename ParametricType>
class ParameterRegion{
public:
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
typedef typename std::map<VariableType, CoefficientType> VariableSubstitutionType;
ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds);
ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds);
virtual ~ParameterRegion();
std::set<VariableType> getVariables() const;
CoefficientType const& getLowerBound(VariableType const& variable) const;
CoefficientType const& getUpperBound(VariableType const& variable) const;
const VariableSubstitutionType getUpperBounds() const;
const VariableSubstitutionType 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())
* ...
* The last entry will map every variable to its upper bound
*
* If the given set of variables is empty, the returned vector will contain an empty map
*/
std::vector<VariableSubstitutionType> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
/*!
* Returns some point that lies within this region
*/
VariableSubstitutionType getSomePoint() const;
RegionCheckResult getCheckResult() const;
void setCheckResult(RegionCheckResult checkResult);
/*!
* Retrieves a point in the region for which is considered property is not satisfied.
* If such a point is not known, the returned map is empty.
*/
VariableSubstitutionType getViolatedPoint() const;
/*!
* Sets a point in the region for which the considered property is not satisfied.
*/
void setViolatedPoint(VariableSubstitutionType const& violatedPoint);
/*!
* Retrieves a point in the region for which is considered property is satisfied.
* If such a point is not known, the returned map is empty.
*/
VariableSubstitutionType getSatPoint() const;
/*!
* Sets a point in the region for which the considered property is satisfied.
*/
void setSatPoint(VariableSubstitutionType const& satPoint);
//returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
std::string toString() const;
/*
* Can be used to parse a single parameter with its bounds from a string of the form "0.3<=p<=0.5".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
* The results will be inserted in the given maps
*
*/
static void parseParameterBounds(
VariableSubstitutionType& lowerBounds,
VariableSubstitutionType& upperBounds,
std::string const& parameterBoundsString
);
/*
* Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static ParameterRegion parseRegion(
std::string const& regionString
);
/*
* Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static std::vector<ParameterRegion> parseMultipleRegions(
std::string const& regionsString
);
/*
* Retrieves the regions that are specified in the settings.
*/
static std::vector<ParameterRegion> getRegionsFromSettings();
private:
void init();
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion{
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType CoefficientType;
ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds);
ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds);
virtual ~ParameterRegion();
std::set<VariableType> getVariables() const;
CoefficientType const& getLowerBound(VariableType const& variable) const;
CoefficientType const& getUpperBound(VariableType const& variable) const;
const std::map<VariableType, CoefficientType> getUpperBounds() const;
const std::map<VariableType, CoefficientType> 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())
* ...
* The last entry will map every variable to its upper bound
*
* If the given set of variables is empty, the returned vector will contain an empty map
*/
std::vector<std::map<VariableType, CoefficientType>> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
/*!
* Returns some point that lies within this region
*/
std::map<VariableType, CoefficientType> getSomePoint() const;
RegionCheckResult getCheckResult() const;
void setCheckResult(RegionCheckResult checkResult);
/*!
* Retrieves a point in the region for which is considered property is not satisfied.
* If such a point is not known, the returned map is empty.
*/
std::map<VariableType, CoefficientType> getViolatedPoint() const;
/*!
* Sets a point in the region for which the considered property is not satisfied.
*/
void setViolatedPoint(std::map<VariableType, CoefficientType> const& violatedPoint);
/*!
* Retrieves a point in the region for which is considered property is satisfied.
* If such a point is not known, the returned map is empty.
*/
std::map<VariableType, CoefficientType> getSatPoint() const;
/*!
* Sets a point in the region for which the considered property is satisfied.
*/
void setSatPoint(std::map<VariableType, CoefficientType> const& satPoint);
//returns the currently set check result as a string
std::string checkResultToString() const;
//returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
std::string toString() const;
/*
* Can be used to parse a single parameter with its bounds from a string of the form "0.3<=p<=0.5".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
* The results will be inserted in the given maps
*
*/
static void parseParameterBounds(
std::map<VariableType, CoefficientType>& lowerBounds,
std::map<VariableType, CoefficientType>& upperBounds,
std::string const& parameterBoundsString
);
/*
* Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static ParameterRegion parseRegion(
std::string const& regionString
);
/*
* Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static std::vector<ParameterRegion> parseMultipleRegions(
std::string const& regionsString
);
/*
* Retrieves the regions that are specified in the settings.
*/
static std::vector<ParameterRegion> getRegionsFromSettings();
private:
void init();
std::map<VariableType, CoefficientType> const lowerBounds;
std::map<VariableType, CoefficientType> const upperBounds;
std::set<VariableType> variables;
RegionCheckResult checkResult;
std::map<VariableType, CoefficientType> satPoint;
std::map<VariableType, CoefficientType> violatedPoint;
};
VariableSubstitutionType const lowerBounds;
VariableSubstitutionType const upperBounds;
std::set<VariableType> variables;
RegionCheckResult checkResult;
VariableSubstitutionType satPoint;
VariableSubstitutionType violatedPoint;
};
} //namespace region
}
}

42
src/modelchecker/region/RegionCheckResult.cpp
View File

@ -0,0 +1,42 @@
/*
* File: RegionCheckResult.cpp
* Author: tim
*
* Created on September 9, 2015, 1:56 PM
*/
#include "RegionCheckResult.h"
#include "src/utility/macros.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
namespace region {
std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult) {
switch (regionCheckResult) {
case RegionCheckResult::UNKNOWN:
os << "Unknown";
break;
case RegionCheckResult::EXISTSSAT:
os << "ExistsSat";
break;
case RegionCheckResult::EXISTSVIOLATED:
os << "ExistsViolated";
break;
case RegionCheckResult::EXISTSBOTH:
os << "ExistsBoth";
break;
case RegionCheckResult::ALLSAT:
os << "AllSat";
break;
case RegionCheckResult::ALLVIOLATED:
os << "AllViolated";
break;
default:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check result. The case has not been implemented");
}
return os;
}
}
}
}

34
src/modelchecker/region/RegionCheckResult.h
View File

@ -0,0 +1,34 @@
/*
* File: RegionCheckResult.h
* Author: tim
*
* Created on September 9, 2015, 1:56 PM
*/
#ifndef STORM_MODELCHECKER_REGION_REGIONCHECKRESULT_H
#define STORM_MODELCHECKER_REGION_REGIONCHECKRESULT_H
#include <ostream>
namespace storm {
namespace modelchecker {
namespace region {
/*!
* The possible results for a single Parameter region
*/
enum class RegionCheckResult {
UNKNOWN, /*!< the result is unknown */
EXISTSSAT, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
EXISTSVIOLATED, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
EXISTSBOTH, /*!< the formula is satisfied for some parameters but also violated for others */
ALLSAT, /*!< the formula is satisfied for all parameters in the given region */
ALLVIOLATED /*!< the formula is violated for all parameters in the given region */
};
std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult);
}
}
}
#endif /* STORM_MODELCHECKER_REGION_REGIONCHECKRESULT_H */

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

@ -8,173 +8,175 @@
#include "src/modelchecker/region/SamplingModel.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/macros.h"
#include "src/utility/region.h"
#include "src/utility/vector.h"
#include "src/utility/regions.h"
#include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "models/sparse/StandardRewardModel.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::SamplingModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
if(this->formula->isEventuallyFormula()){
this->computeRewards=false;
} else if(this->formula->isReachabilityRewardFormula()){
this->computeRewards=true;
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Sampling model only supports eventually or reachability reward formulae.");
}
//Start with the probabilities
storm::storage::SparseMatrix<ConstantType> probabilityMatrix;
std::vector<TableEntry*> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability matrix entry.
// For the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table.
TableEntry constantEntry; //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later)
initializeProbabilities(parametricModel, probabilityMatrix, matrixEntryToEvalTableMapping, &constantEntry);
//Now consider rewards
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ConstantType>> rewardModels;
std::vector<TableEntry*> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
if(this->computeRewards){
boost::optional<std::vector<ConstantType>> stateRewards;
initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, &constantEntry);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(std::move(stateRewards))));
}
//Obtain other model ingredients and the sampling model itself
storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling());
boost::optional<storm::storage::SparseMatrix<ConstantType>> noTransitionRewards;
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> noChoiceLabeling;
this->model=std::make_shared<storm::models::sparse::Dtmc<ConstantType>>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling));
//translate the matrixEntryToEvalTableMapping into the actual probability mapping
auto sampleModelEntry = this->model->getTransitionMatrix().begin();
auto parModelEntry = parametricModel.getTransitionMatrix().begin();
for(auto tableEntry : 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(tableEntry == &constantEntry){
sampleModelEntry->setValue(storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parModelEntry->getValue())));
template<typename ParametricSparseModelType, typename ConstantType>
SamplingModel<ParametricSparseModelType, ConstantType>::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
if(this->formula->isEventuallyFormula()){
this->computeRewards=false;
} else if(this->formula->isReachabilityRewardFormula()){
this->computeRewards=true;
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only");
} else {
this->probabilityMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelEntry));
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Sampling model only supports eventually or reachability reward formulae.");
}
//Start with the probabilities
storm::storage::SparseMatrix<ConstantType> probabilityMatrix;
std::vector<TableEntry*> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability matrix entry.
// For the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table.
TableEntry constantEntry; //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later)
initializeProbabilities(parametricModel, probabilityMatrix, matrixEntryToEvalTableMapping, &constantEntry);
//Now consider rewards
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ConstantType>> rewardModels;
std::vector<TableEntry*> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
if(this->computeRewards){
boost::optional<std::vector<ConstantType>> stateRewards;
initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, &constantEntry);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(std::move(stateRewards))));
}
//Obtain other model ingredients and the sampling model itself
storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling());
boost::optional<storm::storage::SparseMatrix<ConstantType>> noTransitionRewards;
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> noChoiceLabeling;
this->model=std::make_shared<storm::models::sparse::Dtmc<ConstantType>>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling));
//translate the matrixEntryToEvalTableMapping into the actual probability mapping
auto sampleModelEntry = this->model->getTransitionMatrix().begin();
auto parModelEntry = parametricModel.getTransitionMatrix().begin();
for(auto tableEntry : 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(tableEntry == &constantEntry){
sampleModelEntry->setValue(storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parModelEntry->getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelEntry));
}
++sampleModelEntry;
++parModelEntry;
}
//also do this for the rewards
if(this->computeRewards){
auto sampleModelStateRewardEntry = this->model->getUniqueRewardModel()->second.getStateRewardVector().begin();
for(auto tableEntry : rewardEntryToEvalTableMapping){
if(tableEntry != &constantEntry){
this->stateRewardMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelStateRewardEntry));
}
++sampleModelStateRewardEntry;
}
}
++sampleModelEntry;
++parModelEntry;
}
//also do this for the rewards
if(this->computeRewards){
auto sampleModelStateRewardEntry = this->model->getUniqueRewardModel()->second.getStateRewardVector().begin();
for(auto tableEntry : rewardEntryToEvalTableMapping){
if(tableEntry != &constantEntry){
this->stateRewardMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelStateRewardEntry));
template<typename ParametricSparseModelType, typename ConstantType>
void SamplingModel<ParametricSparseModelType, ConstantType>::initializeProbabilities(ParametricSparseModelType const& parametricModel,
storm::storage::SparseMatrix<ConstantType>& probabilityMatrix,
std::vector<TableEntry*>& matrixEntryToEvalTableMapping,
TableEntry* constantEntry) {
// Run through the rows of the original model and obtain the probability evaluation table, a matrix with dummy entries and the mapping between the two.
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates(), parametricModel.getTransitionMatrix().getEntryCount());
matrixEntryToEvalTableMapping.reserve(parametricModel.getTransitionMatrix().getEntryCount());
std::size_t numOfNonConstEntries=0;
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
ConstantType dummyEntry=storm::utility::one<ConstantType>();
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
if(storm::utility::isConstant(entry.getValue())){
matrixEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(entry.getValue(), storm::utility::zero<ConstantType>())).first;
matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
matrixBuilder.addNextValue(row,entry.getColumn(), dummyEntry);
dummyEntry=storm::utility::zero<ConstantType>();
}
++sampleModelStateRewardEntry;
}
this->probabilityMapping.reserve(numOfNonConstEntries);
probabilityMatrix=matrixBuilder.build();
}
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
storm::storage::SparseMatrix<ConstantType>& probabilityMatrix,
std::vector<TableEntry*>& matrixEntryToEvalTableMapping,
TableEntry* constantEntry) {
// Run through the rows of the original model and obtain the probability evaluation table, a matrix with dummy entries and the mapping between the two.
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates(), parametricModel.getTransitionMatrix().getEntryCount());
matrixEntryToEvalTableMapping.reserve(parametricModel.getTransitionMatrix().getEntryCount());
std::size_t numOfNonConstEntries=0;
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
ConstantType dummyEntry=storm::utility::one<ConstantType>();
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
if(storm::utility::isConstant(entry.getValue())){
matrixEntryToEvalTableMapping.emplace_back(constantEntry);
template<typename ParametricSparseModelType, typename ConstantType>
void SamplingModel<ParametricSparseModelType, ConstantType>::initializeRewards(ParametricSparseModelType const& parametricModel,
boost::optional<std::vector<ConstantType>>& stateRewards,
std::vector<TableEntry*>& rewardEntryToEvalTableMapping,
TableEntry* constantEntry) {
// run through the state reward vector of the parametric model. Constant entries can be set directly. Parametric entries are inserted into the table
std::vector<ConstantType> stateRewardsAsVector(parametricModel.getNumberOfStates());
rewardEntryToEvalTableMapping.reserve(parametricModel.getNumberOfStates());
std::size_t numOfNonConstEntries=0;
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){
stateRewardsAsVector[state] = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state]));
rewardEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(entry.getValue(), storm::utility::zero<ConstantType>())).first;
matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero<ConstantType>())).first;
rewardEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
matrixBuilder.addNextValue(row,entry.getColumn(), dummyEntry);
dummyEntry=storm::utility::zero<ConstantType>();
}
}
this->probabilityMapping.reserve(numOfNonConstEntries);
probabilityMatrix=matrixBuilder.build();
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
boost::optional<std::vector<ConstantType>>& stateRewards,
std::vector<TableEntry*>& rewardEntryToEvalTableMapping,
TableEntry* constantEntry) {
// run through the state reward vector of the parametric model. Constant entries can be set directly. Parametric entries are inserted into the table
std::vector<ConstantType> stateRewardsAsVector(parametricModel.getNumberOfStates());
rewardEntryToEvalTableMapping.reserve(parametricModel.getNumberOfStates());
std::size_t numOfNonConstEntries=0;
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){
stateRewardsAsVector[state] = storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state]));
rewardEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero<ConstantType>())).first;
rewardEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
this->stateRewardMapping.reserve(numOfNonConstEntries);
stateRewards=std::move(stateRewardsAsVector);
}
this->stateRewardMapping.reserve(numOfNonConstEntries);
stateRewards=std::move(stateRewardsAsVector);
}
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::~SamplingModel() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::getModel() const {
return this->model;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::instantiate(std::map<VariableType, CoefficientType>const& point) {
//write entries into evaluation tables
for(auto& tableEntry : this->probabilityEvaluationTable){
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(tableEntry.first, point));
}
for(auto& tableEntry : this->rewardEvaluationTable){
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(tableEntry.first, point));
template<typename ParametricSparseModelType, typename ConstantType>
SamplingModel<ParametricSparseModelType, ConstantType>::~SamplingModel() {
//Intentionally left empty
}
//write the instantiated values to the matrix according to the mappings
for(auto& mappingPair : this->probabilityMapping){
mappingPair.second->setValue(*(mappingPair.first));
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> const& SamplingModel<ParametricSparseModelType, ConstantType>::getModel() const {
return this->model;
}
if(this->computeRewards){
for(auto& mappingPair : this->stateRewardMapping){
*mappingPair.second=*mappingPair.first;
template<typename ParametricSparseModelType, typename ConstantType>
void SamplingModel<ParametricSparseModelType, ConstantType>::instantiate(std::map<VariableType, CoefficientType>const& point) {
//write entries into evaluation tables
for(auto& tableEntry : this->probabilityEvaluationTable){
tableEntry.second=storm::utility::region::convertNumber<ConstantType>(
storm::utility::region::evaluateFunction(tableEntry.first, point));
}
for(auto& tableEntry : this->rewardEvaluationTable){
tableEntry.second=storm::utility::region::convertNumber<ConstantType>(
storm::utility::region::evaluateFunction(tableEntry.first, point));
}
}
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::computeValues() {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(*this->model);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr;
//perform model checking on the dtmc
if(this->computeRewards){
resultPtr = modelChecker.computeReachabilityRewards(this->formula->asReachabilityRewardFormula());
//write the instantiated values to the matrix according to the mappings
for(auto& mappingPair : this->probabilityMapping){
mappingPair.second->setValue(*(mappingPair.first));
}
if(this->computeRewards){
for(auto& mappingPair : this->stateRewardMapping){
*mappingPair.second=*mappingPair.first;
}
}
}
else {
resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asEventuallyFormula());
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> const& SamplingModel<ParametricSparseModelType, ConstantType>::computeValues() {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(*this->model);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr;
//perform model checking on the dtmc
if(this->computeRewards){
resultPtr = modelChecker.computeReachabilityRewards(this->formula->asReachabilityRewardFormula());
}
else {
resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asEventuallyFormula());
}
return resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
return resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SamplingModel<storm::models::sparse::Dtmc<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>, double>;
#endif
} //namespace region
}
}

122
src/modelchecker/region/SamplingModel.h
View File

@ -9,75 +9,73 @@
#define STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H
#include <unordered_map>
#include <memory>
#include "src/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "src/utility/region.h"
#include "src/logic/Formulas.h"
#include "src/models/sparse/Dtmc.h"
#include "src/storage/SparseMatrix.h"
namespace storm {
namespace modelchecker{
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class SamplingModel {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::Formula> formula);
virtual ~SamplingModel();
/*!
* returns the underlying model
*/
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> const& getModel() const;
/*!
* Instantiates the underlying model according to the given point
*/
void instantiate(std::map<VariableType, CoefficientType>const& point);
/*!
* Returns the reachability probabilities for every state according to the current instantiation.
* Undefined behavior if model has not been instantiated first!
*/
std::vector<ConstantType> const& computeValues();
private:
typedef typename std::unordered_map<ParametricType, ConstantType>::value_type TableEntry;
void initializeProbabilities(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<TableEntry*>& matrixEntryToEvalTableMapping, TableEntry* constantEntry);
void initializeRewards(ParametricSparseModelType const& parametricModel, boost::optional<std::vector<ConstantType>>& stateRewards, std::vector<TableEntry*>& rewardEntryToEvalTableMapping, TableEntry* constantEntry);
//The model with which we work
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> model;
//The formula for which we will compute the values
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
// We store one (unique) entry for every occurring function.
// Whenever a sampling point is given, we can then evaluate the functions
// and store the result to the target value of this map
std::unordered_map<ParametricType, ConstantType> probabilityEvaluationTable;
std::unordered_map<ParametricType, ConstantType> rewardEvaluationTable;
//This Vector connects the probability evaluation table with the probability matrix of the model.
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
std::vector<std::pair<ConstantType*, typename std::vector<ConstantType>::iterator>> stateRewardMapping;
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType CoefficientType;
SamplingModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula);
virtual ~SamplingModel();
/*!
* returns the underlying model
*/
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> const& getModel() const;
/*!
* Instantiates the underlying model according to the given point
*/
void instantiate(std::map<VariableType, CoefficientType>const& point);
/*!
* Returns the reachability probabilities for every state according to the current instantiation.
* Undefined behavior if model has not been instantiated first!
*/
std::vector<ConstantType> const& computeValues();
private:
typedef typename std::unordered_map<ParametricType, ConstantType>::value_type TableEntry;
void initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<TableEntry*>& matrixEntryToEvalTableMapping, TableEntry* constantEntry);
void initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, boost::optional<std::vector<ConstantType>>& stateRewards, std::vector<TableEntry*>& rewardEntryToEvalTableMapping, TableEntry* constantEntry);
//The model with which we work
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> model;
//The formula for which we will compute the values
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
// We store one (unique) entry for every occurring function.
// Whenever a sampling point is given, we can then evaluate the functions
// and store the result to the target value of this map
std::unordered_map<ParametricType, ConstantType> probabilityEvaluationTable;
std::unordered_map<ParametricType, ConstantType> rewardEvaluationTable;
//This Vector connects the probability evaluation table with the probability matrix of the model.
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
std::vector<std::pair<ConstantType*, typename std::vector<ConstantType>::iterator>> stateRewardMapping;
};
};
} //namespace region
}
}
#endif /* STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H */

1555
src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
File diff suppressed because it is too large
View File

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

@ -1,289 +1,155 @@
#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_
#define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_
#include<memory>
#include "src/modelchecker/region/AbstractSparseRegionModelChecker.h"
#include "src/storage/sparse/StateType.h"
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/utility/constants.h"
#include "src/utility/regions.h"
#include "src/solver/Smt2SmtSolver.h"
#include "src/models/sparse/Dtmc.h"
#include "src/utility/region.h"
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "src/solver/Smt2SmtSolver.h"
namespace storm {
namespace modelchecker {
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::regions::VariableType<ParametricType> VariableType;
typedef typename storm::utility::regions::CoefficientType<ParametricType> CoefficientType;
/*!
* The possible results for a single Parameter region
*/
enum class RegionCheckResult {
UNKNOWN, /*!< the result is unknown */
EXISTSSAT, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
EXISTSVIOLATED, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
EXISTSBOTH, /*!< the formula is satisfied for some parameters but also violated for others */
ALLSAT, /*!< the formula is satisfied for all parameters in the given region */
ALLVIOLATED /*!< the formula is violated for all parameters in the given region */
};
class ParameterRegion;
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker : public AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType> {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename ParametricSparseModelType::RewardModelType ParametricRewardModelType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
explicit SparseDtmcRegionModelChecker(ParametricSparseModelType const& model);
virtual ~SparseDtmcRegionModelChecker();
/*!
* Checks if the given formula can be handled by This region model checker
* @param formula the formula to be checked
*/
virtual bool canHandle(storm::logic::Formula const& formula) const;
/*!
* Returns the reachability function.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ParametricType> const& getReachabilityFunction();
explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model);
virtual ~SparseDtmcRegionModelChecker();
/*!
* 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.
*/
virtual ConstantType getReachabilityValue(std::map<VariableType, CoefficientType>const& point, bool evaluateFunction=false);
/*!
* Evaluates the reachability function with the given substitution.
* Makes some checks for the case that the result should be constant.
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
*/
CoefficientType evaluateReachabilityFunction(std::map<VariableType, CoefficientType>const& point);
/*!
* Checks if the given formula can be handled by This region model checker
* @param formula the formula to be checked
*/
bool canHandle(storm::logic::Formula const& formula) const;
/*!
* Specifies the considered formula.
* A few preprocessing steps are performed.
* If another formula has been specified before, all 'context' regarding the old formula is lost.
*
* @param formula the formula to be considered.
*/
void specifyFormula(std::shared_ptr<storm::logic::Formula> formula);
protected:
/*!
* Checks whether the approximation technique is applicable and whether the model checking result is independent of parameters (i.e., constant)
*
* Computes a model with a single target and at most one sink state.
* Eliminates all states for which the outgoing transitions are constant.
* If rewards are relevant, transition rewards are transformed to state rewards
*
* @note this->specifiedFormula and this->computeRewards has to be set accordingly before calling this function
*/
virtual void preprocess(std::shared_ptr<ParametricSparseModelType>& simpleModel, std::shared_ptr<storm::logic::Formula>& simpleFormula, bool& isApproximationApplicable, bool& isResultConstant);
/*!
* 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 checkRegions(std::vector<ParameterRegion>& regions);
/*!
* 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 checkRegion(ParameterRegion& region);
/*!
* Returns the reachability function.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ParametricType> 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 <typename ValueType>
ValueType getReachabilityValue(std::map<VariableType, CoefficientType>const& point, bool evaluateFunction=false);
/*!
* Prints statistical information to the given stream.
*/
void printStatisticsToStream(std::ostream& outstream);
private:
class ApproximationModel;
class SamplingModel;
/*!
* 1. Analyzes the formula (sets this->specifiedFormulaBound, this->specifiedFormulaCompType)
*
* 2. Checks whether the approximation technique is applicable and whether the model checking result is independent of parameters (i.e., constant)
* The flags of This model checker are set accordingly.
*
* 3. Computes a model with a single target and at most one sink state.
* Eliminates all states for which the outgoing transitions are constant.
* If rewards are relevant, transition rewards are transformed to state rewards
*
* @note this->specifiedFormula has to be set accordingly, before calling this function
*/
void preprocess();
/*!
* Does some sanity checks and preprocessing steps on the currently specified model and
* reachability probability formula, i.e.,
* * Sets some formula data and that we do not compute rewards
* * Computes maybeStates and targetStates
* * Sets the flags that state whether the result is constant and approximation is applicable
*
* @note The returned set of target states also includes states where an 'actual' target state is reached with probability 1
*
*/
void preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates);
/*!
* Does some sanity checks and preprocessing steps on the currently specified model and
* reachability reward formula, i.e.
* * Sets some formula data and that we do compute rewards
* * Computes maybeStates, targetStates
* * Computes a new stateReward vector that considers state+transition rewards of the original model. (in a sense that we can abstract away from transition rewards)
* * Sets the flags that state whether the result is constant and approximation is applicable
*
* @note stateRewards.size will equal to maybeStates.numberOfSetBits
*
*/
void preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector<ParametricType>& stateRewards);
/*!
* initializes the Approximation Model
*
* @note does not check whether approximation can be applied
*/
void initializeApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& model, std::shared_ptr<storm::logic::Formula> formula);
/*!
* initializes the Sampling Model
*/
void initializeSamplingModel(storm::models::sparse::Dtmc<ParametricType> const& model, std::shared_ptr<storm::logic::Formula> formula);
/*!
* Computes the reachability function via state elimination
* @note computeFlagsAndSimplifiedModel should be called before calling this
*/
void computeReachabilityFunction(storm::models::sparse::Dtmc<ParametricType> const& simpleModel);
/*!
* Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability (or reachability reward).
* If the current region result is EXISTSSAT (or EXISTSVIOLATED), then this function tries to prove ALLSAT (or ALLVIOLATED).
* If this succeeded, then the region check result is changed accordingly.
* If the current region result is UNKNOWN, then this function first tries to prove ALLSAT and if that failed, it tries to prove ALLVIOLATED.
* In any case, the computed bounds are written to the given lowerBounds/upperBounds.
* However, if only the lowerBounds (or upperBounds) have been computed, the other vector is set to a vector of size 0.
* True is returned iff either ALLSAT or ALLVIOLATED could be proved.
*/
bool checkApproximativeValues(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds);
/*!
* Returns the approximation model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ApproximationModel> const& getApproximationModel();
/*!
* Checks the value of the function at some sampling points within the given region.
* May set the satPoint and violatedPoint of the regions if they are not yet specified and such points are found
* Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH
*
* @return true if an violated point as well as a sat point has been found during the process
*/
bool checkSamplePoints(ParameterRegion& region);
/*!
* Checks the value of the function at the given sampling point.
* 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
*
* @param favorViaFunction if not stated otherwise (e.g. in the settings), the sampling will be done via the
* reachabilityFunction 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
*/
bool checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction=false);
/*!
* Returns the sampling model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<SamplingModel> const& getSamplingModel();
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
* Otherwise, a sampingPoint will be computed.
* True is returned iff the solver was successful (i.e., it returned sat or unsat)
* A Sat- or Violated point is set, if the solver has found one (not yet implemented!).
* The region checkResult of the given region is changed accordingly.
*/
bool checkFullSmt(ParameterRegion& region);
//initializes this->smtSolver which can later be used to give an exact result regarding the whole model.
void initializeSMTSolver();
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
template <typename ValueType>
bool valueIsInBoundOfFormula(ValueType const& value);
// The model this model checker is supposed to analyze.
storm::models::sparse::Dtmc<ParametricType> const& model;
//classes that provide auxilliary functions
// Instance of an elimination model checker to access its functions
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>> eliminationModelChecker;
//the following members depend on the currently specified formula:
//the currently specified formula, the bound and the comparison type
std::shared_ptr<storm::logic::Formula> specifiedFormula;
bool computeRewards;
storm::logic::ComparisonType specifiedFormulaCompType;
double specifiedFormulaBound;
// the original model after states with constant transitions have been eliminated
std::shared_ptr<storm::models::sparse::Dtmc<ParametricType>> simpleModel;
// a formula that can be checked on the simplified model
std::shared_ptr<storm::logic::Formula> simpleFormula;
// the model that is used to approximate the reachability values
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 (or: reachability reward) in the initial state
std::shared_ptr<ParametricType> reachabilityFunction;
// a flag that is true if there are only linear functions at transitions of the model
bool isApproximationApplicable;
// a flag that is true iff the resulting reachability function is constant
bool isResultConstant;
// workaround to represent that the result is infinity (utility::infinity<storm::RationalFunction>() does not work at this moment)
bool isResultInfinity;
// the smt solver that is used to prove properties with the help of the reachabilityFunction
std::shared_ptr<storm::solver::Smt2SmtSolver> smtSolver;
// runtimes and other information for statistics.
uint_fast64_t numOfCheckedRegions;
uint_fast64_t numOfRegionsSolvedThroughApproximation;
uint_fast64_t numOfRegionsSolvedThroughSampling;
uint_fast64_t numOfRegionsSolvedThroughFullSmt;
uint_fast64_t numOfRegionsExistsBoth;
uint_fast64_t numOfRegionsAllSat;
uint_fast64_t numOfRegionsAllViolated;
std::chrono::high_resolution_clock::duration timeSpecifyFormula;
std::chrono::high_resolution_clock::duration timePreprocessing;
std::chrono::high_resolution_clock::duration timeInitApproxModel;
std::chrono::high_resolution_clock::duration timeInitSamplingModel;
std::chrono::high_resolution_clock::duration timeComputeReachabilityFunction;
std::chrono::high_resolution_clock::duration timeCheckRegion;
std::chrono::high_resolution_clock::duration timeSampling;
std::chrono::high_resolution_clock::duration timeApproximation;
std::chrono::high_resolution_clock::duration timeMDPBuild;
std::chrono::high_resolution_clock::duration timeFullSmt;
};
private:
/*!
* Does some sanity checks and preprocessing steps on the currently specified model and
* reachability probability formula, i.e.,
* * Sets some formula data and that we do not compute rewards
* * Computes maybeStates and targetStates
* * Sets the flags that state whether the result is constant and approximation is applicable
*
* @note The returned set of target states also includes states where an 'actual' target state is reached with probability 1
*
*/
void preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, bool& isApproximationApplicable, bool& isResultConstant);
/*!
* Does some sanity checks and preprocessing steps on the currently specified model and
* reachability reward formula, i.e.
* * Sets some formula data and that we do compute rewards
* * Computes maybeStates, targetStates
* * Computes a new stateReward vector that considers state+transition rewards of the original model. (in a sense that we can abstract away from transition rewards)
* * Sets the flags that state whether the result is constant and approximation is applicable
*
* @note stateRewards.size will equal to maybeStates.numberOfSetBits
*
*/
void preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector<ParametricType>& stateRewards, bool& isApproximationApplicable, bool& isResultConstant);
/*!
* Computes the reachability function via state elimination
* @note computeFlagsAndSimplifiedModel should be called before calling this
*/
void computeReachabilityFunction(ParametricSparseModelType const& simpleModel);
/*!
* Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability (or reachability reward).
* If the current region result is EXISTSSAT (or EXISTSVIOLATED), then this function tries to prove ALLSAT (or ALLVIOLATED).
* If this succeeded, then the region check result is changed accordingly.
* If the current region result is UNKNOWN, then this function first tries to prove ALLSAT and if that failed, it tries to prove ALLVIOLATED.
* In any case, the computed bounds are written to the given lowerBounds/upperBounds.
* However, if only the lowerBounds (or upperBounds) have been computed, the other vector is set to a vector of size 0.
* True is returned iff either ALLSAT or ALLVIOLATED could be proved.
*/
virtual bool checkApproximativeValues(ParameterRegion<ParametricType>& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds);
/*!
* Checks the value of the function at the given sampling point.
* 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
*
* @param favorViaFunction if not stated otherwise (e.g. in the settings), the sampling will be done via the
* reachabilityFunction 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
*/
virtual bool checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction=false);
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
* Otherwise, a sampingPoint will be computed.
* True is returned iff the solver was successful (i.e., it returned sat or unsat)
* A Sat- or Violated point is set, if the solver has found one (not yet implemented!).
* The region checkResult of the given region is changed accordingly.
*/
bool checkSmt(ParameterRegion<ParametricType>& region);
//initializes this->smtSolver which can later be used to give an exact result regarding the whole model.
void initializeSMTSolver();
// The function for the reachability probability (or: reachability reward) in the initial state
std::shared_ptr<ParametricType> reachabilityFunction;
// workaround to represent that the result is infinity (utility::infinity<storm::RationalFunction>() does not work at this moment)
bool isResultInfinity;
// Instance of an elimination model checker to access its functions
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>> eliminationModelChecker;
// the smt solver that is used to prove properties with the help of the reachabilityFunction
std::shared_ptr<storm::solver::Smt2SmtSolver> smtSolver;
};
} //namespace region
} // namespace modelchecker
} // namespace storm

2
src/utility/regions.h → src/utility/region.h
View File

@ -30,7 +30,7 @@
namespace storm {
namespace utility{
namespace regions {
namespace region {
#ifdef STORM_HAVE_CARL
template<typename FunctionType>

4
src/utility/regions.cpp
View File

@ -7,7 +7,7 @@
#include <string>
#include "src/utility/regions.h"
#include "src/utility/region.h"
#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/settings/SettingsManager.h"
@ -21,7 +21,7 @@
namespace storm {
namespace utility{
namespace regions {
namespace region {
template<>
double convertNumber<double, double>(double const& number){

6
src/utility/storm.h
View File

@ -249,8 +249,8 @@ namespace storm {
if(storm::settings::generalSettings().isParametricRegionSet()){
std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << std::endl;
auto regions=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::getRegionsFromSettings();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
auto regions=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::getRegionsFromSettings();
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) {
modelchecker.specifyFormula(formula);
modelchecker.checkRegions(regions);
@ -259,7 +259,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric region check engine currently does not support this property.");
}
// for(auto const& reg : regions){
// std::cout << reg.toString() << " Result: " << reg.checkResultToString() << std::endl;
// std::cout << reg.toString() << " Result: " << reg.getCheckResult() << std::endl;
// }
modelchecker.printStatisticsToStream(std::cout);

298
test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
View File

@ -37,27 +37,27 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
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);
@ -65,26 +65,26 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -106,32 +106,32 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue<double>(exBothHardRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue<double>(exBothHardRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue<double>(exBothHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue<double>(exBothHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
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);
@ -139,44 +139,44 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH)) ||
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSVIOLATED))
(exBothHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::EXISTSBOTH)) ||
(exBothHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::EXISTSVIOLATED))
);
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75");
auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75");
auto exBothHardRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//test smt + approx
auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto exBothHardRegionSmtApp=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
@ -199,15 +199,15 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("");
EXPECT_EQ(storm::utility::infinity<double>(), modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false)); //instantiation of sampling model
EXPECT_EQ(storm::utility::infinity<double>(), modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true)); //instantiation of sampling model
EXPECT_EQ(storm::utility::infinity<double>(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false)); //instantiation of sampling model
EXPECT_EQ(storm::utility::infinity<double>(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true)); //instantiation of sampling model
//test approximative method
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF);
@ -215,16 +215,16 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -246,21 +246,21 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::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<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
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);
@ -268,26 +268,26 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -309,28 +309,28 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue<double>(allVioHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue<double>(allVioHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
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);
@ -338,44 +338,44 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED)) ||
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSVIOLATED))
(allVioHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::ALLVIOLATED)) ||
(allVioHardRegion.getCheckResult()==(storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult());
//test smt + approx
auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
auto allVioHardRegionSmtApp=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -397,23 +397,23 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8");
EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
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);
@ -421,26 +421,26 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9");
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -462,17 +462,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("");
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
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);
@ -480,16 +480,16 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::region::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}

Write Preview
Loading…
Cancel
Save