Browse Source

build-all-labels for building all labels without building everything, and renamed build-overlapping-guards-label and build-out-of-bounds-state

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
commit
d71e70da42
  1. 1
      src/storm-cli-utilities/model-handling.h
  2. 10
      src/storm/settings/modules/BuildSettings.cpp
  3. 5
      src/storm/settings/modules/BuildSettings.h

1
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<storm::settings::modules::CounterexampleGeneratorSettings>();

10
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<std::string> 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") {

5
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
Loading…
Cancel
Save