sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

slightly modified stats output and fixed memory measurement under linux

tempestpy_adaptions
dehnert 8 years ago
parent
a7e9c5819f
commit
7af65ac804
3 changed files with 20 additions and 49 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 48
      src/storm/cli/cli.cpp
  2. 19
      src/storm/cli/entrypoints.h
  3. 2
      src/storm/utility/Stopwatch.cpp

48
src/storm/cli/cli.cpp
View File

@ -130,47 +130,23 @@ namespace storm {
} }
void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) { void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) {
#ifndef WINDOWS
struct rusage ru; struct rusage ru;
getrusage(RUSAGE_SELF, &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) { if (wallclockMilliseconds != 0) {
std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl;
std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << 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;
}
GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
ULARGE_INTEGER uLargeInteger;
uLargeInteger.LowPart = ftKernel.dwLowDateTime;
uLargeInteger.HighPart = ftKernel.dwHighDateTime;
double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
uLargeInteger.LowPart = ftUser.dwLowDateTime;
uLargeInteger.HighPart = ftUser.dwHighDateTime;
double userTime = static_cast<double>(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[]) { bool parseOptions(const int argc, const char* argv[]) {

19
src/storm/cli/entrypoints.h
View File

@ -81,11 +81,10 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
modelCheckingWatch.stop(); modelCheckingWatch.stop();
if (result) { 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 (initial states): ");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType()); applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
STORM_PRINT_AND_LOG(std::endl);
STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
} else { } else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
} }
@ -104,11 +103,10 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
modelCheckingWatch.stop(); modelCheckingWatch.stop();
if (result) { 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 (initial states): ");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType()); applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType());
STORM_PRINT_AND_LOG(std::endl);
STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
} else { } else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
} }
@ -130,9 +128,9 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
modelCheckingWatch.stop(); modelCheckingWatch.stop();
if (result) { 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 (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 { } else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
} }
@ -182,10 +180,9 @@ namespace storm {
} }
if (result) { 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 (initial states): ");
applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType()); applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
STORM_PRINT_AND_LOG(std::endl);
STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
} else { } else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
} }
@ -210,11 +207,10 @@ namespace storm {
modelCheckingWatch.stop(); modelCheckingWatch.stop();
if (result) { 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 (initial states): ");
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType()); applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
STORM_PRINT_AND_LOG(std::endl);
STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
} else { } else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
} }
@ -231,11 +227,10 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
modelCheckingWatch.stop(); modelCheckingWatch.stop();
if (result) { 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 (initial states): ");
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType()); applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
STORM_PRINT_AND_LOG(std::endl);
STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
} else { } else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
} }

2
src/storm/utility/Stopwatch.cpp
View File

@ -43,7 +43,7 @@ namespace storm {
} }
std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) { 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; return out;
} }

Write Preview
Loading…
Cancel
Save