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

explicit Dijkstra search for pivot state now follows the strategies separately

tempestpy_adaptions
dehnert 7 years ago
parent
bcd3d68c61
commit
8f4f5c555e
6 changed files with 318 additions and 214 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. 179
      src/storm/abstraction/MenuGameRefiner.cpp
  2. 3
      src/storm/abstraction/MenuGameRefiner.h
  3. 304
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  4. 13
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
  5. 21
      src/storm/utility/Stopwatch.cpp
  6. 12
      src/storm/utility/Stopwatch.h

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

@ -1059,65 +1059,136 @@ namespace storm {
return true;
}
template<typename ValueType>
struct ExplicitDijkstraQueueElement {
ExplicitDijkstraQueueElement(ValueType const& distance, uint64_t state, bool lower) : distance(distance), state(state), lower(lower) {
// Intentionally left empty.
}
ValueType distance;
uint64_t state;
bool lower;
};
template<typename ValueType>
struct ExplicitDijkstraQueueElementLess {
bool operator()(ExplicitDijkstraQueueElement<ValueType> const& a, ExplicitDijkstraQueueElement<ValueType> const& b) const {
if (a.distance < b.distance) {
return true;
} else if (a.distance > b.distance) {
return false;
} else {
if (a.state < b.state) {
return true;
} else if (a.state > b.state) {
return false;
} else {
if (a.lower < b.lower) {
return true;
} else {
return false;
}
}
}
}
};
template<typename ValueType>
void performDijkstraStep(std::set<ExplicitDijkstraQueueElement<ValueType>, ExplicitDijkstraQueueElementLess<ValueType>>& dijkstraQueue, bool probabilityDistances, std::vector<ValueType>& distances, std::vector<std::pair<uint64_t, uint64_t>>& predecessors, bool generatePredecessors, bool lower, uint64_t currentState, ValueType const& currentDistance, bool isPivotState, ExplicitGameStrategyPair const& strategyPair, ExplicitGameStrategyPair const& otherStrategyPair, std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Grouping, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& relevantStates) {
if (strategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2Successor = strategyPair.getPlayer1Strategy().getChoice(currentState);
uint64_t player2Choice = strategyPair.getPlayer2Strategy().getChoice(player2Successor);
STORM_LOG_ASSERT(isPivotState || !otherStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) || strategyPair.getPlayer2Strategy().getChoice(player2Successor) == player2Choice, "Did not expect deviation in player 2 strategy.");
STORM_LOG_ASSERT(player2Grouping[player2Successor] <= player2Choice && player2Choice < player2Grouping[player2Successor + 1], "Illegal choice for player 2.");
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
uint64_t player1Successor = entry.getColumn();
if (!relevantStates.get(player1Successor)) {
continue;
}
ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) {
distances[player1Successor] = alternateDistance;
if (generatePredecessors) {
predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[player2Successor]);
}
dijkstraQueue.emplace(alternateDistance, player1Successor, lower);
}
}
} else {
STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting min strategy for non-target states.");
}
}
template<typename ValueType>
boost::optional<ExplicitPivotStateResult<ValueType>> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector<ValueType> const* lowerValues = nullptr, std::vector<ValueType> const* upperValues = nullptr) {
STORM_LOG_ASSERT(!lowerValues || upperValues, "Expected none or both value results.");
STORM_LOG_ASSERT(!upperValues || lowerValues, "Expected none or both value results.");
// Perform Dijkstra search that stays within the relevant states and searches for a state in which the
// strategies for the (commonly chosen) player 1 action leads to a player 2 state in which the choices differ.
ExplicitPivotStateResult<ValueType> result;
// Perform Dijkstra search that stays within the relevant states and searches for a (pivot) state in which
// the strategies the lower or upper player 1 action leads to a player 2 state in which the choices differ.
// To guarantee that the pivot state is reachable by either of the strategies, we do a parallel Dijkstra
// search in both the lower and upper strategy.
bool probabilityDistances = pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MostProbablePath;
uint64_t numberOfStates = initialStates.size();
ValueType inftyDistance = probabilityDistances ? storm::utility::zero<ValueType>() : storm::utility::infinity<ValueType>();
ValueType zeroDistance = probabilityDistances ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
std::vector<ValueType> distances(numberOfStates, inftyDistance);
// Create storages for the lower and upper Dijkstra search.
std::vector<ValueType> lowerDistances(numberOfStates, inftyDistance);
std::vector<std::pair<uint64_t, uint64_t>> lowerPredecessors;
std::vector<ValueType> upperDistances(numberOfStates, inftyDistance);
std::vector<std::pair<uint64_t, uint64_t>> upperPredecessors;
if (generatePredecessors) {
result.predecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR, ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR));
lowerPredecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR, ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR));
upperPredecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR, ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR));
}
// Use set as priority queue with unique membership; default comparison on pair works fine if distance is
// the first entry.
std::set<std::pair<ValueType, uint64_t>, std::greater<std::pair<ValueType, uint64_t>>> dijkstraQueue;
// Use set as priority queue with unique membership.
std::set<ExplicitDijkstraQueueElement<ValueType>, ExplicitDijkstraQueueElementLess<ValueType>> dijkstraQueue;
for (auto initialState : initialStates) {
if (!relevantStates.get(initialState)) {
continue;
}
distances[initialState] = zeroDistance;
dijkstraQueue.emplace(zeroDistance, initialState);
lowerDistances[initialState] = zeroDistance;
upperDistances[initialState] = zeroDistance;
dijkstraQueue.emplace(zeroDistance, initialState, true);
dijkstraQueue.emplace(zeroDistance, initialState, false);
}
// For some heuristics, we need to potentially find more than just one pivot.
bool considerDeviation = (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation || pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) && lowerValues && upperValues;
bool foundPivotState = false;
ExplicitDijkstraQueueElement<ValueType> pivotState(inftyDistance, 0, true);
ValueType pivotStateDeviation = storm::utility::zero<ValueType>();
auto const& player2Grouping = transitionMatrix.getRowGroupIndices();
storm::storage::BitVector visitedStates(initialStates.size());
while (!dijkstraQueue.empty()) {
auto distanceStatePair = *dijkstraQueue.begin();
uint64_t currentState = distanceStatePair.second;
visitedStates.set(currentState);
std::cout << "current: " << currentState << std::endl;
std::cout << "visited: " << visitedStates << std::endl;
ValueType currentDistance = distanceStatePair.first;
// Take out currently best state.
auto currentDijkstraElement = *dijkstraQueue.begin();
ValueType currentDistance = currentDijkstraElement.distance;
uint64_t currentState = currentDijkstraElement.state;
bool currentLower = currentDijkstraElement.lower;
dijkstraQueue.erase(dijkstraQueue.begin());
if (foundPivotState && (probabilityDistances ? currentDistance < result.distance : currentDistance > result.distance)) {
if (foundPivotState && (probabilityDistances ? currentDistance < pivotState.distance : currentDistance > pivotState.distance)) {
if (pivotSelectionHeuristic != storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) {
// For the nearest maximal deviation and most probable path heuristics, future pivot states are
// not important any more, because their distance will be strictly larger, so we can return the
// current pivot state.
return result;
return ExplicitPivotStateResult<ValueType>(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors));
} else if (pivotStateDeviation >= currentDistance) {
// If the heuristic is maximal weighted deviation and the weighted deviation for any future pivot
// state is necessarily at most as high as the current one, we can abort the search.
return result;
return ExplicitPivotStateResult<ValueType>(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors));
}
}
@ -1128,19 +1199,21 @@ namespace storm {
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) {
isPivotState = true;
}
} else if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
}
if (!isPivotState && maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState);
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) {
isPivotState = true;
}
}
// If it is indeed a pivot state, we can abort the search here.
// If it is indeed a pivot state, we can potentially abort the search here.
if (isPivotState) {
if (considerDeviation && foundPivotState) {
ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState];
if (deviationOfCurrentState > pivotStateDeviation) {
result.pivotState = currentState;
pivotState = currentDijkstraElement;
pivotStateDeviation = deviationOfCurrentState;
if (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) {
// Scale the deviation with the distance (probability) for this heuristic.
@ -1148,71 +1221,25 @@ namespace storm {
}
}
} else if (!foundPivotState) {
result.pivotState = currentState;
result.distance = distances[currentState];
pivotState = currentDijkstraElement;
foundPivotState = true;
}
// If there is no need to look at other deviations, stop here.
if (!considerDeviation) {
return result;
return ExplicitPivotStateResult<ValueType>(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors));
}
}
// TODO: remember the strategy from which we came and only go on to explore that further?
// Otherwise, we explore all its relevant successors.
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t minPlayer2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState);
uint64_t minPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor);
STORM_LOG_ASSERT(!maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(minPlayer2Successor) || minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor) == minPlayer2Choice, "Did not expect deviation in player 2 strategy.");
STORM_LOG_ASSERT(player2Grouping[minPlayer2Successor] <= minPlayer2Choice && minPlayer2Choice < player2Grouping[minPlayer2Successor + 1], "Illegal choice for player 2.");
for (auto const& entry : transitionMatrix.getRow(minPlayer2Choice)) {
uint64_t player1Successor = entry.getColumn();
if (!relevantStates.get(player1Successor)) {
continue;
}
ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) {
distances[player1Successor] = alternateDistance;
if (generatePredecessors) {
result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[minPlayer2Successor]);
}
dijkstraQueue.emplace(alternateDistance, player1Successor);
}
}
} else {
STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting min strategy for non-target states.");
}
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t maxPlayer2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState);
uint64_t maxPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor);
STORM_LOG_ASSERT(!minStrategyPair.getPlayer2Strategy().hasDefinedChoice(maxPlayer2Successor) || minStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor) == maxPlayer2Choice, "Did not expect deviation in player 2 strategy.");
STORM_LOG_ASSERT(player2Grouping[maxPlayer2Successor] <= maxPlayer2Choice && maxPlayer2Choice < player2Grouping[maxPlayer2Successor + 1], "Illegal choice for player 2.");
for (auto const& entry : transitionMatrix.getRow(maxPlayer2Choice)) {
uint64_t player1Successor = entry.getColumn();
if (!relevantStates.get(player1Successor)) {
continue;
}
ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) {
distances[player1Successor] = alternateDistance;
if (generatePredecessors) {
result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[maxPlayer2Successor]);
}
dijkstraQueue.emplace(alternateDistance, player1Successor);
}
}
if (currentLower) {
performDijkstraStep(dijkstraQueue, probabilityDistances, lowerDistances, lowerPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, minStrategyPair, maxStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates);
} else {
STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting max strategy for non-target states.");
performDijkstraStep(dijkstraQueue, probabilityDistances, upperDistances, upperPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, maxStrategyPair, minStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates);
}
}
if (foundPivotState) {
ExplicitPivotStateResult<ValueType> result;
return result;
}

