From 0cd03845e8365401b68ee99a6b2e1bd769b8964d Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 22 Aug 2016 15:28:19 +0200 Subject: [PATCH] abstraction loop working for purely qualitative refinement Former-commit-id: ce28ed97c2ec42aa4b0b455951c4fe623254dfd9 --- src/abstraction/AbstractionInformation.cpp | 6 + src/abstraction/AbstractionInformation.h | 12 +- src/abstraction/prism/AbstractProgram.cpp | 78 ++++++++-- src/abstraction/prism/AbstractProgram.h | 8 + src/exceptions/InvalidModelException.h | 13 ++ .../abstraction/GameBasedMdpModelChecker.cpp | 141 ++++++++++-------- 6 files changed, 178 insertions(+), 80 deletions(-) create mode 100644 src/exceptions/InvalidModelException.h diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 041b50d1b..52f032d8c 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -54,6 +54,7 @@ namespace storm { allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); + orderedSuccessorVariables.push_back(newMetaVariable.second); ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; return predicateIndex; } @@ -249,6 +250,11 @@ namespace storm { return successorVariables; } + template + std::vector const& AbstractionInformation::getOrderedSuccessorVariables() const { + return orderedSuccessorVariables; + } + template storm::dd::Bdd const& AbstractionInformation::getAllPredicateIdentities() const { return allPredicateIdentities; diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index 55ba8af6a..ddc359694 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -332,6 +332,13 @@ namespace storm { */ std::set const& getSuccessorVariables() const; + /*! + * Retrieves the ordered collection of successor meta variables. + * + * @return All successor meta variables. + */ + std::vector const& getOrderedSuccessorVariables() const; + /*! * Retrieves a BDD representing the identities of all predicates. * @@ -472,9 +479,12 @@ namespace storm { /// The set of all source variables. std::set sourceVariables; - /// The set of all source variables. + /// The set of all successor variables. std::set successorVariables; + /// An ordered collection of the successor variables. + std::vector orderedSuccessorVariables; + /// The BDDs corresponding to the predicates. std::vector, storm::dd::Bdd>> predicateBdds; diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 84ea2ad19..f3f8c45be 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -2,6 +2,8 @@ #include "src/abstraction/BottomStateResult.h" +#include "src/storage/BitVector.h" + #include "src/storage/prism/Program.h" #include "src/storage/dd/DdManager.h" @@ -110,30 +112,80 @@ namespace storm { } template - void AbstractProgram::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { -// std::cout << "refining in program!" << std::endl; -// lowerChoice.template toAdd().exportToDot("lchoice.dot"); -// upperChoice.template toAdd().exportToDot("uchoice.dot"); -// player1Choice.template toAdd().exportToDot("pl1_choice.dot"); -// pivotState.template toAdd().exportToDot("pivotstate.dot"); + std::map AbstractProgram::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const { + std::map result; + storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); + for (auto const& successorValuePair : lowerChoiceAsAdd) { + uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size()); + + storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates()); + for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) { + auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index]; + if (successorValuePair.first.getBooleanValue(successorVariable)) { + successor.set(index); + } + } + + result[updateIndex] = successor; + } + return result; + } + + template + void AbstractProgram::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { // Decode the index of the command chosen by player 1. storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); auto pl1It = player1ChoiceAsAdd.begin(); uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); + storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; + storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); + + // Check whether there are bottom states in the game and whether one of the choices actually picks the + // bottom state as the successor. + bool buttomStateSuccessor = false; + if (!currentGame->getBottomStates().isZero()) { + buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); + } - bool bottomSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); - if (bottomSuccessor) { - storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; + // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate + // command (that is the player 1 choice). + if (buttomStateSuccessor) { + STORM_LOG_DEBUG("One of the successors is a bottom state, taking a guard as a new predicate."); abstractCommand.notifyGuardIsPredicate(); - storm::expressions::Expression newPredicate = abstractCommand.getConcreteCommand().getGuardExpression(); + storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); this->refine({newPredicate}); } else { - exit(-1); + STORM_LOG_DEBUG("No bottom state successor. Deriving a new predicate using weakest precondition."); + + // Decode both choices to explicit mappings. + std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); + std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); + STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode."); + + // Now go through the mappings and find points of deviation. Currently, we take the first deviation. + storm::expressions::Expression newPredicate; + auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin(); + auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end(); + auto upperIt = upperChoiceUpdateToSuccessorMapping.begin(); + for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { + STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); + uint_fast64_t updateIndex = lowerIt->first; + bool deviates = lowerIt->second != upperIt->second; + if (deviates) { + for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { + if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) { + // Now we know the point of the deviation (command, update, predicate). + newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()); + break; + } + } + } + } + + this->refine({newPredicate}); } - - storm::dd::Add lowerChoiceAsAdd = lowerChoice.template toAdd(); } template diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index e3f04f8b9..8ee848946 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -100,6 +100,14 @@ namespace storm { */ std::unique_ptr> buildGame(); + /*! + * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices + * to bit vectors representing the successors under these updates. + * + * @param choice The choice to decode. + */ + std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + // The concrete program this abstract program refers to. std::reference_wrapper program; diff --git a/src/exceptions/InvalidModelException.h b/src/exceptions/InvalidModelException.h new file mode 100644 index 000000000..3d8b8b7c4 --- /dev/null +++ b/src/exceptions/InvalidModelException.h @@ -0,0 +1,13 @@ +#pragma once + +#include "src/exceptions/BaseException.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(InvalidModelException) + + } // namespace exceptions +} // namespace storm + diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 19cf3052b..9958e37df 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -1,7 +1,7 @@ #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" -#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -18,6 +18,7 @@ #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/InvalidModelException.h" #include "src/modelchecker/results/CheckResult.h" @@ -57,7 +58,7 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); - return performGameBasedAbstractionRefinement(CheckTask(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula())); + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula())); } template @@ -85,12 +86,7 @@ namespace storm { template std::unique_ptr getResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::DdManager const& ddManager, storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& initialStates, bool prob0) { - if (checkTask.isBoundSet()) { - bool result = getResultConsideringBound(prob0 ? storm::utility::zero() : storm::utility::one(), checkTask.getBound()); - return std::make_unique>(reachableStates, initialStates, result ? initialStates : ddManager.getBddZero()); - } else { - return std::make_unique>(reachableStates, initialStates, prob0 ? ddManager.template getAddZero() : initialStates.template toAdd()); - } + return std::make_unique>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero() : storm::utility::one()); } template @@ -143,17 +139,17 @@ namespace storm { bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); - } - - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy(); - storm::dd::Bdd upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract); - upperChoice1.template toAdd().exportToDot("uchoice1.dot"); - upperChoice2.template toAdd().exportToDot("uchoice2.dot"); - - bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); - if (upperChoicesDifferent) { - abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + } else { + storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy(); + storm::dd::Bdd upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + + bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); + if (upperChoicesDifferent) { + abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + } else { + STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); + } } } @@ -171,56 +167,67 @@ namespace storm { } // Derive the optimization direction for player 1 (assuming menu-game abstraction). - storm::OptimizationDirection player1Direction = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; + storm::OptimizationDirection player1Direction; + if (checkTask.isOptimizationDirectionSet()) { + player1Direction = checkTask.getOptimizationDirection(); + } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) { + player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize; + } else { + STORM_LOG_THROW(originalProgram.isDeterministicModel(), storm::exceptions::InvalidPropertyException, "Requiring either min or max annotation in property for nondeterministic models."); + player1Direction = storm::OptimizationDirection::Maximize; + } storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); - // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. - storm::abstraction::MenuGame game = abstractor.abstract(); - STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); - - // 1.5 build a BDD from the transition matrix for various later uses. - storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { + STORM_LOG_TRACE("Starting iteration " << iterations); + abstractor.exportToDot("game" + std::to_string(iterations) + ".dot"); - // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). - detail::GameProb01Result prob01 = computeProb01States(player1Direction, game, transitionMatrixBdd, constraintExpression, targetStateExpression); - - // 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(); - - // 4. if the initial states are not maybe states, then we can refine at this point. - storm::dd::Bdd initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax); - if (initialMaybeStates.isZero()) { - // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. + // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. + storm::abstraction::MenuGame game = abstractor.abstract(); + STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); + STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state."); - // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it. - storm::dd::Bdd tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states; - if (tmp == game.getInitialStates()) { - getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true); - } + // 1.5 build a BDD from the transition matrix for various later uses. + storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); - // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it. - tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states; - if (tmp == game.getInitialStates()) { - getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false); - } + // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). + detail::GameProb01Result prob01 = computeProb01States(player1Direction, game, transitionMatrixBdd, constraintExpression, targetStateExpression); + + // 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(); - // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) - // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. - refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); + // 4. if the initial states are not maybe states, then we can refine at this point. + storm::dd::Bdd initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax); + if (initialMaybeStates.isZero()) { + // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. + STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check."); + + // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it. + storm::dd::Bdd tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states; + if (tmp == game.getInitialStates()) { + return getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true); + } + + // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it. + tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states; + if (tmp == game.getInitialStates()) { + return getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false); + } + + // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) + // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. + refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); + } else { + + // Do not numerically solve the game if there is a qualitative bound around. + + STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)"); + } } - - - -// std::unique_ptr> gameSolverFactory = std::make_unique>(); -// gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates()); -// storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables - - // 3. if the bounds suffice to complete checkTask, return result now. - - // 4. if the bounds do not suffice - + + STORM_LOG_ASSERT(false, "This point must not be reached."); return nullptr; } @@ -247,20 +254,22 @@ namespace storm { STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy."); STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy."); - STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); - STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); + STORM_LOG_TRACE("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); + STORM_LOG_TRACE("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); return detail::GameProb01Result(prob0Min, prob1Min, prob0Max, prob1Max); } template storm::expressions::Expression GameBasedMdpModelChecker::getExpression(storm::logic::Formula const& formula) { - STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); + STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); storm::expressions::Expression result; if (formula.isAtomicLabelFormula()) { result = preprocessedProgram.getLabelExpression(formula.asAtomicLabelFormula().getLabel()); - } else { + } else if (formula.isAtomicExpressionFormula()) { result = formula.asAtomicExpressionFormula().getExpression(); + } else { + result = formula.asBooleanLiteralFormula().isTrueFormula() ? originalProgram.getManager().boolean(true) : originalProgram.getManager().boolean(false); } return result; }