diff --git a/src/storm-pomdp/builder/BeliefMdpExplorer.h b/src/storm-pomdp/builder/BeliefMdpExplorer.h index fd2b54862..e5d233aec 100644 --- a/src/storm-pomdp/builder/BeliefMdpExplorer.h +++ b/src/storm-pomdp/builder/BeliefMdpExplorer.h @@ -473,6 +473,8 @@ namespace storm { std::unique_ptr res(storm::api::verifyWithSparseEngine(exploredMdp, task)); if (res) { values = std::move(res->asExplicitQuantitativeCheckResult().getValueVector()); + STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(lowerValueBounds, values, std::less_equal()), "Computed values are smaller than the lower bound."); + STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(upperValueBounds, values, std::greater_equal()), "Computed values are larger than the upper bound."); } else { STORM_LOG_ASSERT(storm::utility::resources::isTerminate(), "Empty check result!"); STORM_LOG_ERROR("No result obtained while checking."); diff --git a/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h b/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h index 862a82a05..ca4c2192f 100644 --- a/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h +++ b/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h @@ -88,6 +88,7 @@ namespace storm { pomdpScheduler.setChoice(choiceDistribution, state); } } + STORM_LOG_ASSERT(!pomdpScheduler.isPartialScheduler(), "Expected a fully defined scheduler."); auto scheduledModel = underlyingMdp->applyScheduler(pomdpScheduler, false); auto resultPtr2 = storm::api::verifyWithSparseEngine(scheduledModel, storm::api::createTask(formula.asSharedPointer(), false)); @@ -104,6 +105,7 @@ namespace storm { result.lower = std::move(pomdpSchedulerResult); result.upper = std::move(fullyObservableResult); } + STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(result.lower, result.upper, std::less_equal()), "Lower bound is larger than upper bound"); return result; }