From 3f6a8fed92924c5db97191932b10d0590fa26407 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 25 Mar 2018 21:58:19 +0200 Subject: [PATCH] fixed some issues in qualitative sparse solution of game-based abstraction --- .../abstraction/GameBasedMdpModelChecker.cpp | 17 ++++++---- src/storm/utility/graph.cpp | 34 +++++++++---------- src/storm/utility/graph.h | 8 ++--- 3 files changed, 31 insertions(+), 28 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 4b64daac9..9119c498f 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -534,15 +534,18 @@ namespace storm { std::vector player1RowGrouping = transitionMatrix.swapRowGroupIndices(std::move(tmpPlayer2RowGrouping)); auto const& player2RowGrouping = transitionMatrix.getRowGroupIndices(); - // Create the backward transitions for both players. + // Create the player 1 groups and backward transitions (for both players). + std::vector player1Groups(player1RowGrouping.size()); storm::storage::SparseMatrix player1BackwardTransitions = transitionMatrix.transpose(true); std::vector player2BackwardTransitions(transitionMatrix.getRowGroupCount()); + uint64_t player2State = 0; for (uint64_t player1State = 0; player1State < player2RowGrouping.size() - 1; ++player1State) { while (player1RowGrouping[player1State + 1] > player2RowGrouping[player2State]) { player2BackwardTransitions[player2State] = player1State; ++player2State; } + player1Groups[player1State + 1] = player2State; } storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); @@ -551,7 +554,7 @@ namespace storm { // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates); + ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates); // std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); // if (result) { // return result; @@ -627,7 +630,7 @@ namespace storm { } template - ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { + ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { ExplicitQualitativeGameResultMinMax result; @@ -676,10 +679,10 @@ namespace storm { // result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); // } // } else { - result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); - result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); - result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); - result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); // } STORM_LOG_TRACE("Qualitative precomputation completed."); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index d5d2b408b..423641dc2 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1084,7 +1084,7 @@ namespace storm { } template - ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount())); @@ -1134,7 +1134,7 @@ namespace storm { bool addPlayer1State = false; if (player1Strategy == OptimizationDirection::Minimize) { bool allPlayer2Successors = true; - for (uint64_t player2State = player1RowGrouping[player1Predecessor]; player2State < player1RowGrouping[player1Predecessor + 1]; ++player2State) { + for (uint64_t player2State = player1Groups[player1Predecessor]; player2State < player1Groups[player1Predecessor + 1]; ++player2State) { if (!result.player2States.get(player2State)) { allPlayer2Successors = false; break; @@ -1170,18 +1170,18 @@ namespace storm { // At least one player 2 successor is a state with probability 0, find it. bool foundProb0Successor = false; uint64_t player2State; - for (player2State = player1RowGrouping[player1State]; player2State < player1RowGrouping[player1State + 1]; ++player2State) { + for (player2State = player1Groups[player1State]; player2State < player1Groups[player1State + 1]; ++player2State) { if (result.player2States.get(player2State)) { - result.player1Strategy.get()[player1State] = player2State - player1RowGrouping[player1State]; + result.player1Strategy.get()[player1State] = player2State; foundProb0Successor = true; break; } } STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0."); - result.player1Strategy.get()[player1State] = player2State - player1RowGrouping[player1State]; + result.player1Strategy.get()[player1State] = player2State; } else { // Since all player 2 successors are states with probability 0, just pick any. - result.player1Strategy.get()[player1State] = 0; + result.player1Strategy.get()[player1State] = player1Groups[player1State]; } } } @@ -1211,10 +1211,10 @@ namespace storm { } STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0."); - result.player2Strategy.get()[player2State] = row - transitionMatrix.getRowGroupIndices()[player2State]; + result.player2Strategy.get()[player2State] = row; } else { // Since all player 1 successors are states with probability 0, just pick any. - result.player2Strategy.get()[player2State] = 0; + result.player2Strategy.get()[player2State] = transitionMatrix.getRowGroupIndices()[player2State]; } } } @@ -1290,8 +1290,8 @@ namespace storm { } template - ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional const& player1Candidates) { - + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional const& player1Candidates) { + // During the execution, the two state sets in the result hold the potential player 1/2 states. ExplicitGameProb01Result result; if (player1Candidates) { @@ -1335,8 +1335,8 @@ namespace storm { if (!player2Solution.get(player2PredecessorEntry.getColumn())) { bool addPlayer2State = player2Strategy == storm::OptimizationDirection::Minimize ? true : false; - uint64_t validChoice = 0; - for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { + uint64_t validChoice = transitionMatrix.getRowGroupIndices()[player2Predecessor]; + for (uint64_t row = validChoice; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { bool choiceHasSolutionSuccessor = false; bool choiceStaysInMaybeStates = true; for (auto const& entry : transitionMatrix.getRow(row)) { @@ -1351,7 +1351,7 @@ namespace storm { if (choiceHasSolutionSuccessor && choiceStaysInMaybeStates) { if (player2Strategy == storm::OptimizationDirection::Maximize) { - validChoice = row - transitionMatrix.getRowGroupIndices()[player2Predecessor]; + validChoice = row; addPlayer2State = true; break; } @@ -1374,11 +1374,11 @@ namespace storm { if (!player1Solution.get(player1Predecessor)) { bool addPlayer1State = player1Strategy == storm::OptimizationDirection::Minimize ? true : false; - validChoice = 0; - for (uint64_t player2Successor = player1RowGrouping[player1Predecessor]; player2Successor < player1RowGrouping[player1Predecessor + 1]; ++player2Successor) { + validChoice = player1Groups[player1Predecessor]; + for (uint64_t player2Successor = validChoice; player2Successor < player1Groups[player1Predecessor + 1]; ++player2Successor) { if (player2Solution.get(player2Successor)) { if (player1Strategy == storm::OptimizationDirection::Maximize) { - validChoice = player2Successor - player1RowGrouping[player1Predecessor]; + validChoice = player2Successor; addPlayer1State = true; break; } @@ -1395,7 +1395,7 @@ namespace storm { result.player1Strategy.get()[player1Predecessor] = validChoice; } - stack.emplace_back(); + stack.emplace_back(player1Predecessor); } } } diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 5e1fae518..2e37d0318 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -667,7 +667,7 @@ namespace storm { * Computes the set of states that have probability 0 given the strategies of the two players. * * @param transitionMatrix The transition matrix of the model as a BDD. - * @param player1RowGrouping The row grouping of player 1 states. + * @param player1Groups The grouping of player 1 states (in terms of player 2 states). * @param player1BackwardTransitions The backward transitions (player 1 to player 2). * @param player2BackwardTransitions The backward transitions (player 2 to player 1). * @param phiStates The phi states of the model. @@ -676,13 +676,13 @@ namespace storm { * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. */ template - ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); /*! * Computes the set of states that have probability 1 given the strategies of the two players. * * @param transitionMatrix The transition matrix of the model as a BDD. - * @param player1RowGrouping The row grouping of player 1 states. + * @param player1Groups The grouping of player 1 states (in terms of player 2 states). * @param player1BackwardTransitions The backward transitions (player 1 to player 2). * @param player2BackwardTransitions The backward transitions (player 2 to player 1). * @param phiStates The phi states of the model. @@ -692,7 +692,7 @@ namespace storm { * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered. */ template - ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional const& player1Candidates = boost::none); + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional const& player1Candidates = boost::none); /*! * Performs a topological sort of the states of the system according to the given transitions.