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

added option to display information about exploration progress to both jit and explicit builder

main
dehnert 8 years ago
parent
040c1f0d4c
commit
29855e2853
6 changed files with 108 additions and 4 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. 12
      src/storm/builder/BuilderOptions.cpp
  2. 8
      src/storm/builder/BuilderOptions.h
  3. 20
      src/storm/builder/ExplicitModelBuilder.cpp
  4. 44
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  5. 12
      src/storm/settings/modules/IOSettings.cpp
  6. 16
      src/storm/settings/modules/IOSettings.h

12
src/storm/builder/BuilderOptions.cpp
View File

@ -35,7 +35,7 @@ namespace storm {
return boost::get<storm::expressions::Expression>(labelOrExpression); return boost::get<storm::expressions::Expression>(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. // Intentionally left empty.
} }
@ -55,6 +55,8 @@ namespace storm {
} }
explorationChecks = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationChecksSet(); explorationChecks = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationChecksSet();
explorationShowProgress = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationShowProgressSet();
explorationShowProgressDelay = storm::settings::getModule<storm::settings::modules::IOSettings>().getExplorationShowProgressDelay();
} }
void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) { void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) {
@ -163,6 +165,14 @@ namespace storm {
bool BuilderOptions::isExplorationChecksSet() const { bool BuilderOptions::isExplorationChecksSet() const {
return explorationChecks; return explorationChecks;
} }
bool BuilderOptions::isExplorationShowProgressSet() const {
return explorationShowProgress;
}
uint64_t BuilderOptions::getExplorationShowProgressDelay() const {
return explorationShowProgressDelay;
}
BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) { BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) {
explorationChecks = newValue; explorationChecks = newValue;

8
src/storm/builder/BuilderOptions.h
View File

@ -94,6 +94,8 @@ namespace storm {
bool isBuildAllRewardModelsSet() const; bool isBuildAllRewardModelsSet() const;
bool isBuildAllLabelsSet() const; bool isBuildAllLabelsSet() const;
bool isExplorationChecksSet() const; bool isExplorationChecksSet() const;
bool isExplorationShowProgressSet() const;
uint64_t getExplorationShowProgressDelay() const;
BuilderOptions& setBuildAllRewardModels(); BuilderOptions& setBuildAllRewardModels();
BuilderOptions& addRewardModel(std::string const& rewardModelName); BuilderOptions& addRewardModel(std::string const& rewardModelName);
@ -139,6 +141,12 @@ namespace storm {
/// A flag that stores whether exploration checks are to be performed. /// A flag that stores whether exploration checks are to be performed.
bool explorationChecks; 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;
}; };
} }

20
src/storm/builder/ExplicitModelBuilder.cpp
View File

