added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format

src/storm-cli-utilities/model-handling.h

@@ -179,6 +179,7 @@ namespace storm {
             auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             storm::builder::BuilderOptions options(createFormulasToRespect(input.properties));
             options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet());
+            options.setBuildStateValuations(ioSettings.isBuildStateValuationsSet());
             options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
             options.setBuildAllLabels(ioSettings.isBuildFullModelSet());
             options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet());

src/storm/models/sparse/Model.cpp

@@ -317,12 +317,16 @@ namespace storm {
                 for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) {
                     if (subsystem == nullptr || subsystem->get(state)) {
                         outStream << "\t" << state;
-                        if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr) {
+                        if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr || hasStateValuations()) {
                             outStream << " [ ";
                             
                             // If we need to print some extra information, do so now.
-                            if (includeLabeling || firstValue != nullptr || secondValue != nullptr) {
-                                outStream << "label = \"" << state << ": ";
+                            if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) {
+                                outStream << "label = \"" << state;
+                                if (hasStateValuations()) {
+                                    outStream << " " << getStateValuations().getStateInfo(state);
+                                }
+                                outStream << ": ";
                                 
                                 // Now print the state labeling to the stream if requested.
                                 if (includeLabeling) {

src/storm/settings/modules/IOSettings.cpp

@@ -46,6 +46,7 @@ namespace storm {
             const std::string IOSettings::noBuildOptionName = "nobuild";
             const std::string IOSettings::fullModelBuildOptionName = "buildfull";
             const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab";
+            const std::string IOSettings::buildStateValuationsOptionName = "buildstateval";
             const std::string IOSettings::janiPropertyOptionName = "janiproperty";
             const std::string IOSettings::janiPropertyOptionShortName = "jprop";
             const std::string IOSettings::propertyOptionName = "prop";
@@ -76,7 +77,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").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, buildChoiceLabelOptionName, false, "If set, include choice labels").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
@@ -266,6 +268,10 @@ namespace storm {
                 return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet();
             }
 
+           bool IOSettings::isBuildStateValuationsSet() const {
+                return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet();
+            }
+
             bool IOSettings::isPropertySet() const {
                 return this->getOption(propertyOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/IOSettings.h

@@ -325,6 +325,12 @@ namespace storm {
                  */
                 bool isBuildChoiceLabelsSet() const;
 
+                /*!
+                 * Retrieves whether the choice labels should be build
+                 * @return
+                 */
+                bool isBuildStateValuationsSet() const;
+
                 bool check() const override;
                 void finalize() override;
 
@@ -362,6 +368,7 @@ namespace storm {
                 static const std::string fullModelBuildOptionName;
                 static const std::string noBuildOptionName;
                 static const std::string buildChoiceLabelOptionName;
+                static const std::string buildStateValuationsOptionName;
                 static const std::string janiPropertyOptionName;
                 static const std::string janiPropertyOptionShortName;
                 static const std::string propertyOptionName;