diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index e9a682c32..ca26fd8dd 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -22,61 +22,54 @@ namespace storm { } template - storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionsMin, storm::dd::Bdd const& transitionsMax, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { + storm::dd::Bdd pickPivotStateWithMinimalDistance(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionsMin, storm::dd::Bdd const& transitionsMax, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { - // Perform a BFS and pick the first pivot state we encounter. - storm::dd::Bdd pivotState; + // Set up used variables. storm::dd::Bdd frontierMin = initialStates; storm::dd::Bdd frontierMax = initialStates; - storm::dd::Bdd frontierMinPivotStates = frontierMin && pivotStates; - storm::dd::Bdd frontierMaxPivotStates = frontierMinPivotStates; + storm::dd::Bdd frontierPivotStates = frontierMin && pivotStates; + // Check whether we have pivot states on the very first level. uint64_t level = 0; - bool foundPivotState = !frontierMinPivotStates.isZero(); + bool foundPivotState = !frontierPivotStates.isZero(); if (foundPivotState) { - pivotState = frontierMinPivotStates.existsAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state from " << frontierMinPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + return frontierPivotStates.existsAbstractRepresentative(rowVariables); } else { + + // Otherwise, we perform a simulatenous BFS in the sense that we make one step in both the min and max + // transitions and check for pivot states we encounter. while (!foundPivotState) { frontierMin = frontierMin.relationalProduct(transitionsMin, rowVariables, columnVariables); frontierMax = frontierMax.relationalProduct(transitionsMax, rowVariables, columnVariables); - frontierMinPivotStates = frontierMin && pivotStates; - frontierMaxPivotStates = frontierMax && pivotStates; - if (!frontierMinPivotStates.isZero()) { - if (quantitativeResult) { - storm::dd::Add frontierPivotStatesAdd = frontierMinPivotStates.template toAdd(); - storm::dd::Add diff = frontierPivotStatesAdd * quantitativeResult.get().max.values - frontierPivotStatesAdd * quantitativeResult.get().min.values; - pivotState = diff.maxAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - foundPivotState = true; - } else { - pivotState = frontierMinPivotStates.existsAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - foundPivotState = true; - } - } else if (!frontierMaxPivotStates.isZero()) { + frontierPivotStates = (frontierMin && pivotStates) || (frontierMax && pivotStates); + + if (!frontierPivotStates.isZero()) { if (quantitativeResult) { - storm::dd::Add frontierPivotStatesAdd = frontierMaxPivotStates.template toAdd(); + storm::dd::Add frontierPivotStatesAdd = frontierPivotStates.template toAdd(); storm::dd::Add diff = frontierPivotStatesAdd * quantitativeResult.get().max.values - frontierPivotStatesAdd * quantitativeResult.get().min.values; - pivotState = diff.maxAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - foundPivotState = true; + STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + return diff.maxAbstractRepresentative(rowVariables); } else { - pivotState = frontierMinPivotStates.existsAbstractRepresentative(rowVariables); - STORM_LOG_TRACE("Picked pivot state from " << (frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount()) << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - foundPivotState = true; + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + return frontierPivotStates.existsAbstractRepresentative(rowVariables); } } ++level; } } - return pivotState; + STORM_LOG_ASSERT(false, "This point must not be reached, because then no pivot state could be found."); + return storm::dd::Bdd(); } template - void MenuGameRefiner::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { + storm::expressions::Expression MenuGameRefiner::derivePredicateFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { + // Prepare result. + storm::expressions::Expression newPredicate; + + // Get abstraction informatin for easier access. AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); // Decode the index of the command chosen by player 1. @@ -92,9 +85,8 @@ namespace storm { // command (that is the player 1 choice). if (buttomStateSuccessor) { STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); - storm::expressions::Expression newPredicate = abstractor.get().getGuard(player1Index); - STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - this->performRefinement({newPredicate}); + newPredicate = abstractor.get().getGuard(player1Index); + STORM_LOG_DEBUG("Derived new predicate (based on guard): " << newPredicate); } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); @@ -104,7 +96,6 @@ namespace storm { STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); // 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(); @@ -123,43 +114,36 @@ namespace storm { } } STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); - - STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); - this->performRefinement({newPredicate}); + STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate); } STORM_LOG_TRACE("Current set of predicates:"); for (auto const& predicate : abstractionInformation.getPredicates()) { STORM_LOG_TRACE(predicate); } + return newPredicate; } + template + struct PivotStateResult { + storm::dd::Bdd reachableTransitionsMin; + storm::dd::Bdd reachableTransitionsMax; + storm::dd::Bdd pivotStates; + }; + template - bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) const { - STORM_LOG_TRACE("Trying refinement after qualitative check."); - // Get all relevant strategies. - storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); - storm::dd::Bdd minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy(); - storm::dd::Bdd maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy(); - storm::dd::Bdd maxPlayer2Strategy = qualitativeResult.prob1Max.getPlayer2Strategy(); + PivotStateResult computePivotStates(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) { - // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 - // state that is also a prob 0 state. - minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); + PivotStateResult result; // Build the fragment of transitions that is reachable by either the min or the max strategies. - storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy; - reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); - - storm::dd::Bdd reachableTransitionsMin = (transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); - storm::dd::Bdd reachableTransitionsMax = (transitionMatrixBdd && maxPlayer1Strategy && maxPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); + result.reachableTransitionsMin = (transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); + result.reachableTransitionsMax = (transitionMatrixBdd && maxPlayer1Strategy && maxPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); // Start with all reachable states as potential pivot states. - storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()) || - storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables()); - - //storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); - + result.pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), result.reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()) || + storm::utility::dd::computeReachableStates(game.getInitialStates(), result.reachableTransitionsMax, 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 and // that the difference is not because of a missing strategy in either case. @@ -170,22 +154,13 @@ namespace storm { constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); // Then restrict the pivot states by requiring existing and different player 2 choices. - // pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); - pivotStates &= ((minPlayer1Strategy && maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); - - // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either - // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob1 max define - // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state - // is found. In this case, we abort the qualitative refinement here. - if (pivotStates.isZero()) { - return false; - } - - STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to proceed without pivot state candidates."); - - // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitionsMin, reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStates); + result.pivotStates &= ((minPlayer1Strategy && maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + return result; + } + + template + storm::expressions::Expression MenuGameRefiner::derivePredicateFromPivotState(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const { // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); @@ -198,10 +173,10 @@ namespace storm { STORM_LOG_TRACE("Refining based on lower choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - this->refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + storm::expressions::Expression newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - return true; + return newPredicate; } else { storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); @@ -211,15 +186,48 @@ namespace storm { if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - this->refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + storm::expressions::Expression newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - return true; + return newPredicate; } else { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); } } - return false; + } + + template + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) const { + STORM_LOG_TRACE("Trying refinement after qualitative check."); + // Get all relevant strategies. + storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); + storm::dd::Bdd minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy(); + storm::dd::Bdd maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy(); + storm::dd::Bdd maxPlayer2Strategy = qualitativeResult.prob1Max.getPlayer2Strategy(); + + // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 + // state that is also a prob 0 state. + minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); + + // Compute all reached pivot states. + PivotStateResult pivotStateResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + + // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either + // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob1 max define + // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state + // is found. In this case, we abort the qualitative refinement here. + if (pivotStateResult.pivotStates.isZero()) { + return false; + } + STORM_LOG_ASSERT(!pivotStateResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates."); + + // Now that we have the pivot state candidates, we need to pick one. + storm::dd::Bdd pivotState = pickPivotStateWithMinimalDistance(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates); + + // Derive predicate based on the selected pivot state. + storm::expressions::Expression newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + performRefinement({newPredicate}); + return true; } template @@ -231,75 +239,21 @@ namespace storm { storm::dd::Bdd maxPlayer1Strategy = quantitativeResult.max.player1Strategy; storm::dd::Bdd maxPlayer2Strategy = quantitativeResult.max.player2Strategy; - // TODO: fix min strategies to take the max strategies if possible. - - // Build the fragment of transitions that is reachable by both the min and the max strategies. - storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy; - reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); - - storm::dd::Bdd reachableTransitionsMin = (transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); - storm::dd::Bdd reachableTransitionsMax = (transitionMatrixBdd && maxPlayer1Strategy && maxPlayer2Strategy).existsAbstract(game.getNondeterminismVariables()); - - // Start with all reachable states as potential pivot states. - // storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); - storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMin, game.getRowVariables(), game.getColumnVariables()) || - storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables()); + // Compute all reached pivot states. + PivotStateResult pivotStateResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); - + // TODO: required? // Require the pivot state to be a state with a lower bound strictly smaller than the upper bound. - pivotStates &= quantitativeResult.min.values.less(quantitativeResult.max.values); - - STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); - - // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and - // that the difference is not because of a missing strategy in either case. - - // Start with constructing the player 2 states that have a (min) and a (max) strategy. - // TODO: necessary? - storm::dd::Bdd constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); - - // Now construct all player 2 choices that actually exist and differ in the min and max case. - constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); - - // Then restrict the pivot states by requiring existing and different player 2 choices. - // pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); - pivotStates &= ((minPlayer1Strategy && maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); - - STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); + pivotStateResult.pivotStates &= quantitativeResult.min.values.less(quantitativeResult.max.values); + STORM_LOG_ASSERT(!pivotStateResult.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(), reachableTransitionsMin, reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStates, quantitativeResult); - - // 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() && minPlayer1Strategy; - storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); - if (lowerChoicesDifferent) { - STORM_LOG_TRACE("Refining based on lower choice."); - auto refinementStart = std::chrono::high_resolution_clock::now(); - this->refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - } else { - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; - storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); - if (upperChoicesDifferent) { - STORM_LOG_TRACE("Refining based on upper choice."); - auto refinementStart = std::chrono::high_resolution_clock::now(); - this->refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - } else { - STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); - } - } + storm::dd::Bdd pivotState = pickPivotStateWithMinimalDistance(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates); + + // Derive predicate based on the selected pivot state. + storm::expressions::Expression newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + performRefinement({newPredicate}); return true; } diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 5e866f860..7394c14b3 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -52,8 +52,8 @@ namespace storm { bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) const; private: - void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; - + storm::expressions::Expression derivePredicateFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; + storm::expressions::Expression derivePredicateFromPivotState(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; /*! * Takes the given predicates, preprocesses them and then refines the abstractor. */