From 2273fda7c9eb22ea090b258ad1b085b9233efcc3 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 19 Aug 2020 16:53:21 +0200
Subject: [PATCH] ovi helper: Take the relative/absolute precision and the
 maximal iteration count as a parameter because otherwise it is not clear
 whether we should take this information from the NativeEnvironment or the
 MinMaxEnvironment.

---
 src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp | 6 +++++-
 src/storm/solver/NativeLinearEquationSolver.cpp          | 6 +++++-
 src/storm/solver/helper/OptimisticValueIterationHelper.h | 8 +-------
 3 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 02141283e..90837a6b3 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -410,7 +410,11 @@ namespace storm {
                             multiplier.multiplyAndReduce(env, dir, *y, &b, *yPrime);
                             std::swap(y, yPrime);
                         }
-                    }, relevantValues);
+                    },
+                    env.solver().minMax().getRelativeTerminationCriterion(),
+                    storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision()),
+                    env.solver().minMax().getMaximalNumberOfIterations(),
+                    relevantValues);
             auto two = storm::utility::convertNumber<ValueType>(2.0);
             storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(*lowerX, *upperX, x, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; });
 
diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp
index a018d5f02..f06e1f311 100644
--- a/src/storm/solver/NativeLinearEquationSolver.cpp
+++ b/src/storm/solver/NativeLinearEquationSolver.cpp
@@ -686,7 +686,11 @@ namespace storm {
                             multiplier.multiply(env, *y, &b, *yPrime);
                             std::swap(y, yPrime);
                         }
-                    }, relevantValues);
+                    },
+                    env.solver().native().getRelativeTerminationCriterion(),
+                    storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision()),
+                    env.solver().native().getMaximalNumberOfIterations(),
+                    relevantValues);
             auto two = storm::utility::convertNumber<ValueType>(2.0);
             storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(*lowerX, *upperX, x, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; });
             this->logIterations(statusIters.first == SolverStatus::Converged, statusIters.first == SolverStatus::TerminatedEarly, statusIters.second);
diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h
index 781ac9347..5869b74c3 100644
--- a/src/storm/solver/helper/OptimisticValueIterationHelper.h
+++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h
@@ -103,7 +103,7 @@ namespace storm {
              * with precision parameters as given by the environment env.
              */
             template<typename ValueType, typename ValueIterationCallback, typename SingleIterationCallback>
-            std::pair<SolverStatus, uint64_t> solveEquationsOptimisticValueIteration(Environment const& env, std::vector<ValueType>* lowerX, std::vector<ValueType>* upperX, std::vector<ValueType>* auxVector, ValueIterationCallback const& valueIterationCallback, SingleIterationCallback const& singleIterationCallback, boost::optional<storm::storage::BitVector> relevantValues = boost::none) {
+            std::pair<SolverStatus, uint64_t> solveEquationsOptimisticValueIteration(Environment const& env, std::vector<ValueType>* lowerX, std::vector<ValueType>* upperX, std::vector<ValueType>* auxVector, ValueIterationCallback const& valueIterationCallback, SingleIterationCallback const& singleIterationCallback, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional<storm::storage::BitVector> relevantValues = boost::none) {
                 STORM_LOG_ASSERT(lowerX->size() == upperX->size(), "Dimension missmatch.");
                 STORM_LOG_ASSERT(lowerX->size() == auxVector->size(), "Dimension missmatch.");
                 
@@ -120,18 +120,12 @@ namespace storm {
                 // Get some parameters for the algorithm
                 // 2
                 ValueType two = storm::utility::convertNumber<ValueType>(2.0);
-                // Relative errors
-                bool relative = env.solver().minMax().getRelativeTerminationCriterion();
                 // Use no termination guaranteed upper bound iteration method
                 bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod();
-                // Goal precision
-                ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
                 // Desired max difference between upperX and lowerX
                 ValueType doublePrecision = precision * two;
                 // Upper bound only iterations
                 uint64_t upperBoundOnlyIterations = env.solver().ovi().getUpperBoundOnlyIterations();
-                // Maximum number of iterations done overall
-                uint64_t maxOverallIterations = env.solver().minMax().getMaximalNumberOfIterations();
                 ValueType relativeBoundGuessingScaler = (storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(env.solver().ovi().getUpperBoundGuessingFactor()) * precision);
                 // Initial precision for the value iteration calls
                 ValueType iterationPrecision = precision;