From 7b59f4c7559899e72de85fd54b326d0bcd910ae7 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Tue, 19 Jan 2021 17:25:21 +0100
Subject: [PATCH] adaptations for lra computation in GMMXXMultiplier

Still WIP!
---
 .../infinitehorizon/internal/LraViHelper.cpp  | 23 +++++++++++--------
 src/storm/solver/GmmxxMultiplier.cpp          |  3 ++-
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
index da16522f1..e5aeecdd3 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
@@ -185,6 +185,12 @@ namespace storm {
                         // Check if we are done
                         auto convergenceCheckResult = checkConvergence(relative, precision);
                         result = convergenceCheckResult.currentValue;
+
+                        if(gameNondetTs() && iter > 1) {
+                            xOld() = xOldTemp;
+                            xNew() = xNewTemp;
+                        }
+
                         if (convergenceCheckResult.isPrecisionAchieved) {
                             break;
                         }
@@ -192,13 +198,11 @@ namespace storm {
                             break;
                         }
 
-                        if(gameNondetTs() && iter > 1) {
-                            xOld() = xOldTemp;
-                            xNew() = xNewTemp;
-                        }
 
                         // If there will be a next iteration, we have to prepare it.
-                        prepareNextIteration(env);
+                        if(!gameNondetTs()) {
+                            prepareNextIteration(env);
+                        }
 
                     }
                     if (maxIter.is_initialized() && iter == maxIter.get()) {
@@ -211,17 +215,18 @@ namespace storm {
 
                     if (choices) {
                         // We will be doing one more iteration step and track scheduler choices this time.
-                        prepareNextIteration(env);
+                        if(!gameNondetTs()) {
+                            prepareNextIteration(env);
+                        }
                         performIterationStep(env, dir, choices);
                     }
                     std::cout << "result (" << iter << " steps):" << std::endl;
-                    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; }
+                    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; // TODO is "init" always going to be .at(0) ?
                     return result;
                 }
 
diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp
index 0a2843824..a75ab623f 100644
--- a/src/storm/solver/GmmxxMultiplier.cpp
+++ b/src/storm/solver/GmmxxMultiplier.cpp
@@ -228,6 +228,7 @@ namespace storm {
                         }
                         //std::cout << newValue << ", ";
                         //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
+                        if(this->isOverridden(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) {
                             currentValue = newValue;
                             if (choices) {
                                 selectedChoice = currentRow - *row_group_it;
@@ -250,7 +251,7 @@ namespace storm {
                     // Finally write value to target vector.
                     *target_it = currentValue;
                     if(choices) {
-                        if(this->isOverridden(currentRowGroup) ? !compare(currentValue, oldSelectedChoiceValue) : compare(currentValue, oldSelectedChoiceValue) ) {
+                        if(this->isOverridden(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue) ) {
                             *choice_it = selectedChoice;
                         }
                     }