From 3d9b53723b26457cc65589a3f7026fd501a5cc4a Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 19 Aug 2020 17:17:14 +0200
Subject: [PATCH] OVI: added case where the guessed upper bound corresponds to
 the fixpoint.

---
 src/storm/solver/helper/OptimisticValueIterationHelper.h | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h
index 5869b74c3..fb646ce76 100644
--- a/src/storm/solver/helper/OptimisticValueIterationHelper.h
+++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h
@@ -199,7 +199,7 @@ namespace storm {
                                 }
                             }
 
-                            if (newUpperBoundAlwaysHigherEqual & !newUpperBoundAlwaysLowerEqual) {
+                            if (newUpperBoundAlwaysHigherEqual && !newUpperBoundAlwaysLowerEqual) {
                                 // All values moved up or stayed the same
                                 // That means the guess for an upper bound is actually a lower bound
                                 iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues);
@@ -207,7 +207,7 @@ namespace storm {
                                 // Set lowerX to the upper bound candidate
                                 std::swap(lowerX, upperX);
                                 break;
-                            } else if (newUpperBoundAlwaysLowerEqual & !newUpperBoundAlwaysHigherEqual) {
+                            } else if (newUpperBoundAlwaysLowerEqual && !newUpperBoundAlwaysHigherEqual) {
                                 // All values moved down or stayed the same and we have a maximum difference of twice the requested precision
                                 // We can safely use twice the requested precision, as we calculate the center of both vectors
                                 bool reachedPrecision;
@@ -223,6 +223,11 @@ namespace storm {
                                     // From now on, we keep updating both bounds
                                     intervalIterationNeeded = true;
                                 }
+                            } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) {
+                                // In this case, the guessed upper bound is the precise fixpoint
+                                status = SolverStatus::Converged;
+                                std::swap(lowerX, auxVector);
+                                break;
                             }
                             // At this point, the old upper bounds (auxVector) are not needed anymore.