@ -131,6 +131,11 @@ namespace storm {
uint_fast64_t currentRowGroup = 0; uint_fast64_t currentRowGroup = 0;
uint_fast64_t currentRow = 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. // Perform a search through the model.
while (!statesToExplore.empty()) { while (!statesToExplore.empty()) {
// Get the first state in the queue. // Get the first state in the queue.
@ -234,6 +239,21 @@ namespace storm {
} }
++currentRowGroup; ++currentRowGroup;
} }
if (generator->getOptions().isExplorationShowProgressSet()) {
++numberOfExploredStatesSinceLastMessage;
++numberOfExploredStates;
auto now = std::chrono::high_resolution_clock::now();
auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
if (static_cast<uint64_t>(durationSinceLastMessage) >= generator->getOptions().getExplorationShowProgressDelay()) {
auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage;
auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(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) { if (markovianStates) {

44
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -527,6 +527,15 @@ namespace storm {
} }
modelData["exploration_checks"] = cpptempl::make_data(list); modelData["exploration_checks"] = cpptempl::make_data(list);
list = cpptempl::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<storm::RationalNumber, ValueType>::value) { if (std::is_same<storm::RationalNumber, ValueType>::value) {
list.push_back(cpptempl::data_map()); list.push_back(cpptempl::data_map());
} }
@ -541,7 +550,7 @@ namespace storm {
list.push_back(cpptempl::data_map()); list.push_back(cpptempl::data_map());
} }
modelData["double"] = cpptempl::make_data(list); modelData["double"] = cpptempl::make_data(list);
list = cpptempl::data_list(); list = cpptempl::data_list();
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) { if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) {
list.push_back(cpptempl::data_map()); list.push_back(cpptempl::data_map());
@ -1646,12 +1655,17 @@ namespace storm {
std::string sourceTemplate = R"( std::string sourceTemplate = R"(
#define NDEBUG #define NDEBUG
{% if expl_progress %}
#define EXPL_PROGRESS
{% endif %}
#include <cstdint> #include <cstdint>
#include <iostream> #include <iostream>
#include <vector> #include <vector>
#include <queue> #include <queue>
#include <cmath> #include <cmath>
#include <unordered_map> #include <unordered_map>
#include <chrono>
#include <boost/dll/alias.hpp> #include <boost/dll/alias.hpp>
{% if exact %} {% if exact %}
@ -2179,7 +2193,7 @@ namespace storm {
class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> { class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> {
public: public:
JitBuilder(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) {
JitBuilder(ModelComponentsBuilder<IndexType, ValueType>& 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 %}{ {% for state in initialStates %}{
StateType state; StateType state;
{% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; {% for assignment in state %}state.{$assignment.variable} = {$assignment.value};
@ -2262,6 +2276,7 @@ namespace storm {
getOrAddIndex(initialState, statesToExplore); getOrAddIndex(initialState, statesToExplore);
StateBehaviour<IndexType, ValueType> behaviour; StateBehaviour<IndexType, ValueType> behaviour;
while (!statesToExplore.empty()) { while (!statesToExplore.empty()) {
StateType currentState = statesToExplore.get(); StateType currentState = statesToExplore.get();
IndexType currentIndex = getIndex(currentState); IndexType currentIndex = getIndex(currentState);
@ -2300,6 +2315,21 @@ namespace storm {
this->addStateBehaviour(currentIndex, behaviour); this->addStateBehaviour(currentIndex, behaviour);
behaviour.clear(); behaviour.clear();
#ifdef EXPL_PROGRESS
++numberOfExploredStatesSinceLastMessage;
++numberOfExploredStates;
auto now = std::chrono::high_resolution_clock::now();
auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
if (static_cast<uint64_t>(durationSinceLastMessage) >= {$expl_progress_interval}) {
auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage;
auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(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: private:
// State storage.
spp::sparse_hash_map<StateType, IndexType> stateIds; spp::sparse_hash_map<StateType, IndexType> stateIds;
std::vector<StateType> initialStates; std::vector<StateType> initialStates;
std::vector<IndexType> deadlockStates; std::vector<IndexType> deadlockStates;
// Edges.
{% for edge in nonsynch_edges %}Edge edge_{$edge.name}; {% for edge in nonsynch_edges %}Edge edge_{$edge.name};
{% endfor %} {% endfor %}
{% for edge in synch_edges %}Edge edge_{$edge.name}; {% for edge in synch_edges %}Edge edge_{$edge.name};
{% endfor %} {% 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) BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder)

12
src/storm/settings/modules/IOSettings.cpp
View File

@ -34,6 +34,8 @@ namespace storm {
const std::string IOSettings::explorationOrderOptionShortName = "eo"; const std::string IOSettings::explorationOrderOptionShortName = "eo";
const std::string IOSettings::explorationChecksOptionName = "explchecks"; const std::string IOSettings::explorationChecksOptionName = "explchecks";
const std::string IOSettings::explorationChecksOptionShortName = "ec"; 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::transitionRewardsOptionName = "transrew";
const std::string IOSettings::stateRewardsOptionName = "staterew"; const std::string IOSettings::stateRewardsOptionName = "staterew";
const std::string IOSettings::choiceLabelingOptionName = "choicelab"; 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) 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()); .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, 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 + ").") 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()); .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(); 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 { bool IOSettings::isTransitionRewardsSet() const {
return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet();
} }
@ -268,6 +279,7 @@ namespace storm {
} }
void IOSettings::finalize() { void IOSettings::finalize() {
// Intentionally left empty.
} }
bool IOSettings::check() const { bool IOSettings::check() const {

16
src/storm/settings/modules/IOSettings.h
View File

@ -179,6 +179,20 @@ namespace storm {
*/ */
bool isExplorationChecksSet() const; 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. * Retrieves the exploration order if it was set.
* *
@ -334,6 +348,8 @@ namespace storm {
static const std::string jitOptionName; static const std::string jitOptionName;
static const std::string explorationChecksOptionName; static const std::string explorationChecksOptionName;
static const std::string explorationChecksOptionShortName; static const std::string explorationChecksOptionShortName;
static const std::string explorationShowProgressOptionName;
static const std::string explorationShowProgressOptionShortName;
static const std::string explorationOrderOptionName; static const std::string explorationOrderOptionName;
static const std::string explorationOrderOptionShortName; static const std::string explorationOrderOptionShortName;
static const std::string transitionRewardsOptionName; static const std::string transitionRewardsOptionName;

Write Preview
Loading…
Cancel
Save