From 673c329311f17d9b7d87a404e01e05b403f9e986 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 30 Aug 2016 22:35:16 +0200 Subject: [PATCH] prepared upcoming fix for refinement based on quantitative information Former-commit-id: 35dee37951191362d6cb1fa6fc1b466230bb829c --- .../abstraction/GameBasedMdpModelChecker.cpp | 122 +++++++++--------- 1 file changed, 61 insertions(+), 61 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 98715706f..24fe9295b 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -212,7 +212,7 @@ namespace storm { storm::dd::Bdd maxPlayer2Strategy = prob01.max.second.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.. + // state that is also a prob 0 state. minPlayer1Strategy = (maxPlayer1Strategy && prob01.min.first.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); // Build the fragment of transitions that is reachable by both the min and the max strategies. @@ -220,11 +220,6 @@ namespace storm { reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); - (minPlayer1Strategy && pivotStates).template toAdd().exportToDot("piv_min_pl1.dot"); - (maxPlayer1Strategy && pivotStates).template toAdd().exportToDot("piv_max_pl1.dot"); - (minPlayer2Strategy && pivotStates).template toAdd().exportToDot("piv_min_pl2.dot"); - (maxPlayer2Strategy && pivotStates).template toAdd().exportToDot("piv_max_pl2.dot"); - // 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(); @@ -286,8 +281,16 @@ namespace storm { template void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, storm::dd::Add const& minResult, storm::dd::Add const& maxResult, detail::GameProb01Result const& prob01, std::pair, storm::dd::Bdd> const& minStrategyPair, std::pair, storm::dd::Bdd> const& maxStrategyPair, storm::dd::Bdd const& transitionMatrixBdd) { STORM_LOG_TRACE("Refining after quantitative check."); + // Get all relevant strategies. + storm::dd::Bdd minPlayer1Strategy = minStrategyPair.first; + storm::dd::Bdd minPlayer2Strategy = minStrategyPair.second; + storm::dd::Bdd maxPlayer1Strategy = maxStrategyPair.first; + storm::dd::Bdd maxPlayer2Strategy = maxStrategyPair.second; + + // 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 && minStrategyPair.first && minStrategyPair.second && maxStrategyPair.first && maxStrategyPair.second; + 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()); @@ -299,85 +302,82 @@ namespace storm { // 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. + // Start with constructing the player 2 states that have a (min) and a (max) strategy. + // TODO: necessary? storm::dd::Bdd constraint = minStrategyPair.second.existsAbstract(game.getPlayer2Variables()) && maxStrategyPair.second.existsAbstract(game.getPlayer2Variables()); - STORM_LOG_ASSERT(!(constraint && pivotStates).isZero(), "Unable to refine without pivot state candidates."); - - (minStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_min_pl1.dot"); - (maxStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_max_pl1.dot"); - (minStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_min_pl2.dot"); - (maxStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_max_pl2.dot"); +// (minStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_min_pl1.dot"); +// (maxStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_max_pl1.dot"); +// (minStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_min_pl2.dot"); +// (maxStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_max_pl2.dot"); // Now construct all player 2 choices that actually exist and differ in the min and max case. - constraint &= minStrategyPair.second.exclusiveOr(maxStrategyPair.second); - - STORM_LOG_ASSERT(!(constraint && pivotStates).isZero(), "Unable to refine without pivot state candidates."); + constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); // Then restrict the pivot states by requiring existing and different player 2 choices. - pivotStates &= ((minStrategyPair.first || maxStrategyPair.first) && constraint).existsAbstract(game.getNondeterminismVariables()); + 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); - storm::dd::Add pivotStateLower = pivotState.template toAdd() * minResult; - storm::dd::Add pivotStateUpper = pivotState.template toAdd() * maxResult; - storm::dd::Bdd pivotStateIsMinProb0 = pivotState && prob01.min.first.getPlayer1States(); - storm::dd::Bdd pivotStateIsMaxProb0 = pivotState && prob01.max.first.getPlayer1States(); - storm::dd::Bdd pivotStateLowerStrategies = pivotState && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy(); - storm::dd::Bdd pivotStateUpperStrategies = pivotState && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy(); - storm::dd::Bdd pivotStateLowerPl1Strategy = pivotState && prob01.min.first.getPlayer1Strategy(); - storm::dd::Bdd pivotStateUpperPl1Strategy = pivotState && prob01.max.first.getPlayer1Strategy(); - storm::dd::Bdd pivotStateLowerPl2Strategy = pivotState && prob01.min.first.getPlayer2Strategy(); - storm::dd::Bdd pivotStateUpperPl2Strategy = pivotState && prob01.max.first.getPlayer2Strategy(); - - minResult.exportToDot("minresult.dot"); - maxResult.exportToDot("maxresult.dot"); - pivotState.template toAdd().exportToDot("pivot.dot"); - pivotStateLower.exportToDot("pivot_lower.dot"); - pivotStateUpper.exportToDot("pivot_upper.dot"); - pivotStateIsMinProb0.template toAdd().exportToDot("pivot_is_minprob0.dot"); - pivotStateIsMaxProb0.template toAdd().exportToDot("pivot_is_maxprob0.dot"); - pivotStateLowerStrategies.template toAdd().exportToDot("pivot_lower_strats.dot"); - pivotStateUpperStrategies.template toAdd().exportToDot("pivot_upper_strats.dot"); - pivotStateLowerPl1Strategy.template toAdd().exportToDot("pivot_lower_pl1_strat.dot"); - pivotStateUpperPl1Strategy.template toAdd().exportToDot("pivot_upper_pl1_strat.dot"); - pivotStateLowerPl2Strategy.template toAdd().exportToDot("pivot_lower_pl2_strat.dot"); - pivotStateUpperPl2Strategy.template toAdd().exportToDot("pivot_upper_pl2_strat.dot"); +// storm::dd::Add pivotStateLower = pivotState.template toAdd() * minResult; +// storm::dd::Add pivotStateUpper = pivotState.template toAdd() * maxResult; +// storm::dd::Bdd pivotStateIsMinProb0 = pivotState && prob01.min.first.getPlayer1States(); +// storm::dd::Bdd pivotStateIsMaxProb0 = pivotState && prob01.max.first.getPlayer1States(); +// storm::dd::Bdd pivotStateLowerStrategies = pivotState && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy(); +// storm::dd::Bdd pivotStateUpperStrategies = pivotState && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy(); +// storm::dd::Bdd pivotStateLowerPl1Strategy = pivotState && prob01.min.first.getPlayer1Strategy(); +// storm::dd::Bdd pivotStateUpperPl1Strategy = pivotState && prob01.max.first.getPlayer1Strategy(); +// storm::dd::Bdd pivotStateLowerPl2Strategy = pivotState && prob01.min.first.getPlayer2Strategy(); +// storm::dd::Bdd pivotStateUpperPl2Strategy = pivotState && prob01.max.first.getPlayer2Strategy(); +// +// minResult.exportToDot("minresult.dot"); +// maxResult.exportToDot("maxresult.dot"); +// pivotState.template toAdd().exportToDot("pivot.dot"); +// pivotStateLower.exportToDot("pivot_lower.dot"); +// pivotStateUpper.exportToDot("pivot_upper.dot"); +// pivotStateIsMinProb0.template toAdd().exportToDot("pivot_is_minprob0.dot"); +// pivotStateIsMaxProb0.template toAdd().exportToDot("pivot_is_maxprob0.dot"); +// pivotStateLowerStrategies.template toAdd().exportToDot("pivot_lower_strats.dot"); +// pivotStateUpperStrategies.template toAdd().exportToDot("pivot_upper_strats.dot"); +// pivotStateLowerPl1Strategy.template toAdd().exportToDot("pivot_lower_pl1_strat.dot"); +// pivotStateUpperPl1Strategy.template toAdd().exportToDot("pivot_upper_pl1_strat.dot"); +// pivotStateLowerPl2Strategy.template toAdd().exportToDot("pivot_lower_pl2_strat.dot"); +// pivotStateUpperPl2Strategy.template toAdd().exportToDot("pivot_upper_pl2_strat.dot"); // 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() && minStrategyPair.first; - (pivotState && minStrategyPair.first).template toAdd().exportToDot("pl1_choice_in_pivot.dot"); - (pivotState && minStrategyPair.first && maxStrategyPair.second).template toAdd().exportToDot("pl1and2_choice_in_pivot.dot"); - (pivotState && maxStrategyPair.second).template toAdd().exportToDot("pl2_choice_in_pivot.dot"); - storm::dd::Bdd lowerChoice1 = (lowerChoice && minStrategyPair.second).existsAbstract(variablesToAbstract); - lowerChoice.template toAdd().exportToDot("lower.dot"); - maxStrategyPair.second.template toAdd().exportToDot("max_strat.dot"); - storm::dd::Bdd lowerChoice2 = (lowerChoice && maxStrategyPair.second); - lowerChoice2.template toAdd().exportToDot("tmp_lower.dot"); - lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract); - - lowerChoice.template toAdd().exportToDot("ref_lower.dot"); - lowerChoice1.template toAdd().exportToDot("ref_lower1.dot"); - lowerChoice2.template toAdd().exportToDot("ref_lower2.dot"); + storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; +// (pivotState && minStrategyPair.first).template toAdd().exportToDot("pl1_choice_in_pivot.dot"); +// (pivotState && minStrategyPair.first && maxStrategyPair.second).template toAdd().exportToDot("pl1and2_choice_in_pivot.dot"); +// (pivotState && maxStrategyPair.second).template toAdd().exportToDot("pl2_choice_in_pivot.dot"); + storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); +// lowerChoice.template toAdd().exportToDot("lower.dot"); +// maxStrategyPair.second.template toAdd().exportToDot("max_strat.dot"); + storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); +// lowerChoice2.template toAdd().exportToDot("tmp_lower.dot"); +// lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract); + +// lowerChoice.template toAdd().exportToDot("ref_lower.dot"); +// lowerChoice1.template toAdd().exportToDot("ref_lower1.dot"); +// lowerChoice2.template toAdd().exportToDot("ref_lower2.dot"); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Refining based on lower choice."); - abstractor.refine(pivotState, (pivotState && minStrategyPair.first).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); } else { - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxStrategyPair.first; - storm::dd::Bdd upperChoice1 = (upperChoice && minStrategyPair.second).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && maxStrategyPair.second).existsAbstract(variablesToAbstract); + 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."); - abstractor.refine(pivotState, (pivotState && maxStrategyPair.first).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); } else { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); }