BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption.

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.

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();

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;

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();
         }

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
              */

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,10 +85,18 @@ 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();
             }

src/storm/settings/modules/BuildSettings.h

@@ -79,12 +79,21 @@ namespace storm {
                  */
                 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
                  * @return