From 0043d3ebf564416ef68e1ff2102de90dc1cd272a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 8 Sep 2015 17:45:30 +0200 Subject: [PATCH] changed template argument, used unordered_map Former-commit-id: a563503d4ae83a4f2cb7638710b3fdc9c98a45b4 --- .../region/ApproximationModel.cpp | 140 +++++++------- src/modelchecker/region/ApproximationModel.h | 124 +++++++++--- src/modelchecker/region/ParameterRegion.cpp | 94 ++++----- src/modelchecker/region/ParameterRegion.h | 11 +- src/modelchecker/region/SamplingModel.cpp | 79 ++++---- src/modelchecker/region/SamplingModel.h | 41 ++-- .../region/SparseDtmcRegionModelChecker.cpp | 94 ++++----- .../region/SparseDtmcRegionModelChecker.h | 3 +- src/utility/storm.h | 4 +- .../SparseDtmcRegionModelCheckerTest.cpp | 178 +++++++++--------- 10 files changed, 423 insertions(+), 345 deletions(-) diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 1e11a5c8d..64fd10350 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -18,33 +18,35 @@ namespace storm { namespace modelchecker { - template - SparseDtmcRegionModelChecker::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr formula) : formula(formula){ + 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 << ". Sampling model only supports eventually or reachability reward formulae."); + 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 (more precisely: the position in that table). + 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 - const std::size_t constantEntryIndex=std::numeric_limits::max(); //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later) - initializeProbabilities(parametricModel, probabilityMatrix, rowSubstitutions, matrixEntryToEvalTableMapping, constantEntryIndex); + 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 - std::vector transitionRewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping + 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){ - boost::optional> stateActionRewards; - initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, transitionRewardEntryToEvalTableMapping, constantEntryIndex); - rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(boost::optional>(), std::move(stateActionRewards)))); + 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()); @@ -53,27 +55,28 @@ namespace storm { //translate the matrixEntryToEvalTableMapping into the actual probability mapping typename storm::storage::SparseMatrix::index_type matrixRow=0; - auto tableIndex=matrixEntryToEvalTableMapping.begin(); + 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(*tableIndex == constantEntryIndex){ + if(*tableEntry == &constantProbEntry){ approxModelEntry->setValue(storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parEntry.getValue()))); } else { - this->probabilityMapping.emplace_back(std::make_pair(&(std::get<2>(this->probabilityEvaluationTable[*tableIndex])), approxModelEntry)); + this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry)); } ++approxModelEntry; - ++tableIndex; + ++tableEntry; } } } if(this->computeRewards){ //the same for rewards auto approxModelRewardEntry = this->model->getUniqueRewardModel()->second.getStateActionRewardVector().begin(); - for (std::size_t const& tableIndex : rewardEntryToEvalTableMapping){ - if(tableIndex != constantEntryIndex){ - this->rewardMapping.emplace_back(std::make_tuple(&(std::get<2>(this->rewardEvaluationTable[tableIndex])), &(std::get<3>(this->rewardEvaluationTable[tableIndex])), approxModelRewardEntry)); + 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; } @@ -89,12 +92,12 @@ namespace storm { } } - template - void SparseDtmcRegionModelChecker::ApproximationModel::initializeProbabilities(storm::models::sparse::Dtmcconst& parametricModel, + template + void SparseDtmcRegionModelChecker::ApproximationModel::initializeProbabilities(storm::models::sparse::Dtmcconst& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& rowSubstitutions, - std::vector& matrixEntryToEvalTableMapping, - std::size_t const& constantEntryIndex) { + 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()); @@ -131,11 +134,11 @@ namespace storm { ConstantType dummyEntry=storm::utility::one(); for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){ if(storm::utility::isConstant(entry.getValue())){ - matrixEntryToEvalTableMapping.emplace_back(constantEntryIndex); + matrixEntryToEvalTableMapping.emplace_back(constantEntry); } else { ++numOfNonConstEntries; - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->probabilityEvaluationTable, std::tuple(substitutionIndex, entry.getValue(), storm::utility::zero())); - matrixEntryToEvalTableMapping.emplace_back(tableIndex); + 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(); @@ -147,19 +150,17 @@ namespace storm { probabilityMatrix=matrixBuilder.build(); } - template - void SparseDtmcRegionModelChecker::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, + template + void SparseDtmcRegionModelChecker::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, - boost::optional>& stateActionRewardVector, - std::vector& rewardEntryToEvalTableMapping, - std::vector& transitionRewardEntryToEvalTableMapping, - std::size_t const& constantEntryIndex) { + 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 add one entry to the rewardEntryEvalTableMapping - std::vector stateActionRewardsAsVector; - stateActionRewardsAsVector.reserve(probabilityMatrix.getRowCount()); + // 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 @@ -167,22 +168,20 @@ namespace storm { for(std::size_t state=0; state occurringRewVariables; std::set occurringProbVariables; - std::size_t evalTableIndex; 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]; matrixRowsecond.getStateRewardVector()[state], occurringRewVariables); - //For each row in the row group of state, we get the corresponding substitution, substitutionIndex and tableIndex + //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; - std::size_t tableIndex; + RewTableEntry* evalTablePtr; for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRowrewardSubstitutions, std::move(rewardSubstitution)); - tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(substitutionIndex, parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero(), storm::utility::zero())); + 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 - stateActionRewardsAsVector.emplace_back(storm::utility::zero()); - rewardEntryToEvalTableMapping.emplace_back(tableIndex); + stateActionRewardVector.emplace_back(storm::utility::zero()); + rewardEntryToEvalTableMapping.emplace_back(evalTablePtr); ++numOfNonConstRewEntries; } } } - stateActionRewardVector=std::move(stateActionRewardsAsVector); this->rewardMapping.reserve(numOfNonConstRewEntries); } - template - SparseDtmcRegionModelChecker::ApproximationModel::~ApproximationModel() { + template + SparseDtmcRegionModelChecker::ApproximationModel::~ApproximationModel() { //Intentionally left empty } - template - std::shared_ptr> const& SparseDtmcRegionModelChecker::ApproximationModel::getModel() const { + template + std::shared_ptr> const& SparseDtmcRegionModelChecker::ApproximationModel::getModel() const { return this->model; } - template - void SparseDtmcRegionModelChecker::ApproximationModel::instantiate(const ParameterRegion& region) { + 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){ @@ -242,10 +244,10 @@ namespace storm { } //write entries into evaluation table for(auto& tableEntry : this->probabilityEvaluationTable){ - std::get<2>(tableEntry)=storm::utility::regions::convertNumber( + tableEntry.second=storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction( - std::get<1>(tableEntry), - instantiatedSubs[std::get<0>(tableEntry)] + tableEntry.first.getFunction(), + instantiatedSubs[tableEntry.first.getSubstitution()] ) ); } @@ -277,33 +279,33 @@ namespace storm { } //write entries into evaluation table for(auto& tableEntry : this->rewardEvaluationTable){ - ConstantType minValue=storm::utility::infinity(); - ConstantType maxValue=storm::utility::zero(); - //Iterate over the different combinations of lower and upper bounds and update the min/max values - auto const& vertices=region.getVerticesOfRegion(this->choseOptimalRewardPars[std::get<0>(tableEntry)]); + 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& sub : vertex){ - instantiatedRewardSubs[std::get<0>(tableEntry)][sub.first]=sub.second; + for(auto const& vertexSub : vertex){ + instantiatedRewardSubs[funcSub.getSubstitution()][vertexSub.first]=vertexSub.second; } ConstantType currValue = storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction( - std::get<1>(tableEntry), - instantiatedRewardSubs[std::get<0>(tableEntry)] + funcSub.getFunction(), + instantiatedRewardSubs[funcSub.getSubstitution()] ) ); - minValue=std::min(minValue, currValue); - maxValue=std::max(maxValue, currValue); + minMax.first=std::min(minMax.first, currValue); + minMax.second=std::max(minMax.second, currValue); } - std::get<2>(tableEntry)= minValue; - std::get<3>(tableEntry)= maxValue; } //Note: the rewards are written to the model as soon as the optimality type is known (i.e. in computeValues) } } - template - std::vector const& SparseDtmcRegionModelChecker::ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) { + template + std::vector const& SparseDtmcRegionModelChecker::ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) { storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(*this->model); std::unique_ptr resultPtr; @@ -336,7 +338,7 @@ namespace storm { #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker::ApproximationModel; + template class SparseDtmcRegionModelChecker, double>; #endif } } \ No newline at end of file diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index c101a2ac4..272cc67a2 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -8,6 +8,8 @@ #ifndef STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H #define STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H +#include + #include "src/modelchecker/region/SparseDtmcRegionModelChecker.h" #include "src/models/sparse/Mdp.h" #include "src/modelchecker/region/ParameterRegion.h" @@ -16,16 +18,17 @@ namespace storm { namespace modelchecker { - template + template class SparseDtmcRegionModelChecker; - template - class SparseDtmcRegionModelChecker::ApproximationModel{ + template + class SparseDtmcRegionModelChecker::ApproximationModel{ public: - typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; + typedef typename ParametricSparseModelType::ValueType ParametricType; + typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; + typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; /*! * @note this will not check whether approximation is applicable @@ -52,45 +55,110 @@ namespace storm { 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 { + 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; + } + + 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(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& rowSubstitutions, std::vector& matrixEntryToEvalTableMapping, std::size_t const& constantEntryIndex); - void initializeRewards(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& rowSubstitutions, boost::optional>& stateActionRewardVector, std::vector& stateRewardEntryToEvalTableMapping, std::vector& transitionRewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex); + 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); - //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 and the transitionRewardMatrix, respectively. - std::vector::iterator>> rewardMapping; + //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; - //Vector has one (unique) entry for every occurring pair of a non-constant function and - // a substitution, i.e., a mapping of variables to a TypeOfBound - //The first entry represents the substitution as an index in the substitutions vector - //The third entry should contain the result when evaluating the function in the second entry, regarding the substitution given by the second entry. - std::vector> probabilityEvaluationTable; - //For rewards, we have the third entry for the minimal value and the fourth entry for the maximal value - std::vector> rewardEvaluationTable; + // 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 + //depends on the region and whether to minimize/maximize (i.e. CHOSEOPTIMAL parameters) std::vector> rewardSubstitutions; std::vector> choseOptimalRewardPars; - //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; + //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; + }; } } diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index 3216493c2..6128e7c9b 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -19,18 +19,18 @@ namespace storm { namespace modelchecker { - template - SparseDtmcRegionModelChecker::ParameterRegion::ParameterRegion(std::map const& lowerBounds, std::map const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { + 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) { + 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() { + 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); @@ -43,42 +43,42 @@ namespace storm { } } - template - SparseDtmcRegionModelChecker::ParameterRegion::~ParameterRegion() { + template + SparseDtmcRegionModelChecker::ParameterRegion::~ParameterRegion() { //Intentionally left empty } - template - std::set::VariableType> SparseDtmcRegionModelChecker::ParameterRegion::getVariables() const { + template + std::set::VariableType> SparseDtmcRegionModelChecker::ParameterRegion::getVariables() const { return this->variables; } - template - typename SparseDtmcRegionModelChecker::CoefficientType const& SparseDtmcRegionModelChecker::ParameterRegion::getLowerBound(VariableType const& variable) const { + 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 { + 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 { + 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 { + 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 { + 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()); @@ -104,18 +104,18 @@ namespace storm { return resultingVector; } - template - std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSomePoint() const { + template + std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSomePoint() const { return this->getLowerBounds(); } - template - typename SparseDtmcRegionModelChecker::RegionCheckResult SparseDtmcRegionModelChecker::ParameterRegion::getCheckResult() const { + template + typename SparseDtmcRegionModelChecker::RegionCheckResult SparseDtmcRegionModelChecker::ParameterRegion::getCheckResult() const { return checkResult; } - template - void SparseDtmcRegionModelChecker::ParameterRegion::setCheckResult(RegionCheckResult 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"); @@ -129,28 +129,28 @@ namespace storm { this->checkResult = checkResult; } - template - std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getViolatedPoint() const { + template + std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getViolatedPoint() const { return violatedPoint; } - template - void SparseDtmcRegionModelChecker::ParameterRegion::setViolatedPoint(std::map const& violatedPoint) { + template + void SparseDtmcRegionModelChecker::ParameterRegion::setViolatedPoint(std::map const& violatedPoint) { this->violatedPoint = violatedPoint; } - template - std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSatPoint() const { + template + std::map::VariableType, typename SparseDtmcRegionModelChecker::CoefficientType> SparseDtmcRegionModelChecker::ParameterRegion::getSatPoint() const { return satPoint; } - template - void SparseDtmcRegionModelChecker::ParameterRegion::setSatPoint(std::map const& satPoint) { + template + void SparseDtmcRegionModelChecker::ParameterRegion::setSatPoint(std::map const& satPoint) { this->satPoint = satPoint; } - template - std::string SparseDtmcRegionModelChecker::ParameterRegion::checkResultToString() const { + template + std::string SparseDtmcRegionModelChecker::ParameterRegion::checkResultToString() const { switch (this->checkResult) { case RegionCheckResult::UNKNOWN: return "unknown"; @@ -169,8 +169,8 @@ namespace storm { return "ERROR"; } - template - std::string SparseDtmcRegionModelChecker::ParameterRegion::toString() const { + template + std::string SparseDtmcRegionModelChecker::ParameterRegion::toString() const { std::stringstream regionstringstream; for (auto var : this->getVariables()) { regionstringstream << storm::utility::regions::convertNumber(this->getLowerBound(var)); @@ -188,8 +188,8 @@ namespace storm { - template - void SparseDtmcRegionModelChecker::ParameterRegion::parseParameterBounds( + template + void SparseDtmcRegionModelChecker::ParameterRegion::parseParameterBounds( std::map& lowerBounds, std::map& upperBounds, std::string const& parameterBoundsString){ @@ -211,8 +211,8 @@ namespace storm { upperBounds.emplace(std::make_pair(var, ub)); } - template - typename SparseDtmcRegionModelChecker::ParameterRegion SparseDtmcRegionModelChecker::ParameterRegion::parseRegion( + template + typename SparseDtmcRegionModelChecker::ParameterRegion SparseDtmcRegionModelChecker::ParameterRegion::parseRegion( std::string const& regionString){ std::map lowerBounds; std::map upperBounds; @@ -226,8 +226,8 @@ namespace storm { return ParameterRegion(std::move(lowerBounds), std::move(upperBounds)); } - template - std::vector::ParameterRegion> SparseDtmcRegionModelChecker::ParameterRegion::parseMultipleRegions( + template + std::vector::ParameterRegion> SparseDtmcRegionModelChecker::ParameterRegion::parseMultipleRegions( std::string const& regionsString){ std::vector result; std::vector regionsStrVec; @@ -240,8 +240,8 @@ namespace storm { return result; } - template - std::vector::ParameterRegion> SparseDtmcRegionModelChecker::ParameterRegion::getRegionsFromSettings(){ + 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."); @@ -258,7 +258,7 @@ namespace storm { return parseMultipleRegions(regionsString); } #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker::ParameterRegion; + template class SparseDtmcRegionModelChecker, double>; #endif } diff --git a/src/modelchecker/region/ParameterRegion.h b/src/modelchecker/region/ParameterRegion.h index 0f035b15b..104f989e8 100644 --- a/src/modelchecker/region/ParameterRegion.h +++ b/src/modelchecker/region/ParameterRegion.h @@ -13,14 +13,15 @@ namespace storm { namespace modelchecker{ - template + template class SparseDtmcRegionModelChecker; - template - class SparseDtmcRegionModelChecker::ParameterRegion{ + template + class SparseDtmcRegionModelChecker::ParameterRegion{ public: - typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; + 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); diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 58911e9d3..55fe6e27a 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -18,30 +18,30 @@ namespace storm { namespace modelchecker { - template - SparseDtmcRegionModelChecker::SamplingModel::SamplingModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr formula) : formula(formula){ + 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; - // This vector will get an entry for every probability matrix entry. - // For the corresponding matrix entry, it stores the right entry in the probability evaluation table (more precisely: the position in that table). - std::vector matrixEntryToEvalTableMapping; - const std::size_t constantEntryIndex=std::numeric_limits::max(); //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later) - initializeProbabilities(parametricModel, probabilityMatrix, matrixEntryToEvalTableMapping, constantEntryIndex); + 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 + std::vector rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping if(this->computeRewards){ boost::optional> stateRewards; - initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, constantEntryIndex); + initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, &constantEntry); rewardModels.insert(std::pair>("", storm::models::sparse::StandardRewardModel(std::move(stateRewards)))); } @@ -54,33 +54,33 @@ namespace storm { //translate the matrixEntryToEvalTableMapping into the actual probability mapping auto sampleModelEntry = this->model->getTransitionMatrix().begin(); auto parModelEntry = parametricModel.getTransitionMatrix().begin(); - for(std::size_t const& tableIndex : matrixEntryToEvalTableMapping){ + 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(tableIndex == constantEntryIndex){ + if(tableEntry == &constantEntry){ sampleModelEntry->setValue(storm::utility::regions::convertNumber(storm::utility::regions::getConstantPart(parModelEntry->getValue()))); } else { - this->probabilityMapping.emplace_back(std::make_pair(&(this->probabilityEvaluationTable[tableIndex].second), sampleModelEntry)); + this->probabilityMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelEntry)); } ++sampleModelEntry; ++parModelEntry; } - //also do this for the rewards thing + //also do this for the rewards if(this->computeRewards){ auto sampleModelStateRewardEntry = this->model->getUniqueRewardModel()->second.getStateRewardVector().begin(); - for(std::size_t const& tableIndex : rewardEntryToEvalTableMapping){ - if(tableIndex != constantEntryIndex){ - this->stateRewardMapping.emplace_back(std::make_pair(&(this->rewardEvaluationTable[tableIndex].second), sampleModelStateRewardEntry)); + for(auto tableEntry : rewardEntryToEvalTableMapping){ + if(tableEntry != &constantEntry){ + this->stateRewardMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelStateRewardEntry)); } ++sampleModelStateRewardEntry; } } } - template - void SparseDtmcRegionModelChecker::SamplingModel::initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, + template + void SparseDtmcRegionModelChecker::SamplingModel::initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, - std::vector& matrixEntryToEvalTableMapping, - std::size_t const& constantEntryIndex) { + 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()); @@ -89,11 +89,11 @@ namespace storm { ConstantType dummyEntry=storm::utility::one(); for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){ if(storm::utility::isConstant(entry.getValue())){ - matrixEntryToEvalTableMapping.emplace_back(constantEntryIndex); + matrixEntryToEvalTableMapping.emplace_back(constantEntry); } else { ++numOfNonConstEntries; - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->probabilityEvaluationTable, std::pair(entry.getValue(), storm::utility::zero())); - matrixEntryToEvalTableMapping.emplace_back(tableIndex); + 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(); @@ -103,11 +103,11 @@ namespace storm { probabilityMatrix=matrixBuilder.build(); } - template - void SparseDtmcRegionModelChecker::SamplingModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, + template + void SparseDtmcRegionModelChecker::SamplingModel::initializeRewards(storm::models::sparse::Dtmc const& parametricModel, boost::optional>& stateRewards, - std::vector& rewardEntryToEvalTableMapping, - std::size_t const& constantEntryIndex) { + 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()); @@ -115,30 +115,29 @@ namespace storm { 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(constantEntryIndex); + rewardEntryToEvalTableMapping.emplace_back(constantEntry); } else { ++numOfNonConstEntries; - stateRewardsAsVector[state] = storm::utility::zero(); - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::pair(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero())); - rewardEntryToEvalTableMapping.emplace_back(tableIndex); + 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); } - template - SparseDtmcRegionModelChecker::SamplingModel::~SamplingModel() { + template + SparseDtmcRegionModelChecker::SamplingModel::~SamplingModel() { //Intentionally left empty } - template - std::shared_ptr> const& SparseDtmcRegionModelChecker::SamplingModel::getModel() const { + template + std::shared_ptr> const& SparseDtmcRegionModelChecker::SamplingModel::getModel() const { return this->model; } - template - void SparseDtmcRegionModelChecker::SamplingModel::instantiate(std::mapconst& point) { + template + void SparseDtmcRegionModelChecker::SamplingModel::instantiate(std::mapconst& point) { //write entries into evaluation tables for(auto& tableEntry : this->probabilityEvaluationTable){ tableEntry.second=storm::utility::regions::convertNumber( @@ -160,8 +159,8 @@ namespace storm { } } - template - std::vector const& SparseDtmcRegionModelChecker::SamplingModel::computeValues() { + template + std::vector const& SparseDtmcRegionModelChecker::SamplingModel::computeValues() { storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(*this->model); std::unique_ptr resultPtr; //perform model checking on the dtmc @@ -175,7 +174,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker::SamplingModel; + template class SparseDtmcRegionModelChecker, double>; #endif } } \ No newline at end of file diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index ba16be283..efa2742b5 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -8,6 +8,8 @@ #ifndef STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H #define STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H +#include + #include "src/modelchecker/region/SparseDtmcRegionModelChecker.h" #include "src/models/sparse/Dtmc.h" #include "src/storage/SparseMatrix.h" @@ -15,16 +17,17 @@ namespace storm { namespace modelchecker{ - template + template class SparseDtmcRegionModelChecker; - template - class SparseDtmcRegionModelChecker::SamplingModel { + template + class SparseDtmcRegionModelChecker::SamplingModel { public: - typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; - typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; + 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(); @@ -48,19 +51,10 @@ namespace storm { private: - void initializeProbabilities(storm::models::sparse::Dtmc const& parametricModel, storm::storage::SparseMatrix& probabilityMatrix, std::vector& matrixEntryToEvalTableMapping, std::size_t const& constantEntryIndex); - void initializeRewards(storm::models::sparse::Dtmc const& parametricModel, boost::optional>& stateRewards, std::vector& rewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex); - - //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; + typedef typename std::unordered_map::value_type TableEntry; - //Vector has one entry for every distinct, non-constant function that occurs somewhere in the model. - //The second entry should contain the result when evaluating the function in the first entry. - std::vector> probabilityEvaluationTable; - std::vector> rewardEvaluationTable; + 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; @@ -68,6 +62,19 @@ namespace storm { 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; }; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 3331c290c..77ce1f9ff 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -29,21 +29,21 @@ namespace storm { namespace modelchecker { - template - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : + 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(){ + template + SparseDtmcRegionModelChecker::~SparseDtmcRegionModelChecker(){ //intentionally left empty } - template - bool SparseDtmcRegionModelChecker::canHandle(storm::logic::Formula const& formula) const { + 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(); @@ -71,8 +71,8 @@ namespace storm { return false; } - template - void SparseDtmcRegionModelChecker::specifyFormula(std::shared_ptr formula) { + 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."); @@ -127,8 +127,8 @@ namespace storm { this->timeFullSmt=std::chrono::high_resolution_clock::duration::zero(); } - template - void SparseDtmcRegionModelChecker::preprocess(){ + 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."); @@ -286,8 +286,8 @@ namespace storm { this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart; } - template - void SparseDtmcRegionModelChecker::preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates) { + 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(); @@ -329,8 +329,8 @@ namespace storm { } - template - void SparseDtmcRegionModelChecker::preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector& stateRewards) { + template + void SparseDtmcRegionModelChecker::preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector& stateRewards) { this->computeRewards=true; //get the correct reward model @@ -428,8 +428,8 @@ namespace storm { - template - void SparseDtmcRegionModelChecker::initializeApproximationModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula) { + 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(); @@ -437,8 +437,8 @@ namespace storm { STORM_LOG_DEBUG("Initialized Approximation Model"); } - template - void SparseDtmcRegionModelChecker::initializeSamplingModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula) { + 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(); @@ -446,8 +446,8 @@ namespace storm { STORM_LOG_DEBUG("Initialized Sampling Model"); } - template - void SparseDtmcRegionModelChecker::computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel){ + 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()); @@ -479,8 +479,8 @@ namespace storm { this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart; } - template - void SparseDtmcRegionModelChecker::checkRegions(std::vector& regions) { + template + void SparseDtmcRegionModelChecker::checkRegions(std::vector& regions) { STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); std::cout << "Checking " << regions.size() << " regions. Progress: "; std::cout.flush(); @@ -497,8 +497,8 @@ namespace storm { std::cout << " done!" << std::endl; } - template - void SparseDtmcRegionModelChecker::checkRegion(ParameterRegion& region) { + template + void SparseDtmcRegionModelChecker::checkRegion(ParameterRegion& region) { std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now(); ++this->numOfCheckedRegions; @@ -580,8 +580,8 @@ namespace storm { } } - template - bool SparseDtmcRegionModelChecker::checkApproximativeValues(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { + 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); @@ -679,8 +679,8 @@ namespace storm { return false; } - template - std::shared_ptr::ApproximationModel> const& SparseDtmcRegionModelChecker::getApproximationModel() { + 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); @@ -688,8 +688,8 @@ namespace storm { return this->approximationModel; } - template - bool SparseDtmcRegionModelChecker::checkSamplePoints(ParameterRegion& region) { + 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)){ @@ -699,8 +699,8 @@ namespace storm { return false; } - template - bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { + 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)){ @@ -735,8 +735,8 @@ namespace storm { return false; } - template - std::shared_ptr::SamplingModel> const& SparseDtmcRegionModelChecker::getSamplingModel() { + 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); @@ -744,8 +744,8 @@ namespace storm { return this->samplingModel; } - template - std::shared_ptr const& SparseDtmcRegionModelChecker::getReachabilityFunction() { + 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); @@ -753,9 +753,9 @@ namespace storm { return this->reachabilityFunction; } - template + template template - ValueType SparseDtmcRegionModelChecker::getReachabilityValue(std::map const& point, bool evaluateFunction) { + ValueType SparseDtmcRegionModelChecker::getReachabilityValue(std::map const& point, bool evaluateFunction) { if(this->isResultConstant){ //Todo: remove workaround (infinityisResultInfinity){ @@ -773,8 +773,8 @@ namespace storm { } - template - bool SparseDtmcRegionModelChecker::checkFullSmt(ParameterRegion& region) { + 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) @@ -869,8 +869,8 @@ namespace storm { } } - template - void SparseDtmcRegionModelChecker::initializeSMTSolver() { + 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)); @@ -919,9 +919,9 @@ namespace storm { storm::utility::regions::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllViolatedVar, *getReachabilityFunction(), proveAllViolatedRel, bound); } - template + template template - bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType const& value){ + bool SparseDtmcRegionModelChecker::valueIsInBoundOfFormula(ValueType const& value){ STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified."); double valueAsDouble = storm::utility::regions::convertNumber(value); switch (this->specifiedFormulaCompType) { @@ -938,8 +938,8 @@ namespace storm { } } - template - void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { + template + void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { if(this->specifiedFormula==nullptr){ outstream << "Region Model Checker Statistics Error: No formula specified." << std::endl; @@ -1003,7 +1003,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker; + template class SparseDtmcRegionModelChecker, double>; #endif //note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index f54954332..375bbbf5a 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -14,10 +14,11 @@ namespace storm { namespace modelchecker { - template + template class SparseDtmcRegionModelChecker { public: + typedef typename ParametricSparseModelType::ValueType ParametricType; typedef typename storm::utility::regions::VariableType VariableType; typedef typename storm::utility::regions::CoefficientType CoefficientType; diff --git a/src/utility/storm.h b/src/utility/storm.h index d871e0e18..23a8e4fad 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::ParameterRegion::getRegionsFromSettings(); - storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); + auto regions=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::getRegionsFromSettings(); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { modelchecker.specifyFormula(formula); modelchecker.checkRegions(regions); diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 00061d570..eaeaf350f 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -37,14 +37,14 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + 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"); 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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + 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"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); } @@ -106,15 +106,15 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95"); - auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); + 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"); 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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(exBothHardRegion); //At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can) EXPECT_TRUE( - (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH)) || - (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSVIOLATED)) + (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH)) || + (exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSVIOLATED)) ); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75"); - auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); + 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"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); //test smt + approx - auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(exBothHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -199,12 +199,12 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion(""); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); } @@ -246,14 +246,14 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); + 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"); 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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); + 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"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); } @@ -309,15 +309,15 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); - auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + 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"); 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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); modelchecker.checkRegion(allVioHardRegion); //At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can) EXPECT_TRUE( - (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED)) || - (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSVIOLATED)) + (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED)) || + (allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSVIOLATED)) ); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); - auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + 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"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult()); //test smt + approx - auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allVioHardRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); } @@ -397,14 +397,14 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.9<=PF<=0.99"); - auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.9"); - auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.01<=PF<=0.8"); + 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"); 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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); modelchecker.checkRegion(exBothRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); modelchecker.checkRegion(allVioRegion); - EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.9<=PF<=0.99"); - auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.8<=PF<=0.9"); - auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion("0.01<=PF<=0.8"); + 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"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); modelchecker.checkRegion(exBothRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); modelchecker.checkRegion(allVioRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); } @@ -462,12 +462,12 @@ 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 modelchecker(*dtmc); + storm::modelchecker::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker, double>::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 @@ -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::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) - auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker::ParameterRegion::parseRegion(""); + auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker, double>::ParameterRegion::parseRegion(""); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); modelchecker.checkRegion(allSatRegionSmt); -//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); +//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); }