From 8c37d4eade812519e31b4c018b336893d0b34dea Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 27 Sep 2018 11:45:45 +0200 Subject: [PATCH] conversion input settings now properly take a jani property filter --- .../modules/ConversionInputSettings.cpp | 27 +++++++++++++++++-- .../modules/ConversionInputSettings.h | 23 +++++++++++++++- 2 files changed, 47 insertions(+), 3 deletions(-) diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.cpp b/src/storm-conv/settings/modules/ConversionInputSettings.cpp index 090efe901..b1522ab4f 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.cpp +++ b/src/storm-conv/settings/modules/ConversionInputSettings.cpp @@ -5,6 +5,7 @@ #include "storm/settings/OptionBuilder.h" #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include "storm/parser/CSVParser.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -21,20 +22,30 @@ namespace storm { const std::string ConversionInputSettings::prismCompatibilityOptionName = "prismcompat"; const std::string ConversionInputSettings::prismCompatibilityOptionShortName = "pc"; const std::string ConversionInputSettings::janiInputOptionName = "jani"; - + const std::string ConversionInputSettings::janiPropertyOptionName = "janiproperty"; + const std::string ConversionInputSettings::janiPropertyOptionShortName = "jprop"; + ConversionInputSettings::ConversionInputSettings() : ModuleSettings(moduleName) { + // General 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()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build()) .build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (e.g., via --" + prismInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + + // Prism related this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + + // Jani related this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + 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()); + } bool ConversionInputSettings::isPrismInputSet() const { @@ -77,6 +88,18 @@ namespace storm { return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); } + bool ConversionInputSettings::isJaniPropertiesSet() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); + } + + bool ConversionInputSettings::areJaniPropertiesSelected() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet() && (this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString() != ""); + } + + std::vector ConversionInputSettings::getSelectedJaniProperties() const { + return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); + } + void ConversionInputSettings::finalize() { // Intentionally left empty. } diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.h b/src/storm-conv/settings/modules/ConversionInputSettings.h index 27e0b4795..2ca110a20 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.h +++ b/src/storm-conv/settings/modules/ConversionInputSettings.h @@ -31,7 +31,7 @@ namespace storm { */ std::string getPropertyInputFilter() const; - /*! + /*! * Retrieves whether constant definition option was set. * * @return True if the constant definition option was set. @@ -73,6 +73,25 @@ namespace storm { */ std::string getJaniInputFilename() const; + /*! + * Retrieves whether the jani-property option was set + * @return + */ + bool isJaniPropertiesSet() const; + + /*! + * Retrieves whether one or more jani-properties have been selected + * @return + */ + bool areJaniPropertiesSelected() const; + + /*! + * @return The names of the jani properties to check + */ + std::vector getSelectedJaniProperties() const; + + + bool check() const override; void finalize() override; @@ -89,6 +108,8 @@ namespace storm { static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; static const std::string janiInputOptionName; + static const std::string janiPropertyOptionName; + static const std::string janiPropertyOptionShortName; };