diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 97fbcdfaf..2c24a8721 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/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 const& properties) { + auto const& output = storm::settings::getModule(); + auto const& input = storm::settings::getModule(); + auto const& jani = storm::settings::getModule(); 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(); - auto const& input = storm::settings::getModule(); 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(); + + // 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; } diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h index 6e05795a8..499777517 100644 --- a/src/storm-conv/api/storm-conv.h +++ b/src/storm-conv/api/storm-conv.h @@ -34,7 +34,7 @@ namespace storm { std::pair> 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 diff --git a/src/storm-conv/settings/ConvSettings.cpp b/src/storm-conv/settings/ConvSettings.cpp index 0582b80d8..cbb872390 100644 --- a/src/storm-conv/settings/ConvSettings.cpp +++ b/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::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } } diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.cpp b/src/storm-conv/settings/modules/ConversionInputSettings.cpp index e608aa0f3..cc91d597c 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.cpp +++ b/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; } diff --git a/src/storm-conv/settings/modules/ConversionOutputSettings.cpp b/src/storm-conv/settings/modules/ConversionOutputSettings.cpp index 958bdfdd9..61002078d 100644 --- a/src/storm-conv/settings/modules/ConversionOutputSettings.cpp +++ b/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; } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 09e236431..e9a9f9882 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/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(); }