From 02a325ba75574e586282141a200003977a825ba3 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 18 Mar 2020 15:29:37 +0100 Subject: [PATCH] Fixed error that refinement did not stop if initial computation already yields same values for over- and under-approximation --- .../modelchecker/ApproximatePOMDPModelchecker.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index ce37e0f0c..936db1c38 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -142,7 +142,7 @@ namespace storm { STORM_PRINT("==============================" << std::endl << "Initial Computation" << std::endl << "------------------------------" << std::endl) std::shared_ptr> res = computeFirstRefinementStep(targetObservations, min, observationResolutionVector, false, initialOverApproxMap, underApproxMap, underApproxModelSize); ValueType lastMinScore = storm::utility::infinity(); - while (refinementCounter < 1000) { + while (refinementCounter < 1000 && res->overApproxValue - res->underApproxValue > options.refinementPrecision) { // TODO the actual refinement // choose which observation(s) to refine std::vector obsAccumulator(pomdp.getNrObservations(), storm::utility::zero()); @@ -219,9 +219,6 @@ namespace storm { //storm::api::exportSparseModelAsDot(res->overApproxModelPtr, "oa_model_" + std::to_string(refinementCounter +1) + ".dot"); STORM_LOG_ERROR_COND(cc.isLess(res->underApproxValue, res->overApproxValue) || cc.isEqual(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; }