Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -88,10 +88,10 @@ namespace storm {
                     auto const& gridSettings = storm::settings::getModule<storm::settings::modules::GridApproximationSettings>();
                     typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType>::Options options;
                     options.initialGridResolution = gridSettings.getGridResolution();
-                    options.explorationThreshold = gridSettings.getExplorationThreshold();
+                    options.explorationThreshold = storm::utility::convertNumber<ValueType>(gridSettings.getExplorationThreshold());
                     options.doRefinement = gridSettings.isRefineSet();
-                    options.refinementPrecision = gridSettings.getRefinementPrecision();
-                    options.numericPrecision = gridSettings.getNumericPrecision();
+                    options.refinementPrecision = storm::utility::convertNumber<ValueType>(gridSettings.getRefinementPrecision());
+                    options.numericPrecision = storm::utility::convertNumber<ValueType>(gridSettings.getNumericPrecision());
                     options.cacheSubsimplices = gridSettings.isCacheSimplicesSet();
                     if (storm::NumberTraits<ValueType>::IsExact) {
                         if (gridSettings.isNumericPrecisionSetFromDefault()) {

src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp

@@ -217,7 +217,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;