diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index b43e62711..bee46318d 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -498,7 +498,9 @@ namespace storm { // current maximal resolution (needed for refinement heuristic) auto obsRatings = getObservationRatings(overApproximation, observationResolutionVector); // If there is a score < 1, we have not reached a fixpoint, yet - if (std::any_of(obsRatings.begin(), obsRatings.end(), [](ValueType const& value){return value < storm::utility::one();})) { + BeliefValueType numericPresicion = storm::utility::convertNumber(options.numericPrecision); + if (std::any_of(obsRatings.begin(), obsRatings.end(), [&numericPresicion](ValueType const& value){return value + numericPresicion < storm::utility::one();})) { + STORM_LOG_INFO_COND(!fixPoint, "Not reaching a refinement fixpoint because there are still observations to refine."); fixPoint = false; } refinedObservations = storm::utility::vector::filter(obsRatings, [&heuristicParameters](ValueType const& r) { return r <= heuristicParameters.observationThreshold;}); @@ -507,15 +509,16 @@ namespace storm { // Increment the resolution at the refined observations. // Use storm's rational number to 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] = storm::utility::convertNumber(std::numeric_limits::max()); + static_assert(storm::NumberTraits::IsExact || std::is_same::value, "Unhandled belief value type"); + if (!storm::NumberTraits::IsExact && newObsResolutionAsRational > storm::utility::convertNumber(std::numeric_limits::max())) { + observationResolutionVector[obs] = storm::utility::convertNumber(std::numeric_limits::max()); } else { observationResolutionVector[obs] = storm::utility::convertNumber(newObsResolutionAsRational); } } overApproximation->restartExploration(); } - statistics.overApproximationMaxResolution = storm::utility::convertNumber(storm::utility::ceil(*std::max_element(observationResolutionVector.begin(), observationResolutionVector.end()))); + statistics.overApproximationMaxResolution = storm::utility::ceil(*std::max_element(observationResolutionVector.begin(), observationResolutionVector.end())); // Start exploration storm::utility::Stopwatch explorationTime; diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index 0e1b3a715..f5904e0dc 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h @@ -99,7 +99,7 @@ namespace storm { bool overApproximationBuildAborted; storm::utility::Stopwatch overApproximationBuildTime; storm::utility::Stopwatch overApproximationCheckTime; - boost::optional overApproximationMaxResolution; + boost::optional overApproximationMaxResolution; boost::optional underApproximationStates; bool underApproximationBuildAborted;