From 2799412a4d6961cbbb3e0ea48d09f3d3346962a5 Mon Sep 17 00:00:00 2001 From: PBerger Date: Fri, 16 Sep 2016 23:40:43 +0200 Subject: [PATCH] Removed some commented out code and make things compile again. Former-commit-id: eb6b51f12885958367aaf331a49c67910926a78a --- .../abstraction/GameBasedMdpModelChecker.cpp | 42 ------------------- 1 file changed, 42 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index aa79cf5ef..61c5da10f 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -595,48 +595,6 @@ namespace storm { // If we arrived at this point, it means that we have all qualitative and quantitative information // about the game, but we could not yet answer the query. In this case, we need to refine. - // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 state that has the same prob. - // Get all relevant strategies. - /*storm::dd::Add matrix = game.getTransitionMatrix(); - - storm::dd::Add minResultTmp = minResult.swapVariables(game.getRowColumnMetaVariablePairs()); - storm::dd::Add minValuesForPlayer1UnderMinP1Strategy = (matrix * minMaybeStateResult.player1Strategy.template toAdd() * minMaybeStateResult.player2Strategy.template toAdd() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()).sumAbstract(game.getPlayer1Variables()); - storm::dd::Add minValuesForPlayer1UnderMaxP1P2Strategy = (matrix * maxMaybeStateResult.player1Strategy.template toAdd() * maxMaybeStateResult.player2Strategy.template toAdd() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()).sumAbstract(game.getPlayer1Variables()); - storm::dd::Add minValuesForPlayer1UnderMaxP1Strategy = (matrix * maxMaybeStateResult.player1Strategy.template toAdd() * minMaybeStateResult.player2Strategy.template toAdd() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()).sumAbstract(game.getPlayer1Variables()); - - minValuesForPlayer1UnderMinP1Strategy = prob01.min.first.getPlayer1States().ite(game.getManager().template getAddZero(), prob01.min.second.getPlayer1States().ite(game.getManager().template getAddOne(), minValuesForPlayer1UnderMinP1Strategy)); - minValuesForPlayer1UnderMaxP1Strategy = prob01.min.first.getPlayer1States().ite(game.getManager().template getAddZero(), prob01.min.second.getPlayer1States().ite(game.getManager().template getAddOne(), minValuesForPlayer1UnderMaxP1Strategy)); - - // This BDD has a 1 for every state (s) that can switch the strategy. - storm::dd::Bdd minIsGreaterOrEqual = minValuesForPlayer1UnderMinP1Strategy.greaterOrEqual(minValuesForPlayer1UnderMaxP1Strategy); - - minMaybeStateResult.player1Strategy = minIsGreaterOrEqual.ite(maxMaybeStateResult.player1Strategy, minMaybeStateResult.player1Strategy);*/ - - // Start by extending the quantitative strategies by the qualitative ones. - //minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy(); - - storm::dd::Bdd tmp = (prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables())); - STORM_LOG_ASSERT(tmp.isZero(), "wth?"); - tmp = prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy.existsAbstract(game.getPlayer2Variables()); - if (!tmp.isZero()) { - tmp = tmp && prob01.min.first.getPlayer2Strategy().exclusiveOr(minMaybeStateResult.player2Strategy).existsAbstract(game.getPlayer2Variables()); - (tmp && prob01.min.first.getPlayer2Strategy()).template toAdd().exportToDot("prob0_strat.dot"); - (tmp && minMaybeStateResult.player2Strategy).template toAdd().exportToDot("maybe_strat.dot"); - if (!tmp.isZero()) { - storm::dd::Add values = (tmp.template toAdd() * game.getTransitionMatrix() * minResult.swapVariables(game.getRowColumnMetaVariablePairs())).sumAbstract(game.getColumnVariables()); - tmp.template toAdd().exportToDot("illegal.dot"); - minResult.exportToDot("vals.dot"); - } - STORM_LOG_ASSERT(tmp.isZero(), "ddduuuudde?"); - } - STORM_LOG_ASSERT(tmp.isZero(), "wth2?"); - tmp = prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy; - - //(minMaybeStateResult.player2Strategy && (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy())).template toAdd().exportToDot("strat_overlap.dot"); - //minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy(); - //maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy(); - //maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); - // Make sure that all strategies are still valid strategies. STORM_LOG_ASSERT(minMaybeStateResult.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); STORM_LOG_ASSERT(maxMaybeStateResult.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");