From ed56a77d7952fec45fc207b1dd1beed252cea3a6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 29 May 2018 16:43:22 +0200 Subject: [PATCH] started on fixing strategies --- .../modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 35613d9fd..46dde3b65 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -925,6 +925,9 @@ namespace storm { ExplicitQualitativeGameResultMinMax result; + ExplicitQualitativeGameResult problematicStates = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); + std::cout << "Found " << problematicStates.getStates().getNumberOfSetBits() << " problematic states" << std::endl; + result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair); result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair); result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair);