From 0863d0e51a619395dae9e8a379602ca67c43dfca Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 10 Nov 2015 11:39:23 +0100 Subject: [PATCH] don't store ALL the occurring policies... Former-commit-id: f442b97b8b76604fe01421da4ab1d21b68479976 --- .../region/ApproximationModel.cpp | 46 ++++++++----------- src/modelchecker/region/ApproximationModel.h | 25 +++++----- src/utility/region.cpp | 2 +- 3 files changed, 33 insertions(+), 40 deletions(-) diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 82e9c8e6c..0b4d66564 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -27,7 +27,7 @@ namespace storm { namespace region { template - ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) : player1Goal(storm::logic::isLowerBound(formula->getComparisonType())){ + ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) { //First some simple checks and initializations if(formula->isProbabilityOperatorFormula()){ this->computeRewards=false; @@ -39,6 +39,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << formula << ". Approximation model only supports eventually or reachability reward formulae."); } + this->solverData.solverData.player1Goal = storm::solver::SolveGoal(storm::logic::isLowerBound(formula->getComparisonType())); STORM_LOG_THROW(parametricModel.hasLabel("target"), storm::exceptions::InvalidArgumentException, "The given Model has no \"target\"-statelabel."); this->targetStates = parametricModel.getStateLabeling().getStates("target"); STORM_LOG_THROW(parametricModel.hasLabel("sink"), storm::exceptions::InvalidArgumentException, "The given Model has no \"sink\"-statelabel."); @@ -67,8 +68,8 @@ namespace storm { initializePlayer1Matrix(parametricModel); } - this->eqSysResult = std::vector(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one() : ConstantType(0.5)); - this->eqSysInitIndex = newIndices[initialState]; + this->solverData.result = std::vector(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one() : ConstantType(0.5)); + this->solverData.initialStateIndex = newIndices[initialState]; } template @@ -244,7 +245,7 @@ namespace storm { ++curRow; } } - this->player1Matrix = matrixBuilder.build(); + this->solverData.player1Matrix = matrixBuilder.build(); } template @@ -259,7 +260,7 @@ namespace storm { invokeSolver(computeLowerBounds, policy); std::vector result(this->maybeStates.size()); - storm::utility::vector::setVectorValues(result, this->maybeStates, this->eqSysResult); + storm::utility::vector::setVectorValues(result, this->maybeStates, this->solverData.result); storm::utility::vector::setVectorValues(result, this->targetStates, this->computeRewards ? storm::utility::zero() : storm::utility::one()); storm::utility::vector::setVectorValues(result, ~(this->maybeStates | this->targetStates), this->computeRewards ? storm::utility::infinity() : storm::utility::zero()); @@ -269,26 +270,17 @@ namespace storm { template ConstantType ApproximationModel::computeInitialStateValue(ParameterRegion const& region, bool computeLowerBounds) { instantiate(region, computeLowerBounds); - std::shared_ptr policy; - if(computeLowerBounds && !this->minimizingPolicies.empty()){ - policy = std::make_shared(**(this->minimizingPolicies.begin())); //we need a fresh policy, initialized with the values of the old one - } else if(!computeLowerBounds && !this->maximizingPolicies.empty()){ - policy = std::make_shared(**(this->maximizingPolicies.begin())); //we need a fresh policy, initialized with the values of the old one - } else { - policy = std::make_shared(this->matrixData.matrix.getRowGroupCount()); - } - invokeSolver(computeLowerBounds, *policy); - if(computeLowerBounds){ - this->minimizingPolicies.insert(policy); - std::cout << minimizingPolicies.size() << std::endl; - } else { - this->maximizingPolicies.insert(policy); - std::cout << maximizingPolicies.size() << std::endl; + Policy& policy = computeLowerBounds ? this->solverData.lastMinimizingPolicy : this->solverData.lastMaximizingPolicy; + //TODO: at this point, set policy to the one stored in the region. + if(policy.empty()){ + //No guess available (yet) + policy = Policy(this->matrixData.matrix.getRowGroupCount(), 0); } + invokeSolver(computeLowerBounds, policy); //TODO: policy for games. + if(policy->empty()) return this->solverData.result[this->solverData.initialStateIndex]; //This can be deleted as soon as policy for games is supported //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; @@ -304,7 +296,7 @@ namespace storm { } //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]; + 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){ @@ -337,8 +329,8 @@ namespace storm { //std::cout << " APPROXMODEL: variable " << fixVar.first << " is always mapped to " << fixVar.second << std::endl; } - // std::cout << " Result is " << this->eqSysResult[this->eqSysInitIndex] << std::endl; - return this->eqSysResult[this->eqSysInitIndex]; + // std::cout << " Result is " << this->solverData.result[this->solverData.initialStateIndex] << std::endl; + return this->solverData.result[this->solverData.initialStateIndex]; } template @@ -404,15 +396,15 @@ namespace storm { storm::solver::SolveGoal goal(computeLowerBounds); std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); solver->setPolicyTracking(); - solver->solveEquationSystem(goal.direction(), this->eqSysResult, this->vectorData.vector, nullptr, nullptr, &policy); + solver->solveEquationSystem(goal.direction(), this->solverData.result, this->vectorData.vector, nullptr, nullptr, &policy); policy = solver->getPolicy(); } template<> void ApproximationModel, double>::invokeSolver(bool computeLowerBounds, Policy& 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); + std::unique_ptr> solver = storm::utility::solver::GameSolverFactory().create(this->solverData.player1Matrix, this->matrixData.matrix); + solver->solveGame(this->solverData.player1Goal.direction(), player2Goal.direction(), this->solverData.result, this->vectorData.vector); } diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index c4687d274..625f09dc7 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -79,22 +79,23 @@ namespace storm { void instantiate(ParameterRegion const& region, bool computeLowerBounds); void invokeSolver(bool computeLowerBounds, Policy& policy); + //A flag that denotes whether we compute probabilities or rewards + bool computeRewards; + //Some designated states in the original model storm::storage::BitVector targetStates, maybeStates; - //The last result of the solving the equation system. Also serves as first guess for the next call. - //Note: eqSysResult.size==maybeStates.numberOfSetBits - std::vector eqSysResult; - //The index which represents the result for the initial state in the eqSysResult vector - std::size_t eqSysInitIndex; - std::unordered_set> minimizingPolicies; - std::unordered_set> maximizingPolicies; + struct SolverData{ + //The results from the previous instantiation. Serve as first guess for the next call. + std::vector result; //Note: result.size==maybeStates.numberOfSetBits + Policy lastMinimizingPolicy, lastMaximizingPolicy; + std::size_t initialStateIndex; //The index which represents the result for the initial state in the result vector + //Player 1 represents the nondeterminism of the given mdp (so, this is irrelevant if we approximate values of a DTMC) + storm::solver::SolveGoal player1Goal; + storm::storage::SparseMatrix player1Matrix; + Policy lastPlayer1Policy; + } solverData; - //A flag that denotes whether we compute probabilities or rewards - bool computeRewards; - //Player 1 represents the nondeterminism of the given mdp (so, this is irrelevant if we approximate values of a DTMC) - storm::solver::SolveGoal player1Goal; - storm::storage::SparseMatrix player1Matrix; /* The data required for the equation system, i.e., a matrix and a vector. * diff --git a/src/utility/region.cpp b/src/utility/region.cpp index 128762b2a..94e8e4031 100644 --- a/src/utility/region.cpp +++ b/src/utility/region.cpp @@ -101,7 +101,7 @@ namespace storm { return var; } - return carl::VariablePool::getInstance().getFreshVariable(variableName, carlVarType); + return carl::freshVariable(variableName, carlVarType); } template<>