From c4444567e77cd43d29074715a2a83a76fc71da67 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 5 Sep 2015 19:15:18 +0200 Subject: [PATCH] further optimization on approximation model initialization. Also better code structure of preprocessing steps Former-commit-id: e916644a6cccdf0713cff9a6e1e667681ba486a3 --- .../region/ApproximationModel.cpp | 37 ++-- src/modelchecker/region/ApproximationModel.h | 17 +- src/modelchecker/region/SamplingModel.cpp | 20 +- src/modelchecker/region/SamplingModel.h | 5 +- .../region/SparseDtmcRegionModelChecker.cpp | 208 ++++++++++-------- .../region/SparseDtmcRegionModelChecker.h | 27 ++- src/utility/vector.h | 19 -- 7 files changed, 186 insertions(+), 147 deletions(-) diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 4f1ddeb3c..c6945ab30 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -11,13 +11,21 @@ #include "src/utility/vector.h" #include "src/utility/regions.h" #include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace modelchecker { template - SparseDtmcRegionModelChecker::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards) : computeRewards(computeRewards){ + 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; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Sampling model only supports eventually or reachability reward formulae."); + } //Start with the probabilities storm::storage::SparseMatrix probabilityMatrix; std::vector rowSubstitutions;// the substitution used in every row (required if rewards are computed) @@ -128,7 +136,7 @@ namespace storm { matrixEntryToEvalTableMapping.emplace_back(constantEntryIndex); } else { ++numOfNonConstEntries; - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->probabilityEvaluationTable, std::tuple(entry.getValue(), substitutionIndex, storm::utility::zero())); + std::size_t tableIndex=storm::utility::vector::findOrInsert(this->probabilityEvaluationTable, std::tuple(substitutionIndex, entry.getValue(), storm::utility::zero())); matrixEntryToEvalTableMapping.emplace_back(tableIndex); } matrixBuilder.addNextValue(matrixRow, entry.getColumn(), dummyEntry); @@ -193,7 +201,7 @@ namespace storm { } std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution)); //insert table entry and dummy data in the stateRewardVector - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(parametricModel.getStateRewardVector()[state], substitutionIndex, storm::utility::zero(), storm::utility::zero())); + std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(substitutionIndex, parametricModel.getStateRewardVector()[state], storm::utility::zero(), storm::utility::zero())); stateRewardEntryToEvalTableMapping.emplace_back(tableIndex); stateRewardsAsVector[state]=storm::utility::zero(); ++numOfNonConstStateRewEntries; @@ -211,7 +219,7 @@ namespace storm { } std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution)); //insert table entries and dummy data - std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(parametricModel.getStateRewardVector()[state], substitutionIndex, storm::utility::zero(), storm::utility::zero())); + std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple(substitutionIndex, parametricModel.getStateRewardVector()[state], storm::utility::zero(), storm::utility::zero())); for(auto const& matrixEntry : probabilityMatrix.getRow(matrixRow)){ transitionRewardEntryToEvalTableMapping.emplace_back(tableIndex); matrixBuilder.addNextValue(matrixRow, matrixEntry.getColumn(), storm::utility::zero()); @@ -263,8 +271,8 @@ namespace storm { for(auto& tableEntry : this->probabilityEvaluationTable){ std::get<2>(tableEntry)=storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction( - std::get<0>(tableEntry), - instantiatedSubs[std::get<1>(tableEntry)] + std::get<1>(tableEntry), + instantiatedSubs[std::get<0>(tableEntry)] ) ); } @@ -299,16 +307,16 @@ namespace storm { 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<1>(tableEntry)]); + auto const& vertices=region.getVerticesOfRegion(this->choseOptimalRewardPars[std::get<0>(tableEntry)]); for(auto const& vertex : vertices){ //extend the substitution for(auto const& sub : vertex){ - instantiatedRewardSubs[std::get<1>(tableEntry)][sub.first]=sub.second; + instantiatedRewardSubs[std::get<0>(tableEntry)][sub.first]=sub.second; } ConstantType currValue = storm::utility::regions::convertNumber( storm::utility::regions::evaluateFunction( - std::get<0>(tableEntry), - instantiatedRewardSubs[std::get<1>(tableEntry)] + std::get<1>(tableEntry), + instantiatedRewardSubs[std::get<0>(tableEntry)] ) ); minValue=std::min(minValue, currValue); @@ -323,12 +331,10 @@ namespace storm { template std::vector const& SparseDtmcRegionModelChecker::ApproximationModel::computeValues(storm::logic::OptimalityType const& optimalityType) { - storm::modelchecker::SparseMdpPrctlModelChecker modelChecker(*this->model); - std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); std::unique_ptr resultPtr; + if(this->computeRewards){ - storm::logic::ReachabilityRewardFormula reachRewFormula(targetFormulaPtr); //write the reward values into the model switch(optimalityType){ case storm::logic::OptimalityType::Minimize: @@ -351,12 +357,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given optimality Type is not supported."); } //perform model checking on the mdp - resultPtr = modelChecker.computeReachabilityRewards(reachRewFormula, false, optimalityType); + resultPtr = modelChecker.computeReachabilityRewards(this->formula->asReachabilityRewardFormula(), false, optimalityType); } else { - storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); //perform model checking on the mdp - resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula, false, optimalityType); + resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asEventuallyFormula(), false, optimalityType); } return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); } diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index e7037ddae..6d17ee9fe 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -27,8 +27,10 @@ namespace storm { typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - - ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards); + /*! + * @note this will not check whether approximation is applicable + */ + ApproximationModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr formula); virtual ~ApproximationModel(); /*! @@ -70,11 +72,11 @@ namespace storm { //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 second entry represents the substitution as an index in the substitutions vector - //The third entry should contain the result when evaluating the function in the first entry, regarding the substitution given by the second entry. - std::vector> probabilityEvaluationTable; + //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; + std::vector> rewardEvaluationTable; //Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region) std::vector> probabilitySubstitutions; @@ -86,7 +88,8 @@ namespace storm { //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; diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 370070392..b34ab459b 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -11,13 +11,21 @@ #include "src/utility/vector.h" #include "src/utility/regions.h" #include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace modelchecker { template - SparseDtmcRegionModelChecker::SamplingModel::SamplingModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards) : probabilityMapping(), stateRewardMapping(), probabilityEvaluationTable(), computeRewards(computeRewards){ + 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; + } 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. @@ -151,17 +159,13 @@ namespace storm { template std::vector const& SparseDtmcRegionModelChecker::SamplingModel::computeValues() { storm::modelchecker::SparseDtmcPrctlModelChecker modelChecker(*this->model); - std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); std::unique_ptr resultPtr; + //perform model checking on the dtmc if(this->computeRewards){ - storm::logic::ReachabilityRewardFormula reachRewFormula(targetFormulaPtr); - //perform model checking on the dtmc - resultPtr = modelChecker.computeReachabilityRewards(reachRewFormula); + resultPtr = modelChecker.computeReachabilityRewards(this->formula->asReachabilityRewardFormula()); } else { - storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); - //perform model checking on the dtmc - resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula); + resultPtr = modelChecker.computeEventuallyProbabilities(this->formula->asEventuallyFormula()); } return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); } diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index 9eb1c2210..9470f1a8c 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -26,7 +26,7 @@ namespace storm { typedef typename SparseDtmcRegionModelChecker::VariableType VariableType; typedef typename SparseDtmcRegionModelChecker::CoefficientType CoefficientType; - SamplingModel(storm::models::sparse::Dtmc const& parametricModel, bool computeRewards); + SamplingModel(storm::models::sparse::Dtmc const& parametricModel, std::shared_ptr formula); virtual ~SamplingModel(); /*! @@ -64,7 +64,8 @@ namespace storm { //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; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 5bc5ba4a7..9182cb4ef 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -88,17 +88,17 @@ namespace storm { if(!this->isResultConstant){ //now create the model used for Approximation if(storm::settings::regionSettings().doApprox()){ - initializeApproximationModel(*this->simplifiedModel); + initializeApproximationModel(*this->simpleModel, this->simpleFormula); } //now create the model used for Sampling if(storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE || (!storm::settings::regionSettings().doSample() && storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){ - initializeSamplingModel(*this->simplifiedModel); + initializeSamplingModel(*this->simpleModel, this->simpleFormula); } //Check if the reachability function needs to be computed if((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ - computeReachabilityFunction(*this->simplifiedModel); + computeReachabilityFunction(*this->simpleModel); } } //some information for statistics... @@ -148,7 +148,7 @@ namespace storm { // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = this->model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - // eliminate all states with only constant outgoing transitions (and possibly rewards) + // Eliminate all states with only constant outgoing transitions // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. auto flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix); auto flexibleBackwardTransitions= this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix.transpose(), true); @@ -157,27 +157,21 @@ namespace storm { //The states that we consider to eliminate storm::storage::BitVector considerToEliminate(submatrix.getRowCount(), true); considerToEliminate.set(initialState, false); - this->isApproximationApplicable=true; - this->isResultConstant=true; for (auto const& state : considerToEliminate) { bool eliminateThisState=true; for(auto const& entry : flexibleTransitions.getRow(state)){ if(!this->parametricTypeComparator.isConstant(entry.getValue())){ - this->isResultConstant=false; eliminateThisState=false; - this->isApproximationApplicable &= storm::utility::regions::functionIsLinear(entry.getValue()); + break; } } if(!this->parametricTypeComparator.isConstant(oneStepProbabilities[state])){ - this->isResultConstant=false; eliminateThisState=false; - this->isApproximationApplicable &= storm::utility::regions::functionIsLinear(oneStepProbabilities[state]); } if(this->computeRewards && eliminateThisState && !this->parametricTypeComparator.isConstant(stateRewards.get()[state])){ //Note: The state reward does not need to be constant but we need to make sure that //no parameter of this reward function occurs as a parameter in the probability functions of the predecessors - // (otherwise, more complex functions might occur in our simplified model) - // TODO: test if we should really remove these states (the resulting reward functions are less simple this way) + // (otherwise, more complex functions might occur in our simple model) std::set probVars; for(auto const& predecessor : flexibleBackwardTransitions.getRow(state)){ for(auto const& predecessorTransition : flexibleTransitions.getRow(predecessor.getColumn())){ @@ -199,48 +193,8 @@ namespace storm { } } STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions."); - if(this->isResultConstant){ - //Check if this is also the case for the initial state - for(auto const& entry : flexibleTransitions.getRow(initialState)){ - this->isResultConstant&=this->parametricTypeComparator.isConstant(entry.getValue()); - } - this->isResultConstant&=this->parametricTypeComparator.isConstant(oneStepProbabilities[initialState]); - } - if(this->computeRewards && (this->isApproximationApplicable || this->isResultConstant)){ - //We will need to check whether this is also the case for the reward functions. - for(auto const& state : maybeStates){ - std::set rewardVars; - if(this->model.hasStateRewards() && !this->parametricTypeComparator.isConstant(this->model.getStateRewardVector()[state])){ - this->isResultConstant=false; - this->isApproximationApplicable &= storm::utility::regions::functionIsLinear(this->model.getStateRewardVector()[state]); - storm::utility::regions::gatherOccurringVariables(stateRewards.get()[state], rewardVars); - } - if(this->model.hasTransitionRewards()){ - for(auto const& entry : this->model.getTransitionRewardMatrix().getRow(state)) { - if(!this->parametricTypeComparator.isConstant(entry.getValue())){ - this->isResultConstant=false; - this->isApproximationApplicable &= storm::utility::regions::functionIsLinear(entry.getValue()); - storm::utility::regions::gatherOccurringVariables(entry.getValue(), rewardVars); - } - } - } - if(!rewardVars.empty()){ - std::set probVars; - for(auto const& entry: this->model.getTransitionMatrix().getRow(state)){ - storm::utility::regions::gatherOccurringVariables(entry.getValue(), probVars); - } - for(auto const& rewardVar : rewardVars){ - if(probVars.find(rewardVar)!=probVars.end()){ - this->isApproximationApplicable=false; - break; - } - } - } - } - } - STORM_LOG_WARN_COND(!this->isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); - //Build the simplified model + //Build the simple model //The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated. //The new matrix should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly. std::vector newStateIndexMap(flexibleTransitions.getNumberOfRows(), flexibleTransitions.getNumberOfRows()); //initialize with some illegal index to easily check if a transition leads to an unselected state @@ -258,25 +212,25 @@ namespace storm { for(storm::storage::sparse::state_type oldStateIndex : subsystem){ ParametricType missingProbability=storm::utility::regions::getNewFunction(storm::utility::one()); //go through columns: - for(auto const& entry: flexibleTransitions.getRow(oldStateIndex)){ + for(auto& entry: flexibleTransitions.getRow(oldStateIndex)){ STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getNumberOfRows(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated."); missingProbability-=entry.getValue(); - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()],entry.getValue()); + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue())); } if(this->computeRewards){ // the missing probability always leads to target if(!this->parametricTypeComparator.isZero(missingProbability)){ - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState,missingProbability); + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(missingProbability)); } } else{ //transition to target state if(!this->parametricTypeComparator.isZero(oneStepProbabilities[oldStateIndex])){ missingProbability-=oneStepProbabilities[oldStateIndex]; - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, oneStepProbabilities[oldStateIndex]); + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(oneStepProbabilities[oldStateIndex])); } //transition to sink state if(!this->parametricTypeComparator.isZero(missingProbability)){ - matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], sinkState, missingProbability); + matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], sinkState, storm::utility::simplify(missingProbability)); } } } @@ -296,14 +250,29 @@ namespace storm { labeling.addLabel("sink", std::move(sinkLabel)); // other ingredients if(this->computeRewards){ - storm::utility::vector::selectVectorValues(stateRewards.get(), subsystem); - stateRewards->push_back(storm::utility::zero()); //target state - stateRewards->push_back(storm::utility::zero()); //sink state + std::size_t newState = 0; + for (auto oldstate : subsystem) { + if(oldstate!=newState){ + stateRewards.get()[newState++] = std::move(storm::utility::simplify(stateRewards.get()[oldstate])); + } else { + ++newState; + } + } + stateRewards.get()[newState++] = storm::utility::zero(); //target state + stateRewards.get()[newState++] = storm::utility::zero(); //sink state + stateRewards.get().resize(newState); } boost::optional> noTransitionRewards; boost::optional>> noChoiceLabeling; // the final model - this->simplifiedModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(stateRewards), std::move(noTransitionRewards), std::move(noChoiceLabeling)); + this->simpleModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(stateRewards), std::move(noTransitionRewards), std::move(noChoiceLabeling)); + // the corresponding formula + std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); + if(this->computeRewards){ + this->simpleFormula = std::shared_ptr(new storm::logic::ReachabilityRewardFormula(targetFormulaPtr)); + } else { + this->simpleFormula = std::shared_ptr(new storm::logic::EventuallyFormula(targetFormulaPtr)); + } std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart; } @@ -331,6 +300,22 @@ namespace storm { } //extend target states targetStates=statesWithProbability01.second; + + //check if approximation is applicable and whether the result is constant + this->isApproximationApplicable=true; + this->isResultConstant=true; + for (auto state=maybeStates.begin(); (state!=maybeStates.end()) && this->isApproximationApplicable; ++state) { + for(auto const& entry : this->model.getTransitionMatrix().getRow(*state)){ + if(!this->parametricTypeComparator.isConstant(entry.getValue())){ + this->isResultConstant=false; + if(!storm::utility::regions::functionIsLinear(entry.getValue())){ + this->isApproximationApplicable=false; + break; + } + } + } + } + STORM_LOG_WARN_COND(!this->isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); } @@ -373,6 +358,9 @@ namespace storm { storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->model.getStateRewardVector()); storm::utility::vector::addVectors(stateRewards, subStateRewards, stateRewards); } + for(auto& stateReward: stateRewards){ + storm::utility::simplify(stateReward); + } } else { // If only a state-based reward model is available, we take this vector as the // right-hand side. As the state reward vector contains entries not just for the @@ -380,26 +368,73 @@ namespace storm { // first. storm::utility::vector::selectVectorValues(stateRewards, maybeStates, this->model.getStateRewardVector()); } - for(auto& stateReward: stateRewards){ - storm::utility::simplify(stateReward); + //check if approximation is applicable and whether the result is constant + this->isApproximationApplicable=true; + this->isResultConstant=true; + std::set rewardPars; //the set of parameters that occur on a reward function + std::set probPars; //the set of parameters that occur on a probability function + for (auto state=maybeStates.begin(); state!=maybeStates.end() && this->isApproximationApplicable; ++state) { + //Constant/Linear probability functions + for(auto const& entry : this->model.getTransitionMatrix().getRow(*state)){ + if(!this->parametricTypeComparator.isConstant(entry.getValue())){ + this->isResultConstant=false; + if(!storm::utility::regions::functionIsLinear(entry.getValue())){ + this->isApproximationApplicable=false; + break; + } + storm::utility::regions::gatherOccurringVariables(entry.getValue(), probPars); + } + } + //Constant/Linear state rewards + if(this->model.hasStateRewards() && !this->parametricTypeComparator.isConstant(this->model.getStateRewardVector()[*state])){ + this->isResultConstant=false; + if(!storm::utility::regions::functionIsLinear(this->model.getStateRewardVector()[*state])){ + this->isApproximationApplicable=false; + break; + } + storm::utility::regions::gatherOccurringVariables(this->model.getStateRewardVector()[*state], rewardPars); + } + //Constant/Linear transition rewards + if(this->model.hasTransitionRewards()){ + for(auto const& entry : this->model.getTransitionRewardMatrix().getRow(*state)) { + if(!this->parametricTypeComparator.isConstant(entry.getValue())){ + this->isResultConstant=false; + if(!storm::utility::regions::functionIsLinear(entry.getValue())){ + this->isApproximationApplicable=false; + break; + } + storm::utility::regions::gatherOccurringVariables(entry.getValue(), rewardPars); + } + } + } + } + //Finally, we need to check whether rewardPars and probPars are disjoint + //Note: It would also work to simply rename the parameters that occur in both sets. + //This is to avoid getting functions with local maxima like p * (1-p) + for(auto const& rewardVar : rewardPars){ + if(probPars.find(rewardVar)!=probPars.end()){ + this->isApproximationApplicable=false; + break; + } } + STORM_LOG_WARN_COND(!this->isResultConstant, "For the given property, the reachability Value is constant, i.e., independent of the region"); } template - void SparseDtmcRegionModelChecker::initializeApproximationModel(storm::models::sparse::Dtmc const& simpleModel) { + 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(simpleModel, this->computeRewards); + this->approximationModel=std::make_shared(model, formula); std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now(); this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart; STORM_LOG_DEBUG("Initialized Approximation Model"); } template - void SparseDtmcRegionModelChecker::initializeSamplingModel(storm::models::sparse::Dtmc const& simpleModel) { + 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(simpleModel, this->computeRewards); + this->samplingModel=std::make_shared(model, formula); std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now(); this->timeInitSamplingModel = timeInitSamplingModelEnd - timeInitSamplingModelStart; STORM_LOG_DEBUG("Initialized Sampling Model"); @@ -408,8 +443,7 @@ namespace storm { 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 simplified model without target/sink state - //TODO check if this takes long... we could also store the oneSteps while creating the simplified model. Or(?) we keep the matrix the way it is and give the target state one step probability 1. + //get the one step probabilities and the transition matrix of the simple model without target/sink state storm::storage::SparseMatrix backwardTransitions(simpleModel.getBackwardTransitions()); std::vector oneStepProbabilities(simpleModel.getNumberOfStates()-2, storm::utility::zero()); for(auto const& entry : backwardTransitions.getRow(*(simpleModel.getStates("target").begin()))){ @@ -534,7 +568,7 @@ namespace storm { uint_fast64_t progress=0; uint_fast64_t checkedRegions=0; for(auto& region : regions){ - this->checkRegion(region); + checkRegion(region); if((checkedRegions++)*10/regions.size()==progress){ std::cout << progress++; std::cout.flush(); @@ -646,7 +680,7 @@ namespace storm { 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->simplifiedModel); + initializeApproximationModel(*this->simpleModel, this->simpleFormula); } return this->approximationModel; } @@ -701,7 +735,7 @@ namespace storm { 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->simplifiedModel); + initializeSamplingModel(*this->simpleModel, this->simpleFormula); } return this->samplingModel; } @@ -710,7 +744,7 @@ namespace storm { std::shared_ptr 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->simplifiedModel); + computeReachabilityFunction(*this->simpleModel); } return this->reachabilityFunction; } @@ -912,24 +946,26 @@ namespace storm { outstream << "The requested value is constant (i.e. independent of any parameters)" << std::endl; } else{ - outstream << "Simplified model: " << this->simplifiedModel->getNumberOfStates() << " states, " << this->simplifiedModel->getNumberOfTransitions() << " transitions" << std::endl; + outstream << "Simple model: " << this->simpleModel->getNumberOfStates() << " states, " << this->simpleModel->getNumberOfTransitions() << " transitions" << std::endl; } outstream << "Approximation is " << (this->isApproximationApplicable ? "" : "not ") << "applicable" << std::endl; outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl; - outstream << " Number of solved regions: " << numOfSolvedRegions << "(" << numOfSolvedRegions*100/this->numOfCheckedRegions << "%)" << std::endl; - outstream << " AllSat: " << this->numOfRegionsAllSat << "(" << this->numOfRegionsAllSat*100/this->numOfCheckedRegions << "%)" << std::endl; - outstream << " AllViolated: " << this->numOfRegionsAllViolated << "(" << this->numOfRegionsAllViolated*100/this->numOfCheckedRegions << "%)" << std::endl; - outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl; - outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl; - outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl; - outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl; - outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl; - outstream << " " << this->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl; - outstream << std::endl; + if(this->numOfCheckedRegions>0){ + outstream << " Number of solved regions: " << numOfSolvedRegions << "(" << numOfSolvedRegions*100/this->numOfCheckedRegions << "%)" << std::endl; + outstream << " AllSat: " << this->numOfRegionsAllSat << "(" << this->numOfRegionsAllSat*100/this->numOfCheckedRegions << "%)" << std::endl; + outstream << " AllViolated: " << this->numOfRegionsAllViolated << "(" << this->numOfRegionsAllViolated*100/this->numOfCheckedRegions << "%)" << std::endl; + outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl; + outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl; + outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl; + outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl; + outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl; + outstream << " " << this->numOfRegionsSolvedThroughFullSmt << " regions solved through FullSmt" << std::endl; + outstream << std::endl; + } outstream << "Running times:" << std::endl; outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing, bisimulation (if applied))" << std::endl; outstream << " " << timeSpecifyFormulaInMilliseconds.count() << "ms Initialization for the specified formula, including... " << std::endl; - outstream << " " << timePreprocessingInMilliseconds.count() << "ms for Preprocessing (mainly to obtain a simplified model, i.e., state elimination of const transitions)" << std::endl; + outstream << " " << timePreprocessingInMilliseconds.count() << "ms for Preprocessing (mainly: state elimination of const transitions)" << std::endl; outstream << " " << timeInitApproxModelInMilliseconds.count() << "ms to initialize the Approximation Model" << std::endl; outstream << " " << timeInitSamplingModelInMilliseconds.count() << "ms to initialize the Sampling Model" << std::endl; outstream << " " << timeComputeReachabilityFunctionInMilliseconds.count() << "ms to compute the reachability function" << std::endl; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index 8ada7b31d..d07845113 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -104,7 +104,10 @@ namespace storm { /*! * Does some sanity checks and preprocessing steps on the currently specified model and - * reachability probability formula, i.e., Computes maybeStates and targetStates and sets some flags + * reachability probability formula, i.e., + * * Sets some formula data and that we do not compute rewards + * * Computes maybeStates and targetStates + * * Sets the flags that state whether the result is constant and approximation is applicable * * @note The returned set of target states also includes states where an 'actual' target state is reached with probability 1 * @@ -114,24 +117,28 @@ namespace storm { /*! * Does some sanity checks and preprocessing steps on the currently specified model and - * reachability reward formula, i.e., computes some flags, maybeStates, targetStates and - * a new stateReward vector that considers state+transition rewards of the original model. - * @note stateRewards.size = maybeStates.numberOfSetBits + * reachability reward formula, i.e. + * * Sets some formula data and that we do compute rewards + * * Computes maybeStates, targetStates + * * Computes a new stateReward vector that considers state+transition rewards of the original model. (in a sense that we can abstract away from transition rewards) + * * Sets the flags that state whether the result is constant and approximation is applicable + * + * @note stateRewards.size will equal to maybeStates.numberOfSetBits + * */ void preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector& stateRewards); /*! * initializes the Approximation Model * - * @note computeFlagsAndSimplifiedModel should be called before calling this + * @note does not check whether approximation can be applied */ - void initializeApproximationModel(storm::models::sparse::Dtmc const& simpleModel); + void initializeApproximationModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula); /*! * initializes the Sampling Model - * @note computeFlagsAndSimplifiedModel should be called before calling this */ - void initializeSamplingModel(storm::models::sparse::Dtmc const& simpleModel); + void initializeSamplingModel(storm::models::sparse::Dtmc const& model, std::shared_ptr formula); /*! * Computes the reachability function via state elimination @@ -228,7 +235,9 @@ namespace storm { double specifiedFormulaBound; // the original model after states with constant transitions have been eliminated - std::shared_ptr> simplifiedModel; + std::shared_ptr> simpleModel; + // a formula that can be checked on the simplified model + std::shared_ptr simpleFormula; // the model that is used to approximate the reachability values std::shared_ptr approximationModel; // the model that can be instantiated to check the value at a certain point diff --git a/src/utility/vector.h b/src/utility/vector.h index d9163d5c8..4b09c1a5e 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -85,25 +85,6 @@ namespace storm { } } - /*! - * Selects the elements from the given vector at the specified positions and writes them consecutively into the same vector. - * The size of the vector is reduced accordingly. - * @param vector The vector from which to select the elements and into which the selected elements are to be written. - * @param positions The positions at which to select the elements from the values vector. - */ - template - void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - if(oldPosition!=position){ - vector[oldPosition++] = std::move(vector[position]); - } else { - ++oldPosition; - } - } - vector.resize(oldPosition); - } - /*! * Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector. *