From 29855e285388522073a290efa6d644f5c689c129 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Jul 2017 19:52:39 +0200 Subject: [PATCH] added option to display information about exploration progress to both jit and explicit builder --- src/storm/builder/BuilderOptions.cpp | 12 ++++- src/storm/builder/BuilderOptions.h | 8 ++++ src/storm/builder/ExplicitModelBuilder.cpp | 20 +++++++++ .../jit/ExplicitJitJaniModelBuilder.cpp | 44 +++++++++++++++++-- src/storm/settings/modules/IOSettings.cpp | 12 +++++ src/storm/settings/modules/IOSettings.h | 16 +++++++ 6 files changed, 108 insertions(+), 4 deletions(-) diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 453f2e548..6e42745fd 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -35,7 +35,7 @@ namespace storm { return boost::get(labelOrExpression); } - BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false) { + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), explorationShowProgress(false), explorationShowProgressDelay(0) { // Intentionally left empty. } @@ -55,6 +55,8 @@ namespace storm { } explorationChecks = storm::settings::getModule().isExplorationChecksSet(); + explorationShowProgress = storm::settings::getModule().isExplorationShowProgressSet(); + explorationShowProgressDelay = storm::settings::getModule().getExplorationShowProgressDelay(); } void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) { @@ -163,6 +165,14 @@ namespace storm { bool BuilderOptions::isExplorationChecksSet() const { return explorationChecks; } + + bool BuilderOptions::isExplorationShowProgressSet() const { + return explorationShowProgress; + } + + uint64_t BuilderOptions::getExplorationShowProgressDelay() const { + return explorationShowProgressDelay; + } BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) { explorationChecks = newValue; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index b2923f4f5..a06de50eb 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -94,6 +94,8 @@ namespace storm { bool isBuildAllRewardModelsSet() const; bool isBuildAllLabelsSet() const; bool isExplorationChecksSet() const; + bool isExplorationShowProgressSet() const; + uint64_t getExplorationShowProgressDelay() const; BuilderOptions& setBuildAllRewardModels(); BuilderOptions& addRewardModel(std::string const& rewardModelName); @@ -139,6 +141,12 @@ namespace storm { /// A flag that stores whether exploration checks are to be performed. bool explorationChecks; + + /// A flag that stores whether the progress of exploration is to be printed. + bool explorationShowProgress; + + /// The delay for printing progress information. + uint64_t explorationShowProgressDelay; }; } diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 5add225ce..9de544e7b 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -131,6 +131,11 @@ namespace storm { uint_fast64_t currentRowGroup = 0; uint_fast64_t currentRow = 0; + auto timeOfStart = std::chrono::high_resolution_clock::now(); + auto timeOfLastMessage = std::chrono::high_resolution_clock::now(); + uint64_t numberOfExploredStates = 0; + uint64_t numberOfExploredStatesSinceLastMessage = 0; + // Perform a search through the model. while (!statesToExplore.empty()) { // Get the first state in the queue. @@ -234,6 +239,21 @@ namespace storm { } ++currentRowGroup; } + + if (generator->getOptions().isExplorationShowProgressSet()) { + ++numberOfExploredStatesSinceLastMessage; + ++numberOfExploredStates; + + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= generator->getOptions().getExplorationShowProgressDelay()) { + auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage; + auto durationSinceStart = std::chrono::duration_cast(now - timeOfStart).count(); + std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl; + timeOfLastMessage = std::chrono::high_resolution_clock::now(); + numberOfExploredStatesSinceLastMessage = 0; + } + } } if (markovianStates) { diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 5547a71d4..67ff3be5d 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -527,6 +527,15 @@ namespace storm { } modelData["exploration_checks"] = cpptempl::make_data(list); list = cpptempl::data_list(); + if (options.isExplorationShowProgressSet()) { + list.push_back(cpptempl::data_map()); + } + modelData["expl_progress"] = cpptempl::make_data(list); + + std::stringstream progressDelayStream; + progressDelayStream << options.getExplorationShowProgressDelay(); + modelData["expl_progress_interval"] = cpptempl::make_data(progressDelayStream.str()); + list = cpptempl::data_list(); if (std::is_same::value) { list.push_back(cpptempl::data_map()); } @@ -541,7 +550,7 @@ namespace storm { list.push_back(cpptempl::data_map()); } modelData["double"] = cpptempl::make_data(list); - + list = cpptempl::data_list(); if (storm::settings::getModule().isDontFixDeadlocksSet()) { list.push_back(cpptempl::data_map()); @@ -1646,12 +1655,17 @@ namespace storm { std::string sourceTemplate = R"( #define NDEBUG +{% if expl_progress %} +#define EXPL_PROGRESS +{% endif %} + #include #include #include #include #include #include +#include #include {% if exact %} @@ -2179,7 +2193,7 @@ namespace storm { class JitBuilder : public JitModelBuilderInterface { public: - JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) { + JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder), timeOfStart(std::chrono::high_resolution_clock::now()), timeOfLastMessage(std::chrono::high_resolution_clock::now()), numberOfExploredStates(0), numberOfExploredStatesSinceLastMessage(0) { {% for state in initialStates %}{ StateType state; {% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; @@ -2262,6 +2276,7 @@ namespace storm { getOrAddIndex(initialState, statesToExplore); StateBehaviour behaviour; + while (!statesToExplore.empty()) { StateType currentState = statesToExplore.get(); IndexType currentIndex = getIndex(currentState); @@ -2300,6 +2315,21 @@ namespace storm { this->addStateBehaviour(currentIndex, behaviour); behaviour.clear(); + +#ifdef EXPL_PROGRESS + ++numberOfExploredStatesSinceLastMessage; + ++numberOfExploredStates; + + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= {$expl_progress_interval}) { + auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage; + auto durationSinceStart = std::chrono::duration_cast(now - timeOfStart).count(); + std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl; + timeOfLastMessage = std::chrono::high_resolution_clock::now(); + numberOfExploredStatesSinceLastMessage = 0; + } +#endif } } @@ -2395,14 +2425,22 @@ namespace storm { } private: + // State storage. spp::sparse_hash_map stateIds; std::vector initialStates; std::vector deadlockStates; - + + // Edges. {% for edge in nonsynch_edges %}Edge edge_{$edge.name}; {% endfor %} {% for edge in synch_edges %}Edge edge_{$edge.name}; {% endfor %} + + // Statistics. + std::chrono::high_resolution_clock::time_point timeOfStart; + std::chrono::high_resolution_clock::time_point timeOfLastMessage; + uint64_t numberOfExploredStates; + uint64_t numberOfExploredStatesSinceLastMessage; }; BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder) diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 677b78513..7d26b54ac 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -34,6 +34,8 @@ namespace storm { const std::string IOSettings::explorationOrderOptionShortName = "eo"; const std::string IOSettings::explorationChecksOptionName = "explchecks"; const std::string IOSettings::explorationChecksOptionShortName = "ec"; + const std::string IOSettings::explorationShowProgressOptionName = "explprog"; + const std::string IOSettings::explorationShowProgressOptionShortName = "ep"; const std::string IOSettings::transitionRewardsOptionName = "transrew"; const std::string IOSettings::stateRewardsOptionName = "staterew"; const std::string IOSettings::choiceLabelingOptionName = "choicelab"; @@ -84,6 +86,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explorationShowProgressOptionName, false, "Sets when additional information (if available) about the exploration progress is printed.").setShortName(explorationShowProgressOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait between emitting information.").setDefaultValueUnsignedInteger(0).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); @@ -195,6 +198,14 @@ namespace storm { return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); } + bool IOSettings::isExplorationShowProgressSet() const { + return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger() > 0; + } + + uint64_t IOSettings::getExplorationShowProgressDelay() const { + return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger(); + } + bool IOSettings::isTransitionRewardsSet() const { return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); } @@ -268,6 +279,7 @@ namespace storm { } void IOSettings::finalize() { + // Intentionally left empty. } bool IOSettings::check() const { diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 55f777334..e68c6b515 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -179,6 +179,20 @@ namespace storm { */ bool isExplorationChecksSet() const; + /*! + * Retrieves whether to show information about exploration progress. + * + * @return True if information is to be shown. + */ + bool isExplorationShowProgressSet() const; + + /*! + * Retrieves the delay for printing information about the exploration progress. + * + * @return The desired delay in seconds. If 0, no information about the progress shall be printed. + */ + uint64_t getExplorationShowProgressDelay() const; + /*! * Retrieves the exploration order if it was set. * @@ -334,6 +348,8 @@ namespace storm { static const std::string jitOptionName; static const std::string explorationChecksOptionName; static const std::string explorationChecksOptionShortName; + static const std::string explorationShowProgressOptionName; + static const std::string explorationShowProgressOptionShortName; static const std::string explorationOrderOptionName; static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName;