From 6fb9f7e74387c136e4a637b1553fcca4ea51902d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 3 Dec 2019 17:28:33 +0100
Subject: [PATCH] Warn if property could not be checked on DFT

---
 .../modelchecker/dft/DFTModelChecker.cpp         | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 5bc4b0f4c..83887c503 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -466,13 +466,17 @@ namespace storm {
                 singleModelCheckingTimer.start();
                 //STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(
-                        storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property,
-                                                                                                               true)));
-                STORM_LOG_ASSERT(result, "Result does not exist.");
-                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-                ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+                        storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property,true)));
+
+                if (result) {
+                    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+                    ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+                    results.push_back(resultValue);
+                } else {
+                    STORM_LOG_WARN("The property '" << *property << "' could not be checked with the current settings.");
+                    results.push_back(-storm::utility::one<ValueType>());
+                }
                 //STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl);
-                results.push_back(resultValue);
                 singleModelCheckingTimer.stop();
                 //STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl);
             }