From d35d72d5f398e95a80d21bc5c88efd9e7172c014 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 22 Aug 2016 15:57:08 +0200 Subject: [PATCH] slightly reformulated check for initial maybe states Former-commit-id: ac80e101bf1899878d67ef3a491534ef6be96b6a --- src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 9958e37df..250742025 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -199,7 +199,7 @@ namespace storm { storm::dd::Bdd maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); // 4. if the initial states are not maybe states, then we can refine at this point. - storm::dd::Bdd initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax); + storm::dd::Bdd initialMaybeStates = (game.getInitialStates() && maybeMin) || (game.getInitialStates() && maybeMax); if (initialMaybeStates.isZero()) { // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check."); @@ -221,7 +221,8 @@ namespace storm { refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); } else { - // Do not numerically solve the game if there is a qualitative bound around. + // If we can already answer the question, do not solve the game numerically. + STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)"); }