From 2d51ef2c0cb2af8039775f8456651ffb66bb7840 Mon Sep 17 00:00:00 2001 From: PBerger Date: Sun, 11 Sep 2016 21:25:52 +0200 Subject: [PATCH] Fixed a la Christian. Former-commit-id: 59d1d7b40fd44c4ea00586f1124b4b0845091a38 --- 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 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);