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 initialPredicates = getInitialPredicates(constraintExpression, targetStateExpression); // Derive the optimization direction for player 1 (assuming menu-game abstraction). @@ -558,6 +559,7 @@ namespace storm { storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); + setupWatch.stop(); // Enter the main-loop of abstraction refinement. boost::optional> 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(totalSetupTime)/totalTimeMillis << "%)" << std::endl; std::cout << " * abstraction: " << totalAbstractionTimeMillis << "ms (" << 100 * static_cast(totalAbstractionTimeMillis)/totalTimeMillis << "%)" << std::endl; if (this->solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Sparse) { std::cout << " * translation: " << totalTranslationTimeMillis << "ms (" << 100 * static_cast(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; }; }