diff --git a/src/utility/cli.h b/src/utility/cli.h index e9297d5af..4ae261d0a 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -353,6 +353,8 @@ namespace storm { } // Now we are ready to actually build the model. + std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); + std::chrono::high_resolution_clock::time_point buildingTimeStart = std::chrono::high_resolution_clock::now(); std::shared_ptr> model; if (settings.isExplicitSet()) { model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); @@ -362,13 +364,34 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } - + std::chrono::high_resolution_clock::time_point buildingTimeEnd = std::chrono::high_resolution_clock::now(); + // Now, we can do the preprocessing on the model, if it was requested. + std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now(); model = preprocessModel(model, formula); + std::chrono::high_resolution_clock::time_point preprocessingTimeEnd = std::chrono::high_resolution_clock::now(); + std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); // Print some information about the model. model->printModelInformationToStream(std::cout); + if (storm::settings::generalSettings().isShowStatisticsSet()) { + std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; + std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); + std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart; + std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast(buildingTime); + std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart; + std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast(preprocessingTime); + + STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); + STORM_PRINT_AND_LOG(" * time for building: " << buildingTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for preprocessing: " << preprocessingTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(std::endl); + } + // If we were requested to generate a counterexample, we now do so. if (settings.isCounterexampleSet()) { STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");