translate prism to jani with a suffix for location names etc when doing this for multiple models

src/storm/storage/prism/Program.cpp

@@ -1711,16 +1711,16 @@ namespace storm {
             return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
         }
         
-        storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
+        storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
             ToJaniConverter converter;
-            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal);
+            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix);
             STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
             return resultingModel;
         }
 
-        std::pair<storm::jani::Model, std::map<std::string, std::string>> Program::toJaniWithLabelRenaming(bool allVariablesGlobal) const {
+        std::pair<storm::jani::Model, std::map<std::string, std::string>> Program::toJaniWithLabelRenaming(bool allVariablesGlobal, std::string suffix) const {
             ToJaniConverter converter;
-            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal);
+            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix);
             return std::make_pair(resultingModel, converter.getLabelRenaming());
         }
 

src/storm/storage/prism/Program.h

@@ -603,13 +603,13 @@ namespace storm {
             /*!
              * Converts the PRISM model into an equivalent JANI model.
              */
-            storm::jani::Model toJani(bool allVariablesGlobal = false) const;
+            storm::jani::Model toJani(bool allVariablesGlobal = false, std::string suffix = "") const;
             
             /*!
              * Converts the PRISM model into an equivalent JANI model and retrieves possible label renamings that had
              * to be performed in the process.
              */
-            std::pair<storm::jani::Model, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool allVariablesGlobal = false) const;
+            std::pair<storm::jani::Model, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool allVariablesGlobal = false, std::string suffix = "") const;
             
         private:
             /*!

src/storm/storage/prism/ToJaniConverter.cpp

@@ -13,7 +13,7 @@
 namespace storm {
     namespace prism {
         
-        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal) {
+        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) {
             std::shared_ptr<storm::expressions::ExpressionManager> manager = program.getManager().getSharedPointer();
                         
             // Start by creating an empty JANI model.
@@ -95,11 +95,11 @@ namespace storm {
                 }
             }
             
-            // Go through the labels and construct assignments to transient variables that are added to the loctions.
+            // Go through the labels and construct assignments to transient variables that are added to the locations.
             std::vector<storm::jani::Assignment> transientLocationAssignments;
             for (auto const& label : program.getLabels()) {
                 bool renameLabel = manager->hasVariable(label.getName()) || program.hasRewardModel(label.getName());
-                std::string finalLabelName = renameLabel ? "label_" + label.getName() : label.getName();
+                std::string finalLabelName = renameLabel ? "label_" + label.getName() + suffix : label.getName();
                 if (renameLabel) {
                     STORM_LOG_WARN_COND(!renameLabel, "Label '" << label.getName() << "' was renamed to '" << finalLabelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists.");
                     labelRenaming[label.getName()] = finalLabelName;
@@ -161,7 +161,7 @@ namespace storm {
                 // Keep track of the action indices contained in this module.
                 std::set<uint_fast64_t> actionIndicesOfModule;
 
-                storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName()));
+                storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix));
                 for (auto const& variable : module.getIntegerVariables()) {
                     storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
                     std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];

src/storm/storage/prism/ToJaniConverter.h

@@ -14,7 +14,7 @@ namespace storm {
         
         class ToJaniConverter {
         public:
-            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false);
+            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false, std::string suffix = "");
             
             bool labelsWereRenamed() const;
             std::map<std::string, std::string> const& getLabelRenaming() const;