From 5d61329eb34d1d9ad117845ddf93290a076a36a3 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 27 Nov 2018 15:11:18 +0100
Subject: [PATCH] SVI with relative precision computed values that were
 unnecessarily precise.

---
 src/storm/solver/helper/SoundValueIterationHelper.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/storm/solver/helper/SoundValueIterationHelper.cpp b/src/storm/solver/helper/SoundValueIterationHelper.cpp
index 674ea5160..78c541af9 100644
--- a/src/storm/solver/helper/SoundValueIterationHelper.cpp
+++ b/src/storm/solver/helper/SoundValueIterationHelper.cpp
@@ -45,6 +45,8 @@ namespace storm {
             template<typename ValueType>
             SoundValueIterationHelper<ValueType>::SoundValueIterationHelper(SoundValueIterationHelper<ValueType>&& oldHelper, std::vector<ValueType>& x, std::vector<ValueType>& y, bool relative, ValueType const& precision) : x(x), y(y), xTmp(std::move(oldHelper.xTmp)), yTmp(std::move(oldHelper.yTmp)), hasLowerBound(false), hasUpperBound(false), hasDecisionValue(false), convergencePhase1(true), decisionValueBlocks(false), firstIndexViolatingConvergence(0), minIndex(0), maxIndex(0), relative(relative), precision(precision), numRows(std::move(oldHelper.numRows)), matrixValues(std::move(oldHelper.matrixValues)), matrixColumns(std::move(oldHelper.matrixColumns)), rowIndications(std::move(oldHelper.rowIndications)), rowGroupIndices(oldHelper.rowGroupIndices) {
                 
+                // If x0 is the obtained result, we want x0-eps <= x <= x0+eps for the actual solution x. Hence, the difference between the lower and upper bounds can be 2*eps.
+                this->precision *= storm::utility::convertNumber<ValueType>(2.0);
                 x.assign(x.size(), storm::utility::zero<ValueType>());
                 y.assign(x.size(), storm::utility::one<ValueType>());
             }
@@ -349,10 +351,9 @@ namespace storm {
                 return true;
             }
             
-            
             template<typename ValueType>
             bool SoundValueIterationHelper<ValueType>::isPreciseEnough(ValueType const& xi, ValueType const& yi, ValueType const& lb, ValueType const& ub) {
-                return yi * (ub - lb) <= storm::utility::abs<ValueType>((relative ? (precision * xi) : (precision * storm::utility::convertNumber<ValueType>(2.0))));
+                return yi * (ub - lb) <= storm::utility::abs<ValueType>((relative ? (precision * xi) : (precision)));
             }
             
             template<typename ValueType>