From c6e28a3bc7a767e271e6579b7f0132902b546b7f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 1 Jun 2018 20:29:18 +0200
Subject: [PATCH] adding setup timer
---
src/storm/abstraction/MenuGameRefiner.cpp | 2 --
.../modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 4 ++++
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h | 1 +
3 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 4ebfc24ce..3ccae8ab4 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -1568,7 +1568,6 @@ namespace storm {
for (auto const& predicate : predicateClass.second) {
bool addPredicate = true;
for (auto const& atom : cleanedAtomsOfClass) {
- ++checkCounter;
if (predicate.areSame(atom)) {
addPredicate = false;
break;
@@ -1601,7 +1600,6 @@ namespace storm {
for (auto const& newAtom : predicateClass.second) {
bool addAtom = true;
for (auto const& oldPredicate : oldPredicateClassIt->second) {
- ++checkCounter;
if (newAtom.areSame(oldPredicate)) {
addAtom = false;
break;
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index f06c91853..6d74d0897 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -535,6 +535,7 @@ namespace storm {
totalWatch.start();
// Set up initial predicates.
+ setupWatch.start();
std::vector<storm::expressions::Expression> initialPredicates = getInitialPredicates(constraintExpression, targetStateExpression);
// Derive the optimization direction for player 1 (assuming menu-game abstraction).
@@ -558,6 +559,7 @@ namespace storm {
storm::dd::Bdd<Type> globalConstraintStates = abstractor->getStates(constraintExpression);
storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);
+ setupWatch.stop();
// Enter the main-loop of abstraction refinement.
boost::optional<SymbolicQualitativeGameResultMinMax<Type>> previousSymbolicQualitativeResult = boost::none;
@@ -1272,9 +1274,11 @@ namespace storm {
uint64_t totalStrategyProcessingTimeMillis = totalStrategyProcessingWatch.getTimeInMilliseconds();
uint64_t totalSolutionTimeMillis = totalSolutionWatch.getTimeInMilliseconds();
uint64_t totalRefinementTimeMillis = totalRefinementWatch.getTimeInMilliseconds();
+ uint64_t setupTime = setupWatch.getTimeInMilliseconds();
uint64_t totalTimeMillis = totalWatch.getTimeInMilliseconds();
std::cout << "Time breakdown:" << std::endl;
+ std::cout << " * setup: " << setupTime << "ms (" << 100 * static_cast<double>(totalSetupTime)/totalTimeMillis << "%)" << 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;
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
index d76eee4f2..0c585f993 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
@@ -168,6 +168,7 @@ namespace storm {
storm::utility::Stopwatch totalRefinementWatch;
storm::utility::Stopwatch totalTranslationWatch;
storm::utility::Stopwatch totalStrategyProcessingWatch;
+ storm::utility::Stopwatch setupWatch;
storm::utility::Stopwatch totalWatch;
};
}