From 3c5df045c1138457b5a98f49ec59a245cb0f7994 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 8 Apr 2020 12:18:32 +0200
Subject: [PATCH] Added a few assertions

---
 src/storm-pomdp/builder/BeliefMdpExplorer.h                     | 2 ++
 .../modelchecker/TrivialPomdpValueBoundsModelChecker.h          | 2 ++
 2 files changed, 4 insertions(+)

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<storm::modelchecker::CheckResult> res(storm::api::verifyWithSparseEngine<ValueType>(exploredMdp, task));
                 if (res) {
                     values = std::move(res->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
+                    STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(lowerValueBounds, values, std::less_equal<ValueType>()), "Computed values are smaller than the lower bound.");
+                    STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(upperValueBounds, values, std::greater_equal<ValueType>()), "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<ValueType>(scheduledModel, storm::api::createTask<ValueType>(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<ValueType>()), "Lower bound is larger than upper bound");
                     return result;
                 }