From 13ab3bad7ddcdbfeaeaecf04f494e41e3bfd27bb Mon Sep 17 00:00:00 2001 From: PBerger Date: Sun, 11 Sep 2016 14:22:15 +0200 Subject: [PATCH] Tried fixing the quantitative solveMaybeStates step. Former-commit-id: eac561f29241d575474b74b0a430c3123d2d989a --- .../abstraction/GameBasedMdpModelChecker.cpp | 63 ++++++++++++------- 1 file changed, 39 insertions(+), 24 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 71a9a4df6..62c1ea382 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -406,25 +406,27 @@ namespace storm { // Compute the ingredients of the equation system. storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); - storm::dd::Add submatrix = maybeStatesAdd * game.getTransitionMatrix(); + storm::dd::Bdd allStates = game.getReachableStates(); + storm::dd::Add allStatesAdd = allStates.template toAdd(); + storm::dd::Add submatrix = allStatesAdd * game.getTransitionMatrix(); storm::dd::Add prob1StatesAsColumn = prob1States.template toAdd().swapVariables(game.getRowColumnMetaVariablePairs()); storm::dd::Add subvector = submatrix * prob1StatesAsColumn; subvector = subvector.sumAbstract(game.getColumnVariables()); // Cut away all columns targeting non-maybe states. - submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); + submatrix *= allStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); // Cut the starting vector to the maybe states of this query. storm::dd::Add startVector; if (startInfo) { - startVector = startInfo.get().values * maybeStatesAdd; + startVector = startInfo.get().values * allStatesAdd; } else { startVector = game.getManager().template getAddZero(); } // Create the solver and solve the equation system. storm::utility::solver::SymbolicGameSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); + std::unique_ptr> solver = solverFactory.create(submatrix, allStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); solver->setGeneratePlayersStrategies(true); auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none); return MaybeStateResult(values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); @@ -532,7 +534,7 @@ namespace storm { MaybeStateResult minMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); if (!maybeMin.isZero()) { minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); - minResult += minMaybeStateResult.values; + minResult = minMaybeStateResult.values; storm::dd::Add initialStateMin = initialStatesAdd * minResult; // Here we can only require a non-zero count of *at most* one, because the result may actually be 0. STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << "."); @@ -552,7 +554,7 @@ namespace storm { MaybeStateResult maxMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); if (!maybeMax.isZero()) { maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult)); - maxResult += maxMaybeStateResult.values; + maxResult = maxMaybeStateResult.values; storm::dd::Add initialStateMax = (initialStatesAdd * maxResult); // Unlike in the min-case, we can require a non-zero count of 1 here, because if the max was in // fact 0, the result would be 0, which would have been detected earlier by the graph algorithms. @@ -577,16 +579,29 @@ namespace storm { // 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. - // Start by extending the quantitative strategies by the qualitative ones. - minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy(); + // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 state that has the same prob. + // Get all relevant strategies. + storm::dd::Bdd minPlayer1Strategy = minMaybeStateResult.player1Strategy; + storm::dd::Bdd minPlayer2Strategy = minMaybeStateResult.player2Strategy; + storm::dd::Bdd maxPlayer1Strategy = maxMaybeStateResult.player1Strategy; + storm::dd::Bdd maxPlayer2Strategy = maxMaybeStateResult.player2Strategy; + + storm::dd::Add matrix = game.getTransitionMatrix(); + + storm::dd::Add minValuesForPlayer1UnderMinP1Strategy = matrix * minPlayer1Strategy.template toAdd() * minPlayer2Strategy.template toAdd(); + storm::dd::Add minValuesForPlayer1UnderMaxP1Strategy = matrix * maxPlayer1Strategy.template toAdd() * minPlayer2Strategy.template toAdd(); + // This BDD has a 1 for every state (s) that can switch the strategy. + storm::dd::Bdd minIsGreaterOrEqual = minValuesForPlayer1UnderMinP1Strategy.greaterOrEqual(minValuesForPlayer1UnderMaxP1Strategy); + + minPlayer1Strategy = minIsGreaterOrEqual.existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); storm::dd::Bdd tmp = (prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables())); STORM_LOG_ASSERT(tmp.isZero(), "wth?"); - tmp = prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy.existsAbstract(game.getPlayer2Variables()); + tmp = prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); if (!tmp.isZero()) { - tmp = tmp && prob01.min.first.getPlayer2Strategy().exclusiveOr(minMaybeStateResult.player2Strategy).existsAbstract(game.getPlayer2Variables()); + tmp = tmp && prob01.min.first.getPlayer2Strategy().exclusiveOr(minPlayer2Strategy).existsAbstract(game.getPlayer2Variables()); (tmp && prob01.min.first.getPlayer2Strategy()).template toAdd().exportToDot("prob0_strat.dot"); - (tmp && minMaybeStateResult.player2Strategy).template toAdd().exportToDot("maybe_strat.dot"); + (tmp && minPlayer2Strategy).template toAdd().exportToDot("maybe_strat.dot"); if (!tmp.isZero()) { storm::dd::Add values = (tmp.template toAdd() * game.getTransitionMatrix() * minResult.swapVariables(game.getRowColumnMetaVariablePairs())).sumAbstract(game.getColumnVariables()); tmp.template toAdd().exportToDot("illegal.dot"); @@ -595,20 +610,20 @@ namespace storm { STORM_LOG_ASSERT(tmp.isZero(), "ddduuuudde?"); } STORM_LOG_ASSERT(tmp.isZero(), "wth2?"); - tmp = prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy; + //tmp = prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minPlayer2Strategy; - (minMaybeStateResult.player2Strategy && (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy())).template toAdd().exportToDot("strat_overlap.dot"); - minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy(); - maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy(); - maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); + //(minMaybeStateResult.player2Strategy && (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy())).template toAdd().exportToDot("strat_overlap.dot"); + //minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy(); + //maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy(); + //maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(minMaybeStateResult.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); - STORM_LOG_ASSERT(maxMaybeStateResult.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); - STORM_LOG_ASSERT(minMaybeStateResult.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); - STORM_LOG_ASSERT(maxMaybeStateResult.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + STORM_LOG_ASSERT(minPlayer1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); + STORM_LOG_ASSERT(maxPlayer1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); + STORM_LOG_ASSERT(minPlayer2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); + STORM_LOG_ASSERT(maxPlayer2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); - refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); + refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minPlayer1Strategy, minPlayer2Strategy), std::make_pair(maxPlayer1Strategy, maxPlayer2Strategy), transitionMatrixBdd); } } @@ -633,7 +648,7 @@ namespace storm { return std::make_pair(prob0, prob1); } - + template storm::expressions::Expression GameBasedMdpModelChecker::getExpression(storm::logic::Formula const& formula) { STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); @@ -647,11 +662,11 @@ namespace storm { } return result; } - + template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; } -} \ No newline at end of file +}