From b600498d0ebab1ff8418036cea26e9b8ada21970 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 25 Mar 2020 14:06:19 +0100
Subject: [PATCH] Better output for checking the fully observable model.

---
 src/storm-pomdp-cli/storm-pomdp.cpp | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index b18f77933..58637c6e7 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -155,11 +155,20 @@ namespace storm {
                 }
                 if (pomdpSettings.isCheckFullyObservableSet()) {
                     STORM_PRINT_AND_LOG("Analyzing the formula on the fully observable MDP ... ");
-                    auto result = storm::api::verifyWithSparseEngine<ValueType>(pomdp->template as<storm::models::sparse::Mdp<ValueType>>(), storm::api::createTask<ValueType>(formula.asSharedPointer(), true))->template asExplicitQuantitativeCheckResult<ValueType>();
-                    result.filter(storm::modelchecker::ExplicitQualitativeCheckResult(pomdp->getInitialStates()));
-                    STORM_PRINT_AND_LOG("\nResult: ");
-                    printResult(result.getMin(), result.getMax());
-                    STORM_PRINT_AND_LOG(std::endl);
+                    auto resultPtr = storm::api::verifyWithSparseEngine<ValueType>(pomdp->template as<storm::models::sparse::Mdp<ValueType>>(), storm::api::createTask<ValueType>(formula.asSharedPointer(), true));
+                    if (resultPtr) {
+                        auto result = resultPtr->template asExplicitQuantitativeCheckResult<ValueType>();
+                        result.filter(storm::modelchecker::ExplicitQualitativeCheckResult(pomdp->getInitialStates()));
+                        if (storm::utility::resources::isTerminate()) {
+                            STORM_PRINT_AND_LOG("\nResult till abort: ")
+                        } else {
+                            STORM_PRINT_AND_LOG("\nResult: ")
+                        }
+                        printResult(result.getMin(), result.getMax());
+                        STORM_PRINT_AND_LOG(std::endl);
+                    } else {
+                        STORM_PRINT_AND_LOG("\nResult: Not available." << std::endl);
+                    }
                     analysisPerformed = true;
                 }
                 return analysisPerformed;