Added procedure to repeat probability computation with higher resolution

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,

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,