From 8b4595042ee78316a641f1a558366d881c754017 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 24 Apr 2020 08:58:50 +0200 Subject: [PATCH] Only do iteration output if the result bound improved. Handle integer overflows for the observation resolution. --- .../ApproximatePOMDPModelchecker.cpp | 33 +++++++++++++------ 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 31bbea7ce..f8a49765c 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -234,7 +234,8 @@ namespace storm { template void ApproximatePOMDPModelchecker::refineReachability(std::set const &targetObservations, bool min, boost::optional rewardModelName, std::vector const& lowerPomdpValueBounds, std::vector const& upperPomdpValueBounds, Result& result) { - + statistics.refinementSteps = 0; + // Set up exploration data std::vector observationResolutionVector; std::shared_ptr overApproxBeliefManager; @@ -257,7 +258,9 @@ namespace storm { } ValueType const& newValue = overApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateLowerBound(newValue) : result.updateUpperBound(newValue); - STORM_PRINT_AND_LOG("Over-approx result for refinement step #0 is '" << newValue << "' which " << std::string(betterBound ? "improves" : "does not improve") << " the old value. Current runtime is " << statistics.totalTime << " seconds." << std::endl); + if (betterBound) { + STORM_PRINT_AND_LOG("Over-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); + } } std::shared_ptr underApproxBeliefManager; @@ -282,19 +285,19 @@ namespace storm { } ValueType const& newValue = underApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateUpperBound(newValue) : result.updateLowerBound(newValue); - STORM_PRINT_AND_LOG("Under-approx result for refinement step #0 is '" << newValue << "' which " << std::string(betterBound ? "improves" : "does not improve") << " the old value. Current runtime is " << statistics.totalTime << " seconds." << std::endl); + if (betterBound) { + STORM_PRINT_AND_LOG("Under-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); + } } // Start refinement - statistics.refinementSteps = 0; STORM_LOG_WARN_COND(options.refineStepLimit.is_initialized() || !storm::utility::isZero(options.refinePrecision), "No termination criterion for refinement given. Consider to specify a steplimit, a non-zero precisionlimit, or a timeout"); STORM_LOG_WARN_COND(storm::utility::isZero(options.refinePrecision) || (options.unfold && options.discretize), "Refinement goal precision is given, but only one bound is going to be refined."); - while ((!options.refineStepLimit.is_initialized() || statistics.refinementSteps < options.refineStepLimit.get()) && result.diff() > options.refinePrecision) { + while ((!options.refineStepLimit.is_initialized() || statistics.refinementSteps.get() < options.refineStepLimit.get()) && result.diff() > options.refinePrecision) { if (storm::utility::resources::isTerminate()) { break; } ++statistics.refinementSteps.get(); - STORM_PRINT_AND_LOG("Starting refinement step " << statistics.refinementSteps.get() << ". Current difference between lower and upper bound is " << result.diff() << "." << std::endl); if (options.discretize) { // Refine over-approximation @@ -311,7 +314,9 @@ namespace storm { if (overApproximation->hasComputedValues()) { ValueType const& newValue = overApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateLowerBound(newValue) : result.updateUpperBound(newValue); - STORM_PRINT_AND_LOG("Over-approx result for refinement step #" << statistics.refinementSteps.get() << " is '" << newValue << "' which " << std::string(betterBound ? "improves" : "does not improve") << " the old value. Current runtime is " << statistics.totalTime << " seconds." << std::endl); + if (betterBound) { + STORM_PRINT_AND_LOG("Over-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); + } } else { break; } @@ -326,7 +331,9 @@ namespace storm { if (underApproximation->hasComputedValues()) { ValueType const& newValue = underApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateUpperBound(newValue) : result.updateLowerBound(newValue); - STORM_PRINT_AND_LOG("Under-approx result for refinement step #" << statistics.refinementSteps.get() << " is '" << newValue << "' which " << std::string(betterBound ? "improves" : "does not improve") << " the old value. Current runtime is " << statistics.totalTime << " seconds." << std::endl); + if (betterBound) { + STORM_PRINT_AND_LOG("Under-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); + } } else { break; } @@ -415,8 +422,14 @@ namespace storm { refinedObservations = storm::utility::vector::filter(obsRatings, [&heuristicParameters](ValueType const& r) { return r <= heuristicParameters.observationThreshold;}); STORM_LOG_DEBUG("Refining the resolution of " << refinedObservations.getNumberOfSetBits() << "/" << refinedObservations.size() << " observations."); for (auto const& obs : refinedObservations) { - // Increment the resolution at the refined observations - observationResolutionVector[obs] = storm::utility::convertNumber(storm::utility::convertNumber(observationResolutionVector[obs]) * options.resolutionFactor); + // Increment the resolution at the refined observations. + // Detect overflows properly. + storm::RationalNumber newObsResolutionAsRational = storm::utility::convertNumber(observationResolutionVector[obs]) * storm::utility::convertNumber(options.resolutionFactor); + if (newObsResolutionAsRational > storm::utility::convertNumber(std::numeric_limits::max())) { + observationResolutionVector[obs] = std::numeric_limits::max(); + } else { + observationResolutionVector[obs] = storm::utility::convertNumber(newObsResolutionAsRational); + } } overApproximation->restartExploration(); }