3
src/storm/abstraction/MenuGameRefiner.h
View File

@ -76,6 +76,9 @@ namespace storm {
template<typename ValueType>
struct ExplicitPivotStateResult {
ExplicitPivotStateResult() = default;
ExplicitPivotStateResult(uint64_t pivotState, ValueType distance, std::vector<std::pair<uint64_t, uint64_t>>&& predecessors) : pivotState(pivotState), distance(distance), predecessors(std::move(predecessors)) {
// Intentionally left empty.
}
uint64_t pivotState;

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

@ -59,7 +59,7 @@ namespace storm {
using detail::PreviousExplicitResult;
template<storm::dd::DdType Type, typename ModelType>
GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision() * 2, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()) {
GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision() * 2, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()), debug(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isDebugSet()) {
STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants. Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants.");
@ -529,6 +529,8 @@ namespace storm {
// Optimization: do not compute both bounds if not necessary (e.g. if bound given and exceeded, etc.)
totalWatch.start();
// Set up initial predicates.
std::vector<storm::expressions::Expression> initialPredicates = getInitialPredicates(constraintExpression, targetStateExpression);
@ -563,10 +565,11 @@ namespace storm {
STORM_LOG_TRACE("Starting iteration " << iteration << ".");
// (1) build the abstraction.
auto abstractionStart = std::chrono::high_resolution_clock::now();
storm::utility::Stopwatch abstractionWatch(true);
storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
auto abstractionEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
abstractionWatch.stop();
totalAbstractionWatch.add(abstractionWatch);
STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << abstractionWatch.getTimeInMilliseconds() << "ms).");
// (2) Prepare initial, constraint and target state BDDs for later use.
storm::dd::Bdd<Type> initialStates = game.getInitialStates();
@ -592,7 +595,8 @@ namespace storm {
}
if (result) {
printStatistics(*abstractor, game);
totalWatch.stop();
printStatistics(*abstractor, game, iteration);
return result;
}
@ -600,6 +604,8 @@ namespace storm {
STORM_LOG_INFO("Iteration " << iteration << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(iterationEnd - iterationStart).count() << "ms.");
}
totalWatch.stop();
// If this point is reached, we have given up on abstraction.
STORM_LOG_WARN("Could not derive result, maximal number of abstractions exceeded.");
return nullptr;
@ -614,15 +620,16 @@ namespace storm {
storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
// (1) 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();
storm::utility::Stopwatch qualitativeWatch(true);
SymbolicQualitativeGameResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
if (result) {
return result;
}
previousQualitativeResult = qualitativeResult;
auto qualitativeEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Qualitative computation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
qualitativeWatch.stop();
totalSolutionWatch.add(qualitativeWatch);
STORM_LOG_INFO("Qualitative computation completed in " << qualitativeWatch.getTimeInMilliseconds() << "ms.");
// (2) compute the states for which we have to determine quantitative information.
storm::dd::Bdd<Type> maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates();
@ -639,10 +646,11 @@ 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.
auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now();
storm::utility::Stopwatch refinementWatch(true);
qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult);
auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
refinementWatch.stop();
totalRefinementWatch.add(refinementWatch);
STORM_LOG_INFO("Qualitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms.");
}
// (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
@ -652,27 +660,31 @@ namespace storm {
storm::dd::Add<Type, ValueType> initialStatesAdd = initialStates.template toAdd<ValueType>();
auto quantitativeStart = std::chrono::high_resolution_clock::now();
SymbolicQuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
// (7) Solve the min values and check whether we can give the answer already.
storm::utility::Stopwatch quantitativeWatch(true);
quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
quantitativeWatch.stop();
previousMinQuantitativeResult = quantitativeResult.min;
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange());
if (result) {
totalSolutionWatch.add(quantitativeWatch);
return result;
}
// (8) Solve the max values and check whether we can give the answer already.
quantitativeWatch.start();
quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
quantitativeWatch.stop();
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange());
if (result) {
totalSolutionWatch.add(quantitativeWatch);
return result;
}
auto quantitativeEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
totalSolutionWatch.add(quantitativeWatch);
STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
// (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
@ -686,25 +698,118 @@ namespace storm {
STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now();
// (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.
storm::utility::Stopwatch refinementWatch(true);
refiner.refine(game, transitionMatrixBdd, quantitativeResult);
auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
refinementWatch.stop();
totalRefinementWatch.add(refinementWatch);
STORM_LOG_INFO("Quantitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms.");
}
// Return null to indicate no result has been found yet.
return nullptr;
}
template <typename ValueType>
void postProcessStrategies(abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, bool sanityCheck) {
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << ".");
STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << ".");
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ").");
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) {
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) {
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
if (sanityCheck) {
STORM_LOG_TRACE("[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice);
}
}
}
}
}
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ").");
uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) {
minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice);
STORM_LOG_TRACE("[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice);
}
}
}
}
}
if (sanityCheck) {
///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should
///////// still be the lower ones.
storm::storage::SparseMatrixBuilder<ValueType> dtmcMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
if (targetStates.get(state)) {
dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one<ValueType>());
} else {
uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minStrategyPair.getPlayer1Strategy().getChoice(state));
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue());
}
}
}
auto dtmcMatrix = dtmcMatrixBuilder.build();
std::vector<ValueType> sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]) < 1e-4, "Got weird min divergences!");
}
///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should
///////// still be the upper ones.
dtmcMatrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(player1Groups.size() - 1, player1Groups.size() - 1);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
if (targetStates.get(state)) {
dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one<ValueType>());
} else {
uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state));
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue());
}
}
}
dtmcMatrix = dtmcMatrixBuilder.build();
sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]) < 1e-4, "Got weird max divergences!");
}
}
}
template<storm::dd::DdType Type, typename ModelType>
std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStatesBdd, storm::dd::Bdd<Type> const& constraintStatesBdd, storm::dd::Bdd<Type> const& targetStatesBdd, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<PreviousExplicitResult<ValueType>>& previousResult) {
STORM_LOG_TRACE("Using sparse solving.");
// (0) Start by transforming the necessary symbolic elements to explicit ones.
auto translationStart = std::chrono::high_resolution_clock::now();
storm::utility::Stopwatch translationWatch(true);
storm::dd::Odd odd = game.getReachableStates().createOdd();
std::vector<std::set<storm::expressions::Variable>> labelingVariableSets = {game.getPlayer1Variables(), game.getPlayer2Variables()};
@ -756,22 +861,25 @@ namespace storm {
storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd);
storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd);
storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd);
auto translationEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Translation to explicit representation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(translationEnd - translationStart).count() << "ms.");
translationWatch.stop();
totalTranslationWatch.add(translationWatch);
STORM_LOG_INFO("Translation to explicit representation completed in " << translationWatch.getTimeInMilliseconds() << "ms.");
// Prepare the two strategies.
abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount());
abstraction::ExplicitGameStrategyPair maxStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount());
// (1) 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();
storm::utility::Stopwatch qualitativeWatch(true);
ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousResult, odd, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair);
qualitativeWatch.stop();
totalSolutionWatch.add(qualitativeWatch);
STORM_LOG_INFO("Qualitative computation completed in " << qualitativeWatch.getTimeInMilliseconds() << "ms.");
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<ValueType>(checkTask, initialStates, qualitativeResult);
if (result) {
return result;
}
auto qualitativeEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Qualitative computation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
// (2) compute the states for which we have to determine quantitative information.
storm::storage::BitVector maybeMin = ~(qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates());
@ -788,10 +896,11 @@ 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.
auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now();
storm::utility::Stopwatch refinementWatch(true);
qualitativeRefinement = refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
refinementWatch.stop();
totalRefinementWatch.add(refinementWatch);
STORM_LOG_INFO("Qualitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms.");
}
ExplicitQuantitativeResultMinMax<ValueType> quantitativeResult;
@ -802,132 +911,45 @@ namespace storm {
STORM_LOG_TRACE("Starting numerical solution step.");
// (7) Solve the min values and check whether we can give the answer already.
auto quantitativeStart = std::chrono::high_resolution_clock::now();
storm::utility::Stopwatch quantitativeWatch(true);
quantitativeResult.setMin(computeQuantitativeResult<ValueType>(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair, odd, nullptr, nullptr, this->reuseQuantitativeResults ? previousResult : boost::none));
quantitativeWatch.stop();
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates));
if (result) {
totalSolutionWatch.add(quantitativeWatch);
return result;
}
// (8) Solve the max values and check whether we can give the answer already.
quantitativeWatch.start();
quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair));
quantitativeWatch.stop();
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates));
if (result) {
totalSolutionWatch.add(quantitativeWatch);
return result;
}
auto quantitativeEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
// (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.getMin().getRange(initialStates).first, quantitativeResult.getMax().getRange(initialStates).second, comparator);
if (result) {
return result;
}
// std::cout << "target states " << targetStates << std::endl;
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
std::cout << "state " << state << " has values [" << quantitativeResult.getMin().getValues()[state] << ", " << quantitativeResult.getMax().getValues()[state] << "]" << std::endl;
STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << ".");
STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << ".");
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ").");
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) {
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) {
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
std::cout << "[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice << std::endl;
}
}
}
}
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ").");
uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) {
minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice);
std::cout << "[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice << std::endl;
}
}
}
}
}
///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should
///////// still be the lower ones.
storm::storage::SparseMatrixBuilder<ValueType> dtmcMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
if (targetStates.get(state)) {
dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one<ValueType>());
} else {
uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minStrategyPair.getPlayer1Strategy().getChoice(state));
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue());
}
}
}
auto dtmcMatrix = dtmcMatrixBuilder.build();
std::vector<ValueType> sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
std::cout << "state " << state << ": " << sanityValues[state] << " vs " << quantitativeResult.getMin().getValues()[state] << std::endl;
std::cout << "[min] state is prob0? " << qualitativeResult.getProb0Min().getStates().get(state) << ", prob1? " << qualitativeResult.getProb1Min().getStates().get(state) << std::endl;
STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]) < 1e-6, "Got weird min divergences!");
}
///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should
///////// still be the upper ones.
dtmcMatrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(player1Groups.size() - 1, player1Groups.size() - 1);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
if (targetStates.get(state)) {
dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one<ValueType>());
} else {
uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state));
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue());
}
}
}
dtmcMatrix = dtmcMatrixBuilder.build();
sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false);
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
std::cout << "state " << state << ": " << sanityValues[state] << " vs " << quantitativeResult.getMax().getValues()[state] << std::endl;
std::cout << "[max] state is prob0? " << qualitativeResult.getProb0Max().getStates().get(state) << ", prob1? " << qualitativeResult.getProb1Max().getStates().get(state) << std::endl;
STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]) < 1e-6, "Got weird max divergences!");
}
postProcessStrategies(minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->debug);
// Make sure that all strategies are still valid strategies.
STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << ".");
STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << maxStrategyPair.getNumberOfUndefinedPlayer1States() << ".");
auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now();
// (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.
storm::utility::Stopwatch refinementWatch(true);
refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair);
auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
refinementWatch.stop();
totalRefinementWatch.add(refinementWatch);
STORM_LOG_INFO("Quantitative refinement completed in " << refinementWatch.getTimeInMilliseconds() << "ms.");
if (this->reuseQuantitativeResults) {
PreviousExplicitResult<ValueType> nextPreviousResult;
@ -1106,15 +1128,37 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ModelType>
void GameBasedMdpModelChecker<Type, ModelType>::printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const {
void GameBasedMdpModelChecker<Type, ModelType>::printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements) const {
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
storm::abstraction::AbstractionInformation<Type> const& abstractionInformation = abstractor.getAbstractionInformation();
std::streamsize originalPrecision = std::cout.precision();
std::cout << std::fixed << std::setprecision(2);
std::cout << std::endl;
std::cout << "Statistics:" << std::endl;
std::cout << " * player 1 states (final game): " << game.getReachableStates().getNonZeroCount() << std::endl;
std::cout << " * size of final game: " << game.getReachableStates().getNonZeroCount() << " player 1 states" << std::endl;
std::cout << " * transitions (final game): " << game.getTransitionMatrix().getNonZeroCount() << std::endl;
std::cout << " * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl;
std::cout << " * refinements: " << refinements << std::endl;
std::cout << " * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl << std::endl;
uint64_t totalAbstractionTimeMillis = totalAbstractionWatch.getTimeInMilliseconds();
uint64_t totalTranslationTimeMillis = totalTranslationWatch.getTimeInMilliseconds();
uint64_t totalSolutionTimeMillis = totalSolutionWatch.getTimeInMilliseconds();
uint64_t totalRefinementTimeMillis = totalRefinementWatch.getTimeInMilliseconds();
uint64_t totalTimeMillis = totalWatch.getTimeInMilliseconds();
std::cout << "Time breakdown:" << std::endl;
std::cout << " * abstraction: " << totalAbstractionTimeMillis << "ms (" << 100 * static_cast<double>(totalAbstractionTimeMillis)/totalTimeMillis << "%)" << std::endl;
if (this->solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Sparse) {
std::cout << " * translation: " << totalTranslationTimeMillis << "ms (" << 100 * static_cast<double>(totalTranslationTimeMillis)/totalTimeMillis << "%)" << std::endl;
}
std::cout << " * solution: " << totalSolutionTimeMillis << "ms (" << 100 * static_cast<double>(totalSolutionTimeMillis)/totalTimeMillis << "%)" << std::endl;
std::cout << " * refinement: " << totalRefinementTimeMillis << "ms (" << 100 * static_cast<double>(totalRefinementTimeMillis)/totalTimeMillis << "%)" << std::endl;
std::cout << " ---------------------------------------------" << std::endl;
std::cout << " * total: " << totalTimeMillis << "ms" << std::endl << std::endl;
std::cout << std::defaultfloat << std::setprecision(originalPrecision);
}
}

