From 27cb582243d732d5d9e6a09573149494a6da2723 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 6 Oct 2020 21:39:22 +0200
Subject: [PATCH] MDP Instantiation model checker: Fixed setting model checking
 hint information.

---
 .../SparseMdpInstantiationModelChecker.cpp           | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
index 6bbbaa158..eac3df86a 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
@@ -69,6 +69,12 @@ namespace storm {
                 hint.setMaybeStates(std::move(maybeStates));
                 hint.setResultHint(std::move(qualitativeResult));
                 hint.setComputeOnlyMaybeStates(true);
+                
+                // Check if there can be end components within the maybestates
+                if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) ||
+                        storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
+                    hint.setNoEndComponentsInMaybeStates(true);
+                }
             }
             
             std::unique_ptr<CheckResult> result;
@@ -122,6 +128,12 @@ namespace storm {
                 hint.setMaybeStates(std::move(maybeStates));
                 hint.setResultHint(std::move(qualitativeResult));
                 hint.setComputeOnlyMaybeStates(true);
+                
+                // Check if there can be end components within the maybestates
+                if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) ||
+                        storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
+                    hint.setNoEndComponentsInMaybeStates(true);
+                }
             }
             
             std::unique_ptr<CheckResult> result;