From d9d86e4f56125e224bd5b84a53267b1c707b67bc Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 6 Jul 2018 08:49:50 +0200
Subject: [PATCH] asserted that infinity is never obtained as a model checker
 result

---
 .../deterministicScheds/DetSchedsWeightVectorChecker.cpp        | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DetSchedsWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DetSchedsWeightVectorChecker.cpp
index 4beb37fb7..85aa0d212 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DetSchedsWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DetSchedsWeightVectorChecker.cpp
@@ -38,6 +38,7 @@ namespace storm {
                         
                         ValueType currChoiceValue = storm::utility::zero<ValueType>();
                         for (uint64_t objIndex = 0; objIndex < numObjectives; ++objIndex) {
+                            STORM_LOG_ASSERT(!storm::utility::isInfinity(stateResults[objIndex][state]), "Scheduler induces value infinity at a state.");
                             currChoiceValue += weightVector[objIndex] * stateResults[objIndex][state];
                         }
                         
@@ -60,6 +61,7 @@ namespace storm {
                                 }
                             }
                             
+                            // TODO: For non-exact solving this could 'close' End Components which actually decreases
                             if (choiceValue > currChoiceValue) {
                                 schedulerEvaluator->setChoiceAtState(state, choice);
                             }