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(storm::utility::convertNumber(0.00000000001), false); } + template + std::unique_ptr> + ApproximatePOMDPModelchecker::refineReachabilityProbability(storm::models::sparse::Pomdp const &pomdp, + std::set const &targetObservations, bool min, + uint64_t startingResolution, uint64_t stepSize, uint64_t maxNrOfRefinements) { + uint64_t currentResolution = startingResolution; + uint64_t currentRefinement = 0; + std::unique_ptr> res = std::make_unique>( + POMDPCheckResult{storm::utility::one(), storm::utility::zero()}); + while (currentRefinement < maxNrOfRefinements && !cc.isEqual(storm::utility::zero(), 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 std::unique_ptr> ApproximatePOMDPModelchecker::computeReachabilityProbability(storm::models::sparse::Pomdp 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> + refineReachabilityProbability(storm::models::sparse::Pomdp const &pomdp, + std::set const &targetObservations, bool min, + uint64_t startingResolution, uint64_t stepSize, uint64_t maxNrOfRefinements); + std::unique_ptr> computeReachabilityProbability(storm::models::sparse::Pomdp const &pomdp, std::set targetObservations, bool min,