From d16e47882deea27ab16f5a07affe5cef8110d009 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 29 Aug 2016 16:33:46 +0200 Subject: [PATCH] fixed bug and added tons of debug output Former-commit-id: 5bf2d6d82fc04d19c07438d398e80817844e93b8 --- src/abstraction/prism/AbstractCommand.cpp | 3 +- src/abstraction/prism/AbstractProgram.cpp | 23 +++++++- .../abstraction/GameBasedMdpModelChecker.cpp | 57 +++++++++++++++++-- 3 files changed, 75 insertions(+), 8 deletions(-) diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index 0f1dc3932..70438d216 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -69,8 +69,7 @@ namespace storm { this->recomputeCachedBdd(); } - // Refine bottom state abstractor. - // FIXME: Should this only be done if the other BDD needs recomputation? + // Refine bottom state abstractor. Note that this does not trigger a recomputation yet. bottomStateAbstractor.refine(predicates); } diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 7e4f7ee21..ee4a46c03 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -122,12 +122,18 @@ namespace storm { for (auto const& successorValuePair : lowerChoiceAsAdd) { uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size()); + std::cout << "update idx: " << updateIndex << std::endl; storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates()); for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) { auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index]; + std::cout << successorVariable.getName() << " has value"; if (successorValuePair.first.getBooleanValue(successorVariable)) { successor.set(index); + std::cout << " true"; + } else { + std::cout << " false"; } + std::cout << std::endl; } result[updateIndex] = successor; @@ -162,11 +168,25 @@ namespace storm { } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); + lowerChoice.template toAdd().exportToDot("lowerchoice_ref.dot"); + upperChoice.template toAdd().exportToDot("upperchoice_ref.dot"); + // Decode both choices to explicit mappings. + std::cout << "lower" << std::endl; std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); + std::cout << "upper" << std::endl; std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); - STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode."); + STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); + std::cout << "lower" << std::endl; + for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) { + std::cout << entry.first << " -> " << entry.second << std::endl; + } + std::cout << "upper" << std::endl; + for (auto const& entry : upperChoiceUpdateToSuccessorMapping) { + std::cout << entry.first << " -> " << entry.second << std::endl; + } + // Now go through the mappings and find points of deviation. Currently, we take the first deviation. storm::expressions::Expression newPredicate; auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin(); @@ -186,6 +206,7 @@ namespace storm { } } } + STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); STORM_LOG_TRACE("Derived new predicate: " << newPredicate); diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 15cb2049d..2a7b407f2 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -61,13 +61,15 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); - return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula())); + std::map labelToExpressionMapping = preprocessedProgram.getLabelToExpressionMapping(); + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping)); } template std::unique_ptr GameBasedMdpModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); - return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula())); + std::map labelToExpressionMapping = preprocessedProgram.getLabelToExpressionMapping(); + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), originalProgram.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping)); } template @@ -195,6 +197,7 @@ namespace storm { template void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { + STORM_LOG_TRACE("Refining after qualitative check."); // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies. storm::dd::Bdd reachableTransitions = prob01.min.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); reachableTransitions = (prob01.min.first.getPlayer1Strategy() && reachableTransitions) || (prob01.max.second.getPlayer1Strategy() && reachableTransitions); @@ -236,7 +239,8 @@ 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) { + 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."); // 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); @@ -251,12 +255,48 @@ namespace storm { // 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.states; + storm::dd::Bdd pivotStateIsMaxProb0 = pivotState && prob01.max.first.states; + 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); - storm::dd::Bdd lowerChoice2 = (lowerChoice && maxStrategyPair.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"); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { @@ -377,6 +417,13 @@ namespace storm { return result; } + // 2.5 At this point, we need to fix the max strategy for the prob 0 states for player 2. This is because + // there may be player 2 nodes for which there is no choice in the currently computed strategy (by prob0) + // as no choice achieves probability 0. However, later we require the strategies to only differ if necessary + // so we need to force the player 2 strategy to agree with the player 2 strategy for the probability 0 + // states in the min case. + prob01.max.first.player2Strategy = prob01.max.first.getPlayer2Strategy().existsAbstract(game.getPlayer1Variables()).ite(prob01.max.first.getPlayer2Strategy(), prob01.min.first.getPlayer2Strategy()); + // 3. compute the states for which we know the result/for which we know there is more work to be done. storm::dd::Bdd maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates(); storm::dd::Bdd maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); @@ -465,7 +512,7 @@ namespace storm { 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); + refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } }