From a4864f3c3dcaa615f392111335f6222b6721cbca Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 24 Jul 2018 15:40:27 +0200
Subject: [PATCH] Using JaniExportSettings in storm-conv
---
src/storm-conv-cli/storm-conv.cpp | 45 ++++++++++++++++---
src/storm-conv/api/storm-conv.h | 2 +-
src/storm-conv/settings/ConvSettings.cpp | 4 +-
.../modules/ConversionInputSettings.cpp | 2 -
.../modules/ConversionOutputSettings.cpp | 4 +-
.../settings/modules/JaniExportSettings.cpp | 11 -----
6 files changed, 44 insertions(+), 24 deletions(-)
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<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;
}
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<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
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::modules::ConversionGeneralSettings>();
storm::settings::addModule<storm::settings::modules::ConversionInputSettings>();
storm::settings::addModule<storm::settings::modules::ConversionOutputSettings>();
+ storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
}
}
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();
}