add undefined constants in properties to the jani model when converting

src/storm-conv/api/storm-conv.cpp

@@ -2,6 +2,7 @@
 
 #include "storm/storage/prism/Program.h"
 #include "storm/storage/jani/Property.h"
+#include "storm/storage/jani/Constant.h"
 #include "storm/storage/jani/JaniLocationExpander.h"
 #include "storm/storage/jani/JSONExporter.h"
 
@@ -45,6 +46,17 @@ namespace storm {
             if (options.modelName) {
                 janiModel.setName(options.modelName.get());
             }
+            
+            if (options.addPropertyConstants) {
+                for (auto& f : properties) {
+                    for (auto const& constant : f.getUndefinedConstants()) {
+                        if (!janiModel.hasConstant(constant.getName())) {
+                            janiModel.addConstant(storm::jani::Constant(constant.getName(), constant));
+                        }
+                    }
+                }
+            }
+            
         }
         
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {

src/storm-conv/converter/options/JaniConversionOptions.cpp

@@ -3,11 +3,11 @@
 namespace storm {
     namespace converter {
 
-        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
+        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) {
             // Intentionally left empty
         }
 
-        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
+        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) {
             if (settings.isEliminateFunctionsSet()) {
                 allowedModelFeatures.remove(storm::jani::ModelFeature::Functions);
             }

src/storm-conv/converter/options/JaniConversionOptions.h

@@ -33,6 +33,9 @@ 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
+            bool addPropertyConstants;
+            
         };
     }
 }