From e8e87d26d62bf486b5a7a6fa8a8af9c60a763282 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Wed, 10 Oct 2018 13:48:28 +0200
Subject: [PATCH] Add check if result actually contains the given variable

---
 src/storm-pars/analysis/MonotonicityChecker.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index 998a8481d..b6178dfa5 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -26,6 +26,7 @@ namespace storm {
             this->model = model;
             this->formulas = formulas;
             this->validate = validate;
+            this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>();
         }
 
         template <typename ValueType>
@@ -99,7 +100,8 @@ namespace storm {
                     STORM_PRINT("Result is constant" << std::endl);
                 } else {
                     for (auto itr2 = varsMonotone.begin(); itr2 != varsMonotone.end(); ++itr2) {
-                        if (!resultCheckOnSamples[itr2->first].first && !resultCheckOnSamples[itr2->first].second) {
+                        if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
+                            (!resultCheckOnSamples[itr2->first].first && !resultCheckOnSamples[itr2->first].second)) {
                             STORM_PRINT("  - Not monotone in: " << itr2->first << std::endl);
                         } else {
                             if (itr2->second.first) {
@@ -184,7 +186,8 @@ namespace storm {
                     auto val = first.getValue();
                     auto vars = val.gatherVariables();
                     for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
-                        if (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second) {
+                        if (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end() &&
+                            (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second)) {
                             if (varsMonotone.find(*itr) == varsMonotone.end()) {
                                 varsMonotone[*itr].first = false;
                                 varsMonotone[*itr].second = false;