13
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
View File

@ -21,6 +21,7 @@
#include "storm/utility/ConstantsComparator.h"
#include "storm/utility/solver.h"
#include "storm/utility/graph.h"
#include "storm/utility/Stopwatch.h"
namespace storm {
namespace abstraction {
@ -114,7 +115,7 @@ namespace storm {
ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<detail::PreviousExplicitResult<ValueType>> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair);
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements) const;
/*
* Retrieves the expression characterized by the formula. The formula needs to be propositional.
@ -148,6 +149,16 @@ namespace storm {
/// The performed number of refinement iterations.
uint64_t iteration;
/// A flag that indicates whether debug mode is enabled.
bool debug;
/// Data stored for statistics.
storm::utility::Stopwatch totalAbstractionWatch;
storm::utility::Stopwatch totalSolutionWatch;
storm::utility::Stopwatch totalRefinementWatch;
storm::utility::Stopwatch totalTranslationWatch;
storm::utility::Stopwatch totalWatch;
};
}
}

21
src/storm/utility/Stopwatch.cpp
View File

@ -3,7 +3,7 @@
namespace storm {
namespace utility {
Stopwatch::Stopwatch(bool startNow) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
Stopwatch::Stopwatch(bool startNow) : accumulatedTime(std::chrono::nanoseconds::zero()), isStopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
if (startNow) {
start();
}
@ -25,21 +25,30 @@ namespace storm {
accumulatedTime += timeNanoseconds;
}
void Stopwatch::add(Stopwatch const& other) {
STORM_LOG_WARN_COND(other.stopped(), "Expected stopped watch.");
accumulatedTime += other.accumulatedTime;
}
void Stopwatch::stop() {
STORM_LOG_WARN_COND(!stopped, "Stopwatch is already paused.");
stopped = true;
STORM_LOG_WARN_COND(!isStopped, "Stopwatch is already paused.");
isStopped = true;
accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement;
}
void Stopwatch::start() {
STORM_LOG_WARN_COND(stopped, "Stopwatch is already running.");
stopped = false;
STORM_LOG_WARN_COND(isStopped, "Stopwatch is already running.");
isStopped = false;
startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
}
void Stopwatch::reset() {
accumulatedTime = std::chrono::nanoseconds::zero();
stopped = true;
isStopped = true;
}
bool Stopwatch::stopped() const {
return isStopped;
}
std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {

12
src/storm/utility/Stopwatch.h
View File

@ -46,6 +46,11 @@ namespace storm {
*/
void addToTime(std::chrono::nanoseconds timeNanoseconds);
/*!
* Adds the value of the (stopped) watch to the accumulated time of this watch.
*/
void add(Stopwatch const& other);
/*!
* Stop stopwatch and add measured time to total time.
*/
@ -60,6 +65,11 @@ namespace storm {
* Reset the stopwatch.
*/
void reset();
/*!
* Retrieves whether the watch is stopped.
*/
bool stopped() const;
friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch);
@ -68,7 +78,7 @@ namespace storm {
std::chrono::nanoseconds accumulatedTime;
// A flag indicating if the stopwatch is stopped right now.
bool stopped;
bool isStopped;
// The timepoint when the stopwatch was started the last time (if it's not stopped).
std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;

Write Preview
Loading…
Cancel
Save