diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index da11864b4..a262d2ffe 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -1059,65 +1059,136 @@ namespace storm { return true; } + template + struct ExplicitDijkstraQueueElement { + ExplicitDijkstraQueueElement(ValueType const& distance, uint64_t state, bool lower) : distance(distance), state(state), lower(lower) { + // Intentionally left empty. + } + + ValueType distance; + uint64_t state; + bool lower; + }; + + template + struct ExplicitDijkstraQueueElementLess { + bool operator()(ExplicitDijkstraQueueElement const& a, ExplicitDijkstraQueueElement const& b) const { + if (a.distance < b.distance) { + return true; + } else if (a.distance > b.distance) { + return false; + } else { + if (a.state < b.state) { + return true; + } else if (a.state > b.state) { + return false; + } else { + if (a.lower < b.lower) { + return true; + } else { + return false; + } + } + } + } + }; + + template + void performDijkstraStep(std::set, ExplicitDijkstraQueueElementLess>& dijkstraQueue, bool probabilityDistances, std::vector& distances, std::vector>& predecessors, bool generatePredecessors, bool lower, uint64_t currentState, ValueType const& currentDistance, bool isPivotState, ExplicitGameStrategyPair const& strategyPair, ExplicitGameStrategyPair const& otherStrategyPair, std::vector const& player1Labeling, std::vector const& player2Grouping, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& relevantStates) { + if (strategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { + uint64_t player2Successor = strategyPair.getPlayer1Strategy().getChoice(currentState); + uint64_t player2Choice = strategyPair.getPlayer2Strategy().getChoice(player2Successor); + STORM_LOG_ASSERT(isPivotState || !otherStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) || strategyPair.getPlayer2Strategy().getChoice(player2Successor) == player2Choice, "Did not expect deviation in player 2 strategy."); + STORM_LOG_ASSERT(player2Grouping[player2Successor] <= player2Choice && player2Choice < player2Grouping[player2Successor + 1], "Illegal choice for player 2."); + + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + uint64_t player1Successor = entry.getColumn(); + if (!relevantStates.get(player1Successor)) { + continue; + } + + ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); + if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) { + distances[player1Successor] = alternateDistance; + if (generatePredecessors) { + predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[player2Successor]); + } + dijkstraQueue.emplace(alternateDistance, player1Successor, lower); + } + } + } else { + STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting min strategy for non-target states."); + } + } + template boost::optional> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector const* lowerValues = nullptr, std::vector const* upperValues = nullptr) { STORM_LOG_ASSERT(!lowerValues || upperValues, "Expected none or both value results."); STORM_LOG_ASSERT(!upperValues || lowerValues, "Expected none or both value results."); - // Perform Dijkstra search that stays within the relevant states and searches for a state in which the - // strategies for the (commonly chosen) player 1 action leads to a player 2 state in which the choices differ. - ExplicitPivotStateResult result; + // Perform Dijkstra search that stays within the relevant states and searches for a (pivot) state in which + // the strategies the lower or upper player 1 action leads to a player 2 state in which the choices differ. + // To guarantee that the pivot state is reachable by either of the strategies, we do a parallel Dijkstra + // search in both the lower and upper strategy. bool probabilityDistances = pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MostProbablePath; uint64_t numberOfStates = initialStates.size(); ValueType inftyDistance = probabilityDistances ? storm::utility::zero() : storm::utility::infinity(); ValueType zeroDistance = probabilityDistances ? storm::utility::one() : storm::utility::zero(); - std::vector distances(numberOfStates, inftyDistance); + + // Create storages for the lower and upper Dijkstra search. + std::vector lowerDistances(numberOfStates, inftyDistance); + std::vector> lowerPredecessors; + std::vector upperDistances(numberOfStates, inftyDistance); + std::vector> upperPredecessors; + if (generatePredecessors) { - result.predecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult::NO_PREDECESSOR, ExplicitPivotStateResult::NO_PREDECESSOR)); + lowerPredecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult::NO_PREDECESSOR, ExplicitPivotStateResult::NO_PREDECESSOR)); + upperPredecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult::NO_PREDECESSOR, ExplicitPivotStateResult::NO_PREDECESSOR)); } - // Use set as priority queue with unique membership; default comparison on pair works fine if distance is - // the first entry. - std::set, std::greater>> dijkstraQueue; + // Use set as priority queue with unique membership. + std::set, ExplicitDijkstraQueueElementLess> dijkstraQueue; for (auto initialState : initialStates) { if (!relevantStates.get(initialState)) { continue; } - distances[initialState] = zeroDistance; - dijkstraQueue.emplace(zeroDistance, initialState); + lowerDistances[initialState] = zeroDistance; + upperDistances[initialState] = zeroDistance; + dijkstraQueue.emplace(zeroDistance, initialState, true); + dijkstraQueue.emplace(zeroDistance, initialState, false); } // For some heuristics, we need to potentially find more than just one pivot. bool considerDeviation = (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation || pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) && lowerValues && upperValues; bool foundPivotState = false; + + ExplicitDijkstraQueueElement pivotState(inftyDistance, 0, true); ValueType pivotStateDeviation = storm::utility::zero(); auto const& player2Grouping = transitionMatrix.getRowGroupIndices(); - storm::storage::BitVector visitedStates(initialStates.size()); while (!dijkstraQueue.empty()) { - auto distanceStatePair = *dijkstraQueue.begin(); - uint64_t currentState = distanceStatePair.second; - visitedStates.set(currentState); - std::cout << "current: " << currentState << std::endl; - std::cout << "visited: " << visitedStates << std::endl; - - ValueType currentDistance = distanceStatePair.first; + // Take out currently best state. + auto currentDijkstraElement = *dijkstraQueue.begin(); + ValueType currentDistance = currentDijkstraElement.distance; + uint64_t currentState = currentDijkstraElement.state; + bool currentLower = currentDijkstraElement.lower; dijkstraQueue.erase(dijkstraQueue.begin()); - if (foundPivotState && (probabilityDistances ? currentDistance < result.distance : currentDistance > result.distance)) { + if (foundPivotState && (probabilityDistances ? currentDistance < pivotState.distance : currentDistance > pivotState.distance)) { if (pivotSelectionHeuristic != storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) { // For the nearest maximal deviation and most probable path heuristics, future pivot states are // not important any more, because their distance will be strictly larger, so we can return the // current pivot state. - return result; + + return ExplicitPivotStateResult(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors)); } else if (pivotStateDeviation >= currentDistance) { // If the heuristic is maximal weighted deviation and the weighted deviation for any future pivot // state is necessarily at most as high as the current one, we can abort the search. - return result; + return ExplicitPivotStateResult(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors)); } } @@ -1128,19 +1199,21 @@ namespace storm { if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) { isPivotState = true; } - } else if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { + } + if (!isPivotState && maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) { isPivotState = true; } } - // If it is indeed a pivot state, we can abort the search here. + // If it is indeed a pivot state, we can potentially abort the search here. if (isPivotState) { if (considerDeviation && foundPivotState) { ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState]; + if (deviationOfCurrentState > pivotStateDeviation) { - result.pivotState = currentState; + pivotState = currentDijkstraElement; pivotStateDeviation = deviationOfCurrentState; if (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) { // Scale the deviation with the distance (probability) for this heuristic. @@ -1148,71 +1221,25 @@ namespace storm { } } } else if (!foundPivotState) { - result.pivotState = currentState; - result.distance = distances[currentState]; + pivotState = currentDijkstraElement; foundPivotState = true; } // If there is no need to look at other deviations, stop here. if (!considerDeviation) { - return result; + return ExplicitPivotStateResult(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors)); } } - // TODO: remember the strategy from which we came and only go on to explore that further? - - // Otherwise, we explore all its relevant successors. - if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { - uint64_t minPlayer2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState); - uint64_t minPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor); - STORM_LOG_ASSERT(!maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(minPlayer2Successor) || minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor) == minPlayer2Choice, "Did not expect deviation in player 2 strategy."); - STORM_LOG_ASSERT(player2Grouping[minPlayer2Successor] <= minPlayer2Choice && minPlayer2Choice < player2Grouping[minPlayer2Successor + 1], "Illegal choice for player 2."); - - for (auto const& entry : transitionMatrix.getRow(minPlayer2Choice)) { - uint64_t player1Successor = entry.getColumn(); - if (!relevantStates.get(player1Successor)) { - continue; - } - - ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); - if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) { - distances[player1Successor] = alternateDistance; - if (generatePredecessors) { - result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[minPlayer2Successor]); - } - dijkstraQueue.emplace(alternateDistance, player1Successor); - } - } - } else { - STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting min strategy for non-target states."); - } - if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { - uint64_t maxPlayer2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); - uint64_t maxPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor); - STORM_LOG_ASSERT(!minStrategyPair.getPlayer2Strategy().hasDefinedChoice(maxPlayer2Successor) || minStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor) == maxPlayer2Choice, "Did not expect deviation in player 2 strategy."); - STORM_LOG_ASSERT(player2Grouping[maxPlayer2Successor] <= maxPlayer2Choice && maxPlayer2Choice < player2Grouping[maxPlayer2Successor + 1], "Illegal choice for player 2."); - - for (auto const& entry : transitionMatrix.getRow(maxPlayer2Choice)) { - uint64_t player1Successor = entry.getColumn(); - if (!relevantStates.get(player1Successor)) { - continue; - } - - ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); - if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) { - distances[player1Successor] = alternateDistance; - if (generatePredecessors) { - result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[maxPlayer2Successor]); - } - dijkstraQueue.emplace(alternateDistance, player1Successor); - } - } + if (currentLower) { + performDijkstraStep(dijkstraQueue, probabilityDistances, lowerDistances, lowerPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, minStrategyPair, maxStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates); } else { - STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting max strategy for non-target states."); + performDijkstraStep(dijkstraQueue, probabilityDistances, upperDistances, upperPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, maxStrategyPair, minStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates); } } if (foundPivotState) { + ExplicitPivotStateResult result; return result; } diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 276d178fb..60d632694 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -76,6 +76,9 @@ namespace storm { template struct ExplicitPivotStateResult { ExplicitPivotStateResult() = default; + ExplicitPivotStateResult(uint64_t pivotState, ValueType distance, std::vector>&& predecessors) : pivotState(pivotState), distance(distance), predecessors(std::move(predecessors)) { + // Intentionally left empty. + } uint64_t pivotState; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index f7374dd20..ca01fca3b 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -59,7 +59,7 @@ namespace storm { using detail::PreviousExplicitResult; template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision() * 2, storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision() * 2, storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()), debug(storm::settings::getModule().isDebugSet()) { STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants. Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants."); @@ -529,6 +529,8 @@ namespace storm { // Optimization: do not compute both bounds if not necessary (e.g. if bound given and exceeded, etc.) + totalWatch.start(); + // Set up initial predicates. std::vector initialPredicates = getInitialPredicates(constraintExpression, targetStateExpression); @@ -563,10 +565,11 @@ namespace storm { STORM_LOG_TRACE("Starting iteration " << iteration << "."); // (1) build the abstraction. - auto abstractionStart = std::chrono::high_resolution_clock::now(); + storm::utility::Stopwatch abstractionWatch(true); storm::abstraction::MenuGame game = abstractor->abstract(); - auto abstractionEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); + abstractionWatch.stop(); + totalAbstractionWatch.add(abstractionWatch); + STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << abstractionWatch.getTimeInMilliseconds() << "ms)."); // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); @@ -592,7 +595,8 @@ namespace storm { } if (result) { - printStatistics(*abstractor, game); + totalWatch.stop(); + printStatistics(*abstractor, game, iteration); return result; } @@ -600,6 +604,8 @@ namespace storm { STORM_LOG_INFO("Iteration " << iteration << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); } + totalWatch.stop(); + // If this point is reached, we have given up on abstraction. STORM_LOG_WARN("Could not derive result, maximal number of abstractions exceeded."); return nullptr; @@ -614,15 +620,16 @@ namespace storm { storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); // (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(); + storm::utility::Stopwatch qualitativeWatch(true); SymbolicQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { return result; } previousQualitativeResult = qualitativeResult; - auto qualitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); + qualitativeWatch.stop(); + totalSolutionWatch.add(qualitativeWatch); + STORM_LOG_INFO("Qualitative computation completed in " << qualitativeWatch.getTimeInMilliseconds() << "ms."); // (2) compute the states for which we have to determine quantitative information. storm::dd::Bdd maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates(); @@ -639,10 +646,11 @@ namespace storm { // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. - auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); + storm::utility::Stopwatch refinementWatch(true); qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult); - auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); + refinementWatch.stop(); + totalRefinementWatch.add(refinementWatch); + STORM_LOG_INFO("Qualitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms."); } // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. @@ -652,27 +660,31 @@ namespace storm { storm::dd::Add initialStatesAdd = initialStates.template toAdd(); - auto quantitativeStart = std::chrono::high_resolution_clock::now(); - SymbolicQuantitativeGameResultMinMax quantitativeResult; // (7) Solve the min values and check whether we can give the answer already. + storm::utility::Stopwatch quantitativeWatch(true); quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); + quantitativeWatch.stop(); previousMinQuantitativeResult = quantitativeResult.min; result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); if (result) { + totalSolutionWatch.add(quantitativeWatch); return result; } // (8) Solve the max values and check whether we can give the answer already. + quantitativeWatch.start(); quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); + quantitativeWatch.stop(); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); if (result) { + totalSolutionWatch.add(quantitativeWatch); return result; } - auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + totalSolutionWatch.add(quantitativeWatch); + STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); @@ -686,25 +698,118 @@ namespace storm { STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); - auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); - // (10) If we arrived at this point, it means that we have all qualitative and quantitative // information about the game, but we could not yet answer the query. In this case, we need to refine. + storm::utility::Stopwatch refinementWatch(true); refiner.refine(game, transitionMatrixBdd, quantitativeResult); - auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); + refinementWatch.stop(); + totalRefinementWatch.add(refinementWatch); + STORM_LOG_INFO("Quantitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms."); } // Return null to indicate no result has been found yet. return nullptr; } + template + void postProcessStrategies(abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, bool sanityCheck) { + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << "."); + STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << "."); + + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); + + STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ")."); + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + + if (lowerPlayer2Choice != upperPlayer2Choice) { + ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + + if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { + minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); + if (sanityCheck) { + STORM_LOG_TRACE("[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice); + } + } + } + } + } + + if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); + + STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); + uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + + if (lowerPlayer2Choice != upperPlayer2Choice) { + ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + + if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { + minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice); + STORM_LOG_TRACE("[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice); + } + } + } + } + } + + if (sanityCheck) { + ///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should + ///////// still be the lower ones. + storm::storage::SparseMatrixBuilder dtmcMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1); + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + if (targetStates.get(state)) { + dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one()); + } else { + uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minStrategyPair.getPlayer1Strategy().getChoice(state)); + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); + } + } + } + auto dtmcMatrix = dtmcMatrixBuilder.build(); + std::vector sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); + + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]) < 1e-4, "Got weird min divergences!"); + } + ///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should + ///////// still be the upper ones. + dtmcMatrixBuilder = storm::storage::SparseMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1); + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + if (targetStates.get(state)) { + dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one()); + } else { + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)); + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); + } + } + } + dtmcMatrix = dtmcMatrixBuilder.build(); + sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); + + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]) < 1e-4, "Got weird max divergences!"); + } + } + } + template std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult) { STORM_LOG_TRACE("Using sparse solving."); // (0) Start by transforming the necessary symbolic elements to explicit ones. - auto translationStart = std::chrono::high_resolution_clock::now(); + storm::utility::Stopwatch translationWatch(true); storm::dd::Odd odd = game.getReachableStates().createOdd(); std::vector> labelingVariableSets = {game.getPlayer1Variables(), game.getPlayer2Variables()}; @@ -756,22 +861,25 @@ namespace storm { storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd); storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd); - auto translationEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Translation to explicit representation completed in " << std::chrono::duration_cast(translationEnd - translationStart).count() << "ms."); + translationWatch.stop(); + totalTranslationWatch.add(translationWatch); + STORM_LOG_INFO("Translation to explicit representation completed in " << translationWatch.getTimeInMilliseconds() << "ms."); // Prepare the two strategies. abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); abstraction::ExplicitGameStrategyPair maxStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); // (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(); + storm::utility::Stopwatch qualitativeWatch(true); ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousResult, odd, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair); + qualitativeWatch.stop(); + totalSolutionWatch.add(qualitativeWatch); + STORM_LOG_INFO("Qualitative computation completed in " << qualitativeWatch.getTimeInMilliseconds() << "ms."); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { return result; } - auto qualitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); // (2) compute the states for which we have to determine quantitative information. storm::storage::BitVector maybeMin = ~(qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates()); @@ -788,10 +896,11 @@ namespace storm { // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. - auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); + storm::utility::Stopwatch refinementWatch(true); qualitativeRefinement = refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); - auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); + refinementWatch.stop(); + totalRefinementWatch.add(refinementWatch); + STORM_LOG_INFO("Qualitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms."); } ExplicitQuantitativeResultMinMax quantitativeResult; @@ -802,132 +911,45 @@ namespace storm { STORM_LOG_TRACE("Starting numerical solution step."); // (7) Solve the min values and check whether we can give the answer already. - auto quantitativeStart = std::chrono::high_resolution_clock::now(); + storm::utility::Stopwatch quantitativeWatch(true); quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair, odd, nullptr, nullptr, this->reuseQuantitativeResults ? previousResult : boost::none)); + quantitativeWatch.stop(); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates)); if (result) { + totalSolutionWatch.add(quantitativeWatch); return result; } // (8) Solve the max values and check whether we can give the answer already. + quantitativeWatch.start(); quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair)); + quantitativeWatch.stop(); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates)); if (result) { + totalSolutionWatch.add(quantitativeWatch); return result; } - auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms."); // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. result = checkForResultAfterQuantitativeCheck(quantitativeResult.getMin().getRange(initialStates).first, quantitativeResult.getMax().getRange(initialStates).second, comparator); if (result) { return result; } - -// std::cout << "target states " << targetStates << std::endl; - - for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - std::cout << "state " << state << " has values [" << quantitativeResult.getMin().getValues()[state] << ", " << quantitativeResult.getMax().getValues()[state] << "]" << std::endl; - - STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << "."); - STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << "."); - - if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { - uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); - - STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ")."); - uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); - - if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { - uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); - - if (lowerPlayer2Choice != upperPlayer2Choice) { - ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); - ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); - - if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { - minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); - std::cout << "[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice << std::endl; - } - } - } - } - - if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { - uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); - - STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); - uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); - - if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { - uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); - - if (lowerPlayer2Choice != upperPlayer2Choice) { - ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); - ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); - - if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { - minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice); - std::cout << "[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice << std::endl; - } - } - } - } - } - - ///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should - ///////// still be the lower ones. - storm::storage::SparseMatrixBuilder dtmcMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1); - for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - if (targetStates.get(state)) { - dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one()); - } else { - uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minStrategyPair.getPlayer1Strategy().getChoice(state)); - for (auto const& entry : transitionMatrix.getRow(player2Choice)) { - dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); - } - } - } - auto dtmcMatrix = dtmcMatrixBuilder.build(); - std::vector sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); - - for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - std::cout << "state " << state << ": " << sanityValues[state] << " vs " << quantitativeResult.getMin().getValues()[state] << std::endl; - std::cout << "[min] state is prob0? " << qualitativeResult.getProb0Min().getStates().get(state) << ", prob1? " << qualitativeResult.getProb1Min().getStates().get(state) << std::endl; - STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]) < 1e-6, "Got weird min divergences!"); - } - ///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should - ///////// still be the upper ones. - dtmcMatrixBuilder = storm::storage::SparseMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1); - for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - if (targetStates.get(state)) { - dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one()); - } else { - uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)); - for (auto const& entry : transitionMatrix.getRow(player2Choice)) { - dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); - } - } - } - dtmcMatrix = dtmcMatrixBuilder.build(); - sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); - for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - std::cout << "state " << state << ": " << sanityValues[state] << " vs " << quantitativeResult.getMax().getValues()[state] << std::endl; - std::cout << "[max] state is prob0? " << qualitativeResult.getProb0Max().getStates().get(state) << ", prob1? " << qualitativeResult.getProb1Max().getStates().get(state) << std::endl; - STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]) < 1e-6, "Got weird max divergences!"); - } + postProcessStrategies(minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->debug); // Make sure that all strategies are still valid strategies. STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << "."); STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << maxStrategyPair.getNumberOfUndefinedPlayer1States() << "."); - auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); // (10) If we arrived at this point, it means that we have all qualitative and quantitative // information about the game, but we could not yet answer the query. In this case, we need to refine. + storm::utility::Stopwatch refinementWatch(true); refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair); - auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); + refinementWatch.stop(); + totalRefinementWatch.add(refinementWatch); + STORM_LOG_INFO("Quantitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms."); if (this->reuseQuantitativeResults) { PreviousExplicitResult nextPreviousResult; @@ -1106,15 +1128,37 @@ namespace storm { } template - void GameBasedMdpModelChecker::printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const { + void GameBasedMdpModelChecker::printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements) const { if (storm::settings::getModule().isShowStatisticsSet()) { storm::abstraction::AbstractionInformation const& abstractionInformation = abstractor.getAbstractionInformation(); + std::streamsize originalPrecision = std::cout.precision(); + std::cout << std::fixed << std::setprecision(2); + std::cout << std::endl; std::cout << "Statistics:" << std::endl; - std::cout << " * player 1 states (final game): " << game.getReachableStates().getNonZeroCount() << std::endl; + std::cout << " * size of final game: " << game.getReachableStates().getNonZeroCount() << " player 1 states" << std::endl; std::cout << " * transitions (final game): " << game.getTransitionMatrix().getNonZeroCount() << std::endl; - std::cout << " * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl; + std::cout << " * refinements: " << refinements << std::endl; + std::cout << " * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl << std::endl; + + uint64_t totalAbstractionTimeMillis = totalAbstractionWatch.getTimeInMilliseconds(); + uint64_t totalTranslationTimeMillis = totalTranslationWatch.getTimeInMilliseconds(); + uint64_t totalSolutionTimeMillis = totalSolutionWatch.getTimeInMilliseconds(); + uint64_t totalRefinementTimeMillis = totalRefinementWatch.getTimeInMilliseconds(); + uint64_t totalTimeMillis = totalWatch.getTimeInMilliseconds(); + + std::cout << "Time breakdown:" << std::endl; + std::cout << " * abstraction: " << totalAbstractionTimeMillis << "ms (" << 100 * static_cast(totalAbstractionTimeMillis)/totalTimeMillis << "%)" << std::endl; + if (this->solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Sparse) { + std::cout << " * translation: " << totalTranslationTimeMillis << "ms (" << 100 * static_cast(totalTranslationTimeMillis)/totalTimeMillis << "%)" << std::endl; + } + std::cout << " * solution: " << totalSolutionTimeMillis << "ms (" << 100 * static_cast(totalSolutionTimeMillis)/totalTimeMillis << "%)" << std::endl; + std::cout << " * refinement: " << totalRefinementTimeMillis << "ms (" << 100 * static_cast(totalRefinementTimeMillis)/totalTimeMillis << "%)" << std::endl; + std::cout << " ---------------------------------------------" << std::endl; + std::cout << " * total: " << totalTimeMillis << "ms" << std::endl << std::endl; + + std::cout << std::defaultfloat << std::setprecision(originalPrecision); } } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index e93e91c69..cf6d059aa 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -21,6 +21,7 @@ #include "storm/utility/ConstantsComparator.h" #include "storm/utility/solver.h" #include "storm/utility/graph.h" +#include "storm/utility/Stopwatch.h" namespace storm { namespace abstraction { @@ -114,7 +115,7 @@ namespace storm { ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousResult, storm::dd::Odd const& odd, 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, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair); - void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const; + void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game, uint64_t refinements) const; /* * Retrieves the expression characterized by the formula. The formula needs to be propositional. @@ -148,6 +149,16 @@ namespace storm { /// The performed number of refinement iterations. uint64_t iteration; + + /// A flag that indicates whether debug mode is enabled. + bool debug; + + /// Data stored for statistics. + storm::utility::Stopwatch totalAbstractionWatch; + storm::utility::Stopwatch totalSolutionWatch; + storm::utility::Stopwatch totalRefinementWatch; + storm::utility::Stopwatch totalTranslationWatch; + storm::utility::Stopwatch totalWatch; }; } } diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp index 0a08a4e19..8c6f008a4 100644 --- a/src/storm/utility/Stopwatch.cpp +++ b/src/storm/utility/Stopwatch.cpp @@ -3,7 +3,7 @@ namespace storm { namespace utility { - Stopwatch::Stopwatch(bool startNow) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) { + Stopwatch::Stopwatch(bool startNow) : accumulatedTime(std::chrono::nanoseconds::zero()), isStopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) { if (startNow) { start(); } @@ -25,21 +25,30 @@ namespace storm { accumulatedTime += timeNanoseconds; } + void Stopwatch::add(Stopwatch const& other) { + STORM_LOG_WARN_COND(other.stopped(), "Expected stopped watch."); + accumulatedTime += other.accumulatedTime; + } + void Stopwatch::stop() { - STORM_LOG_WARN_COND(!stopped, "Stopwatch is already paused."); - stopped = true; + STORM_LOG_WARN_COND(!isStopped, "Stopwatch is already paused."); + isStopped = true; accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement; } void Stopwatch::start() { - STORM_LOG_WARN_COND(stopped, "Stopwatch is already running."); - stopped = false; + STORM_LOG_WARN_COND(isStopped, "Stopwatch is already running."); + isStopped = false; startOfCurrentMeasurement = std::chrono::high_resolution_clock::now(); } void Stopwatch::reset() { accumulatedTime = std::chrono::nanoseconds::zero(); - stopped = true; + isStopped = true; + } + + bool Stopwatch::stopped() const { + return isStopped; } std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) { diff --git a/src/storm/utility/Stopwatch.h b/src/storm/utility/Stopwatch.h index 4f81ea8a8..e3b41f4e9 100644 --- a/src/storm/utility/Stopwatch.h +++ b/src/storm/utility/Stopwatch.h @@ -46,6 +46,11 @@ namespace storm { */ void addToTime(std::chrono::nanoseconds timeNanoseconds); + /*! + * Adds the value of the (stopped) watch to the accumulated time of this watch. + */ + void add(Stopwatch const& other); + /*! * Stop stopwatch and add measured time to total time. */ @@ -60,6 +65,11 @@ namespace storm { * Reset the stopwatch. */ void reset(); + + /*! + * Retrieves whether the watch is stopped. + */ + bool stopped() const; friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch); @@ -68,7 +78,7 @@ namespace storm { std::chrono::nanoseconds accumulatedTime; // A flag indicating if the stopwatch is stopped right now. - bool stopped; + bool isStopped; // The timepoint when the stopwatch was started the last time (if it's not stopped). std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;