From a6514052da54792c72d3974b7c046164f9da77e9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 4 Dec 2016 18:16:17 +0100
Subject: [PATCH] avoiding dijkstra for interpolation if most-probable path
info is already available
---
src/storm/abstraction/AbstractionInformation.cpp | 1 -
src/storm/abstraction/MenuGameRefiner.cpp | 10 +++++++---
src/storm/abstraction/MenuGameRefiner.h | 1 +
src/storm/abstraction/StateSetAbstractor.cpp | 1 +
src/storm/abstraction/prism/CommandAbstractor.cpp | 3 +++
.../abstraction/GameBasedMdpModelChecker.cpp | 11 ++++++++++-
6 files changed, 22 insertions(+), 5 deletions(-)
diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp
index 4bee18228..ee0878365 100644
--- a/src/storm/abstraction/AbstractionInformation.cpp
+++ b/src/storm/abstraction/AbstractionInformation.cpp
@@ -465,7 +465,6 @@ namespace storm {
template <storm::dd::DdType DdType>
std::tuple<storm::storage::BitVector, uint64_t, uint64_t> AbstractionInformation<DdType>::decodeStatePlayer1ChoiceAndUpdate(storm::dd::Bdd<DdType> const& stateChoiceAndUpdate) const {
- stateChoiceAndUpdate.template toAdd<double>().exportToDot("out.dot");
STORM_LOG_ASSERT(stateChoiceAndUpdate.getNonZeroCount() == 1, "Wrong number of non-zero entries.");
storm::storage::BitVector statePredicates(this->getNumberOfPredicates());
diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 6472b614d..0abca47e0 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -357,8 +357,6 @@ namespace storm {
// Now construct all player 2 choices that actually exist and differ in the min and max case.
constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy);
- minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy).template toAdd<ValueType>().exportToDot("pl2diff.dot");
- constraint.template toAdd<ValueType>().exportToDot("constraint.dot");
// Then restrict the pivot states by requiring existing and different player 2 choices.
result.pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables());
@@ -502,7 +500,12 @@ namespace storm {
AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
// Compute the most probable path from any initial state to the pivot state.
- MostProbablePathsResult<Type, ValueType> mostProbablePathsResult = getMostProbablePathSpanningTree(game, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
+ MostProbablePathsResult<Type, ValueType> mostProbablePathsResult;
+ if (!pivotStateResult.mostProbablePathsResult) {
+ mostProbablePathsResult = getMostProbablePathSpanningTree(game, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
+ } else {
+ mostProbablePathsResult = pivotStateResult.mostProbablePathsResult.get();
+ }
// Create a new expression manager that we can use for the interpolation.
std::shared_ptr<storm::expressions::ExpressionManager> interpolationManager = abstractionInformation.getExpressionManager().clone();
@@ -703,6 +706,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
void MenuGameRefiner<Type, ValueType>::performRefinement(std::vector<RefinementCommand> const& refinementCommands) const {
for (auto const& command : refinementCommands) {
+ STORM_LOG_TRACE("Refining with " << command.getPredicates().size() << " predicates.");
abstractor.get().refine(command);
}
diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h
index e23b03303..e79248509 100644
--- a/src/storm/abstraction/MenuGameRefiner.h
+++ b/src/storm/abstraction/MenuGameRefiner.h
@@ -49,6 +49,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
struct MostProbablePathsResult {
+ MostProbablePathsResult() = default;
MostProbablePathsResult(storm::dd::Add<Type, ValueType> const& maxProbabilities, storm::dd::Bdd<Type> const& spanningTree);
storm::dd::Add<Type, ValueType> maxProbabilities;
diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp
index 456d89c5e..10c392cc5 100644
--- a/src/storm/abstraction/StateSetAbstractor.cpp
+++ b/src/storm/abstraction/StateSetAbstractor.cpp
@@ -80,6 +80,7 @@ namespace storm {
void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() {
// Now check whether we need to recompute the cached BDD.
std::set<uint_fast64_t> newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables);
+
// Since the number of relevant predicates is monotonic, we can simply check for the size here.
STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates.");
bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size();
diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp
index 9d21f1c86..729704a36 100644
--- a/src/storm/abstraction/prism/CommandAbstractor.cpp
+++ b/src/storm/abstraction/prism/CommandAbstractor.cpp
@@ -222,10 +222,13 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
+// std::cout << "new model ----------------" << std::endl;
for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
if (model.getBooleanValue(variableIndexPair.first)) {
+// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is true" << std::endl;
result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
} else {
+// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is false" << std::endl;
result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
}
}
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 49b0af65f..2d80f80eb 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -294,8 +294,10 @@ namespace storm {
STORM_LOG_TRACE("Starting iteration " << iterations << ".");
// (1) build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
+ auto abstractionStart = std::chrono::high_resolution_clock::now();
storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
- STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
+ auto abstractionEnd = std::chrono::high_resolution_clock::now();
+ STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state.");
// (2) Prepare transition matrix BDD and target state BDD for later use.
@@ -340,9 +342,12 @@ namespace storm {
} else {
STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states.");
+ auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now();
// If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
// depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
qualitativeRefinement = refiner.refine(game, transitionMatrixBdd, qualitativeResult);
+ auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
+ STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
}
}
@@ -389,9 +394,13 @@ namespace storm {
STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.isZero() || quantitativeResult.min.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.isZero() || quantitativeResult.max.player2Strategy.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.
refiner.refine(game, transitionMatrixBdd, quantitativeResult);
+ auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
+ STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
+
}
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.");