diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index e943b2219..a862290d3 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -44,6 +44,10 @@ namespace storm { const std::string IOSettings::propertyOptionShortName = "prop"; const std::string IOSettings::toNondetOptionName = "to-nondet"; + const std::string IOSettings::qvbsInputOptionName = "qvbs"; + const std::string IOSettings::qvbsInputOptionShortName = "qvbs"; + const std::string IOSettings::qvbsRootOptionName = "qvbsroot"; + IOSettings::IOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); @@ -82,6 +86,19 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("model", "The short model name as in the benchmark set.").build()) + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("instance-index", "The selected instance of this model.").setDefaultValueUnsignedInteger(0).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The comma separated list of property names to check. Empty string checks all, [] checks none.").setDefaultValueString("").build()) + .build()); +#ifdef STORM_HAVE_QVBS + std::string qvbsRootDefault = STORM_QVBS_ROOT; +#else + std::string qvbsRootDefault = ""; +#endif + this->addOption(storm::settings::OptionBuilder(moduleName, qvbsRootOptionName, false, "Specifies the root directory of the Quantitative Verification Benchmark Set. Default can be set in CMAKE.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The path.").setDefaultValueString(qvbsRootDefault).build()).build()); } bool IOSettings::isExportDotSet() const { @@ -232,21 +249,57 @@ namespace storm { return this->getOption(toNondetOptionName).getHasOptionBeenSet(); } + bool IOSettings::isQvbsInputSet() const { + return this->getOption(qvbsInputOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getQvbsModelName() const { + return this->getOption(qvbsInputOptionName).getArgumentByName("model").getValueAsString(); + } + + uint64_t IOSettings::getQvbsInstanceIndex() const { + return this->getOption(qvbsInputOptionName).getArgumentByName("instance-index").getValueAsUnsignedInteger(); + } + + boost::optional> IOSettings::getQvbsPropertyFilter() const { + std::string listAsString = this->getOption(qvbsInputOptionName).getArgumentByName("filter").getValueAsString(); + if (listAsString == "[]") { + return std::vector(); + } else if (listAsString == "") { + return boost::none; + } else { + return storm::parser::parseCommaSeperatedValues(listAsString); + } + } + + std::string IOSettings::getQvbsRoot() const { + auto const& path = this->getOption(qvbsRootOptionName).getArgumentByName("path"); +#ifndef STORM_HAVE_QVBS + STORM_LOG_THROW(this->getOption(qvbsRootOptionName).getHasOptionBeenSet(), storm::exceptions::InvalidSettingsException, "QVBS Root is not specified. Either use the --" + qvbsRootOptionName + " option or specify it within CMAKE."); +#endif + return path.getValueAsString(); + } + void IOSettings::finalize() { // Intentionally left empty. } bool IOSettings::check() const { - // Ensure that not two symbolic input models were given. - STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet(), storm::exceptions::InvalidSettingsException, "Symbolic model "); + // Ensure that at most one symbolic input model is given. + uint64_t numSymbolicInputs = isJaniInputSet() ? 1 : 0; + numSymbolicInputs += isPrismInputSet() ? 1 : 0; + numSymbolicInputs += isQvbsInputSet() ? 1 : 0; + STORM_LOG_THROW(numSymbolicInputs <= 1, storm::exceptions::InvalidSettingsException, "Multiple symbolic input models."); + STORM_LOG_THROW(!isExportJaniDotSet() || isJaniInputSet() || isQvbsInputSet(), storm::exceptions::InvalidSettingsException, "Jani-to-dot export is only available for jani models" ); // Ensure that not two explicit input models were given. - STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model "); - - STORM_LOG_THROW(!isExportJaniDotSet() || isJaniInputSet(), storm::exceptions::InvalidSettingsException, "Jani-to-dot export is only available for jani models" ); + uint64_t numExplicitInputs = isExplicitSet() ? 1 : 0; + numExplicitInputs += isExplicitDRNSet() ? 1 : 0; + numExplicitInputs += isExplicitIMCASet() ? 1 : 0; + STORM_LOG_THROW(numExplicitInputs <= 1, storm::exceptions::InvalidSettingsException, "Multiple explicit input models"); // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); + STORM_LOG_THROW(numSymbolicInputs + numExplicitInputs <= 1, storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); // Make sure PRISM-to-JANI conversion is only set if the actual input is in PRISM format. STORM_LOG_THROW(!isPrismToJaniSet() || isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the transformation from PRISM to JANI, the input model must be given in the prism format."); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index b812fd936..a23ade12f 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -1,6 +1,8 @@ #ifndef STORM_SETTINGS_MODULES_IOSETTINGS_H_ #define STORM_SETTINGS_MODULES_IOSETTINGS_H_ +#include + #include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" @@ -270,6 +272,31 @@ namespace storm { */ bool isToNondeterministicModelSet() const; + /*! + * Retrieves whether the input model is to be read from the quantitative verification benchmark set (QVBS) + */ + bool isQvbsInputSet() const; + + /*! + * Retrieves the specified model (short-)name of the QVBS + */ + std::string getQvbsModelName() const; + + /*! + * Retrieves the selected model instance (file + open parameters of the model) + */ + uint64_t getQvbsInstanceIndex() const; + + /*! + * Retrieves the selected property names + */ + boost::optional> getQvbsPropertyFilter() const; + + /*! + * Retrieves the specified root directory of qvbs + */ + std::string getQvbsRoot() const; + bool check() const override; void finalize() override; @@ -302,6 +329,9 @@ namespace storm { static const std::string propertyOptionName; static const std::string propertyOptionShortName; static const std::string toNondetOptionName; + static const std::string qvbsInputOptionName; + static const std::string qvbsInputOptionShortName; + static const std::string qvbsRootOptionName; };