simplified processing of janiConversionOptions

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.");
             }

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());

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);
+            }
         };
     }
 }

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;
             
         };
     }