From a663a37e21f407a508a92b54aea056cf6e21c9ab Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 27 Aug 2016 15:48:29 +0200 Subject: [PATCH] fixed a bug that prevented correct strategy generation in iterative solver Former-commit-id: 1df15b439dbc4579519699487178261f13cb5220 --- src/abstraction/prism/AbstractProgram.cpp | 20 ++--- .../abstraction/GameBasedMdpModelChecker.cpp | 89 ++++++++++++++----- src/solver/SymbolicGameSolver.cpp | 2 +- 3 files changed, 75 insertions(+), 36 deletions(-) diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index ec146d67e..7e4f7ee21 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -249,12 +249,14 @@ namespace storm { // Construct the transition matrix by cutting away the transitions of unreachable states. storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; - // If there are bottom states, we need to mark all other states as non-bottom now. + // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions. + transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); + reachableStates &= abstractionInformation.getBottomStateBdd(true, true); + initialStates &= abstractionInformation.getBottomStateBdd(true, true); + + // If there are bottom transitions, exnted the transition matrix and reachable states now. if (hasBottomStates) { - transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); transitionMatrix += bottomStateResult.transitions.template toAdd(); - reachableStates &= abstractionInformation.getBottomStateBdd(true, true); - initialStates &= abstractionInformation.getBottomStateBdd(true, true); reachableStates |= bottomStateResult.states; } @@ -264,15 +266,11 @@ namespace storm { allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); std::set allSourceVariables(abstractionInformation.getSourceVariables()); - if (hasBottomStates) { - allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); - } + allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); - if (hasBottomStates) { - allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); - } + allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, hasBottomStates ? abstractionInformation.getExtendedSourceSuccessorVariablePairs() : abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a71f7ec9c..15cb2049d 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -234,6 +234,48 @@ namespace storm { } } } + + template + void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, std::pair, storm::dd::Bdd> const& minStrategyPair, std::pair, storm::dd::Bdd> const& maxStrategyPair, storm::dd::Bdd const& transitionMatrixBdd) { + // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies. + storm::dd::Bdd reachableTransitions = minStrategyPair.second || maxStrategyPair.second; + reachableTransitions = (minStrategyPair.first && reachableTransitions) || (maxStrategyPair.first && reachableTransitions); + reachableTransitions &= transitionMatrixBdd; + reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); + storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + + // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different. + pivotStates &= ((minStrategyPair.first || maxStrategyPair.first) && (minStrategyPair.second.exclusiveOr(maxStrategyPair.second))).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() && minStrategyPair.first; + storm::dd::Bdd lowerChoice1 = (lowerChoice && minStrategyPair.second).existsAbstract(variablesToAbstract); + storm::dd::Bdd lowerChoice2 = (lowerChoice && maxStrategyPair.second).existsAbstract(variablesToAbstract); + + 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); + } 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); + + 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); + } else { + STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); + } + } + } template struct MaybeStateResult { @@ -275,17 +317,8 @@ namespace storm { 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()); solver->setGeneratePlayersStrategies(true); - auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector); - storm::dd::Bdd player1Strategy = solver->getPlayer1Strategy(); - storm::dd::Bdd player2Strategy = solver->getPlayer2Strategy(); - - // If we were given a starting point, we fix the strategies now. That is, we only deviate from the - if (startInfo) { - player1Strategy = values.greater(startInfo.get().values).ite(player1Strategy, startInfo.get().player1Strategy); - player1Strategy = values.greater(startInfo.get().values).ite(player1Strategy, startInfo.get().player1Strategy); - } - - return MaybeStateResult(values, player1Strategy, player2Strategy); + 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()); } template @@ -380,13 +413,13 @@ namespace storm { storm::dd::Add initialStatesAdd = game.getInitialStates().template toAdd(); ValueType minValue = (prob01.min.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one() : storm::utility::zero(); - MaybeStateResult minMaybeStateResult; + 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.states); 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."); + STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << "."); minValue = initialStateMin.getMax(); } STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << "."); @@ -398,15 +431,14 @@ namespace storm { } ValueType maxValue = (prob01.max.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one() : storm::utility::zero(); - MaybeStateResult maxMaybeStateResult; + MaybeStateResult maxMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); if (!maybeMax.isZero()) { - // FIXME: fix strategy: only change if improved. - maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional>(minMaybeStateResult)); + maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::make_optional(minMaybeStateResult)); 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. - STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states."); + STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states. Expected 1, but got " << initialStateMax.getNonZeroCount() << "."); maxValue = initialStateMax.getMax(); } STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << "."); @@ -427,7 +459,13 @@ 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. - STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)"); + // Start by extending the quantitative strategies by the qualitative ones. + minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy(); + 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(); + + refineAfterQuantitativeCheck(abstractor, game, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } } @@ -438,15 +476,18 @@ namespace storm { template std::pair, storm::utility::graph::GameProb01Result> GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { // Compute the states with probability 0/1. - storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Minimize, player2Direction == storm::OptimizationDirection::Minimize); - storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Maximize, player2Direction == storm::OptimizationDirection::Maximize); +// storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Minimize, player2Direction == storm::OptimizationDirection::Minimize); +// storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Maximize, player2Direction == storm::OptimizationDirection::Maximize); + storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); + storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer1Strategy() && !prob0.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer2Strategy() && !prob0.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer1Strategy() && !prob1.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer2Strategy() && !prob1.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer1Strategy() && (prob0.states.isZero() || !prob0.getPlayer1Strategy().isZero())), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer2Strategy() && (prob0.states.isZero() || !prob0.getPlayer2Strategy().isZero())), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer1Strategy() && (prob1.states.isZero() || !prob1.getPlayer1Strategy().isZero())), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer2Strategy() && (prob1.states.isZero() || !prob1.getPlayer2Strategy().isZero())), "Unable to proceed without strategy."); STORM_LOG_TRACE("Player 1: " << player1Direction << ", player 2: " << player2Direction << ": " << prob0.states.getNonZeroCount() << " 'no' states, " << prob1.states.getNonZeroCount() << " 'yes' states."); + return std::make_pair(prob0, prob1); } diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 962cd540a..d56fba6b6 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -46,7 +46,7 @@ namespace storm { // If we are required to generate a player 2 strategy based on another one that is not the zero strategy, // we need to determine the values, because only then we can update the strategy only if necessary. - previousPlayer2Values = ((this->A * player2Strategy.get().template toAdd()).multiplyMatrix(x.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b).sumAbstract(this->player2Variables); + previousPlayer2Values = (player2Strategy.get().template toAdd() * (this->A.multiplyMatrix(x.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b)).sumAbstract(this->player2Variables); } else { player2Strategy = A.getDdManager().getBddZero(); previousPlayer2Values = A.getDdManager().template getAddZero();