diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index fba7cf500..98e4737b2 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -94,11 +94,14 @@ namespace storm { template void refineAfterQualitativeCheck(storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { - // First, we have to find the pivot states. - storm::dd::Bdd playerPStates = transitionMatrixBdd.existsAbstract(game.getColumnVariables()); + // First, we have to find the pivot state candidates. Start by constructing the reachable fragment of the + // state space *under both* strategy pairs. + storm::dd::Bdd pivotStateCandidates = transitionMatrixBdd.existsAbstract(game.getColumnVariables()); + pivotStateCandidates &= prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy(); + pivotStateCandidates = pivotStateCandidates.existsAbstract(game.getNondeterminismVariables()); -// playerPStates &= prob01.min.first. + std::cout << "found pivot state candidates" << std::endl; } template