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 <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
- return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildFullModelSet());
+ auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
+ return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(), !buildSettings.isApplyNoMaximumProgressAssumptionSet());
}
template <typename ValueType>
@@ -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<storm::settings::modules::CounterexampleGeneratorSettings>();
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<storm::dd::DdType LibraryType, typename ValueType>
- std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false) {
+ std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false, bool applyMaximumProgress = true) {
if (model.isPrismProgram()) {
typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
@@ -51,6 +51,7 @@ namespace storm {
if (buildFullModel) {
options.buildAllLabels = true;
options.buildAllRewardModels = true;
+ options.terminalStates.clear();
}
storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
@@ -63,6 +64,7 @@ namespace storm {
if (buildFullModel) {
options.buildAllLabels = true;
options.buildAllRewardModels = true;
+ options.terminalStates.clear();
}
storm::builder::DdJaniModelBuilder<LibraryType, ValueType> 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<std::string> terminalLabels; // if a state has one of these labels, we can stop exploration
std::vector<std::string> 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