diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 62c1ea382..de5f8de9f 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -588,8 +588,9 @@ namespace storm { storm::dd::Add matrix = game.getTransitionMatrix(); - storm::dd::Add minValuesForPlayer1UnderMinP1Strategy = matrix * minPlayer1Strategy.template toAdd() * minPlayer2Strategy.template toAdd(); - storm::dd::Add minValuesForPlayer1UnderMaxP1Strategy = matrix * maxPlayer1Strategy.template toAdd() * minPlayer2Strategy.template toAdd(); + storm::dd::Add minResultTmp = minResult.swapVariables(game.getRowColumnMetaVariablePairs()); + storm::dd::Add minValuesForPlayer1UnderMinP1Strategy = (matrix * minPlayer1Strategy.template toAdd() * minPlayer2Strategy.template toAdd() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()); + storm::dd::Add minValuesForPlayer1UnderMaxP1Strategy = (matrix * maxPlayer1Strategy.template toAdd() * minPlayer2Strategy.template toAdd() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()); // This BDD has a 1 for every state (s) that can switch the strategy. storm::dd::Bdd minIsGreaterOrEqual = minValuesForPlayer1UnderMinP1Strategy.greaterOrEqual(minValuesForPlayer1UnderMaxP1Strategy);