diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e6508c190..334480cbf 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -448,6 +448,11 @@ namespace storm { options.setBuildAllLabels(true); options.setBuildAllRewardModels(true); } + + if (buildSettings.isAddOverlappingGuardsLabelSet()) { + options.setAddOverlappingGuardsLabel(true); + } + return storm::api::buildSparseModel(input.model.get(), options, useJit, storm::settings::getModule().isDoctorSet()); } diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 3d1852ba5..7ef3c894c 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -33,6 +33,7 @@ namespace storm { const std::string buildChoiceOriginsOptionName = "buildchoiceorig"; const std::string buildStateValuationsOptionName = "buildstateval"; const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; + const std::string buildOverlappingGuardsLabelOptionName = "overlappingguardslabel"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; BuildSettings::BuildSettings() : ModuleSettings(moduleName) { @@ -51,6 +52,7 @@ namespace storm { .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, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildOverlappingGuardsLabelOptionName, false, "For states where multiple guards are enabled, we add a label (for debugging DTMCs)").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build()); } @@ -99,6 +101,10 @@ namespace storm { return this->getOption(buildOutOfBoundsStateOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isAddOverlappingGuardsLabelSet() const { + return this->getOption(buildOverlappingGuardsLabelOptionName).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 3cce0a705..10ae675e3 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -99,7 +99,12 @@ namespace storm { * @return */ bool isBuildOutOfBoundsStateSet() const; - + + /*! + * Retrieves whether to build the overlapping label + */ + bool isAddOverlappingGuardsLabelSet() const; + /*! * Retrieves the number of bits that should be used to represent unbounded integer variables * @return