From dad51771aa4ec7015cb080e932e2ba281fd04da2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Jan 2017 13:34:33 +0100 Subject: [PATCH] Use stopwatch for in storm-dft --- .../modelchecker/dft/DFTModelChecker.cpp | 60 +++++++++---------- .../modelchecker/dft/DFTModelChecker.h | 16 +++-- 2 files changed, 36 insertions(+), 40 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 2de46e599..caa78060c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -20,13 +20,8 @@ namespace storm { template void DFTModelChecker::check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize - this->explorationTime = std::chrono::duration::zero(); - this->buildingTime = std::chrono::duration::zero(); - this->bisimulationTime = std::chrono::duration::zero(); - this->modelCheckingTime = std::chrono::duration::zero(); - this->totalTime = std::chrono::duration::zero(); this->approximationError = approximationError; - totalStart = std::chrono::high_resolution_clock::now(); + totalTimer.start(); // Optimizing DFT storm::storage::DFT dft = origDft.optimize(); @@ -44,7 +39,7 @@ namespace storm { checkResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; } - this->totalTime = std::chrono::high_resolution_clock::now() - totalStart; + totalTimer.stop(); } template @@ -191,7 +186,7 @@ namespace storm { std::shared_ptr> composedModel; for (auto const ft : dfts) { STORM_LOG_INFO("Building Model via parallel composition..."); - std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now(); + explorationTimer.start(); // Find symmetries std::map>> emptySymmetry; @@ -212,7 +207,7 @@ namespace storm { //model->printModelInformationToStream(std::cout); STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTime += std::chrono::high_resolution_clock::now() - checkingStart; + explorationTimer.stop(); STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); std::shared_ptr> ctmc = model->template as>(); @@ -227,10 +222,10 @@ namespace storm { } // Apply bisimulation - std::chrono::high_resolution_clock::time_point bisimulationStart = std::chrono::high_resolution_clock::now(); + bisimulationTimer.start(); composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now(); - bisimulationTime += bisimulationEnd - bisimulationStart; + bisimulationTimer.stop(); STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); @@ -247,7 +242,7 @@ namespace storm { // If we are here, no composition was possible STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now(); + explorationTimer.start(); // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); @@ -268,7 +263,7 @@ namespace storm { //model->printModelInformationToStream(std::cout); STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTime += std::chrono::high_resolution_clock::now() - checkingStart; + explorationTimer.stop(); STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); return model->template as>(); @@ -276,7 +271,7 @@ namespace storm { template typename DFTModelChecker::dft_result DFTModelChecker::checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError) { - std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now(); + explorationTimer.start(); // Find symmetries std::map>> emptySymmetry; @@ -302,12 +297,14 @@ namespace storm { size_t iteration = 0; do { // Iteratively build finer models - std::chrono::high_resolution_clock::time_point explorationStart = std::chrono::high_resolution_clock::now(); + if (iteration > 0) { + explorationTimer.start(); + } STORM_LOG_INFO("Building model..."); // TODO Matthias refine model using existing model and MC results builder.buildModel(labeloptions, iteration, approximationError); - std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now(); - explorationTime += explorationEnd - explorationStart; + explorationTimer.stop(); + buildingTimer.start(); // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one? @@ -317,7 +314,7 @@ namespace storm { // We only output the info from the lower bound as the info for the upper bound is the same STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); - buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd; + buildingTimer.stop(); // Check lower bound std::unique_ptr result = checkModel(model, formula); @@ -328,9 +325,9 @@ namespace storm { // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); - explorationEnd = std::chrono::high_resolution_clock::now(); + buildingTimer.start(); model = builder.getModelApproximation(probabilityFormula ? true : false); - buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd; + buildingTimer.stop(); // Check upper bound result = checkModel(model, formula); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); @@ -340,8 +337,9 @@ namespace storm { ++iteration; STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); - totalTime = std::chrono::high_resolution_clock::now() - totalStart; + totalTimer.stop(); printTimings(); + totalTimer.start(); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); @@ -365,7 +363,7 @@ namespace storm { //model->printModelInformationToStream(std::cout); STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTime += std::chrono::high_resolution_clock::now() - checkingStart; + explorationTimer.stop(); // Model checking std::unique_ptr result = checkModel(model, formula); @@ -377,22 +375,22 @@ namespace storm { template std::unique_ptr DFTModelChecker::checkModel(std::shared_ptr>& model, std::shared_ptr const& formula) { // Bisimulation - std::chrono::high_resolution_clock::time_point bisimulationStart = std::chrono::high_resolution_clock::now(); + bisimulationTimer.start(); if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { STORM_LOG_INFO("Bisimulation..."); model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); } - std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now(); - bisimulationTime += bisimulationEnd - bisimulationStart; + bisimulationTimer.stop(); + modelCheckingTimer.start(); // Check the model STORM_LOG_INFO("Model checking..."); std::unique_ptr result(storm::verifySparseModel(model, formula)); STORM_LOG_INFO("Model checking done."); STORM_LOG_ASSERT(result, "Result does not exist."); - modelCheckingTime += std::chrono::high_resolution_clock::now() - bisimulationEnd; + modelCheckingTimer.stop(); return result; } @@ -414,11 +412,11 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Exploration:\t" << explorationTime.count() << std::endl; - os << "Building:\t" << buildingTime.count() << std::endl; - os << "Bisimulation:\t" << bisimulationTime.count() << std::endl; - os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl; - os << "Total:\t\t" << totalTime.count() << std::endl; + os << "Exploration:\t" << explorationTimer.getTimeSeconds() << "s" << std::endl; + os << "Building:\t" << buildingTimer.getTimeSeconds() << "s" << std::endl; + os << "Bisimulation:\t" << bisimulationTimer.getTimeSeconds() << "s" << std::endl; + os << "Modelchecking:\t" << modelCheckingTimer.getTimeSeconds() << "s" << std::endl; + os << "Total:\t\t" << totalTimer.getTimeSeconds() << "s" << std::endl; } template diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 7cee7b0e4..c714999a8 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -3,11 +3,10 @@ #include "storm/logic/Formula.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/utility/storm.h" // TODO this should not be included here. +#include "storm/utility/Stopwatch.h" #include "storm-dft/storage/dft/DFT.h" -#include - namespace storm { namespace modelchecker { @@ -57,12 +56,11 @@ namespace storm { private: // Timing values - std::chrono::duration buildingTime = std::chrono::duration::zero(); - std::chrono::duration explorationTime = std::chrono::duration::zero(); - std::chrono::duration bisimulationTime = std::chrono::duration::zero(); - std::chrono::duration modelCheckingTime = std::chrono::duration::zero(); - std::chrono::duration totalTime = std::chrono::duration::zero(); - std::chrono::high_resolution_clock::time_point totalStart; + storm::utility::Stopwatch buildingTimer; + storm::utility::Stopwatch explorationTimer; + storm::utility::Stopwatch bisimulationTimer; + storm::utility::Stopwatch modelCheckingTimer; + storm::utility::Stopwatch totalTimer; // Model checking result dft_result checkResult; @@ -137,4 +135,4 @@ namespace storm { }; } -} \ No newline at end of file +}