Browse Source

added setting in storm-conv to make variables global

tempestpy_adaptions
TimQu 6 years ago
parent
commit
56a5dcf7cb
  1. 2
      src/storm-conv-cli/storm-conv.cpp
  2. 6
      src/storm-conv/settings/modules/JaniExportSettings.cpp
  3. 3
      src/storm-conv/settings/modules/JaniExportSettings.h

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

@ -46,7 +46,7 @@ namespace storm {
auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
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);

6
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() {
}

3
src/storm-conv/settings/modules/JaniExportSettings.h

@ -29,6 +29,8 @@ namespace storm {
bool isExportFlattenedSet() const;
bool isLocationVariablesSet() const;
bool isGlobalVarsSet() const;
std::vector<std::pair<std::string, std::string>> 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;
};
}

Loading…
Cancel
Save