diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 771a0f8ee..b9589fbd8 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -424,6 +424,7 @@ namespace storm { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); + options.setBuildAllLabels(buildSettings.isBuildAllLabelsSet()); bool buildChoiceOrigins = buildSettings.isBuildChoiceOriginsSet(); if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { auto counterexampleGeneratorSettings = storm::settings::getModule(); diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 7ef3c894c..83c4b19d4 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -32,8 +32,9 @@ namespace storm { const std::string buildChoiceLabelOptionName = "buildchoicelab"; const std::string buildChoiceOriginsOptionName = "buildchoiceorig"; const std::string buildStateValuationsOptionName = "buildstateval"; - const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; - const std::string buildOverlappingGuardsLabelOptionName = "overlappingguardslabel"; + const std::string buildAllLabelsOptionName = "build-all-labels"; + const std::string buildOutOfBoundsStateOptionName = "build-out-of-bounds-state"; + const std::string buildOverlappingGuardsLabelOptionName = "build-overlapping-guards-label"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; BuildSettings::BuildSettings() : ModuleSettings(moduleName) { @@ -45,6 +46,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceOriginsOptionName, false, "If set, also build information that for each choice indicates the part(s) of the input that yielded the choice.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildAllLabelsOptionName, false, "If set, build all labels").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").setIsAdvanced().build()); std::vector explorationOrders = {"dfs", "bfs"}; @@ -105,6 +107,10 @@ namespace storm { return this->getOption(buildOverlappingGuardsLabelOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isBuildAllLabelsSet() const { + return this->getOption(buildAllLabelsOptionName).getHasOptionBeenSet(); + } + storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const { std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); if (explorationOrderAsString == "dfs") { diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index 10ae675e3..9c81859c3 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -105,6 +105,11 @@ namespace storm { */ bool isAddOverlappingGuardsLabelSet() const; + /*! + * Retrieves whether all labels should be build + */ + bool isBuildAllLabelsSet() const; + /*! * Retrieves the number of bits that should be used to represent unbounded integer variables * @return