diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index ab2753c16..d2ad1570f 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -9,8 +9,10 @@ //forward declaration of friend class namespace storm { namespace modelchecker { - template - class SparseDtmcRegionModelChecker; + namespace region { + template + class SparseDtmcRegionModelChecker; + } } } @@ -19,7 +21,7 @@ namespace storm { template class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker { - template friend class storm::modelchecker::SparseDtmcRegionModelChecker; + template friend class storm::modelchecker::region::SparseDtmcRegionModelChecker; public: typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp new file mode 100644 index 000000000..4e464fd84 --- /dev/null +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -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 + AbstractSparseRegionModelChecker::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 + AbstractSparseRegionModelChecker::~AbstractSparseRegionModelChecker() { + //Intentionally left empty + } + + template + ParametricSparseModelType const& AbstractSparseRegionModelChecker::getModel() const { + return this->model; + } + + template + bool const& AbstractSparseRegionModelChecker::isResultConstant() const { + return this->resultConstant; + } + + template + std::shared_ptr const& AbstractSparseRegionModelChecker::getSimpleModel() const { + return this->simpleModel; + } + + template + bool const& AbstractSparseRegionModelChecker::isComputeRewards() const { + return computeRewards; + } + + template + std::shared_ptr const& AbstractSparseRegionModelChecker::getSpecifiedFormula() const { + return specifiedFormula; + } + + template + ConstantType const& AbstractSparseRegionModelChecker::getSpecifiedFormulaBound() const { + return specifiedFormulaBound; + } + + template + storm::logic::ComparisonType const& AbstractSparseRegionModelChecker::getSpecifiedFormulaCompType() const { + return specifiedFormulaCompType; + } + + template + bool AbstractSparseRegionModelChecker::specifiedFormulaHasUpperBound() const { + return !storm::logic::isLowerBound(this->getSpecifiedFormulaCompType()); + } + + + + template + void AbstractSparseRegionModelChecker::specifyFormula(std::shared_ptr 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(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 + void AbstractSparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr 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>(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 + void AbstractSparseRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now(); + this->samplingModel=std::make_shared>(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 + void AbstractSparseRegionModelChecker::checkRegions(std::vector>& regions) { + STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); + std::cout << "Checking " << regions.size() << " regions. Progress: "; + std::cout.flush(); + + uint_fast64_t progress=0; + uint_fast64_t checkedRegions=0; + for(auto& region : regions){ + this->checkRegion(region); + if((checkedRegions++)*10/regions.size()==progress){ + std::cout << progress++; + std::cout.flush(); + } + } + std::cout << " done!" << std::endl; + } + + template + void AbstractSparseRegionModelChecker::checkRegion(ParameterRegion& 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 lowerBounds; + std::vector 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 + std::shared_ptr> const& AbstractSparseRegionModelChecker::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 + bool AbstractSparseRegionModelChecker::checkSamplePoints(ParameterRegion& 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 + std::shared_ptr> const& AbstractSparseRegionModelChecker::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 + bool AbstractSparseRegionModelChecker::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 + bool AbstractSparseRegionModelChecker::valueIsInBoundOfFormula(CoefficientType const& value){ + return valueIsInBoundOfFormula(storm::utility::region::convertNumber(value)); + } + + template + void AbstractSparseRegionModelChecker::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(this->timeSpecifyFormula); + std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast(this->timePreprocessing); + std::chrono::milliseconds timeInitSamplingModelInMilliseconds = std::chrono::duration_cast(this->timeInitSamplingModel); + std::chrono::milliseconds timeInitApproxModelInMilliseconds = std::chrono::duration_cast(this->timeInitApproxModel); + std::chrono::milliseconds timeComputeReachabilityFunctionInMilliseconds = std::chrono::duration_cast(this->timeComputeReachabilityFunction); + std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast(this->timeCheckRegion); + std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast(this->timeSampling); + std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast(this->timeApproximation); + std::chrono::milliseconds timeApproxModelInstantiationInMilliseconds = std::chrono::duration_cast(this->timeApproxModelInstantiation); + std::chrono::milliseconds timeSmtInMilliseconds = std::chrono::duration_cast(this->timeSmt); + + std::chrono::high_resolution_clock::duration timeOverall = timeSpecifyFormula + timeCheckRegion; // + ... + std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(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>, double>; +#endif + } // namespace region + } //namespace modelchecker +} //namespace storm + diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/modelchecker/region/AbstractSparseRegionModelChecker.h new file mode 100644 index 000000000..e4bb9b08c --- /dev/null +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.h @@ -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 + +#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 + class AbstractSparseRegionModelChecker { + public: + + typedef typename ParametricSparseModelType::ValueType ParametricType; + typedef typename storm::utility::region::VariableType VariableType; + typedef typename storm::utility::region::CoefficientType 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 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>& 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& 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::mapconst& 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 const& getSimpleModel() const; + bool const& isComputeRewards() const; + std::shared_ptr 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& simpleModel, std::shared_ptr& 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& region, std::vector& lowerBounds, std::vector& upperBounds)=0; + + /*! + * Returns the approximation model. + * If it is not yet available, it is computed. + */ + std::shared_ptr> 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 + */ + virtual bool checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction=false) = 0; + + /*! + * Returns the sampling model. + * If it is not yet available, it is computed. + */ + std::shared_ptr> 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& region)=0; + + private: + /*! + * initializes the Approximation Model + * + * @note does not check whether approximation can be applied + */ + void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula); + + /*! + * initializes the Sampling Model + */ + void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula); + + // The model this model checker is supposed to analyze. + ParametricSparseModelType const& model; + //The currently specified formula + std::shared_ptr 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 simpleModel; + // a formula that can be checked on the simplified model + std::shared_ptr 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; + // the model that can be instantiated to check the value at a certain point + std::shared_ptr> 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 */ + diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 64fd10350..546f7f556 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -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 - SparseDtmcRegionModelChecker::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr 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 probabilityMatrix; - std::vector rowSubstitutions;// the substitution used in every row (required if rewards are computed) - std::vector 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> rewardModels; - std::vector 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 stateActionRewards; - initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, &constantRewEntry); - rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(boost::optional>(), boost::optional>(std::move(stateActionRewards))))); - } - //Obtain other model ingredients and the approximation model itself - storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling()); - boost::optional>> noChoiceLabeling; - this->model=std::make_shared>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); - - //translate the matrixEntryToEvalTableMapping into the actual probability mapping - typename storm::storage::SparseMatrix::index_type matrixRow=0; - auto tableEntry=matrixEntryToEvalTableMapping.begin(); - for(typename storm::storage::SparseMatrix::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){ - for (; matrixRowmodel->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(storm::utility::regions::getConstantPart(parEntry.getValue()))); - } else { - this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry)); - } - ++approxModelEntry; - ++tableEntry; - } + template + ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr 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 probabilityMatrix; + std::vector rowSubstitutions;// the substitution used in every row (required if rewards are computed) + std::vector 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> rewardModels; + std::vector 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 stateActionRewards; + initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, &constantRewEntry); + rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(boost::optional>(), boost::optional>(std::move(stateActionRewards))))); } - //Get the sets of reward parameters that map to "CHOSEOPTIMAL". - this->choseOptimalRewardPars = std::vector>(this->rewardSubstitutions.size()); - for(std::size_t index = 0; indexrewardSubstitutions.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>> noChoiceLabeling; + this->model=std::make_shared>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); + + //translate the matrixEntryToEvalTableMapping into the actual probability mapping + typename storm::storage::SparseMatrix::index_type matrixRow=0; + auto tableEntry=matrixEntryToEvalTableMapping.begin(); + for(typename storm::storage::SparseMatrix::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){ + for (; matrixRowmodel->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(storm::utility::region::getConstantPart(parEntry.getValue()))); + } else { + this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry)); + } + ++approxModelEntry; + ++tableEntry; } } } - } - } - - template - void SparseDtmcRegionModelChecker::ApproximationModel::initializeProbabilities(storm::models::sparse::Dtmcconst& parametricModel, - storm::storage::SparseMatrix& probabilityMatrix, - std::vector& rowSubstitutions, - std::vector& 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 matrixBuilder(0, parametricModel.getNumberOfStates(), 0, true, true, parametricModel.getNumberOfStates()); - this->probabilitySubstitutions.emplace_back(std::map()); //we want that the empty substitution is always the first one - std::size_t numOfNonConstEntries=0; - typename storm::storage::SparseMatrix::index_type matrixRow=0; - for(typename storm::storage::SparseMatrix::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 occurringVariables; - for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){ - storm::utility::regions::gatherOccurringVariables(entry.getValue(), occurringVariables); - } - std::size_t numOfSubstitutions=1ull< 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(); - 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())).first; - matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); + //Get the sets of reward parameters that map to "CHOSEOPTIMAL". + this->choseOptimalRewardPars = std::vector>(this->rewardSubstitutions.size()); + for(std::size_t index = 0; indexrewardSubstitutions.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(); } - ++matrixRow; } } - this->probabilityMapping.reserve(numOfNonConstEntries); - probabilityMatrix=matrixBuilder.build(); - } - - template - void SparseDtmcRegionModelChecker::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, - storm::storage::SparseMatrix const& probabilityMatrix, - std::vector const& rowSubstitutions, - std::vector& stateActionRewardVector, - std::vector& 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()); //we want that the empty substitution is always the first one - - for(std::size_t state=0; state occurringRewVariables; - std::set occurringProbVariables; - if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){ - ConstantType reward = storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])); - //Add one of these entries for every row in the row group of state - for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow + void ApproximationModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, + storm::storage::SparseMatrix& probabilityMatrix, + std::vector& rowSubstitutions, + std::vector& 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 matrixBuilder(0, parametricModel.getNumberOfStates(), 0, true, true, parametricModel.getNumberOfStates()); + this->probabilitySubstitutions.emplace_back(std::map()); //we want that the empty substitution is always the first one + std::size_t numOfNonConstEntries=0; + typename storm::storage::SparseMatrix::index_type matrixRow=0; + for(typename storm::storage::SparseMatrix::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 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 rewardSubstitution; - for(auto const& rewardVar : occurringRewVariables){ - typename std::map::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< 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(storm::utility::zero(), storm::utility::zero())) - ).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(); + 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())).first; + matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); + } + matrixBuilder.addNextValue(matrixRow, entry.getColumn(), dummyEntry); + dummyEntry=storm::utility::zero(); } - //insert table entries and dummy data - stateActionRewardVector.emplace_back(storm::utility::zero()); - rewardEntryToEvalTableMapping.emplace_back(evalTablePtr); - ++numOfNonConstRewEntries; + ++matrixRow; } } + this->probabilityMapping.reserve(numOfNonConstEntries); + probabilityMatrix=matrixBuilder.build(); } - this->rewardMapping.reserve(numOfNonConstRewEntries); - } - + template + void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel, + storm::storage::SparseMatrix const& probabilityMatrix, + std::vector const& rowSubstitutions, + std::vector& stateActionRewardVector, + std::vector& 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()); //we want that the empty substitution is always the first one - template - SparseDtmcRegionModelChecker::ApproximationModel::~ApproximationModel() { - //Intentionally left empty - } - - template - std::shared_ptr> const& SparseDtmcRegionModelChecker::ApproximationModel::getModel() const { - return this->model; - } - - template - void SparseDtmcRegionModelChecker::ApproximationModel::instantiate(const ParameterRegion& region) { - //Instantiate the substitutions - std::vector> instantiatedSubs(this->probabilitySubstitutions.size()); - for(uint_fast64_t substitutionIndex=0; substitutionIndexprobabilitySubstitutions.size(); ++substitutionIndex){ - for(std::pair 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 occurringRewVariables; + std::set occurringProbVariables; + if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){ + ConstantType reward = storm::utility::region::convertNumber(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]; matrixRowsecond.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 rewardSubstitution; + for(auto const& rewardVar : occurringRewVariables){ + typename std::map::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(storm::utility::zero(), storm::utility::zero())) + ).first; + evalTablePtr=&(*evalTableIt); + } + //insert table entries and dummy data + stateActionRewardVector.emplace_back(storm::utility::zero()); + 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( - storm::utility::regions::evaluateFunction( - tableEntry.first.getFunction(), - instantiatedSubs[tableEntry.first.getSubstitution()] - ) - ); + + + + template + ApproximationModel::~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 + std::shared_ptr> const& ApproximationModel::getModel() const { + return this->model; } - - if(this->computeRewards){ + + template + void ApproximationModel::instantiate(const ParameterRegion& region) { //Instantiate the substitutions - std::vector> instantiatedRewardSubs(this->rewardSubstitutions.size()); - for(uint_fast64_t substitutionIndex=0; substitutionIndexrewardSubstitutions.size(); ++substitutionIndex){ - for(std::pair const& sub : this->rewardSubstitutions[substitutionIndex]){ + std::vector> instantiatedSubs(this->probabilitySubstitutions.size()); + for(uint_fast64_t substitutionIndex=0; substitutionIndexprobabilitySubstitutions.size(); ++substitutionIndex){ + for(std::pair 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())); + 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(); - minMax.second=storm::utility::zero(); - //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( - storm::utility::regions::evaluateFunction( - funcSub.getFunction(), - instantiatedRewardSubs[funcSub.getSubstitution()] + for(auto& tableEntry : this->probabilityEvaluationTable){ + tableEntry.second=storm::utility::region::convertNumber( + 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 - std::vector const& SparseDtmcRegionModelChecker::ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) { - storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(*this->model); - std::unique_ptr 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> instantiatedRewardSubs(this->rewardSubstitutions.size()); + for(uint_fast64_t substitutionIndex=0; substitutionIndexrewardSubstitutions.size(); ++substitutionIndex){ + for(std::pair 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())); + 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(); + minMax.second=storm::utility::zero(); + //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( + 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 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 + std::vector const& ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) { + storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(*this->model); + std::unique_ptr 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 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().getValueVector(); } - return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); - } #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker, double>; + template class ApproximationModel>, double>; #endif + } //namespace region } } \ No newline at end of file diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index 272cc67a2..d861209ff 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -9,157 +9,156 @@ #define STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H #include +#include +#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 - class SparseDtmcRegionModelChecker; - - template - class SparseDtmcRegionModelChecker::ApproximationModel{ - - public: - - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - - /*! - * @note this will not check whether approximation is applicable - */ - ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr formula); - virtual ~ApproximationModel(); - - /*! - * returns the underlying model - */ - std::shared_ptr> 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 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 + 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 VariableType; + typedef typename storm::utility::region::CoefficientType CoefficientType; + + /*! + * @note this will not check whether approximation is applicable + */ + ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); + virtual ~ApproximationModel(); + + /*! + * returns the underlying model + */ + std::shared_ptr> 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 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()(fun); - std::size_t hs = std::hash()(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()(fun); + std::size_t hs = std::hash()(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::value_type ProbTableEntry; + typedef typename std::unordered_map, FuncSubHash>::value_type RewTableEntry; + + void initializeProbabilities(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& rowSubstitutions, std::vector& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry); + void initializeRewards(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, std::vector& stateActionRewardVector, std::vector& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry); + + //The Model with which we work + std::shared_ptr> model; + //The formula for which we will compute the values + std::shared_ptr 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 probabilityEvaluationTable; + //For rewards, we map to the minimal value and the maximal value (depending on the CHOSEOPTIMAL parameters). + std::unordered_map, FuncSubHash> rewardEvaluationTable; + + //Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region) + std::vector> 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> rewardSubstitutions; + std::vector> 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::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::iterator>> rewardMapping; + }; - - typedef typename std::unordered_map::value_type ProbTableEntry; - typedef typename std::unordered_map, FuncSubHash>::value_type RewTableEntry; - - void initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& rowSubstitutions, std::vector& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry); - void initializeRewards(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, std::vector& stateActionRewardVector, std::vector& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry); - - //The Model with which we work - std::shared_ptr> model; - //The formula for which we will compute the values - std::shared_ptr 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 probabilityEvaluationTable; - //For rewards, we map to the minimal value and the maximal value (depending on the CHOSEOPTIMAL parameters). - std::unordered_map, FuncSubHash> rewardEvaluationTable; - - //Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region) - std::vector> 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> rewardSubstitutions; - std::vector> 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::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::iterator>> rewardMapping; - - }; + } //namespace region } } diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index 6128e7c9b..b7bf64e76 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -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 - SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map const& lowerBounds, std::map const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { - init(); - } - - template - SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map&& lowerBounds, std::map&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) { - init(); - } - - template - void SparseDtmcRegionModelChecker::ParameterRegion::init() { - //check whether both mappings map the same variables, check that lowerbound <= upper bound, and pre-compute the set of variables - for (auto const& variableWithLowerBound : this->lowerBounds) { - auto variableWithUpperBound = this->upperBounds.find(variableWithLowerBound.first); - STORM_LOG_THROW((variableWithUpperBound != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithLowerBound.first); - STORM_LOG_THROW((variableWithLowerBound.second<=variableWithUpperBound->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower bound for " << variableWithLowerBound.first << " is larger then the upper bound"); - this->variables.insert(variableWithLowerBound.first); + template + ParameterRegion::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 + ParameterRegion::ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) { + init(); } - } - - template - SparseDtmcRegionModelChecker::ParameterRegion::~ParameterRegion() { - //Intentionally left empty - } - - template - std::set::VariableType> SparseDtmcRegionModelChecker::ParameterRegion::getVariables() const { - return this->variables; - } - - template - typename SparseDtmcRegionModelChecker::CoefficientType const& SparseDtmcRegionModelChecker::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 SparseDtmcRegionModelChecker::CoefficientType const& SparseDtmcRegionModelChecker::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 - const std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getUpperBounds() const { - return upperBounds; - } - - template - const std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getLowerBounds() const { - return lowerBounds; - } - - template - std::vector::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType>> SparseDtmcRegionModelChecker::ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const { - std::size_t const numOfVariables = consideredVariables.size(); - std::size_t const numOfVertices = std::pow(2, numOfVariables); - std::vector> resultingVector(numOfVertices, std::map()); - if (numOfVertices == 1) { - //no variables are given, the returned vector should still contain an empty map - return resultingVector; + + template + void ParameterRegion::init() { + //check whether both mappings map the same variables, check that lowerbound <= upper bound, and pre-compute the set of variables + for (auto const& variableWithLowerBound : this->lowerBounds) { + auto variableWithUpperBound = this->upperBounds.find(variableWithLowerBound.first); + STORM_LOG_THROW((variableWithUpperBound != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithLowerBound.first); + STORM_LOG_THROW((variableWithLowerBound.second<=variableWithUpperBound->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower bound for " << variableWithLowerBound.first << " is larger then the upper bound"); + this->variables.insert(variableWithLowerBound.first); + } + for (auto const& variableWithBound : 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 + ParameterRegion::~ParameterRegion() { + //Intentionally left empty + } + + template + std::set::VariableType> ParameterRegion::getVariables() const { + return this->variables; + } + + template + typename ParameterRegion::CoefficientType const& 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 ParameterRegion::CoefficientType const& 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 + const typename ParameterRegion::VariableSubstitutionType ParameterRegion::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(variable, getLowerBound(variable))); - } else { - resultingVector[vertexId].insert(std::pair(variable, getUpperBound(variable))); + template + const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getLowerBounds() const { + return lowerBounds; + } + + template + std::vector::VariableSubstitutionType> ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const { + std::size_t const numOfVariables = consideredVariables.size(); + std::size_t const numOfVertices = std::pow(2, numOfVariables); + std::vector 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(variable, getLowerBound(variable))); + } else { + resultingVector[vertexId].insert(std::pair(variable, getUpperBound(variable))); + } + ++variableIndex; } - ++variableIndex; } + return resultingVector; } - return resultingVector; - } - - template - std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSomePoint() const { - return this->getLowerBounds(); - } - - template - typename SparseDtmcRegionModelChecker::RegionCheckResult SparseDtmcRegionModelChecker::ParameterRegion::getCheckResult() const { - return checkResult; - } - - template - void SparseDtmcRegionModelChecker::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 - std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getViolatedPoint() const { - return violatedPoint; - } - - template - void SparseDtmcRegionModelChecker::ParameterRegion::setViolatedPoint(std::map const& violatedPoint) { - this->violatedPoint = violatedPoint; - } - - template - std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSatPoint() const { - return satPoint; - } - - template - void SparseDtmcRegionModelChecker::ParameterRegion::setSatPoint(std::map const& satPoint) { - this->satPoint = satPoint; - } - - template - std::string SparseDtmcRegionModelChecker::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 ParameterRegion::VariableSubstitutionType ParameterRegion::getSomePoint() const { + return this->getLowerBounds(); } - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not identify check result") - return "ERROR"; - } - - template - std::string SparseDtmcRegionModelChecker::ParameterRegion::toString() const { - std::stringstream regionstringstream; - for (auto var : this->getVariables()) { - regionstringstream << storm::utility::regions::convertNumber(this->getLowerBound(var)); - regionstringstream << "<="; - regionstringstream << storm::utility::regions::getVariableName(var); - regionstringstream << "<="; - regionstringstream << storm::utility::regions::convertNumber(this->getUpperBound(var)); - regionstringstream << ","; + + template + RegionCheckResult ParameterRegion::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 - void SparseDtmcRegionModelChecker::ParameterRegion::parseParameterBounds( - std::map& lowerBounds, - std::map& 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(parameter); - CoefficientType lb = storm::utility::regions::convertNumber(parameterBoundsString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::regions::convertNumber(parameterBoundsString.substr(positionOfSecondRelation+2)); - lowerBounds.emplace(std::make_pair(var, lb)); - upperBounds.emplace(std::make_pair(var, ub)); + + template + void 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 SparseDtmcRegionModelChecker::ParameterRegion SparseDtmcRegionModelChecker::ParameterRegion::parseRegion( - std::string const& regionString){ - std::map lowerBounds; - std::map upperBounds; - std::vector 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 ParameterRegion::VariableSubstitutionType ParameterRegion::getViolatedPoint() const { + return violatedPoint; + } + + template + void ParameterRegion::setViolatedPoint(VariableSubstitutionType const& violatedPoint) { + this->violatedPoint = violatedPoint; + } + + template + typename ParameterRegion::VariableSubstitutionType ParameterRegion::getSatPoint() const { + return satPoint; + } + + template + void ParameterRegion::setSatPoint(VariableSubstitutionType const& satPoint) { + this->satPoint = satPoint; + } + + template + std::string ParameterRegion::toString() const { + std::stringstream regionstringstream; + for (auto var : this->getVariables()) { + regionstringstream << storm::utility::region::convertNumber(this->getLowerBound(var)); + regionstringstream << "<="; + regionstringstream << storm::utility::region::getVariableName(var); + regionstringstream << "<="; + regionstringstream << storm::utility::region::convertNumber(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 - std::vector::ParameterRegion> SparseDtmcRegionModelChecker::ParameterRegion::parseMultipleRegions( - std::string const& regionsString){ - std::vector result; - std::vector 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 + void ParameterRegion::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(parameter); + CoefficientType lb = storm::utility::region::convertNumber(parameterBoundsString.substr(0,positionOfFirstRelation)); + CoefficientType ub = storm::utility::region::convertNumber(parameterBoundsString.substr(positionOfSecondRelation+2)); + lowerBounds.emplace(std::make_pair(var, lb)); + upperBounds.emplace(std::make_pair(var, ub)); + } + + template + ParameterRegion ParameterRegion::parseRegion( + std::string const& regionString){ + VariableSubstitutionType lowerBounds; + VariableSubstitutionType upperBounds; + std::vector 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 - std::vector::ParameterRegion> SparseDtmcRegionModelChecker::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 + std::vector> ParameterRegion::parseMultipleRegions( + std::string const& regionsString){ + std::vector result; + std::vector 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 + std::vector> 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(); + } + 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, double>; + template class ParameterRegion; #endif - + } //namespace region } } diff --git a/src/modelchecker/region/ParameterRegion.h b/src/modelchecker/region/ParameterRegion.h index 104f989e8..257935a57 100644 --- a/src/modelchecker/region/ParameterRegion.h +++ b/src/modelchecker/region/ParameterRegion.h @@ -8,125 +8,124 @@ #ifndef STORM_MODELCHECKER_REGION_PARAMETERREGION_H #define STORM_MODELCHECKER_REGION_PARAMETERREGION_H -#include "src/modelchecker/region/SparseDtmcRegionModelChecker.h" +#include + +#include "src/modelchecker/region/RegionCheckResult.h" +#include "src/utility/region.h" + namespace storm { namespace modelchecker{ + namespace region { + template + class ParameterRegion{ + public: + typedef typename storm::utility::region::VariableType VariableType; + typedef typename storm::utility::region::CoefficientType CoefficientType; + typedef typename std::map VariableSubstitutionType; + + ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds); + ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds); + virtual ~ParameterRegion(); + + std::set 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 getVerticesOfRegion(std::set 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 parseMultipleRegions( + std::string const& regionsString + ); + + + /* + * Retrieves the regions that are specified in the settings. + */ + static std::vector getRegionsFromSettings(); + + private: + + void init(); - template - class SparseDtmcRegionModelChecker; - - template - class SparseDtmcRegionModelChecker::ParameterRegion{ - public: - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - - ParameterRegion(std::map const& lowerBounds, std::map const& upperBounds); - ParameterRegion(std::map&& lowerBounds, std::map&& upperBounds); - virtual ~ParameterRegion(); - - std::set getVariables() const; - CoefficientType const& getLowerBound(VariableType const& variable) const; - CoefficientType const& getUpperBound(VariableType const& variable) const; - const std::map getUpperBounds() const; - const std::map getLowerBounds() const; - - /*! - * Returns a vector of all possible combinations of lower and upper bounds of the given variables. - * The first entry of the returned vector will map every variable to its lower bound - * The second entry will map every variable to its lower bound, except the first one (i.e. *getVariables.begin()) - * ... - * 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> getVerticesOfRegion(std::set const& consideredVariables) const; - - /*! - * Returns some point that lies within this region - */ - std::map getSomePoint() const; - - RegionCheckResult getCheckResult() const; - void setCheckResult(RegionCheckResult checkResult); - - /*! - * 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 getViolatedPoint() const; - - /*! - * Sets a point in the region for which the considered property is not satisfied. - */ - void setViolatedPoint(std::map 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 getSatPoint() const; - - /*! - * Sets a point in the region for which the considered property is satisfied. - */ - void setSatPoint(std::map 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& lowerBounds, - std::map& 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 parseMultipleRegions( - std::string const& regionsString - ); - - - /* - * Retrieves the regions that are specified in the settings. - */ - static std::vector getRegionsFromSettings(); - - private: - - void init(); - - std::map const lowerBounds; - std::map const upperBounds; - std::set variables; - RegionCheckResult checkResult; - std::map satPoint; - std::map violatedPoint; - }; + VariableSubstitutionType const lowerBounds; + VariableSubstitutionType const upperBounds; + std::set variables; + RegionCheckResult checkResult; + VariableSubstitutionType satPoint; + VariableSubstitutionType violatedPoint; + }; + } //namespace region } } diff --git a/src/modelchecker/region/RegionCheckResult.cpp b/src/modelchecker/region/RegionCheckResult.cpp new file mode 100644 index 000000000..4ddc13fee --- /dev/null +++ b/src/modelchecker/region/RegionCheckResult.cpp @@ -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; + } + } + } +} \ No newline at end of file diff --git a/src/modelchecker/region/RegionCheckResult.h b/src/modelchecker/region/RegionCheckResult.h new file mode 100644 index 000000000..4c4a95364 --- /dev/null +++ b/src/modelchecker/region/RegionCheckResult.h @@ -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 + +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 */ + diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 55fe6e27a..6880d24fc 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -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 - SparseDtmcRegionModelChecker::SamplingModel::SamplingModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr 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 probabilityMatrix; - std::vector 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> rewardModels; - std::vector rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping - if(this->computeRewards){ - boost::optional> stateRewards; - initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, &constantEntry); - rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(std::move(stateRewards)))); - } - - //Obtain other model ingredients and the sampling model itself - storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling()); - boost::optional> noTransitionRewards; - boost::optional>> noChoiceLabeling; - this->model=std::make_shared>(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(storm::utility::regions::getConstantPart(parModelEntry->getValue()))); + template + SamplingModel::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr 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 probabilityMatrix; + std::vector 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> rewardModels; + std::vector rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping + if(this->computeRewards){ + boost::optional> stateRewards; + initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, &constantEntry); + rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(std::move(stateRewards)))); + } + + //Obtain other model ingredients and the sampling model itself + storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling()); + boost::optional> noTransitionRewards; + boost::optional>> noChoiceLabeling; + this->model=std::make_shared>(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(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 + void SamplingModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, + storm::storage::SparseMatrix& probabilityMatrix, + std::vector& 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 matrixBuilder(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates(), parametricModel.getTransitionMatrix().getEntryCount()); + matrixEntryToEvalTableMapping.reserve(parametricModel.getTransitionMatrix().getEntryCount()); + std::size_t numOfNonConstEntries=0; + for(typename storm::storage::SparseMatrix::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){ + ConstantType dummyEntry=storm::utility::one(); + 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())).first; + matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); + } + matrixBuilder.addNextValue(row,entry.getColumn(), dummyEntry); + dummyEntry=storm::utility::zero(); } - ++sampleModelStateRewardEntry; } + this->probabilityMapping.reserve(numOfNonConstEntries); + probabilityMatrix=matrixBuilder.build(); } - } - - template - void SparseDtmcRegionModelChecker::SamplingModel::initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, - storm::storage::SparseMatrix& probabilityMatrix, - std::vector& 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 matrixBuilder(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates(), parametricModel.getTransitionMatrix().getEntryCount()); - matrixEntryToEvalTableMapping.reserve(parametricModel.getTransitionMatrix().getEntryCount()); - std::size_t numOfNonConstEntries=0; - for(typename storm::storage::SparseMatrix::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){ - ConstantType dummyEntry=storm::utility::one(); - for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){ - if(storm::utility::isConstant(entry.getValue())){ - matrixEntryToEvalTableMapping.emplace_back(constantEntry); + + template + void SamplingModel::initializeRewards(ParametricSparseModelType const& parametricModel, + boost::optional>& stateRewards, + std::vector& 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 stateRewardsAsVector(parametricModel.getNumberOfStates()); + rewardEntryToEvalTableMapping.reserve(parametricModel.getNumberOfStates()); + std::size_t numOfNonConstEntries=0; + for(std::size_t state=0; statesecond.getStateRewardVector()[state])){ + stateRewardsAsVector[state] = storm::utility::region::convertNumber(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())).first; - matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); + auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero())).first; + rewardEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); } - matrixBuilder.addNextValue(row,entry.getColumn(), dummyEntry); - dummyEntry=storm::utility::zero(); - } - } - this->probabilityMapping.reserve(numOfNonConstEntries); - probabilityMatrix=matrixBuilder.build(); - } - - template - void SparseDtmcRegionModelChecker::SamplingModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, - boost::optional>& stateRewards, - std::vector& 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 stateRewardsAsVector(parametricModel.getNumberOfStates()); - rewardEntryToEvalTableMapping.reserve(parametricModel.getNumberOfStates()); - std::size_t numOfNonConstEntries=0; - for(std::size_t state=0; statesecond.getStateRewardVector()[state])){ - stateRewardsAsVector[state] = storm::utility::regions::convertNumber(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())).first; - rewardEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); } + this->stateRewardMapping.reserve(numOfNonConstEntries); + stateRewards=std::move(stateRewardsAsVector); } - this->stateRewardMapping.reserve(numOfNonConstEntries); - stateRewards=std::move(stateRewardsAsVector); - } - - template - SparseDtmcRegionModelChecker::SamplingModel::~SamplingModel() { - //Intentionally left empty - } - - template - std::shared_ptr> const& SparseDtmcRegionModelChecker::SamplingModel::getModel() const { - return this->model; - } - template - void SparseDtmcRegionModelChecker::SamplingModel::instantiate(std::mapconst& point) { - //write entries into evaluation tables - for(auto& tableEntry : this->probabilityEvaluationTable){ - tableEntry.second=storm::utility::regions::convertNumber( - storm::utility::regions::evaluateFunction(tableEntry.first, point)); - } - for(auto& tableEntry : this->rewardEvaluationTable){ - tableEntry.second=storm::utility::regions::convertNumber( - storm::utility::regions::evaluateFunction(tableEntry.first, point)); + template + SamplingModel::~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 + std::shared_ptr> const& SamplingModel::getModel() const { + return this->model; } - if(this->computeRewards){ - for(auto& mappingPair : this->stateRewardMapping){ - *mappingPair.second=*mappingPair.first; + + template + void SamplingModel::instantiate(std::mapconst& point) { + //write entries into evaluation tables + for(auto& tableEntry : this->probabilityEvaluationTable){ + tableEntry.second=storm::utility::region::convertNumber( + storm::utility::region::evaluateFunction(tableEntry.first, point)); + } + for(auto& tableEntry : this->rewardEvaluationTable){ + tableEntry.second=storm::utility::region::convertNumber( + storm::utility::region::evaluateFunction(tableEntry.first, point)); } - } - } - template - std::vector const& SparseDtmcRegionModelChecker::SamplingModel::computeValues() { - storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(*this->model); - std::unique_ptr 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 + std::vector const& SamplingModel::computeValues() { + storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(*this->model); + std::unique_ptr 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().getValueVector(); } - return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); - } #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker, double>; + template class SamplingModel>, double>; #endif + } //namespace region } } \ No newline at end of file diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index efa2742b5..5b1464f91 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -9,75 +9,73 @@ #define STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H #include +#include -#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 + class SamplingModel { + public: + typedef typename ParametricSparseModelType::ValueType ParametricType; + typedef typename storm::utility::region::VariableType VariableType; + typedef typename storm::utility::region::CoefficientType CoefficientType; + + SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); + virtual ~SamplingModel(); + + /*! + * returns the underlying model + */ + std::shared_ptr> const& getModel() const; + + /*! + * Instantiates the underlying model according to the given point + */ + void instantiate(std::mapconst& point); + + /*! + * Returns the reachability probabilities for every state according to the current instantiation. + * Undefined behavior if model has not been instantiated first! + */ + std::vector const& computeValues(); + + + private: + + typedef typename std::unordered_map::value_type TableEntry; + + void initializeProbabilities(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& matrixEntryToEvalTableMapping, TableEntry* constantEntry); + void initializeRewards(ParametricSparseModelType const& parametricModel, boost::optional>& stateRewards, std::vector& rewardEntryToEvalTableMapping, TableEntry* constantEntry); + + //The model with which we work + std::shared_ptr> model; + //The formula for which we will compute the values + std::shared_ptr 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 probabilityEvaluationTable; + std::unordered_map 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::iterator>> probabilityMapping; + std::vector::iterator>> stateRewardMapping; - template - class SparseDtmcRegionModelChecker; - - template - class SparseDtmcRegionModelChecker::SamplingModel { - - public: - - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - - SamplingModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr formula); - virtual ~SamplingModel(); - - /*! - * returns the underlying model - */ - std::shared_ptr> const& getModel() const; - - /*! - * Instantiates the underlying model according to the given point - */ - void instantiate(std::mapconst& point); - - /*! - * Returns the reachability probabilities for every state according to the current instantiation. - * Undefined behavior if model has not been instantiated first! - */ - std::vector const& computeValues(); - - - private: - - typedef typename std::unordered_map::value_type TableEntry; - - void initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& matrixEntryToEvalTableMapping, TableEntry* constantEntry); - void initializeRewards(storm::models::sparse::Dtmc const& parametricModel, boost::optional>& stateRewards, std::vector& rewardEntryToEvalTableMapping, TableEntry* constantEntry); - - //The model with which we work - std::shared_ptr> model; - //The formula for which we will compute the values - std::shared_ptr 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 probabilityEvaluationTable; - std::unordered_map 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::iterator>> probabilityMapping; - std::vector::iterator>> stateRewardMapping; - - }; - + }; + } //namespace region } } #endif /* STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H */ diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 77ce1f9ff..8f53175f6 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -1,20 +1,22 @@ #include "src/modelchecker/region/SparseDtmcRegionModelChecker.h" #include +#include +#include #include "src/adapters/CarlAdapter.h" - -#include "src/modelchecker/region/ParameterRegion.h" -#include "src/modelchecker/region/ApproximationModel.h" -#include "src/modelchecker/region/SamplingModel.h" +#include "src/logic/Formulas.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" - +#include "src/modelchecker/region/RegionCheckResult.h" #include "src/models/sparse/StandardRewardModel.h" -#include "src/utility/graph.h" -#include "src/utility/vector.h" -#include "src/utility/macros.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/RegionSettings.h" +#include "src/solver/OptimizationDirection.h" +#include "src/storage/sparse/StateType.h" +#include "src/utility/constants.h" +#include "src/utility/graph.h" +#include "src/utility/macros.h" +#include "src/utility/vector.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidPropertyException.h" @@ -22,649 +24,433 @@ #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/UnexpectedException.h" -#include "exceptions/InvalidAccessException.h" +#include "exceptions/NotSupportedException.h" namespace storm { namespace modelchecker { - - - template - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : - model(model), - eliminationModelChecker(model), - specifiedFormula(nullptr){ - STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state."); - } - - template - SparseDtmcRegionModelChecker::~SparseDtmcRegionModelChecker(){ - //intentionally left empty - } - - template - bool SparseDtmcRegionModelChecker::canHandle(storm::logic::Formula const& formula) const { - //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) and reachability reward formulas - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - return probabilityOperatorFormula.hasBound() && this->canHandle(probabilityOperatorFormula.getSubformula()); - } else if (formula.isRewardOperatorFormula()) { - storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); - return rewardOperatorFormula.hasBound() && this->canHandle(rewardOperatorFormula.getSubformula()); - } else if (formula.isEventuallyFormula()) { - storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); - if (eventuallyFormula.getSubformula().isPropositionalFormula()) { - return true; - } - } else if (formula.isReachabilityRewardFormula()) { - storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); - if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { - return true; - } - } else if (formula.isConditionalPathFormula()) { - storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula(); - if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { - return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); - } - } - STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula); - return false; - } - - template - void SparseDtmcRegionModelChecker::specifyFormula(std::shared_ptr 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."); - - //Note: canHandle already ensures that the formula has the right shape. - this->specifiedFormula = formula; - this->isResultConstant=false; - this->isResultInfinity=false; - this->simpleFormula=nullptr; - this->isApproximationApplicable=false; - this->smtSolver=nullptr; - this->approximationModel=nullptr; - this->samplingModel=nullptr; - this->reachabilityFunction=nullptr; - - // set some information regarding the formula and model. Also computes a more simple version of the model - preprocess(); - if(!this->isResultConstant){ - //now create the model used for Approximation (if required) - if(storm::settings::regionSettings().doApprox()){ - initializeApproximationModel(*this->simpleModel, this->simpleFormula); - } - //now create the model used for Sampling (if required) - if(storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || - (!storm::settings::regionSettings().doSample() && storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ - initializeSamplingModel(*this->simpleModel, this->simpleFormula); - } - //Check if the reachability function needs to be computed - if((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || - (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ - computeReachabilityFunction(*this->simpleModel); - } - } else { - //for a constant result we just compute the reachability function - if(this->reachabilityFunction==nullptr){ - computeReachabilityFunction(*this->simpleModel); - } - } - //some information for statistics... - std::chrono::high_resolution_clock::time_point timeSpecifyFormulaEnd = std::chrono::high_resolution_clock::now(); - this->timeSpecifyFormula= timeSpecifyFormulaEnd - timeSpecifyFormulaStart; - this->numOfCheckedRegions=0; - this->numOfRegionsSolvedThroughSampling=0; - this->numOfRegionsSolvedThroughApproximation=0; - this->numOfRegionsSolvedThroughFullSmt=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->timeMDPBuild=std::chrono::high_resolution_clock::duration::zero(); - this->timeFullSmt=std::chrono::high_resolution_clock::duration::zero(); - } - - template - void SparseDtmcRegionModelChecker::preprocess(){ - std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now(); - STORM_LOG_THROW(this->model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); - - //first some preprocessing depending on the type of the considered formula - storm::storage::BitVector maybeStates, targetStates; - boost::optional> stateRewards; - if (this->specifiedFormula->isProbabilityOperatorFormula()) { - preprocessForProbabilities(maybeStates, targetStates); - } - else if (this->specifiedFormula->isRewardOperatorFormula()) { - std::vector stateRewardsAsVector; - preprocessForRewards(maybeStates, targetStates, stateRewardsAsVector); - stateRewards=std::move(stateRewardsAsVector); + namespace region { + + template + SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(ParametricSparseModelType const& model) : + AbstractSparseRegionModelChecker(model), + eliminationModelChecker(model){ + //intentionally left empty } - else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The specified property " << this->specifiedFormula << "is not supported"); + + template + SparseDtmcRegionModelChecker::~SparseDtmcRegionModelChecker(){ + //intentionally left empty } - // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->model.getTransitionMatrix(), this->model.getInitialStates(), maybeStates, targetStates); - // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). - maybeStates &= reachableStates; - // Create a vector for the probabilities to go to a target state in one step. - std::vector oneStepProbabilities = this->model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, targetStates); - // Determine the initial state of the sub-model. - storm::storage::sparse::state_type initialState = *(this->model.getInitialStates() % maybeStates).begin(); - // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - // Eliminate all states with only constant outgoing transitions - // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. - auto flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix); - auto flexibleBackwardTransitions= this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix.transpose(), true); - // Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated. - storm::storage::BitVector subsystem(submatrix.getRowCount(), true); - //The states that we consider to eliminate - storm::storage::BitVector considerToEliminate(submatrix.getRowCount(), true); - considerToEliminate.set(initialState, false); - for (auto const& state : considerToEliminate) { - bool eliminateThisState=true; - for(auto const& entry : flexibleTransitions.getRow(state)){ - if(!storm::utility::isConstant(entry.getValue())){ - eliminateThisState=false; - break; + + template + bool SparseDtmcRegionModelChecker::canHandle(storm::logic::Formula const& formula) const { + //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) and reachability reward formulas + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + return probabilityOperatorFormula.hasBound() && this->canHandle(probabilityOperatorFormula.getSubformula()); + } else if (formula.isRewardOperatorFormula()) { + storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); + return rewardOperatorFormula.hasBound() && this->canHandle(rewardOperatorFormula.getSubformula()); + } else if (formula.isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); + if (eventuallyFormula.getSubformula().isPropositionalFormula()) { + return true; } - } - if(!storm::utility::isConstant(oneStepProbabilities[state])){ - eliminateThisState=false; - } - if(this->computeRewards && eliminateThisState && !storm::utility::isConstant(stateRewards.get()[state])){ - //Note: The state reward does not need to be constant but we need to make sure that - //no parameter of this reward function occurs as a parameter in the probability functions of the predecessors - // (otherwise, more complex functions might occur in our simple model) - std::set probVars; - for(auto const& predecessor : flexibleBackwardTransitions.getRow(state)){ - for(auto const& predecessorTransition : flexibleTransitions.getRow(predecessor.getColumn())){ - storm::utility::regions::gatherOccurringVariables(predecessorTransition.getValue(), probVars); - } + } else if (formula.isReachabilityRewardFormula()) { + storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); + if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { + return true; } - std::set rewardVars; - storm::utility::regions::gatherOccurringVariables(stateRewards.get()[state], rewardVars); - for(auto const& rewardVar : rewardVars){ - if(probVars.find(rewardVar)!=probVars.end()){ + } else if (formula.isConditionalPathFormula()) { + storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula(); + if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { + return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); + } + } + STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula); + return false; + } + + template + void SparseDtmcRegionModelChecker::preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, bool& isResultConstant){ + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); + //Reset some data + this->isResultInfinity=false; + this->smtSolver=nullptr; + this->reachabilityFunction=nullptr; + + //Preprocessing depending on the type of the considered formula + storm::storage::BitVector maybeStates, targetStates; + boost::optional> stateRewards; + if (this->isComputeRewards()) { + std::vector stateRewardsAsVector; + preprocessForRewards(maybeStates, targetStates, stateRewardsAsVector, isApproximationApplicable, isResultConstant); + stateRewards=std::move(stateRewardsAsVector); + } else { + preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, isResultConstant); + } + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, targetStates); + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + // Create a vector for the probabilities to go to a target state in one step. + std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, targetStates); + // Determine the initial state of the sub-model. + storm::storage::sparse::state_type initialState = *(this->getModel().getInitialStates() % maybeStates).begin(); + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + // Eliminate all states with only constant outgoing transitions + // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. + auto flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix); + auto flexibleBackwardTransitions= this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix.transpose(), true); + // Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated. + storm::storage::BitVector subsystem(submatrix.getRowCount(), true); + //The states that we consider to eliminate + storm::storage::BitVector considerToEliminate(submatrix.getRowCount(), true); + considerToEliminate.set(initialState, false); + for (auto const& state : considerToEliminate) { + bool eliminateThisState=true; + for(auto const& entry : flexibleTransitions.getRow(state)){ + if(!storm::utility::isConstant(entry.getValue())){ eliminateThisState=false; break; } } - } - if(eliminateThisState){ - this->eliminationModelChecker.eliminateState(flexibleTransitions, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); - subsystem.set(state,false); - } - } - STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions."); - - //Build the simple model - //The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated. - //The new matrix should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly. - std::vector newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index to easily check if a transition leads to an unselected state - storm::storage::sparse::state_type newStateIndex=0; - for(auto const& state : subsystem){ - newStateIndexMap[state]=newStateIndex; - ++newStateIndex; - } - //We need to add a target state to which the oneStepProbabilities will lead as well as a sink state to which the "missing" probability will lead - storm::storage::sparse::state_type numStates=newStateIndex+2; - storm::storage::sparse::state_type targetState=numStates-2; - storm::storage::sparse::state_type sinkState= numStates-1; - //We can now fill in the data. - storm::storage::SparseMatrixBuilder matrixBuilder(numStates, numStates); - for(storm::storage::sparse::state_type oldStateIndex : subsystem){ - ParametricType missingProbability=storm::utility::regions::getNewFunction(storm::utility::one()); - //go through columns: - for(auto& entry: flexibleTransitions.getRow(oldStateIndex)){ - STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getNumberOfRows(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); - missingProbability-=entry.getValue(); - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); - } - if(this->computeRewards){ - // the missing probability always leads to target - if(!storm::utility::isZero(missingProbability)){ - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(missingProbability)); + if(!storm::utility::isConstant(oneStepProbabilities[state])){ + eliminateThisState=false; } - } else{ - //transition to target state - if(!storm::utility::isZero(oneStepProbabilities[oldStateIndex])){ - missingProbability-=oneStepProbabilities[oldStateIndex]; - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(oneStepProbabilities[oldStateIndex])); + if(this->isComputeRewards() && eliminateThisState && !storm::utility::isConstant(stateRewards.get()[state])){ + //Note: The state reward does not need to be constant but we need to make sure that + //no parameter of this reward function occurs as a parameter in the probability functions of the predecessors + // (otherwise, more complex functions might occur in our simple model) + std::set probVars; + for(auto const& predecessor : flexibleBackwardTransitions.getRow(state)){ + for(auto const& predecessorTransition : flexibleTransitions.getRow(predecessor.getColumn())){ + storm::utility::region::gatherOccurringVariables(predecessorTransition.getValue(), probVars); + } + } + std::set rewardVars; + storm::utility::region::gatherOccurringVariables(stateRewards.get()[state], rewardVars); + for(auto const& rewardVar : rewardVars){ + if(probVars.find(rewardVar)!=probVars.end()){ + eliminateThisState=false; + break; + } + } } - //transition to sink state - if(!storm::utility::isZero(missingProbability)){ - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], sinkState, storm::utility::simplify(missingProbability)); + if(eliminateThisState){ + this->eliminationModelChecker.eliminateState(flexibleTransitions, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); + subsystem.set(state,false); } } - } - //add self loops on the additional states (i.e., target and sink) - matrixBuilder.addNextValue(targetState, targetState, storm::utility::one()); - matrixBuilder.addNextValue(sinkState, sinkState, storm::utility::one()); - //The labeling - storm::models::sparse::StateLabeling labeling(numStates); - storm::storage::BitVector initLabel(numStates, false); - initLabel.set(newStateIndexMap[initialState], true); - labeling.addLabel("init", std::move(initLabel)); - storm::storage::BitVector targetLabel(numStates, false); - targetLabel.set(targetState, true); - labeling.addLabel("target", std::move(targetLabel)); - storm::storage::BitVector sinkLabel(numStates, false); - sinkLabel.set(sinkState, true); - labeling.addLabel("sink", std::move(sinkLabel)); - // other ingredients - std::unordered_map> rewardModels; - if(this->computeRewards){ - std::size_t newState = 0; - for (auto oldstate : subsystem) { - if(oldstate!=newState){ - stateRewards.get()[newState++] = std::move(storm::utility::simplify(stateRewards.get()[oldstate])); - } else { - ++newState; + STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions."); + + //Build the simple model + //The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated. + //The new matrix should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly. + std::vector newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index to easily check if a transition leads to an unselected state + storm::storage::sparse::state_type newStateIndex=0; + for(auto const& state : subsystem){ + newStateIndexMap[state]=newStateIndex; + ++newStateIndex; + } + //We need to add a target state to which the oneStepProbabilities will lead as well as a sink state to which the "missing" probability will lead + storm::storage::sparse::state_type numStates=newStateIndex+2; + storm::storage::sparse::state_type targetState=numStates-2; + storm::storage::sparse::state_type sinkState= numStates-1; + //We can now fill in the data. + storm::storage::SparseMatrixBuilder matrixBuilder(numStates, numStates); + for(storm::storage::sparse::state_type oldStateIndex : subsystem){ + ParametricType missingProbability=storm::utility::region::getNewFunction(storm::utility::one()); + //go through columns: + for(auto& entry: flexibleTransitions.getRow(oldStateIndex)){ + STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getNumberOfRows(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); + missingProbability-=entry.getValue(); + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); } - } - stateRewards.get()[newState++] = storm::utility::zero(); //target state - stateRewards.get()[newState++] = storm::utility::zero(); //sink state - stateRewards.get().resize(newState); - rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(std::move(stateRewards)))); - } - boost::optional>> noChoiceLabeling; - // the final model - this->simpleModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); - // the corresponding formula - std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); - if(this->computeRewards){ - this->simpleFormula = std::shared_ptr(new storm::logic::ReachabilityRewardFormula(targetFormulaPtr)); - } else { - this->simpleFormula = std::shared_ptr(new storm::logic::EventuallyFormula(targetFormulaPtr)); - } - std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); - this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart; - } - - template - void SparseDtmcRegionModelChecker::preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates) { - this->computeRewards=false; - //Get bounds, comparison type, target states - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = this->specifiedFormula->asProbabilityOperatorFormula(); - this->specifiedFormulaCompType=probabilityOperatorFormula.getComparisonType(); - this->specifiedFormulaBound=probabilityOperatorFormula.getBound(); - storm::modelchecker::SparsePropositionalModelChecker> modelChecker(this->model); - std::unique_ptr targetStatesResultPtr= modelChecker.checkAtomicLabelFormula(probabilityOperatorFormula.getSubformula().asEventuallyFormula().getSubformula().asAtomicLabelFormula()); - targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); - - //maybeStates: Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model, storm::storage::BitVector(this->model.getNumberOfStates(),true), targetStates); - maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); - // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. - storm::storage::sparse::state_type initialState = *this->model.getInitialStates().begin(); - if (!maybeStates.get(initialState)) { - STORM_LOG_WARN("The probability of the initial state is constant (zero or one)"); - this->reachabilityFunction = std::make_shared(statesWithProbability01.first.get(initialState) ? storm::utility::zero() : storm::utility::one()); - this->isResultConstant=true; - return; //nothing else to do... - } - //extend target states - targetStates=statesWithProbability01.second; - - //check if approximation is applicable and whether the result is constant - this->isApproximationApplicable=true; - this->isResultConstant=true; - for (auto state=maybeStates.begin(); (state!=maybeStates.end()) && this->isApproximationApplicable; ++state) { - for(auto const& entry : this->model.getTransitionMatrix().getRow(*state)){ - if(!storm::utility::isConstant(entry.getValue())){ - this->isResultConstant=false; - if(!storm::utility::regions::functionIsLinear(entry.getValue())){ - this->isApproximationApplicable=false; - break; + if(this->isComputeRewards()){ + // the missing probability always leads to target + if(!storm::utility::isZero(missingProbability)){ + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(missingProbability)); + } + } else{ + //transition to target state + if(!storm::utility::isZero(oneStepProbabilities[oldStateIndex])){ + missingProbability-=oneStepProbabilities[oldStateIndex]; + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(oneStepProbabilities[oldStateIndex])); + } + //transition to sink state + if(!storm::utility::isZero(missingProbability)){ + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], sinkState, storm::utility::simplify(missingProbability)); } } } - } - STORM_LOG_WARN_COND(!this->isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); - } - - - template - void SparseDtmcRegionModelChecker::preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector& stateRewards) { - this->computeRewards=true; - - //get the correct reward model - storm::models::sparse::StandardRewardModel const* rewardModel; - if(this->specifiedFormula->asRewardOperatorFormula().hasRewardModelName()){ - std::string const& rewardModelName = this->specifiedFormula->asRewardOperatorFormula().getRewardModelName(); - STORM_LOG_THROW(this->model.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The Property specifies refers to the reward model '" << rewardModelName << "which is not defined by the given model"); - rewardModel=&(this->model.getRewardModel(rewardModelName)); - } else { - STORM_LOG_THROW(this->model.hasRewardModel(), storm::exceptions::InvalidArgumentException, "No reward model specified"); - STORM_LOG_THROW(this->model.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "Ambiguous reward model. Specify it in the formula!"); - rewardModel=&(this->model.getUniqueRewardModel()->second); - } - - //Get bounds, comparison type, target states - storm::logic::RewardOperatorFormula const& rewardOperatorFormula = this->specifiedFormula->asRewardOperatorFormula(); - this->specifiedFormulaCompType=rewardOperatorFormula.getComparisonType(); - this->specifiedFormulaBound=rewardOperatorFormula.getBound(); - storm::modelchecker::SparsePropositionalModelChecker> modelChecker(this->model); - std::unique_ptr targetStatesResultPtr= modelChecker.checkAtomicLabelFormula(rewardOperatorFormula.getSubformula().asReachabilityRewardFormula().getSubformula().asAtomicLabelFormula()); - targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); - - //maybeStates: Compute the subset of states that has a reachability reward less than infinity. - storm::storage::BitVector statesWithProbability1 = storm::utility::graph::performProb1(this->model.getBackwardTransitions(), storm::storage::BitVector(this->model.getNumberOfStates(), true), targetStates); - maybeStates = ~targetStates & statesWithProbability1; - - //Compute the new state reward vector - stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->model.getTransitionMatrix(), maybeStates); - - // If the initial state is known to have 0 reward or an infinite reachability reward value, we can directly set the reachRewardFunction. - storm::storage::sparse::state_type initialState = *this->model.getInitialStates().begin(); - if (!maybeStates.get(initialState)) { - STORM_LOG_WARN("The expected reward of the initial state is constant (infinity or zero)"); - if(statesWithProbability1.get(initialState)){ - this->reachabilityFunction = std::make_shared(storm::utility::zero()); + //add self loops on the additional states (i.e., target and sink) + matrixBuilder.addNextValue(targetState, targetState, storm::utility::one()); + matrixBuilder.addNextValue(sinkState, sinkState, storm::utility::one()); + //The labeling + storm::models::sparse::StateLabeling labeling(numStates); + storm::storage::BitVector initLabel(numStates, false); + initLabel.set(newStateIndexMap[initialState], true); + labeling.addLabel("init", std::move(initLabel)); + storm::storage::BitVector targetLabel(numStates, false); + targetLabel.set(targetState, true); + labeling.addLabel("target", std::move(targetLabel)); + storm::storage::BitVector sinkLabel(numStates, false); + sinkLabel.set(sinkState, true); + labeling.addLabel("sink", std::move(sinkLabel)); + // other ingredients + std::unordered_map rewardModels; + if(this->isComputeRewards()){ + std::size_t newState = 0; + for (auto oldstate : subsystem) { + if(oldstate!=newState){ + stateRewards.get()[newState++] = std::move(storm::utility::simplify(stateRewards.get()[oldstate])); + } else { + ++newState; + } + } + stateRewards.get()[newState++] = storm::utility::zero(); //target state + stateRewards.get()[newState++] = storm::utility::zero(); //sink state + stateRewards.get().resize(newState); + rewardModels.insert(std::pair("", ParametricRewardModelType(std::move(stateRewards)))); + } + boost::optional>> noChoiceLabeling; + // the final model + simpleModel = std::make_shared(matrixBuilder.build(), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); + // the corresponding formula + std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); + if(this->isComputeRewards()){ + simpleFormula = std::shared_ptr(new storm::logic::ReachabilityRewardFormula(targetFormulaPtr)); } else { - this->reachabilityFunction = std::make_shared(storm::utility::one()); - this->isResultInfinity=true; + simpleFormula = std::shared_ptr(new storm::logic::EventuallyFormula(targetFormulaPtr)); + } + //Check if the reachability function needs to be computed + if((isResultConstant && this->reachabilityFunction==nullptr) || //If the result is constant, we can already compute it now. + (storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || //The smt solver will need it + (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ //The sampling will need it + this->computeReachabilityFunction(*simpleModel); } - this->isResultConstant=true; - return; //nothing else to do... } - //check if approximation is applicable and whether the result is constant - this->isApproximationApplicable=true; - this->isResultConstant=true; - std::set rewardPars; //the set of parameters that occur on a reward function - std::set probPars; //the set of parameters that occur on a probability function - for (auto state=maybeStates.begin(); state!=maybeStates.end() && this->isApproximationApplicable; ++state) { - //Constant/Linear probability functions - for(auto const& entry : this->model.getTransitionMatrix().getRow(*state)){ - if(!storm::utility::isConstant(entry.getValue())){ - this->isResultConstant=false; - if(!storm::utility::regions::functionIsLinear(entry.getValue())){ - this->isApproximationApplicable=false; - break; + template + void SparseDtmcRegionModelChecker::preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, bool& isApproximationApplicable /* = 0 */, bool& isResultConstant /* = 0 */) { + //Get Target States + storm::logic::AtomicLabelFormula const& labelFormula = this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asAtomicLabelFormula(); + storm::modelchecker::SparsePropositionalModelChecker modelChecker(this->getModel()); + std::unique_ptr targetStatesResultPtr = modelChecker.checkAtomicLabelFormula(labelFormula); + targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); + //maybeStates: Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly. + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); + maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); + // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. + storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); + if (!maybeStates.get(initialState)) { + STORM_LOG_WARN("The probability of the initial state is constant (zero or one)"); + this->reachabilityFunction = std::make_shared(statesWithProbability01.first.get(initialState) ? storm::utility::zero() : storm::utility::one()); + isResultConstant=true; + return; //nothing else to do... + } + //extend target states + targetStates=statesWithProbability01.second; + //check if approximation is applicable and whether the result is constant + isApproximationApplicable=true; + isResultConstant=true; + for (auto state=maybeStates.begin(); (state!=maybeStates.end()) && isApproximationApplicable; ++state) { + for(auto const& entry : this->getModel().getTransitionMatrix().getRow(*state)){ + if(!storm::utility::isConstant(entry.getValue())){ + isResultConstant=false; + if(!storm::utility::region::functionIsLinear(entry.getValue())){ + isApproximationApplicable=false; + break; + } } - storm::utility::regions::gatherOccurringVariables(entry.getValue(), probPars); } } - //Constant/Linear state rewards - if(rewardModel->hasStateRewards() && !storm::utility::isConstant(rewardModel->getStateRewardVector()[*state])){ - this->isResultConstant=false; - if(!storm::utility::regions::functionIsLinear(rewardModel->getStateRewardVector()[*state])){ - this->isApproximationApplicable=false; - break; + STORM_LOG_WARN_COND(!isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); + } + + + template + void SparseDtmcRegionModelChecker::preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector& stateRewards, bool& isApproximationApplicable /* = true */, bool& isResultConstant /* = false */) { + //get the correct reward model + ParametricRewardModelType const* rewardModel; + if(this->getSpecifiedFormula()->asRewardOperatorFormula().hasRewardModelName()){ + std::string const& rewardModelName = this->getSpecifiedFormula()->asRewardOperatorFormula().getRewardModelName(); + STORM_LOG_THROW(this->getModel().hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The Property specifies refers to the reward model '" << rewardModelName << "which is not defined by the given model"); + rewardModel=&(this->getModel().getRewardModel(rewardModelName)); + } else { + STORM_LOG_THROW(this->getModel().hasRewardModel(), storm::exceptions::InvalidArgumentException, "No reward model specified"); + STORM_LOG_THROW(this->getModel().hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "Ambiguous reward model. Specify it in the formula!"); + rewardModel=&(this->getModel().getUniqueRewardModel()->second); + } + //Get target states + storm::logic::AtomicLabelFormula const& labelFormula = this->getSpecifiedFormula()->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula().getSubformula().asAtomicLabelFormula(); + storm::modelchecker::SparsePropositionalModelChecker modelChecker(this->getModel()); + std::unique_ptr targetStatesResultPtr= modelChecker.checkAtomicLabelFormula(labelFormula); + targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); + //maybeStates: Compute the subset of states that has a reachability reward less than infinity. + storm::storage::BitVector statesWithProbability1 = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), targetStates); + maybeStates = ~targetStates & statesWithProbability1; + //Compute the new state reward vector + stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); + // If the initial state is known to have 0 reward or an infinite reachability reward value, we can directly set the reachRewardFunction. + storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); + if (!maybeStates.get(initialState)) { + STORM_LOG_WARN("The expected reward of the initial state is constant (infinity or zero)"); + if(statesWithProbability1.get(initialState)){ + this->reachabilityFunction = std::make_shared(storm::utility::zero()); + } else { + this->reachabilityFunction = std::make_shared(storm::utility::one()); + this->isResultInfinity=true; } - storm::utility::regions::gatherOccurringVariables(rewardModel->getStateRewardVector()[*state], rewardPars); - } - //Constant/Linear transition rewards - if(rewardModel->hasTransitionRewards()){ - for(auto const& entry : rewardModel->getTransitionRewardMatrix().getRow(*state)) { + isResultConstant=true; + return; //nothing else to do... + } + //check if approximation is applicable and whether the result is constant + isApproximationApplicable=true; + isResultConstant=true; + std::set rewardPars; //the set of parameters that occur on a reward function + std::set probPars; //the set of parameters that occur on a probability function + for (auto state=maybeStates.begin(); state!=maybeStates.end() && isApproximationApplicable; ++state) { + //Constant/Linear probability functions + for(auto const& entry : this->getModel().getTransitionMatrix().getRow(*state)){ if(!storm::utility::isConstant(entry.getValue())){ - this->isResultConstant=false; - if(!storm::utility::regions::functionIsLinear(entry.getValue())){ - this->isApproximationApplicable=false; + isResultConstant=false; + if(!storm::utility::region::functionIsLinear(entry.getValue())){ + isApproximationApplicable=false; break; } - storm::utility::regions::gatherOccurringVariables(entry.getValue(), rewardPars); + storm::utility::region::gatherOccurringVariables(entry.getValue(), probPars); + } + } + //Constant/Linear state rewards + if(rewardModel->hasStateRewards() && !storm::utility::isConstant(rewardModel->getStateRewardVector()[*state])){ + isResultConstant=false; + if(!storm::utility::region::functionIsLinear(rewardModel->getStateRewardVector()[*state])){ + isApproximationApplicable=false; + break; + } + storm::utility::region::gatherOccurringVariables(rewardModel->getStateRewardVector()[*state], rewardPars); + } + //Constant/Linear transition rewards + if(rewardModel->hasTransitionRewards()){ + for(auto const& entry : rewardModel->getTransitionRewardMatrix().getRow(*state)) { + if(!storm::utility::isConstant(entry.getValue())){ + isResultConstant=false; + if(!storm::utility::region::functionIsLinear(entry.getValue())){ + isApproximationApplicable=false; + break; + } + storm::utility::region::gatherOccurringVariables(entry.getValue(), rewardPars); + } } } } - } - //Finally, we need to check whether rewardPars and probPars are disjoint - //Note: It would also work to simply rename the parameters that occur in both sets. - //This is to avoid getting functions with local maxima like p * (1-p) - for(auto const& rewardVar : rewardPars){ - if(probPars.find(rewardVar)!=probPars.end()){ - this->isApproximationApplicable=false; - break; - } - } - STORM_LOG_WARN_COND(!this->isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); - } - - - - template - void SparseDtmcRegionModelChecker::initializeApproximationModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula) { - std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now(); - this->approximationModel=std::make_shared(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 - void SparseDtmcRegionModelChecker::initializeSamplingModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula) { - std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now(); - this->samplingModel=std::make_shared(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 - void SparseDtmcRegionModelChecker::computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel){ - std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionStart = std::chrono::high_resolution_clock::now(); - //get the one step probabilities and the transition matrix of the simple model without target/sink state - storm::storage::SparseMatrix backwardTransitions(simpleModel.getBackwardTransitions()); - std::vector oneStepProbabilities(simpleModel.getNumberOfStates()-2, storm::utility::zero()); - for(auto const& entry : backwardTransitions.getRow(*(simpleModel.getStates("target").begin()))){ - if(entry.getColumn() forwardTransitions=simpleModel.getTransitionMatrix().getSubmatrix(false,maybeStates,maybeStates); - //now compute the functions using methods from elimination model checker - storm::storage::BitVector newInitialStates = simpleModel.getInitialStates() % maybeStates; - storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true); - boost::optional> stateRewards; - if(this->computeRewards){ - stateRewards = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); - } - std::vector statePriorities = this->eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); - this->reachabilityFunction=std::make_shared(this->eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , phiStates, simpleModel.getStates("target"), stateRewards, statePriorities)); - /* std::string funcStr = " (/ " + - this->reachabilityFunction->nominator().toString(false, true) + " " + - this->reachabilityFunction->denominator().toString(false, true) + - " )"; - std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl;*/ - STORM_LOG_DEBUG("Computed reachabilityFunction"); - std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionEnd = std::chrono::high_resolution_clock::now(); - this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart; - } - - template - void SparseDtmcRegionModelChecker::checkRegions(std::vector& regions) { - STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); - std::cout << "Checking " << regions.size() << " regions. Progress: "; - std::cout.flush(); - - uint_fast64_t progress=0; - uint_fast64_t checkedRegions=0; - for(auto& region : regions){ - checkRegion(region); - if((checkedRegions++)*10/regions.size()==progress){ - std::cout << progress++; - std::cout.flush(); - } - } - std::cout << " done!" << std::endl; - } - - template - void SparseDtmcRegionModelChecker::checkRegion(ParameterRegion& region) { - std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now(); - ++this->numOfCheckedRegions; - - STORM_LOG_THROW(this->specifiedFormula!=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 doFullSmt=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(valueIsInBoundOfFormula(this->getReachabilityValue(region.getSomePoint(), true))){ - 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 lowerBounds; - std::vector upperBounds; - if(!done && doApproximation){ - STORM_LOG_DEBUG("Checking approximative values..."); - if(checkApproximativeValues(region, lowerBounds, upperBounds)){ - ++this->numOfRegionsSolvedThroughApproximation; - STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through approximation."); - done=true; + //Finally, we need to check whether rewardPars and probPars are disjoint + //Note: It would also work to simply rename the parameters that occur in both sets. + //This is to avoid getting functions with local maxima like p * (1-p) + for(auto const& rewardVar : rewardPars){ + if(probPars.find(rewardVar)!=probPars.end()){ + isApproximationApplicable=false; + break; + } } + STORM_LOG_WARN_COND(!isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); } - 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(checkSamplePoints(region)){ - ++this->numOfRegionsSolvedThroughSampling; - STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through sampling."); - done=true; - } + + template + void SparseDtmcRegionModelChecker::computeReachabilityFunction(ParametricSparseModelType const& simpleModel){ + std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionStart = std::chrono::high_resolution_clock::now(); + //get the one step probabilities and the transition matrix of the simple model without target/sink state + storm::storage::SparseMatrix backwardTransitions(simpleModel.getBackwardTransitions()); + std::vector oneStepProbabilities(simpleModel.getNumberOfStates()-2, storm::utility::zero()); + for(auto const& entry : backwardTransitions.getRow(*(simpleModel.getStates("target").begin()))){ + if(entry.getColumn() forwardTransitions=simpleModel.getTransitionMatrix().getSubmatrix(false,maybeStates,maybeStates); + //now compute the functions using methods from elimination model checker + storm::storage::BitVector newInitialStates = simpleModel.getInitialStates() % maybeStates; + storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true); + boost::optional> stateRewards; + if(this->isComputeRewards()){ + stateRewards = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); + } + std::vector statePriorities = this->eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); + this->reachabilityFunction=std::make_shared(this->eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , phiStates, simpleModel.getStates("target"), stateRewards, statePriorities)); + /* std::string funcStr = " (/ " + + this->reachabilityFunction->nominator().toString(false, true) + " " + + this->reachabilityFunction->denominator().toString(false, true) + + " )"; + std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl;*/ + STORM_LOG_DEBUG("Computed reachabilityFunction"); + std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionEnd = std::chrono::high_resolution_clock::now(); + this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart; } - std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now(); - - std::chrono::high_resolution_clock::time_point timeFullSmtStart = std::chrono::high_resolution_clock::now(); - if(!done && doFullSmt){ - STORM_LOG_DEBUG("Checking with Smt Solving..."); - if(checkFullSmt(region)){ - ++this->numOfRegionsSolvedThroughFullSmt; - STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through Smt Solving."); - done=true; + + template + bool SparseDtmcRegionModelChecker::checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { + std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); + this->getApproximationModel()->instantiate(region); + std::chrono::high_resolution_clock::time_point timeMDPBuildEnd = std::chrono::high_resolution_clock::now(); + this->timeApproxModelInstantiation += timeMDPBuildEnd-timeMDPBuildStart; + + // Decide whether to prove allsat or allviolated. (Hence, there are 4 cases) + bool proveAllSat; + switch (region.getCheckResult()){ + case RegionCheckResult::UNKNOWN: + switch(storm::settings::regionSettings().getApproxMode()){ + case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST: + //Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED + checkPoint(region,region.getSomePoint(), false); + proveAllSat= (region.getCheckResult()==RegionCheckResult::EXISTSSAT); + break; + case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLSAT: + proveAllSat=true; + break; + case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLVIOLATED: + proveAllSat=false; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The specified approxmode is not supported"); + } + break; + case RegionCheckResult::ALLSAT: + STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)"); + //Intentionally no break; + case RegionCheckResult::EXISTSSAT: + proveAllSat=true; + break; + case RegionCheckResult::ALLVIOLATED: + STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)"); + //Intentionally no break; + case RegionCheckResult::EXISTSVIOLATED: + proveAllSat=false; + break; + default: + STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative values"); + proveAllSat=true; } - } - std::chrono::high_resolution_clock::time_point timeFullSmtEnd = 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->timeFullSmt += timeFullSmtEnd - timeFullSmtStart; - switch(region.getCheckResult()){ - case RegionCheckResult::EXISTSBOTH: - ++this->numOfRegionsExistsBoth; - break; - case RegionCheckResult::ALLSAT: - ++this->numOfRegionsAllSat; - break; - case RegionCheckResult::ALLVIOLATED: - ++this->numOfRegionsAllViolated; - break; - default: - break; - } - } - - template - bool SparseDtmcRegionModelChecker::checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { - STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions."); - std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); - getApproximationModel()->instantiate(region); - std::chrono::high_resolution_clock::time_point timeMDPBuildEnd = std::chrono::high_resolution_clock::now(); - this->timeMDPBuild += timeMDPBuildEnd-timeMDPBuildStart; - - // Decide whether the formula has an upper or a lower bond ({<, <=} or {>, >=}) and whether to prove allsat or allviolated. (Hence, there are 4 cases) - bool formulaHasUpperBound = this->specifiedFormulaCompType==storm::logic::ComparisonType::Less || this->specifiedFormulaCompType==storm::logic::ComparisonType::LessEqual; - STORM_LOG_THROW((formulaHasUpperBound != (this->specifiedFormulaCompType==storm::logic::ComparisonType::Greater || this->specifiedFormulaCompType==storm::logic::ComparisonType::GreaterEqual)), - storm::exceptions::UnexpectedException, "Unexpected comparison Type of formula"); - bool proveAllSat; - switch (region.getCheckResult()){ - case RegionCheckResult::UNKNOWN: - switch(storm::settings::regionSettings().getApproxMode()){ - case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST: - //Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED - checkPoint(region,region.getSomePoint(), false); - proveAllSat= (region.getCheckResult()==RegionCheckResult::EXISTSSAT); - break; - case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLSAT: - proveAllSat=true; - break; - case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLVIOLATED: - proveAllSat=false; - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The specified approxmode is not supported"); - } - break; - case RegionCheckResult::ALLSAT: - STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)"); - //Intentionally no break; - case RegionCheckResult::EXISTSSAT: - proveAllSat=true; - break; - case RegionCheckResult::ALLVIOLATED: - STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)"); - //Intentionally no break; - case RegionCheckResult::EXISTSVIOLATED: - proveAllSat=false; - break; - default: - STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative values"); - proveAllSat=true; - } - - bool formulaSatisfied; - if((formulaHasUpperBound && proveAllSat) || (!formulaHasUpperBound && !proveAllSat)){ - //these are the cases in which we need to compute upper bounds - upperBounds = getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); - lowerBounds = std::vector(); - formulaSatisfied = valueIsInBoundOfFormula(upperBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); - } - else{ - //for the remaining cases we compute lower bounds - lowerBounds = getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); - upperBounds = std::vector(); - formulaSatisfied = valueIsInBoundOfFormula(lowerBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); - } - - //check if approximation was conclusive - if(proveAllSat && formulaSatisfied){ - region.setCheckResult(RegionCheckResult::ALLSAT); - return true; - } - if(!proveAllSat && !formulaSatisfied){ - region.setCheckResult(RegionCheckResult::ALLVIOLATED); - return true; - } - - if(region.getCheckResult()==RegionCheckResult::UNKNOWN){ - //In this case, it makes sense to try to prove the contrary statement - proveAllSat=!proveAllSat; - - if(lowerBounds.empty()){ - lowerBounds = getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); - formulaSatisfied=valueIsInBoundOfFormula(lowerBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); + + bool formulaSatisfied; + if((this->specifiedFormulaHasUpperBound() && proveAllSat) || (!this->specifiedFormulaHasUpperBound() && !proveAllSat)){ + //these are the cases in which we need to compute upper bounds + upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); + lowerBounds = std::vector(); + formulaSatisfied = this->valueIsInBoundOfFormula(upperBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ - upperBounds = getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); - formulaSatisfied=valueIsInBoundOfFormula(upperBounds[*getApproximationModel()->getModel()->getInitialStates().begin()]); + //for the remaining cases we compute lower bounds + lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); + upperBounds = std::vector(); + formulaSatisfied = this->valueIsInBoundOfFormula(lowerBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); } - + //check if approximation was conclusive if(proveAllSat && formulaSatisfied){ region.setCheckResult(RegionCheckResult::ALLSAT); @@ -674,338 +460,261 @@ namespace storm { region.setCheckResult(RegionCheckResult::ALLVIOLATED); return true; } - } - //if we reach this point than the result is still inconclusive. - return false; - } - - template - std::shared_ptr::ApproximationModel> const& SparseDtmcRegionModelChecker::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->simpleModel, this->simpleFormula); - } - return this->approximationModel; - } - - template - bool SparseDtmcRegionModelChecker::checkSamplePoints(ParameterRegion& 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 - bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { - bool valueInBoundOfFormula; - if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || - (!storm::settings::regionSettings().doSample() && favorViaFunction)){ - //evaluate the reachability function - valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue(point, true)); - } - else{ - //instantiate the sampling model - valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue(point, false)); - } - - if(valueInBoundOfFormula){ - if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){ - region.setSatPoint(point); - if(region.getCheckResult()==RegionCheckResult::EXISTSVIOLATED){ - region.setCheckResult(RegionCheckResult::EXISTSBOTH); + + if(region.getCheckResult()==RegionCheckResult::UNKNOWN){ + //In this case, it makes sense to try to prove the contrary statement + proveAllSat=!proveAllSat; + + if(lowerBounds.empty()){ + lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); + formulaSatisfied=this->valueIsInBoundOfFormula(lowerBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); + } + else{ + upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); + formulaSatisfied=this->valueIsInBoundOfFormula(upperBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); + } + + //check if approximation was conclusive + if(proveAllSat && formulaSatisfied){ + region.setCheckResult(RegionCheckResult::ALLSAT); return true; } - region.setCheckResult(RegionCheckResult::EXISTSSAT); - } - } - else{ - if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){ - region.setViolatedPoint(point); - if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){ - region.setCheckResult(RegionCheckResult::EXISTSBOTH); + if(!proveAllSat && !formulaSatisfied){ + region.setCheckResult(RegionCheckResult::ALLVIOLATED); return true; } - region.setCheckResult(RegionCheckResult::EXISTSVIOLATED); } + //if we reach this point than the result is still inconclusive. + return false; } - return false; - } - - template - std::shared_ptr::SamplingModel> const& SparseDtmcRegionModelChecker::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->simpleModel, this->simpleFormula); - } - return this->samplingModel; - } - - template - std::shared_ptr::ParametricType> const& SparseDtmcRegionModelChecker::getReachabilityFunction() { - if(this->reachabilityFunction==nullptr){ - STORM_LOG_WARN("Reachability Function requested but it has not been computed when specifying the formula. Will compute it now."); - computeReachabilityFunction(*this->simpleModel); - } - return this->reachabilityFunction; - } - - template - template - ValueType SparseDtmcRegionModelChecker::getReachabilityValue(std::map const& point, bool evaluateFunction) { - if(this->isResultConstant){ - //Todo: remove workaround (infinityisResultInfinity){ - return storm::utility::infinity(); - } - STORM_LOG_THROW(storm::utility::isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); - return storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(*getReachabilityFunction())); - } - if(evaluateFunction){ - return storm::utility::regions::convertNumber(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point)); - } else { - getSamplingModel()->instantiate(point); - return storm::utility::regions::convertNumber(getSamplingModel()->computeValues()[*getSamplingModel()->getModel()->getInitialStates().begin()]); - } - } + template + bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { + bool valueInBoundOfFormula; + if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) || + (!storm::settings::regionSettings().doSample() && favorViaFunction)){ + //evaluate the reachability function + valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue(point, true)); + } + else{ + //instantiate the sampling model + valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue(point, false)); + } - template - bool SparseDtmcRegionModelChecker::checkFullSmt(ParameterRegion& region) { - STORM_LOG_THROW((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented."); - if (region.getCheckResult()==RegionCheckResult::UNKNOWN){ - //Sampling needs to be done (on a single point) - checkPoint(region,region.getSomePoint(), true); - } - - if(this->smtSolver==nullptr){ - initializeSMTSolver(); - } - - this->smtSolver->push(); - - //add constraints for the region - for(auto const& variable : region.getVariables()) { - storm::utility::regions::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::GreaterEqual, region.getLowerBound(variable)); - storm::utility::regions::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::LessEqual, region.getUpperBound(variable)); - } - - //add constraint that states what we want to prove - VariableType proveAllSatVar=storm::utility::regions::getVariableFromString("storm_proveAllSat"); - VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString("storm_proveAllViolated"); - switch(region.getCheckResult()){ - case RegionCheckResult::EXISTSBOTH: - STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkFullSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now..."); - case RegionCheckResult::ALLSAT: - STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLSAT), "checkFullSmt invoked although the result is already clear (ALLSAT). Will validate this now..."); - case RegionCheckResult::EXISTSSAT: - storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, true); - storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, false); - break; - case RegionCheckResult::ALLVIOLATED: - STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLVIOLATED), "checkFullSmt invoked although the result is already clear (ALLVIOLATED). Will validate this now..."); - case RegionCheckResult::EXISTSVIOLATED: - storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, false); - storm::utility::regions::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, true); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not handle the current region CheckResult: " << region.checkResultToString()); - } - - storm::solver::SmtSolver::CheckResult solverResult= this->smtSolver->check(); - this->smtSolver->pop(); - - switch(solverResult){ - case storm::solver::SmtSolver::CheckResult::Sat: - switch(region.getCheckResult()){ - case RegionCheckResult::EXISTSSAT: + if(valueInBoundOfFormula){ + if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){ + region.setSatPoint(point); + if(region.getCheckResult()==RegionCheckResult::EXISTSVIOLATED){ region.setCheckResult(RegionCheckResult::EXISTSBOTH); - //There is also a violated point - STORM_LOG_WARN("Extracting a violated point from the smt solver is not yet implemented!"); - break; - case RegionCheckResult::EXISTSVIOLATED: - region.setCheckResult(RegionCheckResult::EXISTSBOTH); - //There is also a sat point - STORM_LOG_WARN("Extracting a sat point from the smt solver is not yet implemented!"); - break; - case RegionCheckResult::EXISTSBOTH: - //That was expected - STORM_LOG_WARN("result EXISTSBOTH Validated!"); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (sat)"); - } - return true; - case storm::solver::SmtSolver::CheckResult::Unsat: - switch(region.getCheckResult()){ - case RegionCheckResult::EXISTSSAT: - region.setCheckResult(RegionCheckResult::ALLSAT); - break; - case RegionCheckResult::EXISTSVIOLATED: - region.setCheckResult(RegionCheckResult::ALLVIOLATED); - break; - case RegionCheckResult::ALLSAT: - //That was expected... - STORM_LOG_WARN("result ALLSAT Validated!"); - break; - case RegionCheckResult::ALLVIOLATED: - //That was expected... - STORM_LOG_WARN("result ALLVIOLATED Validated!"); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (unsat)"); + return true; + } + region.setCheckResult(RegionCheckResult::EXISTSSAT); } - return true; - case storm::solver::SmtSolver::CheckResult::Unknown: - default: - STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)"); - if(this->smtSolver->isNeedsRestart()){ - initializeSMTSolver(); + } + else{ + if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){ + region.setViolatedPoint(point); + if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){ + region.setCheckResult(RegionCheckResult::EXISTSBOTH); + return true; + } + region.setCheckResult(RegionCheckResult::EXISTSVIOLATED); } - return false; - } - } - - template - void SparseDtmcRegionModelChecker::initializeSMTSolver() { - - storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions.. - this->smtSolver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); - - ParametricType bound= storm::utility::regions::convertNumber(this->specifiedFormulaBound); - - // To prove that the property is satisfied in the initial state for all parameters, - // we ask the solver whether the negation of the property is satisfiable and invert the answer. - // In this case, assert that this variable is true: - VariableType proveAllSatVar=storm::utility::regions::getNewVariable("storm_proveAllSat", storm::utility::regions::VariableSort::VS_BOOL); - - //Example: - //Property: P<=p [ F 'target' ] holds iff... - // f(x) <= p - // Hence: If f(x) > p is unsat, the property is satisfied for all parameters. - - storm::logic::ComparisonType proveAllSatRel; //the relation from the property needs to be inverted - switch (this->specifiedFormulaCompType) { - case storm::logic::ComparisonType::Greater: - proveAllSatRel=storm::logic::ComparisonType::LessEqual; - break; - case storm::logic::ComparisonType::GreaterEqual: - proveAllSatRel=storm::logic::ComparisonType::Less; - break; - case storm::logic::ComparisonType::Less: - proveAllSatRel=storm::logic::ComparisonType::GreaterEqual; - break; - case storm::logic::ComparisonType::LessEqual: - proveAllSatRel=storm::logic::ComparisonType::Greater; - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); + } + return false; } - storm::utility::regions::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllSatVar, *getReachabilityFunction(), proveAllSatRel, bound); - - // To prove that the property is violated in the initial state for all parameters, - // we ask the solver whether the the property is satisfiable and invert the answer. - // In this case, assert that this variable is true: - VariableType proveAllViolatedVar=storm::utility::regions::getNewVariable("storm_proveAllViolated", storm::utility::regions::VariableSort::VS_BOOL); - - //Example: - //Property: P<=p [ F 'target' ] holds iff... - // f(x) <= p - // Hence: If f(x) <= p is unsat, the property is violated for all parameters. - storm::logic::ComparisonType proveAllViolatedRel = this->specifiedFormulaCompType; - storm::utility::regions::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllViolatedVar, *getReachabilityFunction(), proveAllViolatedRel, bound); - } - - template - template - bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType const& value){ - STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified."); - double valueAsDouble = storm::utility::regions::convertNumber(value); - switch (this->specifiedFormulaCompType) { - case storm::logic::ComparisonType::Greater: - return (valueAsDouble > this->specifiedFormulaBound); - case storm::logic::ComparisonType::GreaterEqual: - return (valueAsDouble >= this->specifiedFormulaBound); - case storm::logic::ComparisonType::Less: - return (valueAsDouble < this->specifiedFormulaBound); - case storm::logic::ComparisonType::LessEqual: - return (valueAsDouble <= this->specifiedFormulaBound); - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); + + template + std::shared_ptr::ParametricType> const& SparseDtmcRegionModelChecker::getReachabilityFunction() { + if(this->reachabilityFunction==nullptr){ + STORM_LOG_WARN("Reachability Function requested but it has not been computed when specifying the formula. Will compute it now."); + computeReachabilityFunction(*this->getSimpleModel()); + } + return this->reachabilityFunction; } - } - - template - void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { - - if(this->specifiedFormula==nullptr){ - outstream << "Region Model Checker Statistics Error: No formula specified." << std::endl; - return; + + template + ConstantType SparseDtmcRegionModelChecker::getReachabilityValue(std::map const& point, bool evaluateFunction) { + if(this->isResultConstant()){ + //Todo: remove workaround (infinity() does not work) + if(this->isResultInfinity){ + return storm::utility::infinity(); + } + STORM_LOG_THROW(storm::utility::isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); + return storm::utility::region::convertNumber(storm::utility::region::getConstantPart(*getReachabilityFunction())); + } + if(evaluateFunction){ + return storm::utility::region::convertNumber(this->evaluateReachabilityFunction(point)); + } else { + this->getSamplingModel()->instantiate(point); + return storm::utility::region::convertNumber(this->getSamplingModel()->computeValues()[*this->getSamplingModel()->getModel()->getInitialStates().begin()]); + } } - std::chrono::milliseconds timeSpecifyFormulaInMilliseconds = std::chrono::duration_cast(this->timeSpecifyFormula); - std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast(this->timePreprocessing); - std::chrono::milliseconds timeInitSamplingModelInMilliseconds = std::chrono::duration_cast(this->timeInitSamplingModel); - std::chrono::milliseconds timeInitApproxModelInMilliseconds = std::chrono::duration_cast(this->timeInitApproxModel); - std::chrono::milliseconds timeComputeReachabilityFunctionInMilliseconds = std::chrono::duration_cast(this->timeComputeReachabilityFunction); - std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast(this->timeCheckRegion); - std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast(this->timeSampling); - std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast(this->timeApproximation); - std::chrono::milliseconds timeMDPBuildInMilliseconds = std::chrono::duration_cast(this->timeMDPBuild); - std::chrono::milliseconds timeFullSmtInMilliseconds = std::chrono::duration_cast(this->timeFullSmt); - - std::chrono::high_resolution_clock::duration timeOverall = timeSpecifyFormula + timeCheckRegion; // + ... - std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(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->specifiedFormula << std::endl; - if(this->isResultConstant){ - outstream << "The requested value is constant (i.e. independent of any parameters)" << std::endl; + template + typename SparseDtmcRegionModelChecker::CoefficientType SparseDtmcRegionModelChecker::evaluateReachabilityFunction(std::map const& point) { + if(this->isResultConstant()){ + //Todo: remove workaround (infinity() does not work) + STORM_LOG_THROW(!this->isResultInfinity, storm::exceptions::NotSupportedException, "Requested the reachability value but can not represent it as a Coefficient type (The value is infinity)"); + STORM_LOG_THROW(storm::utility::isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); + return storm::utility::region::convertNumber(storm::utility::region::getConstantPart(*getReachabilityFunction())); + } + return storm::utility::region::evaluateFunction(*getReachabilityFunction(), point); } - else{ - outstream << "Simple model: " << this->simpleModel->getNumberOfStates() << " states, " << this->simpleModel->getNumberOfTransitions() << " transitions" << std::endl; + + + template + bool SparseDtmcRegionModelChecker::checkSmt(ParameterRegion& region) { + STORM_LOG_THROW((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented."); + if (region.getCheckResult()==RegionCheckResult::UNKNOWN){ + //Sampling needs to be done (on a single point) + checkPoint(region,region.getSomePoint(), true); + } + + if(this->smtSolver==nullptr){ + initializeSMTSolver(); + } + + this->smtSolver->push(); + + //add constraints for the region + for(auto const& variable : region.getVariables()) { + storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::GreaterEqual, region.getLowerBound(variable)); + storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::LessEqual, region.getUpperBound(variable)); + } + + //add constraint that states what we want to prove + VariableType proveAllSatVar=storm::utility::region::getVariableFromString("storm_proveAllSat"); + VariableType proveAllViolatedVar=storm::utility::region::getVariableFromString("storm_proveAllViolated"); + switch(region.getCheckResult()){ + case RegionCheckResult::EXISTSBOTH: + STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now..."); + case RegionCheckResult::ALLSAT: + STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLSAT), "checkSmt invoked although the result is already clear (ALLSAT). Will validate this now..."); + case RegionCheckResult::EXISTSSAT: + storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, true); + storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, false); + break; + case RegionCheckResult::ALLVIOLATED: + STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLVIOLATED), "checkSmt invoked although the result is already clear (ALLVIOLATED). Will validate this now..."); + case RegionCheckResult::EXISTSVIOLATED: + storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, false); + storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, true); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not handle the current region CheckResult: " << region.getCheckResult()); + } + + storm::solver::SmtSolver::CheckResult solverResult= this->smtSolver->check(); + this->smtSolver->pop(); + + switch(solverResult){ + case storm::solver::SmtSolver::CheckResult::Sat: + switch(region.getCheckResult()){ + case RegionCheckResult::EXISTSSAT: + region.setCheckResult(RegionCheckResult::EXISTSBOTH); + //There is also a violated point + STORM_LOG_WARN("Extracting a violated point from the smt solver is not yet implemented!"); + break; + case RegionCheckResult::EXISTSVIOLATED: + region.setCheckResult(RegionCheckResult::EXISTSBOTH); + //There is also a sat point + STORM_LOG_WARN("Extracting a sat point from the smt solver is not yet implemented!"); + break; + case RegionCheckResult::EXISTSBOTH: + //That was expected + STORM_LOG_WARN("result EXISTSBOTH Validated!"); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (sat)"); + } + return true; + case storm::solver::SmtSolver::CheckResult::Unsat: + switch(region.getCheckResult()){ + case RegionCheckResult::EXISTSSAT: + region.setCheckResult(RegionCheckResult::ALLSAT); + break; + case RegionCheckResult::EXISTSVIOLATED: + region.setCheckResult(RegionCheckResult::ALLVIOLATED); + break; + case RegionCheckResult::ALLSAT: + //That was expected... + STORM_LOG_WARN("result ALLSAT Validated!"); + break; + case RegionCheckResult::ALLVIOLATED: + //That was expected... + STORM_LOG_WARN("result ALLVIOLATED Validated!"); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (unsat)"); + } + return true; + case storm::solver::SmtSolver::CheckResult::Unknown: + default: + STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)"); + if(this->smtSolver->isNeedsRestart()){ + initializeSMTSolver(); + } + return false; + } } - 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->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl; - outstream << std::endl; + + template + void SparseDtmcRegionModelChecker::initializeSMTSolver() { + + storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions.. + this->smtSolver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); + + ParametricType bound= storm::utility::region::convertNumber(this->getSpecifiedFormulaBound()); + + // To prove that the property is satisfied in the initial state for all parameters, + // we ask the solver whether the negation of the property is satisfiable and invert the answer. + // In this case, assert that this variable is true: + VariableType proveAllSatVar=storm::utility::region::getNewVariable("storm_proveAllSat", storm::utility::region::VariableSort::VS_BOOL); + + //Example: + //Property: P<=p [ F 'target' ] holds iff... + // f(x) <= p + // Hence: If f(x) > p is unsat, the property is satisfied for all parameters. + + storm::logic::ComparisonType proveAllSatRel; //the relation from the property needs to be inverted + switch (this->getSpecifiedFormulaCompType()) { + case storm::logic::ComparisonType::Greater: + proveAllSatRel=storm::logic::ComparisonType::LessEqual; + break; + case storm::logic::ComparisonType::GreaterEqual: + proveAllSatRel=storm::logic::ComparisonType::Less; + break; + case storm::logic::ComparisonType::Less: + proveAllSatRel=storm::logic::ComparisonType::GreaterEqual; + break; + case storm::logic::ComparisonType::LessEqual: + proveAllSatRel=storm::logic::ComparisonType::Greater; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); + } + storm::utility::region::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllSatVar, *getReachabilityFunction(), proveAllSatRel, bound); + + // To prove that the property is violated in the initial state for all parameters, + // we ask the solver whether the the property is satisfiable and invert the answer. + // In this case, assert that this variable is true: + VariableType proveAllViolatedVar=storm::utility::region::getNewVariable("storm_proveAllViolated", storm::utility::region::VariableSort::VS_BOOL); + + //Example: + //Property: P<=p [ F 'target' ] holds iff... + // f(x) <= p + // Hence: If f(x) <= p is unsat, the property is violated for all parameters. + storm::logic::ComparisonType proveAllViolatedRel = this->getSpecifiedFormulaCompType(); + storm::utility::region::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllViolatedVar, *getReachabilityFunction(), proveAllViolatedRel, bound); } - 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)" << 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 << " " << timeComputeReachabilityFunctionInMilliseconds.count() << "ms to compute the reachability function" << std::endl; - outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; - outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; - outstream << " " << timeMDPBuildInMilliseconds.count() << "ms to build the MDP" << std::endl; - outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl; - outstream << " " << timeFullSmtInMilliseconds.count() << "ms Smt solving" << std::endl; - outstream << "-----------------------------------------------" << std::endl; - - } - + + + #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker, double>; + template class SparseDtmcRegionModelChecker>, double>; #endif - //note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h - + //note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h + } // namespace region } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index 375bbbf5a..f3b993137 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -1,289 +1,155 @@ #ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ -#include +#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 - class SparseDtmcRegionModelChecker { - public: - - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename storm::utility::regions::VariableType VariableType; - typedef typename storm::utility::regions::CoefficientType 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 + class SparseDtmcRegionModelChecker : public AbstractSparseRegionModelChecker { + public: + + typedef typename ParametricSparseModelType::ValueType ParametricType; + typedef typename ParametricSparseModelType::RewardModelType ParametricRewardModelType; + typedef typename storm::utility::region::VariableType VariableType; + typedef typename storm::utility::region::CoefficientType 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 const& getReachabilityFunction(); - explicit SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc 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::mapconst& 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::mapconst& 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 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& simpleModel, std::shared_ptr& 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& 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 const& getReachabilityFunction(); - - /*! - * Returns the reachability Value at the specified point. - * The given flag decides whether to initialize a sampling model or to evaluate a reachability function. - * Might invoke sampling model initialization or the computation of the reachability function (if these are not available yet) - * - * @param point The point (i.e. parameter evaluation) at which to compute the reachability value. - * @param evaluateFunction If set, the reachability function is evaluated. Otherwise, the sampling model is instantiated. - */ - template - ValueType getReachabilityValue(std::mapconst& point, bool evaluateFunction=false); - - /*! - * Prints statistical information to the given stream. - */ - 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& stateRewards); - - /*! - * initializes the Approximation Model - * - * @note does not check whether approximation can be applied - */ - void initializeApproximationModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula); - - /*! - * initializes the Sampling Model - */ - void initializeSamplingModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula); - - /*! - * Computes the reachability function via state elimination - * @note computeFlagsAndSimplifiedModel should be called before calling this - */ - void computeReachabilityFunction(storm::models::sparse::Dtmc 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& lowerBounds, std::vector& upperBounds); - - /*! - * Returns the approximation model. - * If it is not yet available, it is computed. - */ - std::shared_ptr 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::mapconst& point, bool favorViaFunction=false); - - /*! - * Returns the sampling model. - * If it is not yet available, it is computed. - */ - std::shared_ptr 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 - bool valueIsInBoundOfFormula(ValueType const& value); - - // The model this model checker is supposed to analyze. - storm::models::sparse::Dtmc const& model; - - //classes that provide auxilliary functions - // Instance of an elimination model checker to access its functions - storm::modelchecker::SparseDtmcEliminationModelChecker> eliminationModelChecker; - - //the following members depend on the currently specified formula: - //the currently specified formula, the bound and the comparison type - std::shared_ptr specifiedFormula; - bool computeRewards; - storm::logic::ComparisonType specifiedFormulaCompType; - double specifiedFormulaBound; - - // the original model after states with constant transitions have been eliminated - std::shared_ptr> simpleModel; - // a formula that can be checked on the simplified model - std::shared_ptr simpleFormula; - // the model that is used to approximate the reachability values - std::shared_ptr approximationModel; - // the model that can be instantiated to check the value at a certain point - std::shared_ptr samplingModel; - // The function for the reachability probability (or: reachability reward) in the initial state - std::shared_ptr 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() does not work at this moment) - bool isResultInfinity; - // the smt solver that is used to prove properties with the help of the reachabilityFunction - std::shared_ptr smtSolver; - - // 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& 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& region, std::vector& lowerBounds, std::vector& 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& region, std::mapconst& 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& 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 reachabilityFunction; + // workaround to represent that the result is infinity (utility::infinity() does not work at this moment) + bool isResultInfinity; + + // Instance of an elimination model checker to access its functions + storm::modelchecker::SparseDtmcEliminationModelChecker> eliminationModelChecker; + + // the smt solver that is used to prove properties with the help of the reachabilityFunction + std::shared_ptr smtSolver; + + }; + } //namespace region } // namespace modelchecker } // namespace storm diff --git a/src/utility/regions.h b/src/utility/region.h similarity index 99% rename from src/utility/regions.h rename to src/utility/region.h index 7547f47b6..9595845ee 100644 --- a/src/utility/regions.h +++ b/src/utility/region.h @@ -30,7 +30,7 @@ namespace storm { namespace utility{ - namespace regions { + namespace region { #ifdef STORM_HAVE_CARL template diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index 868e62b8f..2592f3a68 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -7,7 +7,7 @@ #include -#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 const& number){ diff --git a/src/utility/storm.h b/src/utility/storm.h index 23a8e4fad..d1e96b60f 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -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, double>::ParameterRegion::getRegionsFromSettings(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + auto regions=storm::modelchecker::region::ParameterRegion::getRegionsFromSettings(); + storm::modelchecker::region::SparseDtmcRegionModelChecker, 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); diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index eaeaf350f..1034811de 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -37,27 +37,27 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); - EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + 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, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); + auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); + auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95"); - auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95"); + auto exBothHardRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); - EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue(exBothHardRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue(exBothHardRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue(exBothHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue(exBothHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + 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, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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, double>::RegionCheckResult::EXISTSBOTH)) || - (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker, 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, 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, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75"); - auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); + auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95"); + auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75"); + auto exBothHardRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); //test smt + approx - auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker, 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::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, 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion(""); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); - EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false)); //instantiation of sampling model - EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true)); //instantiation of sampling model + EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false)); //instantiation of sampling model + EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true)); //instantiation of sampling model //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); @@ -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, 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, double>::ParameterRegion::parseRegion(""); + auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion(""); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, 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, 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, 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::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::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::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); - EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + 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, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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, 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, 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, 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::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::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::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, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); - auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); + auto allVioHardRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); - EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue(allVioHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue(allVioHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + 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, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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, double>::RegionCheckResult::ALLVIOLATED)) || - (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker, 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, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); - auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); + auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); + auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); + auto allVioHardRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult()); //test smt + approx - auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + auto allVioHardRegionSmtApp=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allVioHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8"); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.9<=PF<=0.99"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.9"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.01<=PF<=0.8"); - EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model - EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + 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, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8"); + auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.9<=PF<=0.99"); + auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.9"); + auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.01<=PF<=0.8"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program.get(), options)->as>(); ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); + storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion(""); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); - EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function - EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function + 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, 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, double>::ParameterRegion::parseRegion(""); + auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion(""); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); }