From a147552be048e1deb5d7d96f951561162b862a3e Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Mon, 15 Mar 2021 14:23:47 +0100
Subject: [PATCH] warn the user of no shielding action is possible

---
 src/storm/shields/PostSafetyShield.cpp | 14 +++++---------
 src/storm/shields/PreSafetyShield.cpp  |  5 +++++
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostSafetyShield.cpp
index 33b86a815..6b5773854 100644
--- a/src/storm/shields/PostSafetyShield.cpp
+++ b/src/storm/shields/PostSafetyShield.cpp
@@ -13,24 +13,21 @@ namespace tempest {
         template<typename ValueType, typename IndexType>
         storm::storage::PostScheduler<ValueType> PostSafetyShield<ValueType, IndexType>::construct() {
             storm::storage::PostScheduler<ValueType> shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes());
-            STORM_LOG_DEBUG(this->rowGroupIndices.size());
-            STORM_LOG_DEBUG(this->relevantStates);
-            STORM_LOG_DEBUG(this->coalitionStates.get());
-            for(auto const& x : this->choiceValues) {
-                STORM_LOG_DEBUG(x << ",");
-            }
             auto choice_it = this->choiceValues.begin();
             if(this->coalitionStates.is_initialized()) {
                 this->relevantStates &= this->coalitionStates.get();
             }
-            STORM_LOG_DEBUG(this->relevantStates);
             for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) {
                 if(this->relevantStates.get(state)) {
                     uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state];
                     auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it;
                     ValueType maxProbability = *(choice_it + maxProbabilityIndex);
+                    if(!allowedValue<ValueType, IndexType>(maxProbability, maxProbability, this->shieldingExpression)) {
+                        STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
+                        shield.setChoice(0, storm::storage::Distribution<ValueType, IndexType>(), state);
+                        continue;
+                    }
                     for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
-                        STORM_LOG_DEBUG("processing " << state << " with rowGroupSize of " << rowGroupSize << " choice index " << choice << " prob: " << *choice_it << " > " << maxProbability);
                         storm::storage::Distribution<ValueType, IndexType> actionDistribution;
                         if(allowedValue<ValueType, IndexType>(maxProbability, *choice_it, this->shieldingExpression)) {
                             actionDistribution.addProbability(choice, 1);
@@ -38,7 +35,6 @@ namespace tempest {
                             actionDistribution.addProbability(maxProbabilityIndex, 1);
                         }
                         actionDistribution.normalize();
-                        STORM_LOG_DEBUG("  dist: " << actionDistribution);
                         shield.setChoice(choice, storm::storage::SchedulerChoice<ValueType>(actionDistribution), state);
                     }
                 } else {
diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp
index d1c769b2b..fb63387d7 100644
--- a/src/storm/shields/PreSafetyShield.cpp
+++ b/src/storm/shields/PreSafetyShield.cpp
@@ -22,6 +22,11 @@ namespace tempest {
                     uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state];
                     storm::storage::Distribution<ValueType, IndexType> actionDistribution;
                     ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize);
+                    if(!allowedValue<ValueType, IndexType>(maxProbability, maxProbability, this->shieldingExpression)) {
+                        STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
+                        shield.setChoice(storm::storage::Distribution<ValueType, IndexType>(), state);
+                        continue;
+                    }
                     for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
                         if(allowedValue<ValueType, IndexType>(maxProbability, *choice_it, this->shieldingExpression)) {
                             actionDistribution.addProbability(choice, *choice_it);