diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index aa5c1896e..95ca5c4ee 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -18,8 +18,12 @@ namespace storm { void transformJani(storm::jani::Model& janiModel, std::vector<storm::jani::Property>& properties, storm::converter::JaniConversionOptions const& options) { + if (options.replaceUnassignedVariablesWithConstants) { + janiModel.replaceUnassignedVariablesWithConstants(); + } + if (options.substituteConstants) { - janiModel = janiModel.substituteConstants(); + janiModel.substituteConstantsInPlace(); } if (options.localVars) { diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index e4df3bf5b..c8a4ab8a3 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -3,11 +3,11 @@ namespace storm { namespace converter { - JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { + JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(false) { // Intentionally left empty } - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(settings.isReplaceUnassignedVariablesWithConstantsSet()) { if (settings.isEliminateFunctionsSet()) { allowedModelFeatures.remove(storm::jani::ModelFeature::Functions); } diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h index 8ecf1ca56..65f6f7ce5 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -39,9 +39,11 @@ namespace storm { /// Only these model features are allowed in the output storm::jani::ModelFeatures allowedModelFeatures; - // Add constants that are defined in the properties to the model + /// Add constants that are defined in the properties to the model bool addPropertyConstants; + /// If set, local and global variables that are (a) not assigned to some value and (b) have a known initial value are replaced by constants. + bool replaceUnassignedVariablesWithConstants; }; } } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 11fb061cf..cc6aeef29 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp @@ -22,6 +22,7 @@ namespace storm { const std::string JaniExportSettings::compactJsonOptionName = "compactjson"; const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays"; const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions"; + const std::string JaniExportSettings::replaceUnassignedVariablesWithConstantsOptionName = "replace-unassigned-vars"; 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 of automaton and local variable names seperated by a dot, e.g. A.x,B.y.").setDefaultValueString("").build()).build()); @@ -32,6 +33,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, replaceUnassignedVariablesWithConstantsOptionName, false, "If set, local and global variables that are (a) not assigned to some value and (b) have a known initial value are replaced by constants.").build()); } bool JaniExportSettings::isAllowEdgeAssignmentsSet() const { @@ -82,6 +84,10 @@ namespace storm { return this->getOption(eliminateFunctionsOptionName).getHasOptionBeenSet(); } + bool JaniExportSettings::isReplaceUnassignedVariablesWithConstantsSet() const { + return this->getOption(replaceUnassignedVariablesWithConstantsOptionName).getHasOptionBeenSet(); + } + void JaniExportSettings::finalize() { } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index 469ef6b71..c91097b5f 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -29,6 +29,8 @@ namespace storm { bool isEliminateArraysSet() const; bool isEliminateFunctionsSet() const; + + bool isReplaceUnassignedVariablesWithConstantsSet() const; std::vector<std::pair<std::string, std::string>> getLocationVariables() const; @@ -46,6 +48,7 @@ namespace storm { static const std::string compactJsonOptionName; static const std::string eliminateArraysOptionName; static const std::string eliminateFunctionsOptionName; + static const std::string replaceUnassignedVariablesWithConstantsOptionName; }; }