added export shield iosetting

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

@@ -1043,15 +1043,18 @@ namespace storm {
                                                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
                                                 }
                                             }
-                                            if (result->isExplicitQuantitativeCheckResult()) {
-                                                if (result-> template asExplicitQuantitativeCheckResult<ValueType>().hasShield()) {
-                                                    auto shield = result->template asExplicitQuantitativeCheckResult<ValueType>().getShield();
-                                                    STORM_PRINT_AND_LOG("Exporting shield ...");
+                                            if (ioSettings.isExportShieldSet()) {
+                                                if (result->isExplicitQuantitativeCheckResult()) {
+                                                    if (result-> template asExplicitQuantitativeCheckResult<ValueType>().hasShield()) {
+                                                        auto shield = result->template asExplicitQuantitativeCheckResult<ValueType>().getShield();
+                                                        STORM_PRINT_AND_LOG("Exporting shield ... ");
                                                         
-                                                    storm::api::exportShield(sparseModel, shield, shield->getShieldFileName());
+                                                        storm::api::exportShield(sparseModel, shield, ioSettings.getExportShieldFilename());
+                                                    }
                                                 }
                                             }
                                           
+
                                             if (ioSettings.isExportCheckResultSet()) {
                                                 STORM_LOG_WARN_COND(sparseModel->hasStateValuations(), "No information of state valuations available. The result output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval.");
                                                 STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties.");

src/storm/settings/modules/IOSettings.cpp

@@ -25,6 +25,7 @@ namespace storm {
             const std::string IOSettings::exportCdfOptionName = "exportcdf";
             const std::string IOSettings::exportCdfOptionShortName = "cdf";
             const std::string IOSettings::exportSchedulerOptionName = "exportscheduler";
+            const std::string IOSettings::exportShieldOptionName = "exportshield";
             const std::string IOSettings::exportCheckResultOptionName = "exportresult";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
@@ -64,6 +65,7 @@ namespace storm {
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportShieldOptionName, false, "Exports the the generated shield to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportCheckResultOptionName, false, "Exports the result to a given file (if supported by engine). The export will be in json.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
@@ -178,6 +180,14 @@ namespace storm {
                 return this->getOption(exportSchedulerOptionName).getArgumentByName("filename").getValueAsString();
             }
 
+            bool IOSettings::isExportShieldSet() const {
+                return this->getOption(exportShieldOptionName).getHasOptionBeenSet();
+            }
+
+            std::string IOSettings::getExportShieldFilename() const {
+                return this->getOption(exportShieldOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
             bool IOSettings::isExportCheckResultSet() const {
                 return this->getOption(exportCheckResultOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/IOSettings.h

@@ -106,6 +106,16 @@ namespace storm {
                  */
                  std::string getExportSchedulerFilename() const;
 
+                /*!
+                 * Retrieves whether a shield is to be exported.
+                 */
+                bool isExportShieldSet() const;
+
+                /*!
+                 * Retrieves a filename to which a shield will be exported.
+                 */
+                std::string getExportShieldFilename() const;
+
                 /*!
                  * Retrieves whether the check result should be exported.
                  */
@@ -365,6 +375,7 @@ namespace storm {
                 static const std::string exportCdfOptionName;
                 static const std::string exportCdfOptionShortName;
                 static const std::string exportSchedulerOptionName;
+                static const std::string exportShieldOptionName;
                 static const std::string exportCheckResultOptionName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;