From b550e6167761ed2d5b92672b5524e7bd683153c8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 18 Aug 2016 14:27:45 +0200
Subject: [PATCH] started working on refinement based on qualitative check

Former-commit-id: 3569a55851b5cf3a5fb1e4387a5be3e9792de74b
---
 .../abstraction/GameBasedMdpModelChecker.cpp             | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

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<storm::dd::DdType Type, typename ValueType>
         void refineAfterQualitativeCheck(storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
-            // First, we have to find the pivot states.
-            storm::dd::Bdd<Type> 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<Type> 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<storm::dd::DdType Type, typename ValueType>