From 8ea869ef14c1d0c964a33078b7cb82a3ac51218c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 6 Apr 2016 21:56:25 +0200
Subject: [PATCH] changed detection of terminal states a bit

Former-commit-id: a9229fa174420bb20cf0b50fed73850fc003cb0b
---
 .../SparseMdpLearningModelChecker.cpp             | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
index d2f1c47bf..76765d367 100644
--- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
@@ -216,17 +216,16 @@ namespace storm {
                 STORM_LOG_TRACE("State has " << behavior.getNumberOfChoices() << " choices.");
                 
                 // Clumsily check whether we have found a state that forms a trivial BMEC.
-                if (behavior.getNumberOfChoices() == 0) {
-                    isTerminalState = true;
-                } else if (behavior.getNumberOfChoices() == 1) {
-                    auto const& onlyChoice = *behavior.begin();
-                    if (onlyChoice.size() == 1) {
-                        auto const& onlyEntry = *onlyChoice.begin();
-                        if (onlyEntry.first == currentStateId) {
-                            isTerminalState = true;
+                bool otherSuccessor = false;
+                for (auto const& choice : behavior) {
+                    for (auto const& entry : choice) {
+                        if (entry.first != currentStateId) {
+                            otherSuccessor = true;
+                            break;
                         }
                     }
                 }
+                isTerminalState = !otherSuccessor;
                 
                 // If the state was neither a trivial (non-accepting) terminal state nor a target state, we
                 // need to store its behavior.