From 04d269d563ca3ebcf198bdae24be67f26b633577 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 24 Nov 2016 15:57:21 +0100 Subject: [PATCH] fixed bug introduced in refactoring --- src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index bca2c7e99..f33002332 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -483,7 +483,7 @@ namespace storm { storm::dd::Add initialStatesAdd = game.getInitialStates().template toAdd(); storm::dd::Bdd combinedMinPlayer1QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer1Strategy() || qualitativeResult.prob1Min.getPlayer1Strategy()); - storm::dd::Bdd combinedMinPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy()); + storm::dd::Bdd combinedMinPlayer2QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer2Strategy() || qualitativeResult.prob1Min.getPlayer2Strategy()); // The minimal value after qualitative checking can only be zero. It it was 1, we could have given // the result right away.