From f9d23873f1925fd88e55bd9c3fb0ee0a1016815a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 20 May 2018 20:52:51 +0200
Subject: [PATCH] fixed minor bug in game-based abstraction

---
 .../modelchecker/abstraction/GameBasedMdpModelChecker.cpp     | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 2b545a54b..eadaccead 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -641,10 +641,6 @@ namespace storm {
                 qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult);
                 auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
                 STORM_LOG_INFO("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
-            } else if (initialMaybeStates == initialStates && checkTask.isQualitativeSet()) {
-                // If all initial states are 'maybe' states and the property we needed to check is a qualitative one,
-                // we can return the result here.
-                return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), ValueType(0.5));
             }
             
             // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.