diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index e31327157..af8f73e2c 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -2,6 +2,8 @@
#include "storm/abstraction/MenuGameAbstractor.h"
+#include "storm/utility/dd.h"
+
namespace storm {
namespace abstraction {
@@ -15,6 +17,191 @@ namespace storm {
abstractor.get().refine(predicates);
}
+ template<storm::dd::DdType Type>
+ storm::dd::Bdd<Type> pickPivotState(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Bdd<Type> const& pivotStates) {
+
+ // Perform a BFS and pick the first pivot state we encounter.
+ storm::dd::Bdd<Type> pivotState;
+ storm::dd::Bdd<Type> frontier = initialStates;
+ storm::dd::Bdd<Type> frontierPivotStates = frontier && pivotStates;
+
+ uint64_t level = 0;
+ bool foundPivotState = !frontierPivotStates.isZero();
+ if (foundPivotState) {
+ pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
+ STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
+ } else {
+ while (!foundPivotState) {
+ frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables);
+ frontierPivotStates = frontier && pivotStates;
+
+ if (!frontierPivotStates.isZero()) {
+ STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
+ pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
+ foundPivotState = true;
+ }
+ ++level;
+ }
+ }
+
+ return pivotState;
+ }
+
+ template<storm::dd::DdType Type, typename ValueType>
+ bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) {
+ STORM_LOG_TRACE("Trying refinement after qualitative check.");
+ // Get all relevant strategies.
+ storm::dd::Bdd<Type> minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy();
+ storm::dd::Bdd<Type> minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy();
+ storm::dd::Bdd<Type> maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy();
+ storm::dd::Bdd<Type> 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);
+
+ // Build the fragment of transitions that is reachable by both the min and the max strategies.
+ storm::dd::Bdd<Type> reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy;
+ reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables());
+ storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables());
+
+ // Require the pivot state to be a [0, 1] state.
+ // TODO: is this restriction necessary or is it already implied?
+ // pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States();
+
+ // 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 prob 0 (min) and prob 1 (max) strategy.
+ storm::dd::Bdd<Type> 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());
+
+ // 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 prob0 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<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
+
+ // Compute the lower and the upper choice for the pivot state.
+ std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
+ variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
+ storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
+ storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
+ storm::dd::Bdd<Type> 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();
+
+ abstractor.get().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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
+ return true;
+ } else {
+ storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
+ storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
+ storm::dd::Bdd<Type> 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();
+ abstractor.get().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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
+ return true;
+ } else {
+ STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
+ }
+ }
+ return false;
+ }
+
+ template<storm::dd::DdType Type, typename ValueType>
+ bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) {
+ STORM_LOG_TRACE("Refining after quantitative check.");
+ // Get all relevant strategies.
+ storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.player1Strategy;
+ storm::dd::Bdd<Type> minPlayer2Strategy = quantitativeResult.min.player2Strategy;
+ storm::dd::Bdd<Type> maxPlayer1Strategy = quantitativeResult.max.player1Strategy;
+ storm::dd::Bdd<Type> 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<Type> reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy;
+ reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables());
+ storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables());
+
+ // 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<Type> 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());
+
+ STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates.");
+
+ // Now that we have the pivot state candidates, we need to pick one.
+ storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
+
+ // Compute the lower and the upper choice for the pivot state.
+ std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
+ variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
+ storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
+ storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
+ storm::dd::Bdd<Type> 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();
+ abstractor.get().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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
+ } else {
+ storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
+ storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
+ storm::dd::Bdd<Type> 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();
+ abstractor.get().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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
+ } else {
+ STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
+ }
+ }
+ }
+
+
template class MenuGameRefiner<storm::dd::DdType::CUDD, double>;
template class MenuGameRefiner<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 05a8d8105..88a067cac 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -19,7 +19,6 @@
#include "storm/solver/SymbolicGameSolver.h"
#include "storm/utility/solver.h"
-#include "storm/utility/dd.h"
#include "storm/utility/prism.h"
#include "storm/utility/macros.h"
@@ -177,191 +176,6 @@ namespace storm {
return result;
}
- template<storm::dd::DdType Type>
- storm::dd::Bdd<Type> pickPivotState(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Bdd<Type> const& pivotStates) {
-
- // Perform a BFS and pick the first pivot state we encounter.
- storm::dd::Bdd<Type> pivotState;
- storm::dd::Bdd<Type> frontier = initialStates;
- storm::dd::Bdd<Type> frontierPivotStates = frontier && pivotStates;
-
- uint64_t level = 0;
- bool foundPivotState = !frontierPivotStates.isZero();
- if (foundPivotState) {
- pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
- STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
- } else {
- while (!foundPivotState) {
- frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables);
- frontierPivotStates = frontier && pivotStates;
-
- if (!frontierPivotStates.isZero()) {
- STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
- pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
- foundPivotState = true;
- }
- ++level;
- }
- }
-
- return pivotState;
- }
-
- template<storm::dd::DdType Type, typename ValueType>
- bool refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, QualitativeResultMinMax<Type> const& qualitativeResult, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
- STORM_LOG_TRACE("Trying refinement after qualitative check.");
- // Get all relevant strategies.
- storm::dd::Bdd<Type> minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy();
- storm::dd::Bdd<Type> minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy();
- storm::dd::Bdd<Type> maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy();
- storm::dd::Bdd<Type> 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);
-
- // Build the fragment of transitions that is reachable by both the min and the max strategies.
- storm::dd::Bdd<Type> reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy;
- reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables());
- storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables());
-
- // Require the pivot state to be a [0, 1] state.
- // TODO: is this restriction necessary or is it already implied?
-// pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States();
-
- // 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 prob 0 (min) and prob 1 (max) strategy.
- storm::dd::Bdd<Type> 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());
-
- // 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 prob0 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<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
-
- // Compute the lower and the upper choice for the pivot state.
- std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
- variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
- storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
- storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
- storm::dd::Bdd<Type> 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();
-
- abstractor.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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
- return true;
- } else {
- storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
- storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
- storm::dd::Bdd<Type> 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();
- abstractor.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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
- return true;
- } else {
- STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
- }
- }
- return false;
- }
-
-
- template<storm::dd::DdType Type, typename ValueType>
- void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) {
- STORM_LOG_TRACE("Refining after quantitative check.");
- // Get all relevant strategies.
- storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.player1Strategy;
- storm::dd::Bdd<Type> minPlayer2Strategy = quantitativeResult.min.player2Strategy;
- storm::dd::Bdd<Type> maxPlayer1Strategy = quantitativeResult.max.player1Strategy;
- storm::dd::Bdd<Type> 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<Type> reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || maxPlayer1Strategy) && minPlayer2Strategy && maxPlayer2Strategy;
- reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables());
- storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables());
-
- // 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<Type> 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());
-
- STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates.");
-
- // Now that we have the pivot state candidates, we need to pick one.
- storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
-
- // Compute the lower and the upper choice for the pivot state.
- std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
- variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
- storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
- storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
- storm::dd::Bdd<Type> 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();
- abstractor.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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
- } else {
- storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
- storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
- storm::dd::Bdd<Type> 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();
- abstractor.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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
- } else {
- STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
- }
- }
- }
-
template<storm::dd::DdType Type, typename ValueType>
QuantitativeResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<QuantitativeResult<Type, ValueType>> const& startInfo = boost::none) {
@@ -516,7 +330,7 @@ namespace storm {
// 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 = refineAfterQualitativeCheck(abstractor, game, qualitativeResult, transitionMatrixBdd);
+ qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult);
}
}
@@ -562,7 +376,7 @@ namespace storm {
// (10) If we arrived at this point, it means that we have all qualitative and quantitative
// information about the game, but we could not yet answer the query. In this case, we need to refine.
- refineAfterQuantitativeCheck(abstractor, game, transitionMatrixBdd, quantitativeResult);
+ refiner.refine(game, transitionMatrixBdd, quantitativeResult);
}
auto iterationEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(iterationEnd - iterationStart).count() << "ms.");