Over-Approximation: Taking current values as new lower/upper bounds for next refinement step.

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 {

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();