diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 09e7d6b24..0227e9044 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -179,23 +179,22 @@ namespace storm { auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>(); // Parse the jani model - auto janiModelProperties = storm::api::parseJaniModel(input.getJaniInputFilename()); - storm::storage::SymbolicModelDescription janiModel(janiModelProperties.first); + auto janiModelProperties = storm::api::parseJaniModel(input.getJaniInputFilename(), storm::jani::getAllKnownModelFeatures()); // Parse properties (if available, otherwise take the ones from the jani file) std::vector<storm::jani::Property> properties; if (input.isPropertyInputSet()) { boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter()); - properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), janiModel, propertyFilter); + properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), janiModelProperties.first, propertyFilter); } else { for (auto const& p : janiModelProperties.second) { properties.push_back(p.second); } } - // Substitute constant definitions in program and properties. + // Substitute constant definitions in model and properties. std::string constantDefinitionString = input.getConstantDefinitionString(); - auto constantDefinitions = janiModel.parseConstantDefinitions(constantDefinitionString); - janiModel = janiModel.preprocess(constantDefinitions); + auto constantDefinitions = janiModelProperties.first.parseConstantDefinitions(constantDefinitionString); + auto janiModel = janiModelProperties.first..defineUndefinedConstants(constantDefinitions).substituteConstants(); if (!properties.empty()) { properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions); } @@ -203,7 +202,7 @@ namespace storm { // Branch on the type of output auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>(); if (output.isJaniOutputSet()) { - processJaniInputJaniOutput(janiModel.asJaniModel(), properties); + processJaniInputJaniOutput(janiModel, properties); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible."); } diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index 7b7f4d806..ff4d89276 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -35,13 +35,8 @@ namespace storm { janiModel.makeStandardJaniCompliant(); } - if (!options.allowArrays && janiModel.getModelFeatures().hasArrays()) { - janiModel.eliminateArrays(properties); - } - - if (!options.allowFunctions && janiModel.getModelFeatures().hasFunctions()) { - janiModel.substituteFunctions(properties); - } + auto uneliminatedFeatures = janiModel.restrictToFeatures(options.allowedModelFeatures); + STORM_LOG_WARN(uneliminatedFeatures.empty(), "The following model features could not be eliminated: " << uneliminatedFeatures.toString()); if (options.modelName) { janiModel.setName(options.modelName.get()); diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index 4b7a78d76..1fe36cfe2 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -3,12 +3,17 @@ namespace storm { namespace converter { - JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), flatten(false), allowArrays(true), allowFunctions(true) { + JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), flatten(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { // Intentionally left empty }; - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), allowArrays(!settings.isEliminateArraysSet()), allowFunctions(!settings.isEliminateFunctionsSet()) { - // Intentionally left empty + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + if (settings.isEliminateFunctionsSet()) { + allowedModelFeatures.remove(storm::jani::ModelFeature::Functions); + } + if (settings.isEliminateArraysSet()) { + allowedModelFeatures.remove(storm::jani::ModelFeature::Arrays); + } }; } } diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h index 34452315b..8758d480f 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -5,6 +5,7 @@ #include <boost/optional.hpp> #include "storm-conv/settings/modules/JaniExportSettings.h" +#include "storm/storage/jani/ModelFeatures.h" namespace storm { namespace converter { @@ -26,11 +27,8 @@ namespace storm { /// If given, the model will get this name boost::optional<std::string> modelName; - /// If not set, arrays in the model are eliminated - bool allowArrays; - - /// if not set, functions in the model are eliminated - bool allowFunctions; + /// Only these model features are allowed in the output + storm::jani::ModelFeatures allowedModelFeatures; }; }