From cf648b5bf15bd5ffb6799dfd7333db06ad311f3d Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 19 Jun 2016 18:30:05 +0200 Subject: [PATCH] output of runtimes and other statistics Former-commit-id: 3eaf89f5d584adc837613bf9616b7c336fd584fd --- .../mdp/benchmarks_numerical.sh | 39 +++++++++-- .../SparseMdpMultiObjectiveModelChecker.cpp | 31 ++++++++- src/storm.cpp | 7 ++ src/utility/Stopwatch.h | 68 +++++++++++++++++++ 4 files changed, 138 insertions(+), 7 deletions(-) create mode 100644 src/utility/Stopwatch.h diff --git a/examples/multi-objective/mdp/benchmarks_numerical.sh b/examples/multi-objective/mdp/benchmarks_numerical.sh index 5c80dcb85..e633ad137 100755 --- a/examples/multi-objective/mdp/benchmarks_numerical.sh +++ b/examples/multi-objective/mdp/benchmarks_numerical.sh @@ -3,10 +3,41 @@ mkdir benchmarks_numerical +executable=../../../build/src/Release/storm +options='--precision 0.000001 --multiObjective:precision 0.0001' +modelcommand='-s' +propertycommand='-prop' +logfilepostfix='.storm.output' +$executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_3_2$logfilepostfix +$executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_4_2$logfilepostfix +$executable $modelcommand consensus/consensus2_5_2.nm $propertycommand consensus/consensus2_5_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_5_2$logfilepostfix +$executable $modelcommand consensus/consensus3_3_2.nm $propertycommand consensus/consensus3_3_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus3_3_2$logfilepostfix +$executable $modelcommand consensus/consensus3_4_2.nm $propertycommand consensus/consensus3_4_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus3_4_2$logfilepostfix +$executable $modelcommand consensus/consensus3_5_2.nm $propertycommand consensus/consensus3_5_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus3_5_2$logfilepostfix +$executable $modelcommand zeroconf/zeroconf4.nm $propertycommand zeroconf/zeroconf4_numerical.pctl $options | tee benchmarks_numerical/2_zeroconf4$logfilepostfix +$executable $modelcommand zeroconf/zeroconf6.nm $propertycommand zeroconf/zeroconf6_numerical.pctl $options | tee benchmarks_numerical/2_zeroconf6$logfilepostfix +$executable $modelcommand zeroconf/zeroconf8.nm $propertycommand zeroconf/zeroconf8_numerical.pctl $options | tee benchmarks_numerical/2_zeroconf8$logfilepostfix +$executable $modelcommand zeroconf-tb/zeroconf-tb2_14.nm $propertycommand zeroconf-tb/zeroconf-tb2_14_numerical.pctl $options | tee benchmarks_numerical/3_zeroconf-tb2_14$logfilepostfix +$executable $modelcommand zeroconf-tb/zeroconf-tb4_10.nm $propertycommand zeroconf-tb/zeroconf-tb4_10_numerical.pctl $options | tee benchmarks_numerical/3_zeroconf-tb4_10$logfilepostfix +$executable $modelcommand zeroconf-tb/zeroconf-tb4_14.nm $propertycommand zeroconf-tb/zeroconf-tb4_14_numerical.pctl $options | tee benchmarks_numerical/3_zeroconf-tb4_14$logfilepostfix +$executable $modelcommand team/team2obj_3.nm $propertycommand team/team2obj_3_numerical.pctl $options | tee benchmarks_numerical/4_team2obj_3$logfilepostfix +$executable $modelcommand team/team3obj_3.nm $propertycommand team/team3obj_3_numerical.pctl $options | tee benchmarks_numerical/5_team3obj_3$logfilepostfix +$executable $modelcommand team/team2obj_4.nm $propertycommand team/team2obj_4_numerical.pctl $options | tee benchmarks_numerical/4_team2obj_4$logfilepostfix +$executable $modelcommand team/team3obj_4.nm $propertycommand team/team3obj_4_numerical.pctl $options | tee benchmarks_numerical/5_team3obj_4$logfilepostfix +$executable $modelcommand team/team2obj_5.nm $propertycommand team/team2obj_5_numerical.pctl $options | tee benchmarks_numerical/4_team2obj_5$logfilepostfix +$executable $modelcommand team/team3obj_5.nm $propertycommand team/team3obj_5_numerical.pctl $options | tee benchmarks_numerical/5_team3obj_5$logfilepostfix +$executable $modelcommand scheduler/scheduler05.nm $propertycommand scheduler/scheduler05_numerical.pctl $options | tee benchmarks_numerical/6_scheduler05$logfilepostfix +$executable $modelcommand scheduler/scheduler25.nm $propertycommand scheduler/scheduler25_numerical.pctl $options | tee benchmarks_numerical/6_scheduler25$logfilepostfix +$executable $modelcommand scheduler/scheduler50.nm $propertycommand scheduler/scheduler50_numerical.pctl $options | tee benchmarks_numerical/6_scheduler50$logfilepostfix +$executable $modelcommand dpm/dpm100.nm $propertycommand dpm/dpm100_numerical.pctl $options | tee benchmarks_numerical/7_dpm100$logfilepostfix +$executable $modelcommand dpm/dpm200.nm $propertycommand dpm/dpm200_numerical.pctl $options | tee benchmarks_numerical/7_dpm200$logfilepostfix +$executable $modelcommand dpm/dpm300.nm $propertycommand dpm/dpm300_numerical.pctl $options | tee benchmarks_numerical/7_dpm300$logfilepostfix + + executable=../../../../prism/prism-4.3-src/bin/prism options='-epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g' -modelcommand= -propertycommand= +modelcommand='' +propertycommand='' logfilepostfix='.prism.output' $executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_3_2$logfilepostfix $executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_4_2$logfilepostfix @@ -35,8 +66,8 @@ $executable $modelcommand dpm/dpm300.nm $propertycommand dpm/dpm300_numerical.pc executable=../../../../prism/prism-4.3-src/bin/prism options='-epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs' -modelcommand= -propertycommand= +modelcommand='' +propertycommand='' logfilepostfix='.prism-gs.output' $executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_3_2$logfilepostfix $executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee benchmarks_numerical/1_consensus2_4_2$logfilepostfix diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 6cc793fc4..230cc9f53 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -13,6 +13,8 @@ #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h" +#include "src/utility/Stopwatch.h" + #include "src/exceptions/NotImplementedException.h" namespace storm { @@ -35,20 +37,43 @@ namespace storm { template std::unique_ptr SparseMdpMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported."); + storm::utility::Stopwatch swModelChecking; std::unique_ptr result; #ifdef STORM_HAVE_CARL + storm::utility::Stopwatch swPreprocessing; auto preprocessorData = helper::SparseMultiObjectivePreprocessor::preprocess(checkTask.getFormula(), this->getModel()); + swPreprocessing.pause(); std::cout << std::endl; - std::cout << "Preprocessing done." << std::endl; preprocessorData.printToStream(std::cout); + STORM_LOG_DEBUG("Preprocessing done."); + + storm::utility::Stopwatch swHelper; auto resultData = helper::SparseMultiObjectiveHelper::check(preprocessorData); - std::cout << "Modelchecking done." << std::endl; + swHelper.pause(); + STORM_LOG_DEBUG("Modelchecking done."); + + storm::utility::Stopwatch swPostprocessing; result = helper::SparseMultiObjectivePostprocessor::postprocess(preprocessorData, resultData); - std::cout << "Postprocessing done." << std::endl; + swPostprocessing.pause(); + STORM_LOG_DEBUG("Postprocessing done."); #else STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi objective model checking requires carl."); #endif + std::cout << std::endl; + std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; + std::cout << " Multi-objective Model Checking Statistics: " << std::endl; + std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; + std::cout << std::endl; + std::cout << "Runtimes (in seconds):" << std::endl; + std::cout << "\t Preprocessing: " << std::setw(8) << swPreprocessing << std::endl; + std::cout << "\t Value Iterations: " << std::setw(8) << swHelper << std::endl; + std::cout << "\t Postprocessing: " << std::setw(8) << swPostprocessing << std::endl; + std::cout << "\t Combined: " << std::setw(8) << swModelChecking << std::endl; + std::cout << std::endl; + std::cout << "Performed Refinement Steps: " << resultData.refinementSteps().size() << std::endl; + std::cout << std::endl; + std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; return result; } diff --git a/src/storm.cpp b/src/storm.cpp index 464dda56f..554f771ff 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -3,6 +3,7 @@ #include "src/utility/macros.h" #include "src/cli/cli.h" #include "src/utility/initialize.h" +#include "src/utility/Stopwatch.h" #include "src/settings/SettingsManager.h" @@ -12,6 +13,8 @@ int main(const int argc, const char** argv) { try { + storm::utility::Stopwatch stopwatch; + storm::utility::setUp(); storm::cli::printHeader("SToRM", argc, argv); storm::settings::initializeAll("SToRM", "storm"); @@ -25,6 +28,10 @@ int main(const int argc, const char** argv) { // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); + + storm::cli::printUsage(); + std::cout << "OVERALL_TIME; " << stopwatch << std::endl; + return 0; } catch (storm::exceptions::BaseException const& exception) { STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what()); diff --git a/src/utility/Stopwatch.h b/src/utility/Stopwatch.h new file mode 100644 index 000000000..0af496c54 --- /dev/null +++ b/src/utility/Stopwatch.h @@ -0,0 +1,68 @@ +#ifndef STORM_UTILITY_STOPWATCH_H_ +#define STORM_UTILITY_STOPWATCH_H_ + +#include +#include + +#include "src/utility/macros.h" + +namespace storm { + namespace utility { + // A class that provides convenience operations to display run times. + class Stopwatch { + public: + Stopwatch(double initialValueInSeconds = 0.0) : accumulatedSeconds(initialValueInSeconds), paused(false), startOfCurrentMeasurement(std::chrono::high_resolution_clock::now()) { + // Intentionally left empty + } + + ~Stopwatch() = default; + + double getAccumulatedSeconds() const { + if(paused) { + return accumulatedSeconds; + } else { + return accumulatedSeconds + std::chrono::duration(std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement).count(); + } + } + + void pause() { + if(paused) { + STORM_LOG_WARN("Tried to pause a stopwatch that was already paused."); + } else { + accumulatedSeconds = getAccumulatedSeconds(); + paused = true; + } + } + + void unpause() { + if(paused) { + startOfCurrentMeasurement = std::chrono::high_resolution_clock::now(); + paused = false; + } else { + STORM_LOG_WARN("Tried to unpause a stopwatch that was not paused."); + } + } + + // Note: Does NOT unpause if stopwatch is currently paused. + void reset() { + accumulatedSeconds = 0.0; + startOfCurrentMeasurement = std::chrono::high_resolution_clock::now(); + } + + friend std::ostream& operator<<(std::ostream& out, Stopwatch const& sw) { + out << (round(sw.getAccumulatedSeconds()*1000)/1000); + return out; + } + + + private: + double accumulatedSeconds; + bool paused; + std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement; + + + }; + } +} + +#endif /* STORM_UTILITY_STOPWATCH_H_ */