From fefdc7b2168325f2838d7bec100aa32baf43c410 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 Dec 2016 21:38:18 +0100 Subject: [PATCH] more time measurements --- .../abstraction/prism/PrismMenuGameAbstractor.cpp | 15 +++++---------- .../abstraction/GameBasedMdpModelChecker.cpp | 11 +++++++++-- src/storm/utility/dd.cpp | 5 ++++- 3 files changed, 18 insertions(+), 13 deletions(-) diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 0ed031fe3..6bfa3a30b 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -142,17 +142,12 @@ namespace storm { GameBddResult game = modules.front().abstract(); if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { + auto validBlockStart = std::chrono::high_resolution_clock::now(); storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); - - // Cut away all invalid blocks for both source and targets. - storm::dd::Bdd newGameBdd = game.bdd; - newGameBdd &= validBlocks; - newGameBdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); - - if (newGameBdd != game.bdd) { - STORM_LOG_TRACE("Global invalid block detection reduced the number of transitions from " << game.bdd.getNonZeroCount() << " to " << newGameBdd.getNonZeroCount() << "."); - game.bdd = newGameBdd; - } + // Cut away all invalid successor blocks. + game.bdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); + auto validBlockEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Global invalid block detection completed in " << std::chrono::duration_cast(validBlockEnd - validBlockStart).count() << "ms."); } // Construct a set of all unnecessary variables, so we can abstract from it. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 2d80f80eb..1a9cbc1e7 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -435,12 +435,17 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + // TODO: use MDP functions when the directions of the players agree? + qualitativeResult.prob0Min = computeProb01States(true, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates); qualitativeResult.prob1Min = computeProb01States(false, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); if (!result) { qualitativeResult.prob0Max = computeProb01States(true, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates); - qualitativeResult.prob1Max = computeProb01States(false, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates); + + // As all states that have a probability 1 when player 2 minimizes will also have probability 1 when + // player 2 maximizes, we can take this set as the target states for thiw operation. + qualitativeResult.prob1Max = computeProb01States(false, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, qualitativeResult.prob1Min.player1States); result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); } return result; @@ -448,6 +453,7 @@ namespace storm { template storm::utility::graph::GameProb01Result GameBasedMdpModelChecker::computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + auto start = std::chrono::high_resolution_clock::now(); storm::utility::graph::GameProb01Result result; if (prob0) { result = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); @@ -462,7 +468,8 @@ namespace storm { } STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); - STORM_LOG_TRACE("Computed states with probability " << (prob0 ? "0" : "1") << " (player 1: " << player1Direction << ", player 2: " << player2Direction << "): " << result.getPlayer1States().getNonZeroCount() << " '" << (prob0 ? "no" : "yes") << "' states."); + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Computed states with probability " << (prob0 ? "0" : "1") << " (player 1: " << player1Direction << ", player 2: " << player2Direction << "): " << result.getPlayer1States().getNonZeroCount() << " '" << (prob0 ? "no" : "yes") << "' states (completed in " << std::chrono::duration_cast(end - start).count() << "ms."); return result; } diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 517f4ef81..db490b8c5 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -11,13 +11,13 @@ namespace storm { template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables) { + auto start = std::chrono::high_resolution_clock::now(); storm::dd::Bdd reachableStates = initialStates; // Perform the BFS to discover all reachable states. bool changed = true; uint_fast64_t iteration = 0; do { - STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); changed = false; storm::dd::Bdd tmp = reachableStates.relationalProduct(transitions, rowMetaVariables, columnMetaVariables); storm::dd::Bdd newReachableStates = tmp && (!reachableStates); @@ -31,6 +31,9 @@ namespace storm { ++iteration; } while (changed); + + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Reachability computation completed in " << iteration << " iterations (" << std::chrono::duration_cast(end - start).count() << "ms."); return reachableStates; }