sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

moved parts of refine functionality from model checker to refiner class

tempestpy_adaptions
dehnert 8 years ago
parent
fe0e5c3793
commit
a2f85ffcff
2 changed files with 189 additions and 188 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 187
      src/storm/abstraction/MenuGameRefiner.cpp
  2. 190
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

187
src/storm/abstraction/MenuGameRefiner.cpp
View File

@ -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>;

190
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -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.");

Write Preview
Loading…
Cancel
Save