From 75bacaa6b249f4a33614c556676569116bd92e04 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:46:14 +0200 Subject: [PATCH] deleted BoundedGloballyGameViHelper --- .../internal/BoundedGloballyGameViHelper.cpp | 132 ------------------ .../internal/BoundedGloballyGameViHelper.h | 76 ---------- 2 files changed, 208 deletions(-) delete mode 100644 src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp delete mode 100644 src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp deleted file mode 100644 index 6742476ef..000000000 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ /dev/null @@ -1,132 +0,0 @@ -#include "BoundedGloballyGameViHelper.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 - BoundedGloballyGameViHelper::BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { - } - - template - void BoundedGloballyGameViHelper::prepareSolversAndMultipliers(const Environment& env) { - _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); - } - - template - void BoundedGloballyGameViHelper::performValueIteration(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); - } - performIterationStep(env, dir); - } - - x = _x; - } - - template - void BoundedGloballyGameViHelper::performIterationStep(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 BoundedGloballyGameViHelper::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 BoundedGloballyGameViHelper::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 BoundedGloballyGameViHelper::setProduceScheduler(bool value) { - _produceScheduler = value; - } - - template - bool BoundedGloballyGameViHelper::isProduceSchedulerSet() const { - return _produceScheduler; - } - - template - std::vector const& BoundedGloballyGameViHelper::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& BoundedGloballyGameViHelper::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 BoundedGloballyGameViHelper::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 class BoundedGloballyGameViHelper; -#ifdef STORM_HAVE_CARL - template class BoundedGloballyGameViHelper; -#endif - } - } - } -} diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h deleted file mode 100644 index 8dcb8e848..000000000 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ /dev/null @@ -1,76 +0,0 @@ -#pragma once - -#include "storm/storage/SparseMatrix.h" -#include "storm/solver/LinearEquationSolver.h" -#include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/solver/Multiplier.h" - -namespace storm { - class Environment; - - namespace storage { - template class Scheduler; - } - - namespace modelchecker { - namespace helper { - namespace internal { - - template - class BoundedGloballyGameViHelper { - public: - BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); - - void prepareSolversAndMultipliers(const Environment& env); - - void performValueIteration(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 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); - - /*! - * Sets whether an optimal scheduler shall be constructed during the computation - */ - void setProduceScheduler(bool value); - - /*! - * @return whether an optimal scheduler shall be constructed during the computation - */ - bool isProduceSchedulerSet() const; - - storm::storage::Scheduler extractScheduler() const; - - private: - void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - - /*! - * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. - * @return the produced scheduler of the most recent call. - */ - std::vector const& getProducedOptimalChoices() const; - - /*! - * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. - * @return the produced scheduler of the most recent call. - */ - std::vector& getProducedOptimalChoices(); - - storm::storage::SparseMatrix _transitionMatrix; - storm::storage::BitVector _statesOfCoalition; - std::vector _x; - std::unique_ptr> _multiplier; - - bool _produceScheduler = false; - boost::optional> _producedOptimalChoices; - }; - } - } - } -}