From de483cd3c16182cbfda5554189dae9d429ea0ccf Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 18 Mar 2020 13:59:29 +0100 Subject: [PATCH 1/2] Added missing number conversion. --- src/storm-pomdp-cli/storm-pomdp.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index e0000c0d6..ac48327b5 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -88,10 +88,10 @@ namespace storm { auto const& gridSettings = storm::settings::getModule(); typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker::Options options; options.initialGridResolution = gridSettings.getGridResolution(); - options.explorationThreshold = gridSettings.getExplorationThreshold(); + options.explorationThreshold = storm::utility::convertNumber(gridSettings.getExplorationThreshold()); options.doRefinement = gridSettings.isRefineSet(); - options.refinementPrecision = gridSettings.getRefinementPrecision(); - options.numericPrecision = gridSettings.getNumericPrecision(); + options.refinementPrecision = storm::utility::convertNumber(gridSettings.getRefinementPrecision()); + options.numericPrecision = storm::utility::convertNumber(gridSettings.getNumericPrecision()); options.cacheSubsimplices = gridSettings.isCacheSimplicesSet(); if (storm::NumberTraits::IsExact) { if (gridSettings.isNumericPrecisionSetFromDefault()) { From 581e165fb91b1d16658fd362eb74d7b711cc7221 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 18 Mar 2020 13:59:46 +0100 Subject: [PATCH 2/2] Actually use the refinement precision.... --- src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 1c40e96f6..eb5ac7048 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -219,7 +219,8 @@ namespace storm { res = computeRefinementStep(targetObservations, min, observationResolutionVector, false, res, changedObservations, initialOverApproxMap, underApproxMap, underApproxModelSize); //storm::api::exportSparseModelAsDot(res->overApproxModelPtr, "oa_model_" + std::to_string(refinementCounter +1) + ".dot"); - if (cc.isEqual(res->overApproxValue, res->underApproxValue)) { + STORM_LOG_ERROR_COND(cc.isLess(res->underApproxValue, res->overApproxValue), "The value for the under-approximation is larger than the value for the over-approximation."); + if (res->overApproxValue - res->underApproxValue <= options.refinementPrecision) { break; } ++refinementCounter;