From 56a5dcf7cb6d5acb62123277dd7bcf72f0c5e939 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 31 Jul 2018 16:43:41 +0200 Subject: [PATCH] added setting in storm-conv to make variables global --- src/storm-conv-cli/storm-conv.cpp | 2 +- src/storm-conv/settings/modules/JaniExportSettings.cpp | 6 ++++++ src/storm-conv/settings/modules/JaniExportSettings.h | 3 +++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index e1199cc1d..c398ef69a 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -46,7 +46,7 @@ namespace storm { auto const& jani = storm::settings::getModule(); storm::converter::PrismToJaniConverterOptions options; - options.allVariablesGlobal = true; + options.allVariablesGlobal = jani.isGlobalVarsSet(); options.suffix = ""; options.janiOptions = storm::converter::JaniConversionOptions(jani); auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options); diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 5e56ed782..4a84e637b 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp @@ -18,12 +18,14 @@ namespace storm { const std::string JaniExportSettings::standardCompliantOptionShortName = "standard"; const std::string JaniExportSettings::exportFlattenOptionName = "flatten"; const std::string JaniExportSettings::locationVariablesOptionName = "location-variables"; + const std::string JaniExportSettings::globalVariablesOptionName = "globalvars"; JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) { 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()); + this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, true, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build()); } bool JaniExportSettings::isExportAsStandardJaniSet() const { @@ -54,6 +56,10 @@ namespace storm { return result; } + bool JaniExportSettings::isGlobalVarsSet() const { + return this->getOption(exportFlattenOptionName).getHasOptionBeenSet(); + } + void JaniExportSettings::finalize() { } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index d61b923fc..90dc532f0 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -29,6 +29,8 @@ namespace storm { bool isExportFlattenedSet() const; bool isLocationVariablesSet() const; + + bool isGlobalVarsSet() const; std::vector> getLocationVariables() const; @@ -44,6 +46,7 @@ namespace storm { static const std::string standardCompliantOptionShortName; static const std::string exportFlattenOptionName; static const std::string locationVariablesOptionName; + static const std::string globalVariablesOptionName; }; }