conversion input settings now properly take a jani property filter

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<std::string> ConversionInputSettings::getSelectedJaniProperties() const {
+                return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString());
+            }
+
 			void ConversionInputSettings::finalize() {
                 // Intentionally left empty.
             }

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<std::string> 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;
             };