From 7af65ac804183c3a711c4446565346eab5523839 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 14 Jan 2017 21:54:47 +0100 Subject: [PATCH] slightly modified stats output and fixed memory measurement under linux --- src/storm/cli/cli.cpp | 48 +++++++++------------------------ src/storm/cli/entrypoints.h | 19 +++++-------- src/storm/utility/Stopwatch.cpp | 2 +- 3 files changed, 20 insertions(+), 49 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 7d0d514cb..a8e02dd46 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -130,47 +130,23 @@ namespace storm { } void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) { -#ifndef WINDOWS struct rusage ru; getrusage(RUSAGE_SELF, &ru); - std::cout << "Performance statistics:" << std::endl; - std::cout << " * peak memory usage: " << ru.ru_maxrss/1024/1024 << " mb" << std::endl; - std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << std::endl << "Performance statistics:" << std::endl; +#ifdef MACOS + // For Mac OS, this is returned in bytes. + uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024; +#endif +#ifdef LINUX + // For Linux, this is returned in kilobytes. + uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024; +#endif + std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl; + std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << "s" << std::endl; if (wallclockMilliseconds != 0) { - std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl; - } -#else - HANDLE hProcess = GetCurrentProcess (); - FILETIME ftCreation, ftExit, ftUser, ftKernel; - PROCESS_MEMORY_COUNTERS pmc; - if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { - std::cout << "Memory Usage: " << std::endl; - std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; - std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; - std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; - std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; - std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; - std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; - std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; - std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; - std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; + std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << std::endl; } - - GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); - - ULARGE_INTEGER uLargeInteger; - uLargeInteger.LowPart = ftKernel.dwLowDateTime; - uLargeInteger.HighPart = ftKernel.dwHighDateTime; - double kernelTime = static_cast(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds - uLargeInteger.LowPart = ftUser.dwLowDateTime; - uLargeInteger.HighPart = ftUser.dwHighDateTime; - double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; - - std::cout << "CPU Time: " << std::endl; - std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; - std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; -#endif } bool parseOptions(const int argc, const char* argv[]) { diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 4097d0bc3..ce7d62227 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -81,11 +81,10 @@ namespace storm { std::unique_ptr result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); modelCheckingWatch.stop(); if (result) { - STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); STORM_PRINT_AND_LOG("Result (initial states): "); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); - STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); } @@ -104,11 +103,10 @@ namespace storm { std::unique_ptr result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); modelCheckingWatch.stop(); if (result) { - STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); STORM_PRINT_AND_LOG("Result (initial states): "); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); - STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); } @@ -130,9 +128,9 @@ namespace storm { std::unique_ptr result(storm::verifySymbolicModelWithAbstractionRefinementEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); modelCheckingWatch.stop(); if (result) { - STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); STORM_PRINT_AND_LOG("Result (initial states): "); - STORM_PRINT_AND_LOG(*result << std::endl); + STORM_PRINT_AND_LOG(*result); + STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); } @@ -182,10 +180,9 @@ namespace storm { } if (result) { - STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); STORM_PRINT_AND_LOG("Result (initial states): "); applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); - STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); } @@ -210,11 +207,10 @@ namespace storm { modelCheckingWatch.stop(); if (result) { - STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); STORM_PRINT_AND_LOG("Result (initial states): "); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); - STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); } @@ -231,11 +227,10 @@ namespace storm { std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); modelCheckingWatch.stop(); if (result) { - STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); STORM_PRINT_AND_LOG("Result (initial states): "); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); - STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); } diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp index fd77c0d59..faefdb472 100644 --- a/src/storm/utility/Stopwatch.cpp +++ b/src/storm/utility/Stopwatch.cpp @@ -43,7 +43,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) { - out << stopwatch.getTimeInSeconds() << "." << (stopwatch.getTimeInMilliseconds() % 1000) << "s"; + out << stopwatch.getTimeInSeconds() << "." << std::setw(3) << std::setfill('0') << (stopwatch.getTimeInMilliseconds() % 1000) << "s"; return out; }