From bc52aa86cae75c8e2d4b8e9b0e2296e4d701579a Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 8 Nov 2019 10:48:55 +0100
Subject: [PATCH] Added procedure to repeat probability computation with higher
 resolution

---
 .../ApproximatePOMDPModelchecker.cpp          | 21 +++++++++++++++++++
 .../ApproximatePOMDPModelchecker.h            |  5 +++++
 2 files changed, 26 insertions(+)

diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
index 063f80146..14428c5bf 100644
--- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
+++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
@@ -21,6 +21,27 @@ namespace storm {
                 cc = storm::utility::ConstantsComparator<ValueType>(storm::utility::convertNumber<ValueType>(0.00000000001), false);
             }
 
+            template<typename ValueType, typename RewardModelType>
+            std::unique_ptr<POMDPCheckResult<ValueType>>
+            ApproximatePOMDPModelchecker<ValueType, RewardModelType>::refineReachabilityProbability(storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
+                                                                                                    std::set<uint32_t> const &targetObservations, bool min,
+                                                                                                    uint64_t startingResolution, uint64_t stepSize, uint64_t maxNrOfRefinements) {
+                uint64_t currentResolution = startingResolution;
+                uint64_t currentRefinement = 0;
+                std::unique_ptr<POMDPCheckResult<ValueType>> res = std::make_unique<POMDPCheckResult<ValueType>>(
+                        POMDPCheckResult<ValueType>{storm::utility::one<ValueType>(), storm::utility::zero<ValueType>()});
+                while (currentRefinement < maxNrOfRefinements && !cc.isEqual(storm::utility::zero<ValueType>(), res->OverapproximationValue - res->UnderapproximationValue)) {
+                    STORM_PRINT("--------------------------------------------------------------" << std::endl)
+                    STORM_PRINT("Refinement Step " << currentRefinement + 1 << " - Resolution " << currentResolution << std::endl)
+                    STORM_PRINT("--------------------------------------------------------------" << std::endl)
+                    res = computeReachabilityProbability(pomdp, targetObservations, min, currentResolution);
+                    currentResolution += stepSize;
+                    ++currentRefinement;
+                }
+                STORM_PRINT("Procedure took " << currentRefinement << " refinement steps" << std::endl)
+                return res;
+            }
+
             template<typename ValueType, typename RewardModelType>
             std::unique_ptr<POMDPCheckResult<ValueType>>
             ApproximatePOMDPModelchecker<ValueType, RewardModelType>::computeReachabilityProbability(storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h
index f3947dcdc..4792f9127 100644
--- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h
+++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h
@@ -20,6 +20,11 @@ namespace storm {
             public:
                 explicit ApproximatePOMDPModelchecker();
 
+                std::unique_ptr<POMDPCheckResult<ValueType>>
+                refineReachabilityProbability(storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
+                                               std::set<uint32_t> const &targetObservations, bool min,
+                                               uint64_t startingResolution, uint64_t stepSize, uint64_t maxNrOfRefinements);
+
                 std::unique_ptr<POMDPCheckResult<ValueType>>
                 computeReachabilityProbability(storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
                                                std::set<uint32_t> targetObservations, bool min,