diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index af0c46121..9d1229b34 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -391,7 +391,7 @@ namespace storm { } template - ExplicitQuantitativeResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& minStrategyPair) { + ExplicitQuantitativeResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& strategyPair) { bool player1Min = player1Direction == storm::OptimizationDirection::Minimize; bool player2Min = player2Direction == storm::OptimizationDirection::Minimize; @@ -400,18 +400,44 @@ namespace storm { auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States(); auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States(); - // Determine which rows to keep. - storm::storage::BitVector player2MaybeStates(transitionMatrix.getRowCount()); - for (uint64_t player2State = 0; player2State < transitionMatrix.getRowGroupCount(); ++player2State) { - if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) { - player2MaybeStates.set(player2State); + // Determine which row groups to keep. + storm::storage::BitVector player2MaybeStates = ~(player2Prob0States | player2Prob1States); + + // Create the sub-game. + std::cout << "maybe: " << maybeStates << std::endl; + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, player1Prob1States); + std::vector subPlayer1Groups(maybeStates.getNumberOfSetBits() + 1); + uint64_t position = 0; + uint64_t previousPlayer2States = 0; + for (auto state : maybeStates) { + subPlayer1Groups[position] = previousPlayer2States; + + bool hasMaybePlayer2Successor = false; + for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { + if (player2MaybeStates.get(player2State)) { + hasMaybePlayer2Successor = true; + ++previousPlayer2States; + } } + STORM_LOG_ASSERT(hasMaybePlayer2Successor, "Player 1 maybe state has no player2 maybe successor."); + ++position; } + subPlayer1Groups.back() = previousPlayer2States; + + // Solve the sub-game. + auto gameSolver = storm::solver::GameSolverFactory().create(env, subPlayer1Groups, submatrix); + std::vector lowerValues(maybeStates.getNumberOfSetBits()); + gameSolver->solveGame(env, player1Direction, player2Direction, lowerValues, b); + + // Create combined result for all states. + ExplicitQuantitativeResult result(maybeStates.size()); + storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one()); + storm::utility::vector::setVectorValues(result.getValues(), maybeStates, lowerValues); + + // Obtain strategies from solver and fuse them with the pre-existing strategy pair for the qualitative result. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates); - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, maybeStates); - auto gameSolver = storm::solver::GameSolverFactory().create(env, player1Groups, transitionMatrix); exit(-1); } diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 4d4cfd03c..3d9e4975d 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -234,7 +234,7 @@ namespace storm { std::vector* newX = auxiliaryP1RowGroupVector.get(); std::vector* currentX = &x; - + // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations. uint64_t iterations = 0;