From 954eadc54614feeadc4e663216907a556a740b92 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 18 Dec 2016 21:20:39 +0100 Subject: [PATCH] improved detection for early result detection in game based engine --- .../abstraction/AbstractionInformation.cpp | 6 + .../abstraction/AbstractionInformation.h | 10 + src/storm/abstraction/QuantitativeResult.h | 4 +- .../abstraction/jani/AutomatonAbstractor.cpp | 4 +- src/storm/abstraction/jani/EdgeAbstractor.cpp | 16 +- src/storm/abstraction/jani/EdgeAbstractor.h | 2 +- .../jani/JaniMenuGameAbstractor.cpp | 3 +- .../abstraction/prism/CommandAbstractor.cpp | 6 +- .../prism/PrismMenuGameAbstractor.cpp | 1 + .../abstraction/GameBasedMdpModelChecker.cpp | 196 +++++++++--------- .../abstraction/GameBasedMdpModelChecker.h | 2 +- 11 files changed, 134 insertions(+), 116 deletions(-) diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 804a8ee33..f1dca42cc 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -63,6 +63,7 @@ namespace storm { allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); + sourcePredicateVariables.insert(newMetaVariable.first); orderedSourcePredicateVariables.push_back(newMetaVariable.first); orderedSuccessorPredicateVariables.push_back(newMetaVariable.second); ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; @@ -278,6 +279,11 @@ namespace storm { return successorVariables; } + template + std::set const& AbstractionInformation::getSourcePredicateVariables() const { + return sourcePredicateVariables; + } + template std::vector const& AbstractionInformation::getOrderedSourcePredicateVariables() const { return orderedSourcePredicateVariables; diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index 46b6804ee..55a9e0105 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -341,6 +341,13 @@ namespace storm { */ std::set const& getSuccessorVariables() const; + /*! + * Retrieves the set of source predicate meta variables. + * + * @return All source predicate meta variables. + */ + std::set const& getSourcePredicateVariables() const; + /*! * Retrieves a BDD representing the identities of all predicates. * @@ -551,6 +558,9 @@ namespace storm { /// The set of all successor variables. std::set successorVariables; + /// The set of all source predicate variables. + std::set sourcePredicateVariables; + /// An ordered collection of the source variables. std::vector orderedSourcePredicateVariables; diff --git a/src/storm/abstraction/QuantitativeResult.h b/src/storm/abstraction/QuantitativeResult.h index d0c949952..f2975067a 100644 --- a/src/storm/abstraction/QuantitativeResult.h +++ b/src/storm/abstraction/QuantitativeResult.h @@ -11,11 +11,11 @@ namespace storm { struct QuantitativeResult { QuantitativeResult() = default; - QuantitativeResult(ValueType initialStateValue, storm::dd::Add const& values, storm::dd::Bdd const& player1Strategy, storm::dd::Bdd const& player2Strategy) : initialStateValue(initialStateValue), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + QuantitativeResult(std::pair initialStatesRange, storm::dd::Add const& values, storm::dd::Bdd const& player1Strategy, storm::dd::Bdd const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { // Intentionally left empty. } - ValueType initialStateValue; + std::pair initialStatesRange; storm::dd::Add values; storm::dd::Bdd player1Strategy; storm::dd::Bdd player2Strategy; diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 33731ddcc..08a401608 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -79,7 +79,7 @@ namespace storm { BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); for (auto& edge : edges) { - BottomStateResult commandBottomStateResult = edge.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + BottomStateResult commandBottomStateResult = edge.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables, locationVariables); result.states |= commandBottomStateResult.states; result.transitions |= commandBottomStateResult.transitions; } @@ -98,7 +98,7 @@ namespace storm { template storm::dd::Bdd AutomatonAbstractor::getInitialLocationsBdd() const { - if (automaton.get().getNumberOfLocations()) { + if (automaton.get().getNumberOfLocations() == 1) { return this->getAbstractionInformation().getDdManager().getBddOne(); } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index 51fef5753..b333739ef 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -620,7 +620,10 @@ namespace storm { } template - BottomStateResult EdgeAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult EdgeAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables, boost::optional> const& locationVariables) { + // Compute the reachable states that have this edge enabled. + storm::dd::Bdd reachableStatesWithEdge = (reachableStates && abstractGuard && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex())).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); + STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard()); BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); @@ -632,8 +635,8 @@ namespace storm { // Use the state abstractor to compute the set of abstract states that has this edge enabled but still // has a transition to a bottom state. - bottomStateAbstractor.constrain(reachableStates && abstractGuard); - result.states = bottomStateAbstractor.getAbstractStates(); + bottomStateAbstractor.constrain(reachableStatesWithEdge); + result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithEdge && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex()); // If the result is empty one time, we can skip the bottom state computation from now on. if (result.states.isZero()) { @@ -643,12 +646,15 @@ namespace storm { // Now equip all these states with an actual transition to a bottom state. result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false); - // Mark the states as bottom states. + // Mark the states as bottom states and add source location information. result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); - // Add the edge encoding and the next free player 2 encoding. + // Add the edge encoding. result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, 0,numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); + // Add the location identity to the transitions. + result.transitions &= this->getAbstractionInformation().getAllLocationIdentities(); + return result; } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index b0deaf1e9..674805666 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -93,7 +93,7 @@ namespace storm { * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2. * @return The bottom state transitions in the form of a BDD. */ - BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables, boost::optional> const& locationVariables); /*! * Retrieves an ADD that maps the encoding of the edge, source/target locations and its updates to their probabilities. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 83a7181c8..d2f948d69 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -152,6 +152,7 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates(); + initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, @@ -167,7 +168,7 @@ namespace storm { // Compute bottom states and the appropriate transitions if necessary. BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); - bottomStateResult = automata.front().getBottomStateTransitions(reachableStates.existsAbstract(abstractionInformation.getSourceLocationVariables()), game.numberOfPlayer2Variables); + bottomStateResult = automata.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); bool hasBottomStates = !bottomStateResult.states.isZero(); // Construct the transition matrix by cutting away the transitions of unreachable states. diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 12e883e9b..cf116afcd 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -630,10 +630,12 @@ namespace storm { return result; } + storm::dd::Bdd reachableStatesWithCommand = reachableStates && abstractGuard; + // Use the state abstractor to compute the set of abstract states that has this command enabled but // still has a transition to a bottom state. - bottomStateAbstractor.constrain(reachableStates && abstractGuard); - result.states = bottomStateAbstractor.getAbstractStates(); + bottomStateAbstractor.constrain(reachableStatesWithCommand); + result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithCommand; // If the result is empty one time, we can skip the bottom state computation from now on. if (result.states.isZero()) { diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index c08b306f1..49fb8c2bd 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -150,6 +150,7 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); + initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a14030c2d..21dc3e73e 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -91,32 +91,33 @@ namespace storm { return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), preprocessedModel.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping)); } - template - std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& statesMin, storm::dd::Bdd const& statesMax, bool prob0) { - std::unique_ptr result; - if ((initialStates && statesMin && statesMax) == initialStates) { - result = std::make_unique>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero() : storm::utility::one()); - } - return result; - } - template std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& prob0, storm::dd::Bdd const& prob1) { std::unique_ptr result; boost::optional> const& bound = checkTask.getOptionalBound(); if (bound) { - if (player2Direction == storm::OptimizationDirection::Minimize && storm::logic::isLowerBound(bound.get().comparisonType)) { - if ((prob1 && initialStates) == initialStates) { - result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); - } else if (checkTask.isQualitativeSet()) { - result = std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); + // Despite having a bound, we create a quanitative result so that the next layer can perform the comparison. + + if (player2Direction == storm::OptimizationDirection::Minimize) { + if (storm::logic::isLowerBound(bound.get().comparisonType)) { + if ((prob1 && initialStates) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } + } else { + if (!(prob1 && initialStates).isZero()) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } } - } else if (player2Direction == storm::OptimizationDirection::Maximize && !storm::logic::isLowerBound(bound.get().comparisonType)) { - if ((prob0 && initialStates) == initialStates) { - result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); - } else if (checkTask.isQualitativeSet()) { - result = std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); + } else if (player2Direction == storm::OptimizationDirection::Maximize) { + if (!storm::logic::isLowerBound(bound.get().comparisonType)) { + if ((prob0 && initialStates) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } + } else { + if (!(prob0 && initialStates).isZero()) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } } } } @@ -127,11 +128,11 @@ namespace storm { template std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, QualitativeResultMinMax const& qualitativeResult) { // Check whether we can already give the answer based on the current information. - std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob0Max.getPlayer1States(), true); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); if (result) { return result; } - result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult.prob1Min.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States(), false); + result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); if (result) { return result; } @@ -139,7 +140,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, ValueType const& value) { + std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, std::pair const& initialValueRange) { std::unique_ptr result; // If the minimum value exceeds an upper threshold or the maximum value is below a lower threshold, we can @@ -151,31 +152,34 @@ namespace storm { return result; } + ValueType const& lowerValue = initialValueRange.first; + ValueType const& upperValue = initialValueRange.second; + storm::logic::ComparisonType comparisonType = bound.get().comparisonType; ValueType threshold = bound.get().threshold; if (storm::logic::isLowerBound(comparisonType)) { if (player2Direction == storm::OptimizationDirection::Minimize) { - if ((storm::logic::isStrict(comparisonType) && value > threshold) - || (!storm::logic::isStrict(comparisonType) && value >= threshold)) { - result = std::make_unique>(storm::storage::sparse::state_type(0), value); + if ((storm::logic::isStrict(comparisonType) && lowerValue > threshold) + || (!storm::logic::isStrict(comparisonType) && lowerValue >= threshold)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), lowerValue); } } else { - if ((storm::logic::isStrict(comparisonType) && value <= threshold) - || (!storm::logic::isStrict(comparisonType) && value < threshold)) { - result = std::make_unique>(storm::storage::sparse::state_type(0), value); + if ((storm::logic::isStrict(comparisonType) && upperValue <= threshold) + || (!storm::logic::isStrict(comparisonType) && upperValue < threshold)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), upperValue); } } - } else if (!storm::logic::isLowerBound(comparisonType)) { + } else { if (player2Direction == storm::OptimizationDirection::Maximize) { - if ((storm::logic::isStrict(comparisonType) && value < threshold) || - (!storm::logic::isStrict(comparisonType) && value <= threshold)) { - result = std::make_unique>(storm::storage::sparse::state_type(0), value); + if ((storm::logic::isStrict(comparisonType) && upperValue < threshold) || + (!storm::logic::isStrict(comparisonType) && upperValue <= threshold)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), upperValue); } } else { - if ((storm::logic::isStrict(comparisonType) && value >= threshold) || - (!storm::logic::isStrict(comparisonType) && value > threshold)) { - result = std::make_unique>(storm::storage::sparse::state_type(0), value); + if ((storm::logic::isStrict(comparisonType) && lowerValue >= threshold) || + (!storm::logic::isStrict(comparisonType) && lowerValue > threshold)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), lowerValue); } } } @@ -223,7 +227,7 @@ namespace storm { 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, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none); - return QuantitativeResult(storm::utility::zero(), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); + return QuantitativeResult(std::make_pair(storm::utility::zero(), storm::utility::one()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); } template @@ -232,10 +236,6 @@ namespace storm { bool min = player2Direction == storm::OptimizationDirection::Minimize; QuantitativeResult result; - // The minimal value after qualitative checking can only be zero. If it was 1, we could have given - // the result right away. Similarly, the maximal value can only be one at this point. - result.initialStateValue = min ? storm::utility::zero() : storm::utility::one(); - // We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative // preprocessing if possible. storm::dd::Bdd combinedPlayer1QualitativeStrategies; @@ -265,15 +265,6 @@ namespace storm { // Extend the values of the maybe states by the qualitative values. result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd() : qualitativeResult.prob1Max.getPlayer1States().template toAdd(); - - // Construct an ADD holding the initial values of initial states and check it for validity. - storm::dd::Add initialStateValueAdd = initialStatesAdd * result.values; - // For min, we can only require a non-zero count of *at most* one, because the result may actually be 0. - STORM_LOG_ASSERT((!min && initialStateValueAdd.getNonZeroCount() == 1) || (min && initialStateValueAdd.getNonZeroCount() <= 1), "Wrong number of results for initial states. Expected " << (min ? "<= 1" : "1") << ", but got " << initialStateValueAdd.getNonZeroCount() << "."); - result.initialStateValue = result.initialStateValue = initialStateValueAdd.getMax(); - - result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy); - result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy); } else { STORM_LOG_TRACE("No maybe states."); @@ -281,8 +272,20 @@ namespace storm { result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd() : qualitativeResult.prob1Max.getPlayer1States().template toAdd(); } + // Construct an ADD holding the initial values of initial states and extract the bound on the initial states. + storm::dd::Add initialStateValueAdd = initialStatesAdd * result.values; + + ValueType maxValueOverInitialStates = initialStateValueAdd.getMax(); + initialStateValueAdd += (!game.getInitialStates()).template toAdd(); + ValueType minValueOverInitialStates = initialStateValueAdd.getMin(); + + result.initialStatesRange = std::make_pair(minValueOverInitialStates, maxValueOverInitialStates); + + result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy); + result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy); + auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Obtained quantitative " << (player2Direction == storm::OptimizationDirection::Minimize ? "lower" : "upper") << " bound " << result.initialStateValue << " in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_TRACE("Obtained quantitative " << (min ? "lower" : "upper") << " bound " << (min ? result.initialStatesRange.first : result.initialStatesRange.second) << " in " << std::chrono::duration_cast(end - start).count() << "ms."); return result; } @@ -313,7 +316,7 @@ namespace storm { storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); - globalTargetStates.template toAdd().exportToDot("target.dot"); + // globalTargetStates.template toAdd().exportToDot("target.dot"); // Enter the main-loop of abstraction refinement. boost::optional> previousQualitativeResult = boost::none; @@ -327,11 +330,11 @@ namespace storm { storm::abstraction::MenuGame game = abstractor->abstract(); auto abstractionEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); - STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state."); // (2) Prepare transition matrix BDD and target state BDD for later use. storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); storm::dd::Bdd initialStates = game.getInitialStates(); + STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states."); storm::dd::Bdd constraintStates = globalConstraintStates && game.getReachableStates(); storm::dd::Bdd targetStates = globalTargetStates && game.getReachableStates(); if (player1Direction == storm::OptimizationDirection::Minimize) { @@ -344,8 +347,8 @@ namespace storm { // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - QualitativeResultMinMax qualitativeResult; - std::unique_ptr result = computeProb01States(checkTask, qualitativeResult, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates, refiner.addedAllGuards()); + QualitativeResultMinMax qualitativeResult = computeProb01States(checkTask, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { printStatistics(*abstractor, game); return result; @@ -365,20 +368,18 @@ namespace storm { // 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."); - result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); - if (result) { - printStatistics(*abstractor, game); - return result; - } else { - STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); - - auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); - // 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. - qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult); - auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); - } + STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); + + // 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. + auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); + qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult); + auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); + } else if (initialMaybeStates == initialStates && checkTask.isQualitativeSet()) { + // If all initial states are 'maybe' states and the property we needed to check is a qualitative one, + // we can return the result here. + return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); } // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. @@ -395,7 +396,7 @@ namespace storm { // (7) Solve the min values and check whether we can give the answer already. quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); previousMinQuantitativeResult = quantitativeResult.min; - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStatesRange); if (result) { printStatistics(*abstractor, game); return result; @@ -403,17 +404,17 @@ namespace storm { // (8) Solve the max values and check whether we can give the answer already. quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStateValue); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStatesRange); if (result) { printStatistics(*abstractor, game); return result; } auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStateValue << ", " << quantitativeResult.max.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStatesRange.first << ", " << quantitativeResult.max.initialStatesRange.second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. - result = checkForResultAfterQuantitativeCheck(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue, comparator); + result = checkForResultAfterQuantitativeCheck(checkTask, quantitativeResult.min.initialStatesRange.first, quantitativeResult.max.initialStatesRange.second, comparator); if (result) { printStatistics(*abstractor, game); return result; @@ -471,6 +472,7 @@ namespace storm { } else { STORM_LOG_ASSERT(result.hasPlayer1Strategy() && ((result.getPlayer1States() && !targetStates).isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); } + STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); return true; @@ -487,23 +489,25 @@ namespace storm { } template - std::unique_ptr GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, bool addedAllGuards) { + QualitativeResultMinMax GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + + QualitativeResultMinMax result; if (reuseQualitativeResults) { // Depending on the player 1 direction, we choose a different order of operations. if (player1Direction == storm::OptimizationDirection::Minimize) { // (1) min/min: compute prob0 using the game functions - qualitativeResult.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); // (2) min/min: compute prob1 using the MDP functions - storm::dd::Bdd candidates = game.getReachableStates() && !qualitativeResult.prob0Min.player1States; + storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Min.player1States; storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, constraintStates, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates); // (3) min/min: compute prob1 using the game functions - qualitativeResult.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp)); + result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp)); // (4) min/max: compute prob 0 using the game functions - qualitativeResult.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); // (5) min/max: compute prob 1 using the game functions // We know that only previous prob1 states can now be prob 1 states again, because the upper bound @@ -512,51 +516,39 @@ namespace storm { if (previousQualitativeResult) { prob1Candidates = previousQualitativeResult.get().prob1Max.player1States; } - qualitativeResult.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, prob1Candidates); + result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, prob1Candidates); } else { // (1) max/max: compute prob0 using the game functions - qualitativeResult.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states. - storm::dd::Bdd candidates = game.getReachableStates() && !qualitativeResult.prob0Max.player1States; + storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Max.player1States; if (previousQualitativeResult) { candidates &= previousQualitativeResult.get().prob1Max.player1States; } storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(game, transitionMatrixBdd, constraintStates, targetStates, candidates); // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation - qualitativeResult.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, boost::make_optional(prob1MaxMaxMdp)); + result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, boost::make_optional(prob1MaxMaxMdp)); // (4) max/min: compute prob0 using the game functions - qualitativeResult.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); // (5) max/min: compute prob1 using the game functions, use prob1 from max/max as the candidate set - qualitativeResult.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); + result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); } } else { - qualitativeResult.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); - qualitativeResult.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); - qualitativeResult.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); - qualitativeResult.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); } STORM_LOG_TRACE("Qualitative precomputation completed."); - STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << qualitativeResult.prob0Min.player1States.getNonZeroCount() << " 'no', " << qualitativeResult.prob1Min.player1States.getNonZeroCount() << " 'yes'."); - STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << qualitativeResult.prob0Max.player1States.getNonZeroCount() << " 'no', " << qualitativeResult.prob1Max.player1States.getNonZeroCount() << " 'yes'."); - - STORM_LOG_ASSERT(checkQualitativeStrategies(qualitativeResult, targetStates), "Qualitative strategies appear to be broken."); - - // Check for result after qualitative computations. - std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); - if (result) { - return result; - } else { - result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); - if (result) { - return result; - } - } + STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNonZeroCount() << " 'no', " << result.prob1Min.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNonZeroCount() << " 'no', " << result.prob1Max.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_ASSERT(checkQualitativeStrategies(result, targetStates), "Qualitative strategies appear to be broken."); return result; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 1329ef399..de6fd8fc8 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -71,7 +71,7 @@ namespace storm { * Performs a qualitative check on the the given game to compute the (player 1) states that have probability * 0 or 1, respectively, to reach a target state and only visiting constraint states before. */ - std::unique_ptr computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, bool addedAllGuards); + QualitativeResultMinMax computeProb01States(CheckTask const& checkTask, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const;