added option to build all labels/reward models for next-state generators

Former-commit-id: cfb9787d6c

src/builder/DdPrismModelBuilder.cpp

@@ -473,18 +473,18 @@ namespace storm {
         };
         
         template <storm::dd::DdType Type, typename ValueType>
-        DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+        DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), terminalStates(), negatedTerminalStates() {
+        DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
             this->setTerminalStatesFromFormula(formula);
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+        DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -554,22 +554,6 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType Type, typename ValueType>
-        void DdPrismModelBuilder<Type, ValueType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
-            std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
-            
-            // If there is at least one constant that is defined, and the constant definition map does not yet exist,
-            // we need to create it.
-            if (!constantDefinitions && !newConstantDefinitions.empty()) {
-                constantDefinitions = std::map<storm::expressions::Variable, storm::expressions::Expression>();
-            }
-            
-            // Now insert all the entries that need to be defined.
-            for (auto const& entry : newConstantDefinitions) {
-                constantDefinitions.get().insert(entry);
-            }
-        }
-        
         template <storm::dd::DdType Type, typename ValueType>
         struct DdPrismModelBuilder<Type, ValueType>::SystemResult {
             SystemResult(storm::dd::Add<Type, ValueType> const& allTransitionsDd, DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) {
@@ -1248,11 +1232,7 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::build(storm::prism::Program const& program, Options const& options) {
-            if (options.constantDefinitions) {
-                preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
-            } else {
-                preparedProgram = program;
-            }
+            preparedProgram = program;
             
             if (preparedProgram->hasUndefinedConstants()) {
                 std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();

src/generator/NextStateGenerator.cpp

@@ -5,7 +5,7 @@
 #include "src/logic/Formulas.h"
 
 #include "src/utility/macros.h"
-#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace generator {
@@ -34,16 +34,16 @@ namespace storm {
             return boost::get<storm::expressions::Expression const&>(labelOrExpression);
         }
         
-        NextStateGeneratorOptions::NextStateGeneratorOptions() : buildChoiceLabels(false) {
+        NextStateGeneratorOptions::NextStateGeneratorOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) {
             // Intentionally left empty.
         }
         
-        NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) {
+        NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) : NextStateGeneratorOptions() {
             this->preserveFormula(formula);
             this->setTerminalStatesFromFormula(formula);
         }
         
-        NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : NextStateGeneratorOptions() {
             if (!formulas.empty()) {
                 for (auto const& formula : formulas) {
                     this->preserveFormula(*formula);
@@ -112,8 +112,8 @@ namespace storm {
             return rewardModelNames;
         }
         
-        std::set<std::string> const& NextStateGeneratorOptions::getLabels() const {
-            return labels;
+        std::set<std::string> const& NextStateGeneratorOptions::getLabelNames() const {
+            return labelNames;
         }
         
         std::vector<storm::expressions::Expression> const& NextStateGeneratorOptions::getExpressionLabels() const {
@@ -135,19 +135,39 @@ namespace storm {
         bool NextStateGeneratorOptions::isBuildChoiceLabelsSet() const {
             return buildChoiceLabels;
         }
+        
+        bool NextStateGeneratorOptions::isBuildAllRewardModelsSet() const {
+            return buildAllRewardModels;
+        }
+        
+        bool NextStateGeneratorOptions::isBuildAllLabelsSet() const {
+            return buildAllLabels;
+        }
 
+        NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllRewardModels() {
+            buildAllRewardModels = true;
+            return *this;
+        }
+        
         NextStateGeneratorOptions& NextStateGeneratorOptions::addRewardModel(std::string const& rewardModelName) {
+            STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway.");
             rewardModelNames.emplace_back(rewardModelName);
             return *this;
         }
-        
+
+        NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllLabels() {
+            buildAllLabels = true;
+            return *this;
+        }
+
         NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) {
             expressionLabels.emplace_back(expression);
             return *this;
         }
         
-        NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& label) {
-            labels.insert(label);
+        NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& labelName) {
+            STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
+            labelNames.insert(labelName);
             return *this;
         }
         

src/generator/NextStateGenerator.h

@@ -48,7 +48,7 @@ namespace storm {
             /*!
              * Creates an object representing the default options.
              */
-            NextStateGeneratorOptions();
+            NextStateGeneratorOptions(bool buildAllRewardModels = false, bool buildAllLabels = false);
             
             /*!
              * Creates an object representing the suggested building options assuming that the given formula is the
@@ -85,26 +85,37 @@ namespace storm {
             void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
             
             std::vector<std::string> const& getRewardModelNames() const;
-            std::set<std::string> const& getLabels() const;
+            std::set<std::string> const& getLabelNames() const;
             std::vector<storm::expressions::Expression> const& getExpressionLabels() const;
             std::vector<std::pair<LabelOrExpression, bool>> const& getTerminalStates() const;
             bool hasTerminalStates() const;
             void clearTerminalStates();
             bool isBuildChoiceLabelsSet() const;
+            bool isBuildAllRewardModelsSet() const;
+            bool isBuildAllLabelsSet() const;
             
+            NextStateGeneratorOptions& setBuildAllRewardModels();
             NextStateGeneratorOptions& addRewardModel(std::string const& rewardModelName);
+            NextStateGeneratorOptions& setBuildAllLabels();
             NextStateGeneratorOptions& addLabel(storm::expressions::Expression const& expression);
-            NextStateGeneratorOptions& addLabel(std::string const& label);
+            NextStateGeneratorOptions& addLabel(std::string const& labelName);
             NextStateGeneratorOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
             NextStateGeneratorOptions& addTerminalLabel(std::string const& label, bool value);
             NextStateGeneratorOptions& setBuildChoiceLabels(bool newValue);
             
         private:
+            /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are
+            /// to be ignored.
+            bool buildAllRewardModels;
+            
             /// The names of the reward models to generate.
             std::vector<std::string> rewardModelNames;
 
+            /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored.
+            bool buildAllLabels;
+            
             /// A set of labels to build.
-            std::set<std::string> labels;
+            std::set<std::string> labelNames;
             
             /// The expression that are to be used for creating the state labeling.
             std::vector<storm::expressions::Expression> expressionLabels;

src/generator/PrismNextStateGenerator.cpp

@@ -18,21 +18,27 @@ namespace storm {
         PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator<ValueType, StateType>(options), program(program), rewardModels(), variableInformation(program), evaluator(program.getManager()), state(nullptr), comparator() {
             STORM_LOG_THROW(!program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             
-            // Extract the reward models from the program based on the names we were given.
-            for (auto const& rewardModelName : this->options.getRewardModelNames()) {
-                if (program.hasRewardModel(rewardModelName)) {
-                    rewardModels.push_back(program.getRewardModel(rewardModelName));
-                } else {
-                    STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
-                    STORM_LOG_THROW(program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
-                    STORM_LOG_THROW(program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model.");
+            if (this->options.isBuildAllRewardModelsSet()) {
+                for (auto const& rewardModel : program.getRewardModels()) {
+                    rewardModels.push_back(rewardModel);
+                }
+            } else {
+                // Extract the reward models from the program based on the names we were given.
+                for (auto const& rewardModelName : this->options.getRewardModelNames()) {
+                    if (program.hasRewardModel(rewardModelName)) {
+                        rewardModels.push_back(program.getRewardModel(rewardModelName));
+                    } else {
+                        STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
+                        STORM_LOG_THROW(program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
+                        STORM_LOG_THROW(program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model.");
+                    }
+                }
+                
+                // If no reward model was yet added, but there was one that was given in the options, we try to build
+                // standard reward model.
+                if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
+                    rewardModels.push_back(program.getRewardModel(0));
                 }
-            }
-            
-            // If no reward model was yet added, but there was one that was given in the options, we try to build
-            // standard reward model.
-            if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
-                rewardModels.push_back(program.getRewardModel(0));
             }
             
             // If there are terminal states we need to handle, we now need to translate all labels to expressions.
@@ -467,10 +473,16 @@ namespace storm {
         storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
             // Gather a vector of labels and their expressions so we can iterate it over it a lot.
             std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
-            for (auto const& label : this->options.getLabels()) {
-                labels.push_back(std::make_pair(label, program.getLabelExpression(label)));
+            if (this->options.isBuildAllLabelsSet()) {
+                for (auto const& label : program.getLabels()) {
+                    labels.push_back(std::make_pair(label.getName(), label.getStatePredicateExpression()));
+                }
+            } else {
+                for (auto const& labelName : this->options.getLabelNames()) {
+                    labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
+                }
             }
-            
+        
             // Make the labels unique.
             std::sort(labels.begin(), labels.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
             auto it = std::unique(labels.begin(), labels.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );

src/utility/storm.h

@@ -121,7 +121,6 @@ namespace storm {
         } else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
             typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
             options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
-            options.addConstantDefinitionsFromString(program, constantDefinitionString);
 
             storm::builder::DdPrismModelBuilder<LibraryType> builder;
             result.model = builder.build(program, options);