diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 8f4800128..2426268b5 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -114,9 +114,11 @@ namespace storm { } template - void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { + void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { prepareSolversAndMultipliers(env); _x = x; + _b = b; + if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); @@ -125,10 +127,21 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { if(iter == upperBound - 1) { - _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues); + STORM_LOG_DEBUG("before multipliing ..."); + STORM_LOG_DEBUG("_x = " << _x); + STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + + _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); + STORM_LOG_DEBUG("before multipliing ..."); + STORM_LOG_DEBUG("_x = " << _x); + STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + } performIterationStepUpperBound(env, dir); } + x = _x; } @@ -140,57 +153,13 @@ namespace storm { // multiplyandreducegaussseidel // Ax = x' if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, &_b, _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()); - uint bitIndex = 0; - for(uint i = 0; i < filledVector.size(); i++) { - if (relevantStates.get(i)) { - filledVector.at(i) = result.at(bitIndex); - bitIndex++; - } - else if (psiStates.get(i)) { - filledVector.at(i) = 1; - } - } - result = filledVector; - } - - template - void GameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { - std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); - auto choice_it = choiceValues.begin(); - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - if (psiStates.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; - } - } - } - choiceValues = allChoices; - } - template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; @@ -201,6 +170,11 @@ namespace storm { return _produceScheduler; } + template + void GameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { + _transitionMatrix = newTransitionMatrix; + } + template std::vector const& GameViHelper::getProducedOptimalChoices() const { STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); @@ -230,6 +204,21 @@ namespace storm { _multiplier->multiply(env, x, &_b, choiceValues); } + template + void GameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { + std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (psiStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; + } + template std::vector& GameViHelper::xNew() { return _x1IsCurrent ? _x1 : _x2; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 2d1b1538a..8f2c8143f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -31,22 +31,7 @@ namespace storm { /*! * 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 - */ - void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); - - /*! - * Fills the choice values vector to the original size with zeros for ~psiState choices. - */ - void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + void performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); /*! * Sets whether an optimal scheduler shall be constructed during the computation @@ -58,9 +43,20 @@ namespace storm { */ bool isProduceSchedulerSet() const; + /*! + * Changes the transitionMatrix of the gameViHelper to the given one. + */ + void updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix); + storm::storage::Scheduler extractScheduler() const; void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); + + /*! + * Fills the choice values vector to the original size with zeros for ~psiState choices. + */ + void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + private: /*! * Performs one iteration step for value iteration