more time measurements

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -142,17 +142,12 @@ namespace storm {
                 GameBddResult<DdType> game = modules.front().abstract();
                 
                 if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
+                    auto validBlockStart = std::chrono::high_resolution_clock::now();
                     storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
-                    
-                    // Cut away all invalid blocks for both source and targets.
-                    storm::dd::Bdd<DdType> 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<std::chrono::milliseconds>(validBlockEnd - validBlockStart).count() << "ms.");
                 }
                 
                 // Construct a set of all unnecessary variables, so we can abstract from it.

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -435,12 +435,17 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ModelType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(CheckTask<storm::logic::Formula> const& checkTask, QualitativeResultMinMax<Type>& qualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> 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<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(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<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States());
             }
             return result;
@@ -448,6 +453,7 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ModelType>
         storm::utility::graph::GameProb01Result<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
+            auto start = std::chrono::high_resolution_clock::now();
             storm::utility::graph::GameProb01Result<Type> 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<std::chrono::milliseconds>(end - start).count() << "ms.");
             
             return result;
         }

src/storm/utility/dd.cpp

@@ -11,13 +11,13 @@ namespace storm {
             
             template <storm::dd::DdType Type>
             storm::dd::Bdd<Type> computeReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) {
+                auto start = std::chrono::high_resolution_clock::now();
                 storm::dd::Bdd<Type> 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<Type> tmp = reachableStates.relationalProduct(transitions, rowMetaVariables, columnMetaVariables);
                     storm::dd::Bdd<Type> 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<std::chrono::milliseconds>(end - start).count() << "ms.");
                 
                 return reachableStates;
             }