From 61215e4b24fb89e90e2e44665226c50a55794863 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 22 Apr 2020 09:06:28 +0200
Subject: [PATCH] Over-Approximation: Taking current values as new lower/upper
 bounds for next refinement step.

---
 src/storm-pomdp/builder/BeliefMdpExplorer.h              | 9 +++++++++
 .../modelchecker/ApproximatePOMDPModelchecker.cpp        | 5 +++++
 2 files changed, 14 insertions(+)

diff --git a/src/storm-pomdp/builder/BeliefMdpExplorer.h b/src/storm-pomdp/builder/BeliefMdpExplorer.h
index 5fb5bfe26..36f525663 100644
--- a/src/storm-pomdp/builder/BeliefMdpExplorer.h
+++ b/src/storm-pomdp/builder/BeliefMdpExplorer.h
@@ -548,6 +548,15 @@ namespace storm {
                 }
             }
             
+            void takeCurrentValuesAsUpperBounds() {
+                STORM_LOG_ASSERT(status == Status::ModelChecked, "Method call is invalid in current status.");
+                upperValueBounds = values;
+            }
+            
+            void takeCurrentValuesAsLowerBounds() {
+                STORM_LOG_ASSERT(status == Status::ModelChecked, "Method call is invalid in current status.");
+                lowerValueBounds = values;
+            }
             
         private:
             MdpStateType noState() const {
diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
index b35ded61c..8aa83452a 100644
--- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
+++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
@@ -255,6 +255,11 @@ namespace storm {
                     
                     // Refine over-approximation
                     STORM_LOG_DEBUG("Refining over-approximation with aggressiveness " << refinementAggressiveness << ".");
+                    if (min) {
+                        overApproximation->takeCurrentValuesAsLowerBounds();
+                    } else {
+                        overApproximation->takeCurrentValuesAsUpperBounds();
+                    }
                     buildOverApproximation(targetObservations, min, rewardModelName.is_initialized(), true, &refinementAggressiveness, observationResolutionVector, overApproxBeliefManager, overApproximation);
                     if (overApproximation->hasComputedValues()) {
                         overApproxValue = overApproximation->getComputedValueAtInitialState();