From d22233771556c74f79a502ee17dfb5c582109c06 Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Wed, 4 Aug 2021 15:36:47 +0200
Subject: [PATCH] added functionality of BoundedGloballyGameViHelper to
GameViHelper
---
.../rpatl/helper/internal/GameViHelper.cpp | 51 ++++++++++++++++++-
.../rpatl/helper/internal/GameViHelper.h | 23 ++++++++-
2 files changed, 71 insertions(+), 3 deletions(-)
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 <typename ValueType>
GameViHelper<ValueType>::GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+ // Intentionally left empty.
}
template <typename ValueType>
void GameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
-
_x1IsCurrent = false;
}
template <typename ValueType>
void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
prepareSolversAndMultipliers(env);
+ // Get precision for convergence check.
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
_b = b;
-
_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
_x2 = _x1;
@@ -113,6 +113,53 @@ namespace storm {
return true;
}
+ template <typename ValueType>
+ void GameViHelper<ValueType>::performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& 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 <typename ValueType>
+ void GameViHelper<ValueType>::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* 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 <typename ValueType>
+ void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates) {
+ std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
+ 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 <typename ValueType>
void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) {
std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
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<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
+ /*!
+ * Perform value iteration until upper bound
+ */
+ void performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
+
+ /*!
+ * Fills the result vector to the original size with zeros for all states except the relevantStates
+ */
+ void fillResultVector(std::vector<ValueType>& 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<ValueType> const& x, std::vector<ValueType>& choiceValues);
private:
+ /*!
+ * Performs one iteration step for value iteration
+ */
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+ /*!
+ * Performs one iteration step for value iteration with upper bound
+ */
+ void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+
/*!
* Checks whether the curently computed value achieves the desired precision
*/
@@ -77,7 +98,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> _transitionMatrix;
storm::storage::BitVector _statesOfCoalition;
- std::vector<ValueType> _x1, _x2, _b;
+ std::vector<ValueType> _x, _x1, _x2, _b;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
bool _produceScheduler = false;