From ba6f0c0e877af75d8ed4a967bcbc8edac46ac855 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 20 Feb 2020 12:01:55 +0100 Subject: [PATCH] BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption. --- CHANGELOG.md | 2 ++ src/storm-cli-utilities/model-handling.h | 13 +++++++++---- src/storm/api/builder.h | 4 +++- src/storm/builder/TerminalStatesGetter.cpp | 7 +++++++ src/storm/builder/TerminalStatesGetter.h | 5 +++++ src/storm/settings/modules/BuildSettings.cpp | 12 ++++++++++++ src/storm/settings/modules/BuildSettings.h | 13 +++++++++++-- 7 files changed, 49 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3a5c36231..df9f29923 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,8 @@ Version 1.4.x ## Version 1.4.2 (under development) - DRN: support import of choice labelling +- Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`). +- Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata) - `storm-pomdp`: Only accept POMDPs that are canonical - `storm-pomdp`: Prism language extended with observable expressions - `storm-pomdp`: Various fixes that prevented usage. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index a49d244e5..b35b9f0d3 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -260,7 +260,8 @@ namespace storm { template std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule().isBuildFullModelSet()); + auto buildSettings = storm::settings::getModule(); + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(), !buildSettings.isApplyNoMaximumProgressAssumptionSet()); } template @@ -268,19 +269,23 @@ namespace storm { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); - bool buildChoiceOrigins = false; + bool buildChoiceOrigins = buildSettings.isBuildChoiceOriginsSet(); if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { auto counterexampleGeneratorSettings = storm::settings::getModule(); if (counterexampleGeneratorSettings.isCounterexampleSet()) { - buildChoiceOrigins = counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); + buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); } - options.setBuildChoiceOrigins(buildChoiceOrigins); } + options.setBuildChoiceOrigins(buildChoiceOrigins); if (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::POMDP) { options.setBuildChoiceOrigins(true); options.setBuildChoiceLabels(true); } + if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) { + options.setApplyMaximalProgressAssumption(false); + } + options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 0df66c7ff..6be939496 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -43,7 +43,7 @@ namespace storm { } template - std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel = false) { + std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel = false, bool applyMaximumProgress = true) { if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); @@ -51,6 +51,7 @@ namespace storm { if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.terminalStates.clear(); } storm::builder::DdPrismModelBuilder builder; @@ -63,6 +64,7 @@ namespace storm { if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.terminalStates.clear(); } storm::builder::DdJaniModelBuilder builder; diff --git a/src/storm/builder/TerminalStatesGetter.cpp b/src/storm/builder/TerminalStatesGetter.cpp index 11a4ccb85..16779b8d9 100644 --- a/src/storm/builder/TerminalStatesGetter.cpp +++ b/src/storm/builder/TerminalStatesGetter.cpp @@ -60,6 +60,13 @@ namespace storm { } } + void TerminalStates::clear() { + terminalExpressions.clear(); + negatedTerminalExpressions.clear(); + terminalLabels.clear(); + negatedTerminalLabels.clear(); + } + bool TerminalStates::empty() const { return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty(); } diff --git a/src/storm/builder/TerminalStatesGetter.h b/src/storm/builder/TerminalStatesGetter.h index c9eb2c6c0..f41413f28 100644 --- a/src/storm/builder/TerminalStatesGetter.h +++ b/src/storm/builder/TerminalStatesGetter.h @@ -31,6 +31,11 @@ namespace storm { std::vector terminalLabels; // if a state has one of these labels, we can stop exploration std::vector negatedTerminalLabels; // if a state does not have all of these labels, we can stop exploration + /*! + * Clears all terminal states. After calling this, empty() holds. + */ + void clear(); + /*! * True if no terminal states are specified */ diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 3ebc6d109..b460d7ba6 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -29,7 +29,9 @@ namespace storm { const std::string dontFixDeadlockOptionShortName = "ndl"; const std::string noBuildOptionName = "nobuild"; const std::string fullModelBuildOptionName = "buildfull"; + const std::string applyNoMaxProgAssumptionOptionName = "nomaxprog"; const std::string buildChoiceLabelOptionName = "buildchoicelab"; + const std::string buildChoiceOriginsOptionName = "buildchoiceorig"; const std::string buildStateValuationsOptionName = "buildstateval"; const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; @@ -40,7 +42,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, applyNoMaxProgAssumptionOptionName, false, "If set, the maximum progress assumption is not applied while building the model (relevant for MAs)").setIsAdvanced().build()); 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, noBuildOptionName, false, "If set, do not build the model.").setIsAdvanced().build()); @@ -81,9 +85,17 @@ namespace storm { return this->getOption(noBuildOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isApplyNoMaximumProgressAssumptionSet() const { + return this->getOption(applyNoMaxProgAssumptionOptionName).getHasOptionBeenSet(); + } + bool BuildSettings::isBuildChoiceLabelsSet() const { return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); } + + bool BuildSettings::isBuildChoiceOriginsSet() const { + return this->getOption(buildChoiceOriginsOptionName).getHasOptionBeenSet(); + } bool BuildSettings::isBuildStateValuationsSet() const { return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index b80424c7f..274f42da1 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -78,12 +78,21 @@ namespace storm { * @return true iff the full model should be build. */ bool isBuildFullModelSet() const; - + + /*! + * Retrieves whether the maximum progress assumption is to be applied when building the model + */ + bool isApplyNoMaximumProgressAssumptionSet() const; + /*! * Retrieves whether the choice labels should be build - * @return */ bool isBuildChoiceLabelsSet() const; + + /*! + * Retrieves whether the choice origins should be build + */ + bool isBuildChoiceOriginsSet() const; /*! * Retrieves whether the choice labels should be build