diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index b932df8f0..c90852df5 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -1043,14 +1043,17 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property."); } } - if (result->isExplicitQuantitativeCheckResult()) { - if (result-> template asExplicitQuantitativeCheckResult().hasShield()) { - auto shield = result->template asExplicitQuantitativeCheckResult().getShield(); - STORM_PRINT_AND_LOG("Exporting shield ..."); - - storm::api::exportShield(sparseModel, shield, shield->getShieldFileName()); + if (ioSettings.isExportShieldSet()) { + if (result->isExplicitQuantitativeCheckResult()) { + if (result-> template asExplicitQuantitativeCheckResult().hasShield()) { + auto shield = result->template asExplicitQuantitativeCheckResult().getShield(); + STORM_PRINT_AND_LOG("Exporting shield ... "); + + 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."); diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index f0af3f4ad..d94c67a8e 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/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(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 3be8c646d..a03ea372e 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/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;