From a2f85ffcff5c472c037934dc3da9ab361e863b9a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Nov 2016 16:17:17 +0100 Subject: [PATCH] moved parts of refine functionality from model checker to refiner class --- src/storm/abstraction/MenuGameRefiner.cpp | 187 +++++++++++++++++ .../abstraction/GameBasedMdpModelChecker.cpp | 190 +----------------- 2 files changed, 189 insertions(+), 188 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index e31327157..af8f73e2c 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -2,6 +2,8 @@ #include "storm/abstraction/MenuGameAbstractor.h" +#include "storm/utility/dd.h" + namespace storm { namespace abstraction { @@ -15,6 +17,191 @@ namespace storm { abstractor.get().refine(predicates); } + template + storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates) { + + // Perform a BFS and pick the first pivot state we encounter. + storm::dd::Bdd pivotState; + storm::dd::Bdd frontier = initialStates; + storm::dd::Bdd frontierPivotStates = frontier && pivotStates; + + uint64_t level = 0; + bool foundPivotState = !frontierPivotStates.isZero(); + if (foundPivotState) { + pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + } else { + while (!foundPivotState) { + frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables); + frontierPivotStates = frontier && pivotStates; + + if (!frontierPivotStates.isZero()) { + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); + foundPivotState = true; + } + ++level; + } + } + + return pivotState; + } + + template + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) { + STORM_LOG_TRACE("Trying refinement after qualitative check."); + // Get all relevant strategies. + storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); + storm::dd::Bdd minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy(); + storm::dd::Bdd maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy(); + storm::dd::Bdd maxPlayer2Strategy = qualitativeResult.prob1Max.getPlayer2Strategy(); + + // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 + // state that is also a prob 0 state. + minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); + + // Build the fragment of transitions that is reachable by both the min and the max strategies. + storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy; + reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); + storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + + // Require the pivot state to be a [0, 1] state. + // TODO: is this restriction necessary or is it already implied? + // pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States(); + + // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and + // that the difference is not because of a missing strategy in either case. + + // Start with constructing the player 2 states that have a prob 0 (min) and prob 1 (max) strategy. + storm::dd::Bdd constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); + + // Now construct all player 2 choices that actually exist and differ in the min and max case. + constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); + + // Then restrict the pivot states by requiring existing and different player 2 choices. + pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + + // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either + // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob0 max define + // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state + // is found. In this case, we abort the qualitative refinement here. + if (pivotStates.isZero()) { + return false; + } + + STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to proceed without pivot state candidates."); + + // Now that we have the pivot state candidates, we need to pick one. + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); + + // Compute the lower and the upper choice for the pivot state. + std::set variablesToAbstract = game.getNondeterminismVariables(); + variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); + storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; + storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + + bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); + if (lowerChoicesDifferent) { + STORM_LOG_TRACE("Refining based on lower choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); + + abstractor.get().refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); + return true; + } else { + storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; + storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + + bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); + if (upperChoicesDifferent) { + STORM_LOG_TRACE("Refining based on upper choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); + abstractor.get().refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); + return true; + } else { + STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); + } + } + return false; + } + + template + bool MenuGameRefiner::refine(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 = 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. + + // Build the fragment of transitions that is reachable by both the min and the max strategies. + storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy; + reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); + 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 &= quantitativeResult.min.values.less(quantitativeResult.max.values); + + STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); + + // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and + // that the difference is not because of a missing strategy in either case. + + // Start with constructing the player 2 states that have a (min) and a (max) strategy. + // TODO: necessary? + storm::dd::Bdd constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); + + // Now construct all player 2 choices that actually exist and differ in the min and max case. + constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); + + // Then restrict the pivot states by requiring existing and different player 2 choices. + pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + + STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); + + // Now that we have the pivot state candidates, we need to pick one. + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); + + // Compute the lower and the upper choice for the pivot state. + std::set variablesToAbstract = game.getNondeterminismVariables(); + variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); + storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; + storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + + bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); + if (lowerChoicesDifferent) { + STORM_LOG_TRACE("Refining based on lower choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); + abstractor.get().refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); + } else { + storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; + storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + + bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); + if (upperChoicesDifferent) { + STORM_LOG_TRACE("Refining based on upper choice."); + auto refinementStart = std::chrono::high_resolution_clock::now(); + abstractor.get().refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); + } else { + STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); + } + } + } + + template class MenuGameRefiner; template class MenuGameRefiner; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 05a8d8105..88a067cac 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -19,7 +19,6 @@ #include "storm/solver/SymbolicGameSolver.h" #include "storm/utility/solver.h" -#include "storm/utility/dd.h" #include "storm/utility/prism.h" #include "storm/utility/macros.h" @@ -177,191 +176,6 @@ namespace storm { return result; } - template - storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates) { - - // Perform a BFS and pick the first pivot state we encounter. - storm::dd::Bdd pivotState; - storm::dd::Bdd frontier = initialStates; - storm::dd::Bdd frontierPivotStates = frontier && pivotStates; - - uint64_t level = 0; - bool foundPivotState = !frontierPivotStates.isZero(); - if (foundPivotState) { - pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - } else { - while (!foundPivotState) { - frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables); - frontierPivotStates = frontier && pivotStates; - - if (!frontierPivotStates.isZero()) { - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); - foundPivotState = true; - } - ++level; - } - } - - return pivotState; - } - - template - bool refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, QualitativeResultMinMax const& qualitativeResult, storm::dd::Bdd const& transitionMatrixBdd) { - STORM_LOG_TRACE("Trying refinement after qualitative check."); - // Get all relevant strategies. - storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); - storm::dd::Bdd minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy(); - storm::dd::Bdd maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy(); - storm::dd::Bdd maxPlayer2Strategy = qualitativeResult.prob1Max.getPlayer2Strategy(); - - // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 - // state that is also a prob 0 state. - minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); - - // Build the fragment of transitions that is reachable by both the min and the max strategies. - storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy; - reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); - storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); - - // Require the pivot state to be a [0, 1] state. - // TODO: is this restriction necessary or is it already implied? -// pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States(); - - // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and - // that the difference is not because of a missing strategy in either case. - - // Start with constructing the player 2 states that have a prob 0 (min) and prob 1 (max) strategy. - storm::dd::Bdd constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); - - // Now construct all player 2 choices that actually exist and differ in the min and max case. - constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); - - // Then restrict the pivot states by requiring existing and different player 2 choices. - pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); - - // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either - // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob0 max define - // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state - // is found. In this case, we abort the qualitative refinement here. - if (pivotStates.isZero()) { - return false; - } - - STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to proceed without pivot state candidates."); - - // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); - - // Compute the lower and the upper choice for the pivot state. - std::set variablesToAbstract = game.getNondeterminismVariables(); - variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); - storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; - storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); - if (lowerChoicesDifferent) { - STORM_LOG_TRACE("Refining based on lower choice."); - auto refinementStart = std::chrono::high_resolution_clock::now(); - - abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - return true; - } else { - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; - storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); - if (upperChoicesDifferent) { - STORM_LOG_TRACE("Refining based on upper choice."); - auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - return true; - } else { - STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); - } - } - return false; - } - - - template - 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 = 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. - - // Build the fragment of transitions that is reachable by both the min and the max strategies. - storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy; - reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); - 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 &= quantitativeResult.min.values.less(quantitativeResult.max.values); - - STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); - - // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and - // that the difference is not because of a missing strategy in either case. - - // Start with constructing the player 2 states that have a (min) and a (max) strategy. - // TODO: necessary? - storm::dd::Bdd constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); - - // Now construct all player 2 choices that actually exist and differ in the min and max case. - constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); - - // Then restrict the pivot states by requiring existing and different player 2 choices. - pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); - - STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); - - // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); - - // Compute the lower and the upper choice for the pivot state. - std::set variablesToAbstract = game.getNondeterminismVariables(); - variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); - storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; - storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); - if (lowerChoicesDifferent) { - STORM_LOG_TRACE("Refining based on lower choice."); - auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - } else { - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; - storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); - if (upperChoicesDifferent) { - STORM_LOG_TRACE("Refining based on upper choice."); - auto refinementStart = std::chrono::high_resolution_clock::now(); - abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - } else { - STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); - } - } - } - template QuantitativeResult solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, boost::optional> const& startInfo = boost::none) { @@ -516,7 +330,7 @@ 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. - qualitativeRefinement = refineAfterQualitativeCheck(abstractor, game, qualitativeResult, transitionMatrixBdd); + qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult); } } @@ -562,7 +376,7 @@ namespace storm { // (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, quantitativeResult); + refiner.refine(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.");