diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 58a42a397..8f4800128 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -15,22 +15,22 @@ namespace storm { template GameViHelper::GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + // Intentionally left empty. } template void GameViHelper::prepareSolversAndMultipliers(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); - _x1IsCurrent = false; } template void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { prepareSolversAndMultipliers(env); + // Get precision for convergence check. ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x2 = _x1; @@ -113,6 +113,53 @@ namespace storm { return true; } + template + void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { + prepareSolversAndMultipliers(env); + _x = x; + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + for (uint64_t iter = 0; iter < upperBound; iter++) { + if(iter == upperBound - 1) { + _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues); + } + performIterationStepUpperBound(env, dir); + } + x = _x; + } + + template + void GameViHelper::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + if (!_multiplier) { + prepareSolversAndMultipliers(env); + } + // multiplyandreducegaussseidel + // Ax = x' + if (choices == nullptr) { + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); + } else { + // Also keep track of the choices made. + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); + } + } + + template + void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates) { + std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); + uint bitIndex = 0; + for(uint i = 0; i < filledVector.size(); i++) { + if (relevantStates.get(i)) { + filledVector.at(i) = result.at(bitIndex); + bitIndex++; + } + } + result = filledVector; + } + template void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) { std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 00eca9fe6..2d1b1538a 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -23,8 +23,21 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); + /*! + * Perform value iteration until convergence + */ void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); + /*! + * Perform value iteration until upper bound + */ + void performValueIterationUpperBound(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); + + /*! + * Fills the result vector to the original size with zeros for all states except the relevantStates + */ + void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates); + /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates */ @@ -49,8 +62,16 @@ namespace storm { void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); private: + /*! + * Performs one iteration step for value iteration + */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + /*! + * Performs one iteration step for value iteration with upper bound + */ + void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + /*! * Checks whether the curently computed value achieves the desired precision */ @@ -77,7 +98,7 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::BitVector _statesOfCoalition; - std::vector _x1, _x2, _b; + std::vector _x, _x1, _x2, _b; std::unique_ptr> _multiplier; bool _produceScheduler = false;