From e80a1081bb6ed0115d1ffb70feb1a48b07c1a10d Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 29 Oct 2015 18:59:22 +0100 Subject: [PATCH] First steps to identify the parameters for which the optimal policy always choses the same boundary Former-commit-id: c2561730f68c10778ace13f452f2b24cb4efebf7 --- .../region/ApproximationModel.cpp | 118 +++++++++++------- src/modelchecker/region/ApproximationModel.h | 16 +-- src/modelchecker/region/ParameterRegion.cpp | 10 ++ src/modelchecker/region/ParameterRegion.h | 11 ++ src/modelchecker/region/RegionBoundary.cpp | 33 +++++ src/modelchecker/region/RegionBoundary.h | 29 +++++ 6 files changed, 159 insertions(+), 58 deletions(-) create mode 100644 src/modelchecker/region/RegionBoundary.cpp create mode 100644 src/modelchecker/region/RegionBoundary.h diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index c93c0fc25..005a33997 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -57,10 +57,9 @@ namespace storm { } //Now pre-compute the information for the equation system. - std::vector rowSubstitutions;// the substitution used in every row - initializeProbabilities(parametricModel, newIndices, rowSubstitutions); + initializeProbabilities(parametricModel, newIndices); if(this->computeRewards){ - initializeRewards(parametricModel, newIndices, rowSubstitutions); + initializeRewards(parametricModel, newIndices); } this->matrixData.assignment.shrink_to_fit(); this->vectorData.assignment.shrink_to_fit(); @@ -73,7 +72,7 @@ namespace storm { } template - void ApproximationModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices, std::vector& rowSubstitutions) { + void ApproximationModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices) { STORM_LOG_DEBUG("Approximation model initialization for probabilities"); /* First run: get a matrix with dummy entries at the new positions. * This matrix will have a row group for every row in the original matrix, @@ -87,7 +86,7 @@ namespace storm { true, // force dimensions true, //will have custom row grouping 0); //Unknown number of rowgroups - rowSubstitutions.reserve(this->maybeStates.getNumberOfSetBits()); + this->matrixData.rowSubstitutions.reserve(this->maybeStates.getNumberOfSetBits()); storm::storage::BitVector relevantColumns = this->computeRewards ? this->maybeStates : (this->maybeStates | this->targetStates); std::size_t curRow = 0; for (auto oldRowGroup : this->maybeStates){ @@ -105,19 +104,19 @@ namespace storm { //compute actual substitution from substitutionId by interpreting the Id as a bit sequence. //the occurringVariables.size() least significant bits of substitutionId will represent the substitution that we have to consider //(00...0 = lower bounds for all parameters, 11...1 = upper bounds for all parameters) - std::map currSubstitution; + std::map currSubstitution; std::size_t parameterIndex=0ull; for(auto const& parameter : occurringVariables){ if((substitutionId>>parameterIndex)%2==0){ - currSubstitution.insert(std::make_pair(parameter, TypeOfBound::LOWER)); + currSubstitution.insert(typename std::map::value_type(parameter, RegionBoundary::LOWER)); } else{ - currSubstitution.insert(std::make_pair(parameter, TypeOfBound::UPPER)); + currSubstitution.insert(typename std::map::value_type(parameter, RegionBoundary::UPPER)); } ++parameterIndex; } std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->funcSubData.substitutions, std::move(currSubstitution)); - rowSubstitutions.push_back(substitutionIndex); + this->matrixData.rowSubstitutions.push_back(substitutionIndex); //For every substitution, run again through the row and add a dummy entry //Note that this is still executed once, even if no parameters occur. for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){ @@ -130,7 +129,7 @@ namespace storm { } } //Build the matrix. Override the row count (required e.g. when there are only transitions to target for the last matrixrow) - this->matrixData.matrix=matrixBuilder.build(rowSubstitutions.size()); + this->matrixData.matrix=matrixBuilder.build(this->matrixData.rowSubstitutions.size()); //Now run again through both matrices to get the remaining ingredients of the matrixData and vectorData this->matrixData.assignment.reserve(this->matrixData.matrix.getEntryCount()); @@ -158,7 +157,7 @@ namespace storm { if(storm::utility::isConstant(oldEntry.getValue())){ eqSysMatrixEntry->setValue(storm::utility::region::convertNumber(storm::utility::region::getConstantPart(oldEntry.getValue()))); } else { - auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(oldEntry.getValue(), rowSubstitutions[curRow]), dummyValue)).first; + auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(oldEntry.getValue(), this->matrixData.rowSubstitutions[curRow]), dummyValue)).first; this->matrixData.assignment.emplace_back(eqSysMatrixEntry, functionsIt->second); //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. } @@ -169,7 +168,7 @@ namespace storm { if(storm::utility::isConstant(storm::utility::simplify(targetProbability))){ *vectorIt = storm::utility::region::convertNumber(storm::utility::region::getConstantPart(targetProbability)); } else { - auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(targetProbability, rowSubstitutions[curRow]), dummyValue)).first; + auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(targetProbability, this->matrixData.rowSubstitutions[curRow]), dummyValue)).first; this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second); *vectorIt = dummyValue; } @@ -184,7 +183,7 @@ namespace storm { } template - void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices, std::vector const& rowSubstitutions){ + void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices){ STORM_LOG_DEBUG("Approximation model initialization for Rewards"); STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Rewards are only supported for DTMCs (yet)"); //Note: Since the original model is assumed to be a DTMC, there is no outgoing transition of a maybeState that leads to an infinity state. @@ -209,29 +208,15 @@ namespace storm { std::set occurringRewVariables; storm::utility::region::gatherOccurringVariables(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState], occurringRewVariables); // For each row in the row group of oldState, we get the corresponding substitution and insert the FunctionSubstitution - // We might find out that the reward is independent of the probability parameters (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 FunctionSubstitution - bool rewardDependsOnProbVars=true; - typename std::unordered_map::iterator functionsIt; for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRowmatrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){ - auto probabilitySub = this->funcSubData.substitutions[rowSubstitutions[matrixRow]]; - if(rewardDependsOnProbVars){ //always executed in first iteration - rewardDependsOnProbVars=false; //Assume that independent... - //Get the correct substitution for this matrixRow - std::map substitution; - for(auto const& rewardVar : occurringRewVariables){ - typename std::map::iterator const substitutionIt = probabilitySub.find(rewardVar); - if(substitutionIt==probabilitySub.end()){ - substitution.insert(std::make_pair(rewardVar, TypeOfBound::CHOSEOPTIMAL)); - } else { - substitution.insert(*substitutionIt); - rewardDependsOnProbVars=true; //.. assumption wrong - } - } - // insert the substitution and the FunctionSubstitution - std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->funcSubData.substitutions, std::move(substitution)); - functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState], substitutionIndex), dummyValue)).first; + //Extend the substitution for the probabilities with the reward parameters + auto& substitution = this->funcSubData.substitutions[this->matrixData.rowSubstitutions[matrixRow]]; + for(auto const& rewardVar : occurringRewVariables){ + //Note that map::insert does nothing if rewardVar is already contained in the substitution (i.e. if rewardVar also occurs in the probability functions) + substitution.insert(typename std::map::value_type(rewardVar, RegionBoundary::UNSPECIFIED)); } + // insert the FunctionSubstitution + auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState], this->matrixData.rowSubstitutions[matrixRow]), dummyValue)).first; //insert assignment and dummy data this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second); *vectorIt = dummyValue; @@ -270,7 +255,8 @@ namespace storm { template std::vector ApproximationModel::computeValues(ParameterRegion const& region, bool computeLowerBounds) { instantiate(region, computeLowerBounds); - invokeSolver(computeLowerBounds); + std::vector policy; + invokeSolver(computeLowerBounds, policy); std::vector result(this->maybeStates.size()); storm::utility::vector::setVectorValues(result, this->maybeStates, this->eqSysResult); @@ -283,8 +269,45 @@ namespace storm { template ConstantType ApproximationModel::computeInitialStateValue(ParameterRegion const& region, bool computeLowerBounds) { instantiate(region, computeLowerBounds); - invokeSolver(computeLowerBounds); -// std::cout << "initialStateValue is " << this->eqSysResult[this->eqSysInitIndex] << std::endl; + std::vector policy; + invokeSolver(computeLowerBounds, policy); + + //TODO: policy for games. + //TODO: do this only when necessary. + //TODO: (maybe) when a few parameters are mapped to another value, build a "nicer" scheduler and check whether it induces values that are more optimal. + if(policy.empty()) return this->eqSysResult[this->eqSysInitIndex]; + //Get the set of parameters which are (according to the policy) always mapped to the same region boundary. + //First, collect all (relevant) parameters, i.e., the ones that are set to the lower or upper boundary. + std::map fixedVariables; + for(auto const& substitution : this->funcSubData.substitutions){ + for( auto const& sub : substitution){ + if(sub.second!= RegionBoundary::UNSPECIFIED){ + fixedVariables.insert(typename std::map::value_type(sub.first, RegionBoundary::UNSPECIFIED)); + } + } + } + //Now erase the parameters that are mapped to different boundaries. + for(std::size_t rowGroup=0; rowGroupmatrixData.matrix.getRowGroupCount(); ++rowGroup){ + std::size_t row = this->matrixData.matrix.getRowGroupIndices()[rowGroup] + policy[rowGroup]; + for(std::pair const& sub : this->funcSubData.substitutions[this->matrixData.rowSubstitutions[row]]){ + auto fixedVarIt = fixedVariables.find(sub.first); + if(fixedVarIt != fixedVariables.end() && fixedVarIt->second != sub.second){ + if(fixedVarIt->second == RegionBoundary::UNSPECIFIED){ + fixedVarIt->second = sub.second; + } else { + // the solution maps the current variable at least once to lower boundary and at least once to the upper boundary. + fixedVariables.erase(fixedVarIt); + } + } + } + if (fixedVariables.empty()){ + break; + } + } + for (auto const& fixVar : fixedVariables){ + //std::cout << "APPROXMODEL: variable " << fixVar.first << " is always mapped to " << fixVar.second << std::endl; + } + return this->eqSysResult[this->eqSysInitIndex]; } @@ -292,20 +315,20 @@ namespace storm { void ApproximationModel::instantiate(const ParameterRegion& region, bool computeLowerBounds) { //Instantiate the substitutions std::vector> instantiatedSubs(this->funcSubData.substitutions.size()); - std::vector> choseOptimalParameters(this->funcSubData.substitutions.size()); + std::vector> unspecifiedParameters(this->funcSubData.substitutions.size()); for(std::size_t substitutionIndex=0; substitutionIndexfuncSubData.substitutions.size(); ++substitutionIndex){ - for(std::pair const& sub : this->funcSubData.substitutions[substitutionIndex]){ + for(std::pair const& sub : this->funcSubData.substitutions[substitutionIndex]){ switch(sub.second){ - case TypeOfBound::LOWER: + case RegionBoundary::LOWER: instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBound(sub.first))); break; - case TypeOfBound::UPPER: + case RegionBoundary::UPPER: instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBound(sub.first))); break; - case TypeOfBound::CHOSEOPTIMAL: + case RegionBoundary::UNSPECIFIED: //Insert some dummy value instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, storm::utility::one())); - choseOptimalParameters[substitutionIndex].insert(sub.first); + unspecifiedParameters[substitutionIndex].insert(sub.first); break; default: STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of Bound"); @@ -319,7 +342,7 @@ namespace storm { auto& result = functionResult.second; result = computeLowerBounds ? storm::utility::infinity() : 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(choseOptimalParameters[funcSub.getSubstitution()]); + auto const& vertices=region.getVerticesOfRegion(unspecifiedParameters[funcSub.getSubstitution()]); for(auto const& vertex : vertices){ //extend the substitution for(auto const& vertexSub : vertex){ @@ -347,17 +370,16 @@ namespace storm { template<> - void ApproximationModel, double>::invokeSolver(bool computeLowerBounds){ + void ApproximationModel, double>::invokeSolver(bool computeLowerBounds, std::vector& policy){ storm::solver::SolveGoal goal(computeLowerBounds); std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); solver->setPolicyTracking(); solver->solveEquationSystem(this->eqSysResult, this->vectorData.vector); - std::vector policy(solver->getPolicy()); - std::cout << "Policy: " << policy.size() << " entries. [0]=" << policy[0] << " [20]=" << policy[20] << std::endl; + policy = solver->getPolicy(); } template<> - void ApproximationModel, double>::invokeSolver(bool computeLowerBounds){ + void ApproximationModel, double>::invokeSolver(bool computeLowerBounds, std::vector& policy){ storm::solver::SolveGoal player2Goal(computeLowerBounds); std::unique_ptr> solver = storm::utility::solver::GameSolverFactory().create(this->player1Matrix, this->matrixData.matrix); solver->solveGame(this->player1Goal.direction(), player2Goal.direction(), this->eqSysResult, this->vectorData.vector); diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index f59f1f600..787d1f33e 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -19,6 +19,7 @@ #include "src/models/sparse/Model.h" #include "src/storage/SparseMatrix.h" #include "src/solver/SolveGoal.h" +#include "src/modelchecker/region/RegionBoundary.h" namespace storm { namespace modelchecker { @@ -56,12 +57,6 @@ namespace storm { ConstantType computeInitialStateValue(ParameterRegion const& region, bool computeLowerBounds); 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 funcSubData.substitutions (allowing to instantiate the substitutions more easily). @@ -126,11 +121,11 @@ namespace storm { typedef typename std::unordered_map::value_type FunctionEntry; - void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices, std::vector& rowSubstitutions); - void initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices, std::vector const& rowSubstitutions); + void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); + void initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); void initializePlayer1Matrix(ParametricSparseModelType const& parametricModel); void instantiate(ParameterRegion const& region, bool computeLowerBounds); - void invokeSolver(bool computeLowerBounds); + void invokeSolver(bool computeLowerBounds, std::vector& policy); //Some designated states in the original model storm::storage::BitVector targetStates, maybeStates; @@ -160,11 +155,12 @@ namespace storm { // the occurring (function,substitution)-pairs together with the corresponding placeholders for the result std::unordered_map functions; //Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region) - std::vector> substitutions; + std::vector> substitutions; } funcSubData; struct MatrixData { storm::storage::SparseMatrix matrix; //The matrix itself. std::vector::iterator, ConstantType&>> assignment; // Connection of matrix entries with placeholders + std::vector rowSubstitutions; //used to obtain which row corresponds to which substitution (used to retrieve information from a scheduler) } matrixData; struct VectorData { std::vector vector; //The vector itself. diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index b7bf64e76..0b7a75893 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -149,6 +149,16 @@ namespace storm { this->satPoint = satPoint; } + template + void ParameterRegion::fixVariables(std::map const& fixedVariables) { + this->fixedVariables = fixedVariables; + } + + template + std::map::VariableType, RegionBoundary> ParameterRegion::getFixedVariables() const { + return fixedVariables; + } + template std::string ParameterRegion::toString() const { std::stringstream regionstringstream; diff --git a/src/modelchecker/region/ParameterRegion.h b/src/modelchecker/region/ParameterRegion.h index 257935a57..4b1e3fe4e 100644 --- a/src/modelchecker/region/ParameterRegion.h +++ b/src/modelchecker/region/ParameterRegion.h @@ -12,6 +12,7 @@ #include "src/modelchecker/region/RegionCheckResult.h" #include "src/utility/region.h" +#include "RegionBoundary.h" namespace storm { @@ -74,6 +75,15 @@ namespace storm { * Sets a point in the region for which the considered property is satisfied. */ void setSatPoint(VariableSubstitutionType const& satPoint); + + /*! + * Can be used to store that it is ok to fix one or more variables to the corresponding lower/upper boundary of this region during the approximation step + */ + void fixVariables(std::map const& fixedVariables); + /*! + * Returns the variables for which it can be assumed that they always lie on the lower/upper boundary of this region + */ + std::map getFixedVariables() const; //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5; std::string toString() const; @@ -124,6 +134,7 @@ namespace storm { RegionCheckResult checkResult; VariableSubstitutionType satPoint; VariableSubstitutionType violatedPoint; + std::map fixedVariables; }; } //namespace region } diff --git a/src/modelchecker/region/RegionBoundary.cpp b/src/modelchecker/region/RegionBoundary.cpp new file mode 100644 index 000000000..3a03b0505 --- /dev/null +++ b/src/modelchecker/region/RegionBoundary.cpp @@ -0,0 +1,33 @@ +/* + * File: RegionBoundary.h + * Author: Tim Quatmann + * + * Created on October 29, 2015, 2:57 PM + */ + +#include "src/modelchecker/region/RegionBoundary.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + namespace region { + std::ostream& operator<<(std::ostream& os, RegionBoundary const& regionBoundary) { + switch (regionBoundary) { + case RegionBoundary::LOWER: + os << "LowerBoundary"; + break; + case RegionBoundary::UPPER: + os << "UpperBoundary"; + break; + case RegionBoundary::UNSPECIFIED: + os << "UnspecifiedBoundary"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region boundary. The case has not been implemented"); + } + return os; + } + } + } +} diff --git a/src/modelchecker/region/RegionBoundary.h b/src/modelchecker/region/RegionBoundary.h new file mode 100644 index 000000000..31aac0e68 --- /dev/null +++ b/src/modelchecker/region/RegionBoundary.h @@ -0,0 +1,29 @@ +/* + * File: RegionBoundary.h + * Author: Tim Quatmann + * + * Created on October 29, 2015, 2:57 PM + */ + +#ifndef STORM_MODELCHECKER_REGION_REGIONBOUNDARY_H +#define STORM_MODELCHECKER_REGION_REGIONBOUNDARY_H + +#include + +namespace storm { + namespace modelchecker{ + namespace region { + //This enum helps to store how a parameter will be substituted. + enum class RegionBoundary { + LOWER, + UPPER, + UNSPECIFIED + }; + + std::ostream& operator<<(std::ostream& os, RegionBoundary const& regionBoundary); + } + } +} + +#endif /* STORM_MODELCHECKER_REGION_REGIONBOUNDARY_H */ +