From f72c30cdff81c3c19b54fdbcdbd387b8d38d403e Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 12 Sep 2015 14:48:41 +0200 Subject: [PATCH] First version of approximation model (with mdp intead of s2pg) Former-commit-id: 86fdbc5f3615baa0fb330950e751b94d5ee9a76c --- .../AbstractSparseRegionModelChecker.cpp | 102 ++++++++++++++++- .../region/AbstractSparseRegionModelChecker.h | 4 +- .../region/ApproximationModel.cpp | 104 +++++++++++++----- src/modelchecker/region/ApproximationModel.h | 24 ++-- src/modelchecker/region/SamplingModel.cpp | 9 +- .../region/SparseDtmcRegionModelChecker.cpp | 95 ---------------- .../region/SparseDtmcRegionModelChecker.h | 11 -- .../region/SparseMdpRegionModelChecker.cpp | 96 ---------------- .../region/SparseMdpRegionModelChecker.h | 11 -- 9 files changed, 192 insertions(+), 264 deletions(-) diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index 328d2e9b4..2bb506a20 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -81,9 +81,6 @@ namespace storm { return this->simpleFormula; } - - - template void AbstractSparseRegionModelChecker::specifyFormula(std::shared_ptr formula) { std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now(); @@ -153,7 +150,7 @@ namespace storm { 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_DEBUG("The Approximation Model is initialized"); + STORM_LOG_DEBUG("Initializing the Approximation Model..."); 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(); @@ -163,7 +160,7 @@ namespace storm { template void AbstractSparseRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) { - STORM_LOG_DEBUG("The Sampling Model is initialized"); + STORM_LOG_DEBUG("Initializing the Sampling Model...."); 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(); @@ -272,7 +269,102 @@ namespace storm { break; } } + + template + bool AbstractSparseRegionModelChecker::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. + 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((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{ + //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); + 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 = 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; + } + if(!proveAllSat && !formulaSatisfied){ + region.setCheckResult(RegionCheckResult::ALLVIOLATED); + return true; + } + } + //if we reach this point than the result is still inconclusive. + return false; + } + template std::shared_ptr> const& AbstractSparseRegionModelChecker::getApproximationModel() { if(this->approximationModel==nullptr){ diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/modelchecker/region/AbstractSparseRegionModelChecker.h index 70e5d70bc..415145e69 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.h +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.h @@ -130,7 +130,7 @@ namespace storm { * 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; + bool checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds); /*! * Returns the approximation model. @@ -223,10 +223,10 @@ namespace storm { 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 timeApproxModelInstantiation; 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 diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index aba216cc8..f45f5fc77 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -4,9 +4,12 @@ * * Created on August 7, 2015, 9:29 AM */ +#include "src/modelchecker/region/ApproximationModel.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/ModelType.h" #include "src/models/sparse/StandardRewardModel.h" -#include "src/modelchecker/region/ApproximationModel.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/macros.h" @@ -14,6 +17,7 @@ #include "src/utility/vector.h" #include "src/exceptions/UnexpectedException.h" #include "src/exceptions/InvalidArgumentException.h" +#include "exceptions/NotImplementedException.h" namespace storm { namespace modelchecker { @@ -32,12 +36,13 @@ namespace storm { } //Start with the probabilities storm::storage::SparseMatrix probabilityMatrix; + std::vector::index_type> approxRowGroupIndices;// Indicates which rows of the probabilityMatrix belong to a given row of the parametricModel 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); + initializeProbabilities(parametricModel, probabilityMatrix, approxRowGroupIndices, rowSubstitutions, matrixEntryToEvalTableMapping, &constantProbEntry); //Now consider rewards @@ -46,22 +51,34 @@ namespace storm { 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); + initializeRewards(parametricModel, probabilityMatrix, approxRowGroupIndices, 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)); + boost::optional>> noChoiceLabeling; + switch(parametricModel.getType()){ + case storm::models::ModelType::Dtmc: + this->model=std::make_shared>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); + break; + case storm::models::ModelType::Mdp: + //TODO: use a two-player-game here + this->model=std::make_shared>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Tried to build an Approximation model for an unsupported model type"); + } + //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){ + for (; matrixRowmodel->getTransitionMatrix().getRow(matrixRow).begin(); for(auto const& parEntry : parametricModel.getTransitionMatrix().getRow(row)){ if(*tableEntry == &constantProbEntry){ + STORM_LOG_THROW(storm::utility::isConstant(parEntry.getValue()), storm::exceptions::UnexpectedException, "Expected a constant matrix entry but got a non-constant one."); approxModelEntry->setValue(storm::utility::region::convertNumber(storm::utility::region::getConstantPart(parEntry.getValue()))); } else { this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry)); @@ -96,20 +113,37 @@ namespace storm { template void ApproximationModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, + std::vector::index_type>& approxRowGroupIndices, std::vector& rowSubstitutions, std::vector& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry) { + STORM_LOG_DEBUG("Approximation model initialization for probabilities"); // 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 + // a probability matrix with some dummy entries, and the mapping between the two + //TODO: if the parametricModel is nondeterministic, we will need a matrix for a two player game. For now, we assume the two players cooperate, i.e. we get a simple MDP + bool customRowGroups = parametricModel.getTransitionMatrix().hasNontrivialRowGrouping(); + auto curParamRowGroup = parametricModel.getTransitionMatrix().getRowGroupIndices().begin(); + storm::storage::SparseMatrixBuilder matrixBuilder(0, //unknown number of rows + parametricModel.getTransitionMatrix().getColumnCount(), + 0, //Unknown number of entries + true, //force dimensions + true, //will have custom row grouping + parametricModel.getNumberOfStates()); + approxRowGroupIndices.reserve(parametricModel.getTransitionMatrix().getRowCount()+1); 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); + typename storm::storage::SparseMatrix::index_type apprModelMatrixRow=0; + for(typename storm::storage::SparseMatrix::index_type paramRow=0; paramRow < parametricModel.getTransitionMatrix().getRowCount(); ++paramRow ){ + approxRowGroupIndices.push_back(apprModelMatrixRow); + if(customRowGroups && paramRow==*curParamRowGroup){ + //Only make a new row group if the parametric model matrix has a new row group at this position + matrixBuilder.newRowGroup(apprModelMatrixRow); + ++curParamRowGroup; + } else if (!customRowGroups){ + matrixBuilder.newRowGroup(apprModelMatrixRow); + } // 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)){ + for(auto const& entry : parametricModel.getTransitionMatrix().getRow(paramRow)){ storm::utility::region::gatherOccurringVariables(entry.getValue(), occurringVariables); } std::size_t numOfSubstitutions=1ull<(); - for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){ + for(auto const& entry : parametricModel.getTransitionMatrix().getRow(paramRow)){ if(storm::utility::isConstant(entry.getValue())){ matrixEntryToEvalTableMapping.emplace_back(constantEntry); } else { @@ -141,30 +175,33 @@ namespace storm { auto evalTableIt = this->probabilityEvaluationTable.insert(ProbTableEntry(FunctionSubstitution(entry.getValue(), substitutionIndex), storm::utility::zero())).first; matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt)); } - matrixBuilder.addNextValue(matrixRow, entry.getColumn(), dummyEntry); + matrixBuilder.addNextValue(apprModelMatrixRow, entry.getColumn(), dummyEntry); dummyEntry=storm::utility::zero(); } - ++matrixRow; + ++apprModelMatrixRow; } } this->probabilityMapping.reserve(numOfNonConstEntries); probabilityMatrix=matrixBuilder.build(); + approxRowGroupIndices.push_back(apprModelMatrixRow); } template void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, + std::vector::index_type> const& approxRowGroupIndices, std::vector const& rowSubstitutions, std::vector& stateActionRewardVector, std::vector& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry){ + STORM_LOG_DEBUG("Approximation model initialization for Rewards"); + STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Rewards are only supported for DTMCs (yet)"); // Todo : check if this code also works for rewards on mdps (we should then consider state action rewards of the original model and approxRowGroupIndices) // 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; @@ -185,7 +222,7 @@ namespace storm { 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); @@ -193,7 +230,7 @@ namespace storm { rewardSubstitution.insert(std::make_pair(rewardVar, TypeOfBound::CHOSEOPTIMAL)); } else { rewardSubstitution.insert(*substitutionIt); - rewardDependsOnProbVars=true; + rewardDependsOnProbVars=true; //.. assumption wrong } } std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution)); @@ -221,7 +258,7 @@ namespace storm { } template - std::shared_ptr> const& ApproximationModel::getModel() const { + std::shared_ptr> const& ApproximationModel::getModel() const { return this->model; } @@ -306,13 +343,26 @@ namespace storm { } template - std::vector const& ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) { - storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(*this->model); + std::vector const& ApproximationModel::computeValues(storm::solver::OptimizationDirection const& approximationOpDir) { + std::unique_ptr modelChecker; + switch(this->getModel()->getType()){ + case storm::models::ModelType::Mdp: + modelChecker = std::make_unique>>(*this->model->template as>()); + break; + case storm::models::ModelType::S2pg: + //TODO: instantiate right model checker here + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation with two player games not yet implemented"); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Tried to build an approximation model for an unsupported model type"); + } std::unique_ptr resultPtr; + //TODO: use this when two player games are available + boost::optional formulaOpDir = storm::logic::isLowerBound(this->formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; if(this->computeRewards){ //write the reward values into the model - switch(optDir){ + switch(approximationOpDir){ case storm::solver::OptimizationDirection::Minimize: for(auto& mappingTriple : this->rewardMapping){ *std::get<2>(mappingTriple)=*std::get<0>(mappingTriple); @@ -326,13 +376,13 @@ namespace storm { default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given optimality Type is not supported."); } - //perform model checking on the mdp + //perform model checking boost::optional noRewardModelName; //it should be uniquely given - resultPtr = modelChecker.computeReachabilityRewards(this->formula->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula(), noRewardModelName, false, optDir); + resultPtr = modelChecker->computeReachabilityRewards(this->formula->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula(), noRewardModelName, false, approximationOpDir); } else { - //perform model checking on the mdp - resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(), false, optDir); + //perform model checking + resultPtr = modelChecker->computeEventuallyProbabilities(this->formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(), false, approximationOpDir); } return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); } diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index ca25267cf..0e5866ab8 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -10,12 +10,11 @@ #include #include -#include "src/utility/region.h" -#include "src/logic/Formulas.h" +#include "src/utility/region.h" #include "src/modelchecker/region/ParameterRegion.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/Mdp.h" +#include "src/logic/Formulas.h" +#include "src/models/sparse/Model.h" #include "src/storage/SparseMatrix.h" namespace storm { @@ -29,7 +28,8 @@ namespace storm { typedef typename storm::utility::region::CoefficientType CoefficientType; /*! - * @note this will not check whether approximation is applicable + * Creates an Approximation model + * @note This will not check whether approximation is applicable */ ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); virtual ~ApproximationModel(); @@ -37,7 +37,7 @@ namespace storm { /*! * returns the underlying model */ - std::shared_ptr> const& getModel() const; + std::shared_ptr> const& getModel() const; /*! * Instantiates the underlying model according to the given region @@ -45,11 +45,11 @@ namespace storm { void instantiate(ParameterRegion const& region); /*! - * Returns the approximated reachability probabilities or expected values for every state. + * Returns the approximated reachability probabilities or reward values 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 + * @param approximationOpDir Use MAXIMIZE to get upper bounds or MINIMIZE to get lower bounds */ - std::vector const& computeValues(storm::solver::OptimizationDirection const& optDir); + std::vector const& computeValues(storm::solver::OptimizationDirection const& approximationOpDir); private: @@ -123,11 +123,11 @@ namespace storm { 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); + void initializeProbabilities(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector::index_type>& approxRowGroupIndices, std::vector& rowSubstitutions, std::vector& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry); + void initializeRewards(ParametricSparseModelType const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector::index_type> const& approxRowGroupIndices, std::vector const& rowSubstitutions, std::vector& stateActionRewardVector, std::vector& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry); //The Model with which we work - std::shared_ptr> model; + 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 diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 8282e777e..2ff5a37e5 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -9,6 +9,8 @@ #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Mdp.h" +#include "src/models/ModelType.h" +#include "models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -17,9 +19,6 @@ #include "src/utility/vector.h" #include "src/exceptions/UnexpectedException.h" #include "src/exceptions/InvalidArgumentException.h" -#include "models/sparse/StandardRewardModel.h" -#include "cuddObj.hh" -#include "exceptions/IllegalArgumentException.h" namespace storm { namespace modelchecker { @@ -63,7 +62,7 @@ namespace storm { this->model=std::make_shared>(std::move(probabilityMatrix), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); break; default: - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Tried to build a sampling model for an unsupported model type"); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Tried to build a sampling model for an unsupported model type"); } //translate the matrixEntryToEvalTableMapping into the actual probability mapping @@ -196,7 +195,7 @@ namespace storm { modelChecker = std::make_unique>>(*this->model->template as>()); break; default: - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Tried to build a sampling model for an unsupported model type"); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Tried to build a sampling model for an unsupported model type"); } std::unique_ptr resultPtr; //perform model checking diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index d0ae9bc8d..b349a475e 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -409,101 +409,6 @@ namespace storm { this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart; } - 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. - 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((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{ - //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); - 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 = 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; - } - if(!proveAllSat && !formulaSatisfied){ - region.setCheckResult(RegionCheckResult::ALLVIOLATED); - return true; - } - } - //if we reach this point than the result is still inconclusive. - return false; - } - template bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { bool valueInBoundOfFormula; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index a36b22b80..53bbf6d09 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -89,17 +89,6 @@ namespace storm { */ 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. diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index 37fe200a5..d0c2da693 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -131,102 +131,6 @@ namespace storm { } } - template - bool SparseMdpRegionModelChecker::checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { - std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The approximation model for mdps has not been implemented yet"); - 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. - 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((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{ - //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); - 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 = 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; - } - if(!proveAllSat && !formulaSatisfied){ - region.setCheckResult(RegionCheckResult::ALLVIOLATED); - return true; - } - } - //if we reach this point than the result is still inconclusive. - return false; - } - template bool SparseMdpRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { if(this->valueIsInBoundOfFormula(this->getReachabilityValue(point))){ diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.h b/src/modelchecker/region/SparseMdpRegionModelChecker.h index 19a3dbd3b..da5503b49 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.h @@ -55,17 +55,6 @@ namespace storm { */ void preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, bool& isApproximationApplicable, boost::optional& constantResult); - /*! - * 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.