Using JaniExportSettings in storm-conv

src/storm-conv-cli/storm-conv.cpp

@@ -16,6 +16,7 @@
 
 
 #include "storm-cli-utilities/cli.h"
+#include "storm/exceptions/OptionParserException.h"
 
 namespace storm {
     namespace conv {
@@ -40,15 +41,18 @@ namespace storm {
         }
         
         void processPrismInputJaniOutput(storm::prism::Program const& prismProg, std::vector<storm::jani::Property> const& properties) {
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+            auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
             
             storm::converter::PrismToJaniConverterOptions options;
             options.allVariablesGlobal = true;
-            // TODO: fill in options
+            options.suffix = "";
+            options.janiOptions.standardCompliant = jani.isExportAsStandardJaniSet();
+            options.janiOptions.locationVariables = jani.getLocationVariables();
+            options.janiOptions.exportFlattened = jani.isExportFlattenedSet();
             auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
-
             
-            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
-            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
             std::string outputFilename = "";
             if (output.isJaniOutputFilenameSet()) {
                 outputFilename = output.getJaniOutputFilename();
@@ -116,6 +120,35 @@ namespace storm {
     }
 }
 
+bool parseOptions(const int argc, const char* argv[]) {
+    try {
+        storm::settings::mutableManager().setFromCommandLine(argc, argv);
+    } catch (storm::exceptions::OptionParserException& e) {
+        storm::settings::manager().printHelp();
+        throw e;
+        return false;
+    }
+    
+    auto const& general = storm::settings::getModule<storm::settings::modules::ConversionGeneralSettings>();
+    
+    // Set options from config file (if given)
+    if (general.isConfigSet()) {
+        storm::settings::mutableManager().setFromConfigurationFile(general.getConfigFilename());
+    }
+
+    bool result = true;
+    if (general.isHelpSet()) {
+        storm::settings::manager().printHelp(general.getHelpModuleName());
+        result = false;
+    }
+    
+    if (general.isVersionSet()) {
+        storm::cli::printVersion("storm-conv");
+        result = false;;
+    }
+
+    return result;
+}
 
 /*!
  * Main entry point of the executable storm-conv.
@@ -129,7 +162,7 @@ int main(const int argc, const char** argv) {
         bool outputToStdOut = false;
         for (int i = 1; i < argc; ++i) {
             if (std::string(argv[i]) == "--" + storm::settings::modules::ConversionOutputSettings::stdoutOptionName) {
-                outputToStdOut = false;
+                outputToStdOut = true;
             }
         }
         if (outputToStdOut) {
@@ -139,7 +172,7 @@ int main(const int argc, const char** argv) {
         }
         
         storm::settings::initializeConvSettings("Storm-conv", "storm-conv");
-        if (!storm::cli::parseOptions(argc, argv)) {
+        if (!parseOptions(argc, argv)) {
             return -1;
         }
 

src/storm-conv/api/storm-conv.h

@@ -34,7 +34,7 @@ namespace storm {
             std::pair<storm::jani::Model, std::vector<storm::jani::Property>> res;
         
             // Perform conversion
-            auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix);
+            auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix, options.janiOptions.standardCompliant);
             res.first = std::move(modelAndRenaming.first);
         
             // Amend properties to potentially changed labels

src/storm-conv/settings/ConvSettings.cpp

@@ -3,19 +3,21 @@
 #include "storm-conv/settings/modules/ConversionGeneralSettings.h"
 #include "storm-conv/settings/modules/ConversionInputSettings.h"
 #include "storm-conv/settings/modules/ConversionOutputSettings.h"
+#include "storm-conv/settings/modules/JaniExportSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 
 
 namespace storm {
     namespace settings {
-        void initializeParsSettings(std::string const& name, std::string const& executableName) {
+        void initializeConvSettings(std::string const& name, std::string const& executableName) {
             storm::settings::mutableManager().setName(name, executableName);
         
             // Register relevant settings modules.
             storm::settings::addModule<storm::settings::modules::ConversionGeneralSettings>();
             storm::settings::addModule<storm::settings::modules::ConversionInputSettings>();
             storm::settings::addModule<storm::settings::modules::ConversionOutputSettings>();
+            storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
         }
     
     }

src/storm-conv/settings/modules/ConversionInputSettings.cpp

@@ -71,8 +71,6 @@ namespace storm {
             }
 
             bool ConversionInputSettings::check() const {
-                // Ensure that exactly one input is specified
-                STORM_LOG_THROW(isPrismInputSet(), storm::exceptions::InvalidSettingsException, "No Input specified.");
                 return true;
             }
             

src/storm-conv/settings/modules/ConversionOutputSettings.cpp

@@ -20,7 +20,7 @@ namespace storm {
             ConversionOutputSettings::ConversionOutputSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, stdoutOptionName, false, "If set, the output will be printed to stdout.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiOutputOptionName, false, "converts the input model to Jani.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("")).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("").build()).build());
             }
             
             bool ConversionOutputSettings::isStdOutOutputEnabled() const {
@@ -48,8 +48,6 @@ namespace storm {
             }
 
             bool ConversionOutputSettings::check() const {
-                // Ensure that exactly one Output is specified
-                STORM_LOG_THROW(isJaniOutputSet(), storm::exceptions::InvalidSettingsException, "No Output specified.");
                 STORM_LOG_THROW(!isJaniOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getJaniOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getJaniOutputFilename());
                 return true;
             }

src/storm-conv/settings/modules/JaniExportSettings.cpp

@@ -14,8 +14,6 @@ namespace storm {
         namespace modules {
             const std::string JaniExportSettings::moduleName = "exportJani";
             
-            const std::string JaniExportSettings::janiFileOptionName = "jani-output";
-            const std::string JaniExportSettings::janiFileOptionShortName = "output";
             const std::string JaniExportSettings::standardCompliantOptionName = "standard-compliant";
             const std::string JaniExportSettings::standardCompliantOptionShortName = "standard";
             const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
@@ -23,20 +21,11 @@ namespace storm {
 
             
             JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, janiFileOptionName, false, "Destination for the jani model.").setShortName(janiFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list with local variables.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, true, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
             }
             
-            bool JaniExportSettings::isJaniFileSet() const {
-                return this->getOption(janiFileOptionName).getHasOptionBeenSet();
-            }
-            
-            std::string JaniExportSettings::getJaniFilename() const {
-                return this->getOption(janiFileOptionName).getArgumentByName("filename").getValueAsString();
-            }
-            
             bool JaniExportSettings::isExportAsStandardJaniSet() const {
                 return this->getOption(standardCompliantOptionName).getHasOptionBeenSet();
             }