From 059f55eefc3b38b21caad71052d824d7fea43a8b Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 31 Aug 2016 22:44:10 +0200 Subject: [PATCH] commit to switch workplace, debugging in progress Former-commit-id: 9ab5d903e94e8048efb461a60e99d06f19b3f2b5 --- src/abstraction/AbstractionInformation.cpp | 2 +- .../abstraction/GameBasedMdpModelChecker.cpp | 38 ++++++++++++++++--- src/solver/SymbolicGameSolver.cpp | 10 ++++- src/utility/graph.cpp | 6 ++- 4 files changed, 47 insertions(+), 9 deletions(-) diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 395e23d0d..f2999f9cd 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -283,7 +283,7 @@ namespace storm { std::map> result; for (uint_fast64_t index = 0; index < predicates.size(); ++index) { - result[predicates[index]] = predicateBdds[index].first; + result[predicates[index]] = predicateBdds[index].first && !bottomStateBdds.first; } return result; diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 24fe9295b..98afc4325 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -335,7 +335,7 @@ namespace storm { // // minResult.exportToDot("minresult.dot"); // maxResult.exportToDot("maxresult.dot"); -// pivotState.template toAdd().exportToDot("pivot.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"); @@ -361,9 +361,9 @@ namespace storm { // 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"); + 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) { @@ -478,6 +478,9 @@ namespace storm { if (result) { return result; } + if (iterations == 18) { + exit(-1); + } prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States()); if (result) { @@ -529,8 +532,6 @@ namespace storm { minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); minResult += minMaybeStateResult.values; storm::dd::Add initialStateMin = initialStatesAdd * minResult; - initialStatesAdd.exportToDot("init.dot"); - initialStateMin.exportToDot("initmin.dot"); // 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() << "."); minValue = initialStateMin.getMax(); @@ -576,10 +577,35 @@ namespace storm { // Start by extending the quantitative strategies by the qualitative ones. minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy(); + + 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()); + if (!tmp.isZero()) { + tmp = tmp && prob01.min.first.getPlayer2Strategy().exclusiveOr(minMaybeStateResult.player2Strategy).existsAbstract(game.getPlayer2Variables()); + (tmp && prob01.min.first.getPlayer2Strategy()).template toAdd().exportToDot("prob0_strat.dot"); + (tmp && minMaybeStateResult.player2Strategy).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"); + minResult.exportToDot("vals.dot"); + } + STORM_LOG_ASSERT(tmp.isZero(), "ddduuuudde?"); + } + STORM_LOG_ASSERT(tmp.isZero(), "wth2?"); + tmp = prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy; + + (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."); + refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } } diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index d56fba6b6..f158ab665 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -53,12 +53,15 @@ namespace storm { } } + this->A.exportToDot("matrix.dot"); + do { // Compute tmp = A * x + b. storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); storm::dd::Add tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); tmp += b; - + tmp.exportToDot("tmp_pre_" + std::to_string(iterations) + ".dot"); + // Now abstract from player 2 and player 1 variables. if (player2Goal == storm::OptimizationDirection::Maximize) { storm::dd::Add newValues = tmp.maxAbstract(this->player2Variables); @@ -74,9 +77,11 @@ namespace storm { } else { tmp = (tmp + illegalPlayer2Mask); storm::dd::Add newValues = tmp.minAbstract(this->player2Variables); + newValues.exportToDot("vals_iter_" + std::to_string(iterations) + ".dot"); if (generatePlayer2Strategy) { player2Strategy = tmp.minAbstractRepresentative(this->player2Variables); + player2Strategy.get().template toAdd().exportToDot("pl2_strat_iter_" + std::to_string(iterations) + ".dot"); } tmp = newValues; @@ -103,6 +108,8 @@ namespace storm { tmp = newValues; } + tmp.exportToDot("pl1_vals_iter_" + std::to_string(iterations) + ".dot"); + // Now check if the process already converged within our precision. converged = xCopy.equalModuloPrecision(tmp, precision, relative); @@ -113,6 +120,7 @@ namespace storm { ++iterations; } while (!converged && iterations < maximalNumberOfIterations); + STORM_LOG_TRACE("Numerically solving the game took " << iterations << " iterations."); return xCopy; } diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index fa492a096..b16221e45 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -929,7 +929,7 @@ namespace storm { // The solution sets. storm::dd::Bdd player1States = psiStates; storm::dd::Bdd player2States = model.getManager().getBddZero(); - + bool done = false; uint_fast64_t iterations = 0; while (!done) { @@ -960,14 +960,18 @@ namespace storm { } // Since we have determined the complements of the desired sets, we need to complement it now. + player1States.template toAdd().exportToDot("not_pl1_prob0.dot"); + (!player1States).template toAdd().exportToDot("pl1_negated_prob0.dot"); player1States = !player1States && model.getReachableStates(); player2States = !player2States && model.getReachableStates(); // Determine all transitions between prob0 states. storm::dd::Bdd transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs())); + player1States.template toAdd().exportToDot("pl1_prob0.dot"); // Determine the distributions that have only successors that are prob0 states. storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); + onlyProb0Successors.template toAdd().exportToDot("only_prob0.dot"); boost::optional> player2StrategyBdd; if (producePlayer2Strategy) {