From db697e7bfc34bda19ed00055069fbdd213ee7b8d Mon Sep 17 00:00:00 2001
From: Jan Erik Karuc <jan.karuc@rwth-aachen.de>
Date: Sun, 23 Feb 2020 17:23:13 +0100
Subject: [PATCH] Split upper bound guessing for relative and absolute

---
 .../IterativeMinMaxLinearEquationSolver.cpp   | 22 ++++++++++++-------
 .../IterativeMinMaxLinearEquationSolver.h     |  3 ++-
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 8cdfa8394..989db3e22 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -389,9 +389,9 @@ namespace storm {
             std::vector<ValueType> ubDiffV(newX->size());
             std::vector<ValueType> boundsDiffV(currentX->size());
 
-            ValueType one = storm::utility::one<ValueType>();
             ValueType two = storm::utility::convertNumber<ValueType>(2.0);
             ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
+            ValueType relativeBoundGuessingScaler = (storm::utility::one<ValueType>() + precision);
             ValueType doublePrecision = precision * two;
             ValueType terminationPrecision = doublePrecision;
             ValueType iterationPrecision = precision;
@@ -414,7 +414,12 @@ namespace storm {
                     currentVerificationIterations = 0;
 
                     currentUpperBound = *currentX;
-                    guessUpperBound(*currentX, currentUpperBound, precision, relative, one);
+                    if (relative) {
+                        guessUpperBoundRelative(*currentX, currentUpperBound, relativeBoundGuessingScaler);
+                    } else {
+                        guessUpperBoundAbsolute(*currentX, currentUpperBound, precision);
+                    }
+
                     newUpperBound = currentUpperBound;
 
                     // TODO: More efficient check for verification iterations
@@ -508,12 +513,13 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void IterativeMinMaxLinearEquationSolver<ValueType>::guessUpperBound(std::vector<ValueType> &x, std::vector<ValueType> &target, ValueType const& precision, bool const& relative, ValueType const& one) const {
-            if (relative) {
-                storm::utility::vector::scaleVectorInPlace<ValueType, ValueType>(target, (one + precision));
-            } else {
-                storm::utility::vector::applyPointwise<ValueType, ValueType>(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; });
-            }
+        void IterativeMinMaxLinearEquationSolver<ValueType>::guessUpperBoundRelative(std::vector<ValueType> &x, std::vector<ValueType> &target, ValueType const& relativeBoundGuessingScaler) const {
+            storm::utility::vector::scaleVectorInPlace<ValueType, ValueType>(target, relativeBoundGuessingScaler);
+        }
+
+        template<typename ValueType>
+        void IterativeMinMaxLinearEquationSolver<ValueType>::guessUpperBoundAbsolute(std::vector<ValueType> &x, std::vector<ValueType> &target, ValueType const& precision) const {
+            storm::utility::vector::applyPointwise<ValueType, ValueType>(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; });
         }
 
         template<typename ValueType>
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h
index 65f8c1e3e..a43dde906 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h
@@ -45,7 +45,8 @@ namespace storm {
             bool solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
             bool solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
 
-            void guessUpperBound(std::vector<ValueType> &x, std::vector<ValueType> &target, ValueType const& precision, bool const& relative, ValueType const& one) const;
+            void guessUpperBoundRelative(std::vector<ValueType> &x, std::vector<ValueType> &target, ValueType const& relativeBoundGuessingScaler) const;
+            void guessUpperBoundAbsolute(std::vector<ValueType> &x, std::vector<ValueType> &target, ValueType const& precision) const;
 
             bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;