From 29fb202761ede7143d284572df29d82da5131053 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Mon, 26 Jul 2021 16:51:28 +0200
Subject: [PATCH] cleaned up GameVi and LraViHelper
---
.../infinitehorizon/internal/LraViHelper.cpp | 11 ++++-----
.../rpatl/helper/internal/GameViHelper.cpp | 24 ++-----------------
2 files changed, 6 insertions(+), 29 deletions(-)
diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
index 41b08ac1b..15c12ba95 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
@@ -221,13 +221,10 @@ namespace storm {
}
performIterationStep(env, dir, choices);
}
- //std::cout << "result (" << iter << " steps):" << std::endl;
- storm::utility::vector::applyPointwise<ValueType, ValueType>(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; });
- //for(int i = 0; i < xNew().size() ; i++ ) {
- // std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl;
- // //if(i == 50) {std::cout << "only showing top 50 lines"; break; }
- //}
- if(gameNondetTs()) result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ?
+ if(gameNondetTs()) {
+ storm::utility::vector::applyPointwise<ValueType, ValueType>(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; });
+ result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ?
+ }
return result;
}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
index 0a5bf93f3..58a42a397 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
@@ -8,8 +8,6 @@
#include "storm/utility/SignalHandler.h"
#include "storm/utility/vector.h"
-// TODO this will undergo major refactoring as soon as we implement model checking of further properties
-
namespace storm {
namespace modelchecker {
namespace helper {
@@ -21,10 +19,6 @@ namespace storm {
template <typename ValueType>
void GameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
- // TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper
- // -> clip statesofcoalition
- // -> compute b vector from psiStates
- // -> clip transitionmatrix and create multiplier
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
_x1IsCurrent = false;
@@ -75,29 +69,16 @@ namespace storm {
}
_x1IsCurrent = !_x1IsCurrent;
- // multiplyandreducegaussseidel
- // Ax + b
if (choices == nullptr) {
- //STORM_LOG_DEBUG("\n" << _transitionMatrix);
- //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld()));
- //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b));
- //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew()));
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition);
- //std::cin.get();
} else {
- // Also keep track of the choices made.
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition);
}
// compare applyPointwise
storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType {
- if(storm::solver::maximize(dir)) {
- if(a > b) return a;
- else return b;
- } else {
- if(a > b) return a;
- else return b;
- }
+ if(a > b) return a;
+ else return b;
});
}
@@ -129,7 +110,6 @@ namespace storm {
return false;
}
}
- // TODO needs checking
return true;
}