#include "GameViHelper.h" #include "storm/environment/Environment.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/GameSolverEnvironment.h" #include "storm/utility/SignalHandler.h" #include "storm/utility/vector.h" namespace storm { namespace modelchecker { namespace helper { namespace internal { 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, std::vector& constrainedChoiceValues) { 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()); _x1 = x; _x2 = _x1; if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); } this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); } uint64_t iter = 0; constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); while (iter < maxIter) { if(iter == maxIter - 1) { _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); rowGroupIndices.erase(rowGroupIndices.begin()); _multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew()); break; } performIterationStep(env, dir); if (checkConvergence(precision)) { _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); break; } if (storm::utility::resources::isTerminate()) { break; } ++iter; } x = xNew(); if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. performIterationStep(env, dir, &_producedOptimalChoices.get()); } } template void GameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { if (!_multiplier) { prepareSolversAndMultipliers(env); } _x1IsCurrent = !_x1IsCurrent; if (choices == nullptr) { _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); } else { _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); } } template bool GameViHelper::checkConvergence(ValueType threshold) const { STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); // Now check whether the currently produced results are precise enough STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); auto x1It = xOld().begin(); auto x1Ite = xOld().end(); auto x2It = xNew().begin(); ValueType maxDiff = (*x2It - *x1It); ValueType minDiff = maxDiff; // The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now. for (++x1It, ++x2It; x1It != x1Ite; ++x1It, ++x2It) { ValueType diff = (*x2It - *x1It); // Potentially update maxDiff or minDiff bool skipCheck = false; if (maxDiff < diff) { maxDiff = diff; } else if (minDiff > diff) { minDiff = diff; } else { skipCheck = true; } // Check convergence if (!skipCheck && (maxDiff - minDiff) > threshold) { return false; } } return true; } template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; } template bool GameViHelper::isProduceSchedulerSet() const { return _produceScheduler; } template void GameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { _transitionMatrix = newTransitionMatrix; } template void GameViHelper::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) { _statesOfCoalition = newStatesOfCoalition; } template std::vector const& GameViHelper::getProducedOptimalChoices() const { STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); return this->_producedOptimalChoices.get(); } template std::vector& GameViHelper::getProducedOptimalChoices() { STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); return this->_producedOptimalChoices.get(); } template storm::storage::Scheduler GameViHelper::extractScheduler() const{ auto const& optimalChoices = getProducedOptimalChoices(); storm::storage::Scheduler scheduler(optimalChoices.size()); for (uint64_t state = 0; state < optimalChoices.size(); ++state) { scheduler.setChoice(optimalChoices[state], state); } return scheduler; } template void GameViHelper::getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues) { _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; } template std::vector const& GameViHelper::xNew() const { return _x1IsCurrent ? _x1 : _x2; } template std::vector& GameViHelper::xOld() { return _x1IsCurrent ? _x2 : _x1; } template std::vector const& GameViHelper::xOld() const { return _x1IsCurrent ? _x2 : _x1; } template class GameViHelper; #ifdef STORM_HAVE_CARL template class GameViHelper; #endif } } } }