From 5503e91bb36d2d7a781d8b349f35ab5d0716118a Mon Sep 17 00:00:00 2001 From: PBerger Date: Thu, 5 Jun 2014 00:31:36 +0200 Subject: [PATCH] Added detailed time measurement using std::chrono, leading to more useful information for comparison against Prism, etc. Former-commit-id: 98e3e8e0976c7dcf87d3df9ffda0044538268c28 --- src/storm.cpp | 50 +++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 47 insertions(+), 3 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index c7b40247a..db3f233fb 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -117,8 +117,8 @@ void printUsage() { double userTime = uLargeInteger.QuadPart / 10000.0; std::cout << "CPU Time: " << std::endl; - std::cout << "\tKernel Time: " << std::setprecision(3) << kernelTime << std::endl; - std::cout << "\tUser Time: " << std::setprecision(3) << userTime << 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 } @@ -451,6 +451,9 @@ int main(const int argc, const char* argv[]) { stormSetAlarm(timeout); } + // Execution Time measurement, start + std::chrono::high_resolution_clock::time_point executionStart = std::chrono::high_resolution_clock::now(); + // Now, the settings are received and the specified model is parsed. The actual actions taken depend on whether // the model was provided in explicit or symbolic format. if (s->isSet("explicit")) { @@ -468,6 +471,10 @@ int main(const int argc, const char* argv[]) { std::shared_ptr> model = storm::parser::AutoParser::parseModel(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile); + // Model Parsing Time Measurement, End + std::chrono::high_resolution_clock::time_point parsingEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Parsing the given model took " << std::chrono::duration_cast(parsingEnd - executionStart).count() << " milliseconds." << std::endl; + if (s->isSet("exportdot")) { std::ofstream outputFileStream; outputFileStream.open(s->getOptionByLongName("exportdot").getArgument(0).getValueAsString(), std::ofstream::out); @@ -475,11 +482,16 @@ int main(const int argc, const char* argv[]) { outputFileStream.close(); } - //Should there be a counterexample generated in case the formula is not satisfied? + // Should there be a counterexample generated in case the formula is not satisfied? if(s->isSet("counterexample")) { + // Counterexample Time Measurement, Start + std::chrono::high_resolution_clock::time_point counterexampleStart = std::chrono::high_resolution_clock::now(); generateCounterExample(model); + // Counterexample Time Measurement, End + std::chrono::high_resolution_clock::time_point counterexampleEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Generating the counterexample took " << std::chrono::duration_cast(counterexampleEnd - counterexampleStart).count() << " milliseconds." << std::endl; } else { // Determine which engine is to be used to choose the right model checker. LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); @@ -488,6 +500,9 @@ int main(const int argc, const char* argv[]) { storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; model->printModelInformationToStream(std::cout); + // Modelchecking Time Measurement, Start + std::chrono::high_resolution_clock::time_point modelcheckingStart = std::chrono::high_resolution_clock::now(); + switch (model->getType()) { case storm::models::DTMC: LOG4CPLUS_INFO(logger, "Model is a DTMC."); @@ -529,8 +544,15 @@ int main(const int argc, const char* argv[]) { if (modelchecker != nullptr) { delete modelchecker; } + + // Modelchecking Time Measurement, End + std::chrono::high_resolution_clock::time_point modelcheckingEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Running the ModelChecker took " << std::chrono::duration_cast(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl; } } else if (s->isSet("symbolic")) { + // Program Translation Time Measurement, Start + std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now(); + // First, we build the model using the given symbolic model description and constant definitions. std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); @@ -538,6 +560,10 @@ int main(const int argc, const char* argv[]) { std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); model->printModelInformationToStream(std::cout); + // Program Translation Time Measurement, End + std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl; + if (s->isSet("mincmd")) { if (model->getType() != storm::models::MDP) { LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP."); @@ -549,6 +575,9 @@ int main(const int argc, const char* argv[]) { // Determine whether we are required to use the MILP-version or the SAT-version. bool useMILP = s->getOptionByLongName("mincmd").getArgumentByName("method").getValueAsString() == "milp"; + // MinCMD Time Measurement, Start + std::chrono::high_resolution_clock::time_point minCmdStart = std::chrono::high_resolution_clock::now(); + // Now parse the property file and receive the list of parsed formulas. std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString(); std::list*> formulaList = storm::parser::PrctlFileParser(propertyFile); @@ -564,6 +593,10 @@ int main(const int argc, const char* argv[]) { // Once we are done with the formula, delete it. delete formulaPtr; } + + // MinCMD Time Measurement, End + std::chrono::high_resolution_clock::time_point minCmdEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Minimal command Counterexample generation took " << std::chrono::duration_cast(minCmdStart - minCmdEnd).count() << " milliseconds." << std::endl; } else if (s->isSet("prctl")) { // Determine which engine is to be used to choose the right model checker. LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); @@ -571,6 +604,9 @@ int main(const int argc, const char* argv[]) { // Depending on the model type, the appropriate model checking procedure is chosen. storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; + // Modelchecking Time Measurement, Start + std::chrono::high_resolution_clock::time_point modelcheckingStart = std::chrono::high_resolution_clock::now(); + switch (model->getType()) { case storm::models::DTMC: LOG4CPLUS_INFO(logger, "Model is a DTMC."); @@ -602,8 +638,16 @@ int main(const int argc, const char* argv[]) { if (modelchecker != nullptr) { delete modelchecker; } + + // Modelchecking Time Measurement, End + std::chrono::high_resolution_clock::time_point modelcheckingEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Running the PRCTL ModelChecker took " << std::chrono::duration_cast(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl; } } + + // Execution Time Measurement, End + std::chrono::high_resolution_clock::time_point executionEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Complete execution took " << std::chrono::duration_cast(executionEnd - executionStart).count() << " milliseconds." << std::endl; // Perform clean-up and terminate. cleanUp();