From fe0e5c37935d43fb3dc79461b343d274d4a40329 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Nov 2016 15:33:29 +0100 Subject: [PATCH] more refactoring --- .../abstraction/GameBasedMdpModelChecker.cpp | 37 ++++++++++--------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index b03f72340..05a8d8105 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -35,6 +35,7 @@ namespace storm { namespace modelchecker { using storm::abstraction::QuantitativeResult; + using storm::abstraction::QuantitativeResultMinMax; template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory) { @@ -291,13 +292,13 @@ namespace storm { template - void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResult const& minResult, QuantitativeResult const& maxResult) { + void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) { STORM_LOG_TRACE("Refining after quantitative check."); // Get all relevant strategies. - storm::dd::Bdd minPlayer1Strategy = minResult.player1Strategy; - storm::dd::Bdd minPlayer2Strategy = minResult.player2Strategy; - storm::dd::Bdd maxPlayer1Strategy = maxResult.player1Strategy; - storm::dd::Bdd maxPlayer2Strategy = maxResult.player2Strategy; + storm::dd::Bdd minPlayer1Strategy = quantitativeResult.min.player1Strategy; + storm::dd::Bdd minPlayer2Strategy = quantitativeResult.min.player2Strategy; + storm::dd::Bdd maxPlayer1Strategy = quantitativeResult.max.player1Strategy; + storm::dd::Bdd maxPlayer2Strategy = quantitativeResult.max.player2Strategy; // TODO: fix min strategies to take the max strategies if possible. @@ -307,7 +308,7 @@ namespace storm { storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); // Require the pivot state to be a state with a lower bound strictly smaller than the upper bound. - pivotStates &= minResult.values.less(maxResult.values); + pivotStates &= quantitativeResult.min.values.less(quantitativeResult.max.values); STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); @@ -528,38 +529,40 @@ namespace storm { STORM_LOG_TRACE("Starting numerical solution step."); auto quantitativeStart = std::chrono::high_resolution_clock::now(); + QuantitativeResultMinMax quantitativeResult; + // (7) Solve the min values and check whether we can give the answer already. - QuantitativeResult minResult = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin); - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, minResult.initialStateValue); + quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue); if (result) { return result; } // (8) Solve the max values and check whether we can give the answer already. - QuantitativeResult maxResult = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(minResult)); - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, maxResult.initialStateValue); + quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStateValue); if (result) { return result; } auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Obtained quantitative bounds [" << minResult.initialStateValue << ", " << maxResult.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStateValue << ", " << quantitativeResult.max.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. - result = checkForResultAfterQuantitativeCheck(checkTask, minResult.initialStateValue, maxResult.initialStateValue); + result = checkForResultAfterQuantitativeCheck(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue); if (result) { return result; } // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(minResult.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); - STORM_LOG_ASSERT(maxResult.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); - STORM_LOG_ASSERT(minResult.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); - STORM_LOG_ASSERT(maxResult.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); + STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); // (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. - refineAfterQuantitativeCheck(abstractor, game, transitionMatrixBdd, minResult, maxResult); + refineAfterQuantitativeCheck(abstractor, game, transitionMatrixBdd, quantitativeResult); } auto iterationEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms.");