prism2jani no longer fails if a reward model has the same name as a formula/variable

src/storm-cli-utilities/model-handling.h

@@ -136,16 +136,11 @@ namespace storm {
                 
                 if (transformToJani) {
                     storm::prism::Program const& model = output.model.get().asPrismProgram();
-                    auto modelAndRenaming = model.toJaniWithLabelRenaming(true, "", false);
-                    output.model = modelAndRenaming.first;
-                    
-                    if (!modelAndRenaming.second.empty()) {
-                        std::map<std::string, std::string> const& labelRenaming = modelAndRenaming.second;
-                        std::vector<storm::jani::Property> amendedProperties;
-                        for (auto const& property : output.properties) {
-                            amendedProperties.emplace_back(property.substituteLabels(labelRenaming));
-                        }
-                        output.preprocessedProperties = std::move(amendedProperties);
+                    auto modelAndProperties = model.toJani(output.properties, true, "", false);
+                    output.model = modelAndProperties.first;
+                    
+                    if (!modelAndProperties.second.empty()) {
+                        output.preprocessedProperties = std::move(modelAndProperties.second);
                     }
                 }
             }

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

@@ -36,7 +36,7 @@ namespace storm {
             }
             
             auto uneliminatedFeatures = janiModel.restrictToFeatures(options.allowedModelFeatures);
-            STORM_LOG_WARN(uneliminatedFeatures.empty(), "The following model features could not be eliminated: " << uneliminatedFeatures.toString());
+            STORM_LOG_WARN_COND(uneliminatedFeatures.empty(), "The following model features could not be eliminated: " << uneliminatedFeatures.toString());
             
             if (options.modelName) {
                 janiModel.setName(options.modelName.get());
@@ -44,15 +44,15 @@ namespace storm {
         }
         
         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) {
-            std::pair<storm::jani::Model, std::vector<storm::jani::Property>> res;
         
             // Perform conversion
-            auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix, options.janiOptions.standardCompliant);
-            res.first = std::move(modelAndRenaming.first);
-        
-            // Amend properties to potentially changed labels
-            for (auto const& property : properties) {
-                res.second.emplace_back(property.substituteLabels(modelAndRenaming.second));
+            auto res = program.toJani(properties, true, "", false);
+            if (res.second.empty()) {
+                std::vector<storm::jani::Property> clondedProperties;
+                for (auto const& p : properties) {
+                    clondedProperties.push_back(p.clone());
+                }
+                res.second = std::move(clondedProperties);
             }
             
             // Postprocess Jani model based on the options

src/storm/storage/SymbolicModelDescription.cpp

@@ -5,6 +5,7 @@
 #include "storm/utility/jani.h"
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/jani/Automaton.h"
 
 
@@ -130,13 +131,13 @@ namespace storm {
             }
         }
         
-        std::pair<SymbolicModelDescription, std::map<std::string, std::string>> SymbolicModelDescription::toJaniWithLabelRenaming(bool makeVariablesGlobal, bool standardCompliant) const {
+        std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> SymbolicModelDescription::toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal, bool standardCompliant) const {
             if (this->isJaniModel()) {
-                return std::make_pair(*this, std::map<std::string, std::string>());
+                return std::make_pair(*this, std::vector<storm::jani::Property>());
             }
             if (this->isPrismProgram()) {
-                auto modelAndRenaming = this->asPrismProgram().toJaniWithLabelRenaming(makeVariablesGlobal, "", standardCompliant);
-                return std::make_pair(SymbolicModelDescription(modelAndRenaming.first), modelAndRenaming.second);
+                auto modelProperties = this->asPrismProgram().toJani(properties, makeVariablesGlobal, "", standardCompliant);
+                return std::make_pair(SymbolicModelDescription(modelProperties.first), modelProperties.second);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
             }

src/storm/storage/SymbolicModelDescription.h

@@ -39,7 +39,16 @@ namespace storm {
             std::vector<std::string> getParameterNames() const;
             
             SymbolicModelDescription toJani(bool makeVariablesGlobal = true, bool standardCompliant = false) const;
-            std::pair<SymbolicModelDescription, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool makeVariablesGlobal = true, bool standardCompliant = false) const;
+            
+            /*!
+             * Ensures that this model is a JANI model by, e.g., converting prism to jani.
+             * If labels or reward models had to be converted during conversion, the renamings are applied to the given properties
+             *
+             * @return The jani model of this and either the new set of properties or an empty vector if no renamings were necessary
+             *
+             * @note The returned property vector might be empty in case no renaming is necessary.
+             */
+            std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal, bool standardCompliant) const;
             
             SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
             SymbolicModelDescription preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;

src/storm/storage/prism/Program.cpp

@@ -1741,15 +1741,20 @@ namespace storm {
         
         storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const {
             ToJaniConverter converter;
-            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant);
+            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant);
             STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
-            return resultingModel;
+            STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
+            return janiModel;
         }
 
-        std::pair<storm::jani::Model, std::map<std::string, std::string>> Program::toJaniWithLabelRenaming(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const {
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix, bool standardCompliant) const {
             ToJaniConverter converter;
-            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant);
-            return std::make_pair(resultingModel, converter.getLabelRenaming());
+            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant);
+            std::vector<storm::jani::Property> newProperties;
+            if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
+                newProperties = converter.applyRenaming(properties);
+            }
+            return std::make_pair(janiModel, newProperties);
         }
 
         storm::expressions::ExpressionManager& Program::getManager() const {

src/storm/storage/prism/Program.h

@@ -626,10 +626,11 @@ namespace storm {
             storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const;
             
             /*!
-             * Converts the PRISM model into an equivalent JANI model and retrieves possible label renamings that had
-             * to be performed in the process.
+             * Converts the PRISM model into an equivalent JANI model and if labels or reward models had
+             * to be renamed in the process, the renamings are applied to the given properties
+             * @return The jani model of this and either the new set of properties or an empty vector if no renamings were necessary
              */
-            std::pair<storm::jani::Model, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const;
+            std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const;
             
         private:
             /*!

src/storm/storage/prism/ToJaniConverter.cpp

@@ -5,6 +5,7 @@
 #include "storm/storage/prism/Program.h"
 #include "storm/storage/prism/CompositionToJaniVisitor.h"
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/expressions/FunctionCallExpression.h"
 
@@ -17,6 +18,9 @@ namespace storm {
     namespace prism {
         
         storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix, bool standardCompliant) {
+            labelRenaming.clear();
+            rewardModelRenaming.clear();
+            
             std::shared_ptr<storm::expressions::ExpressionManager> manager = program.getManager().getSharedPointer();
             
             bool produceStateRewards = !standardCompliant || program.getModelType() == storm::prism::Program::ModelType::CTMC || program.getModelType() == storm::prism::Program::ModelType::MA;
@@ -125,7 +129,7 @@ namespace storm {
                 bool renameLabel = manager->hasVariable(label.getName()) || program.hasRewardModel(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.");
+                    STORM_LOG_INFO("Label '" << label.getName() << "' was renamed to '" << finalLabelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists.");
                     labelRenaming[label.getName()] = finalLabelName;
                 }
                 auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName);
@@ -155,8 +159,22 @@ namespace storm {
             // edges and transient assignments that are added to the locations.
             std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments;
             for (auto const& rewardModel : program.getRewardModels()) {
-                auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default_reward_model" : rewardModel.getName());
-                storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true));
+                std::string finalRewardModelName;
+                if (rewardModel.getName().empty()) {
+                    finalRewardModelName = "default_reward_model";
+                } else {
+                    if (manager->hasVariable(rewardModel.getName())) {
+                        // Rename
+                        finalRewardModelName = "rewardmodel_" + rewardModel.getName() + suffix;
+                        STORM_LOG_INFO("Rewardmodel '" << rewardModel.getName() << "' was renamed to '" << finalRewardModelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists.");
+                        rewardModelRenaming[rewardModel.getName()] = finalRewardModelName;
+                    } else {
+                        finalRewardModelName = rewardModel.getName();
+                    }
+                }
+                
+                auto newExpressionVariable = manager->declareRationalVariable(finalRewardModelName);
+                storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(finalRewardModelName, newExpressionVariable, manager->rational(0.0), true));
                 
                 if (rewardModel.hasStateRewards()) {
                     storm::expressions::Expression transientLocationExpression;
@@ -375,9 +393,40 @@ namespace storm {
             return !labelRenaming.empty();
         }
         
+        bool ToJaniConverter::rewardModelsWereRenamed() const {
+            return !rewardModelRenaming.empty();
+        }
+        
         std::map<std::string, std::string> const& ToJaniConverter::getLabelRenaming() const {
             return labelRenaming;
         }
         
+        std::map<std::string, std::string> const& ToJaniConverter::getRewardModelRenaming() const {
+            return rewardModelRenaming;
+        }
+        
+        storm::jani::Property ToJaniConverter::applyRenaming(storm::jani::Property const& property) const {
+            if (rewardModelsWereRenamed()) {
+                auto res = property.substituteRewardModelNames(getRewardModelRenaming());
+                if (labelsWereRenamed()) {
+                    res = res.substituteLabels(getLabelRenaming());
+                }
+                return res;
+            } else {
+                if (labelsWereRenamed()) {
+                    return property.substituteLabels(getLabelRenaming());
+                } else {
+                    return property.clone();
+                }
+            }
+        }
+        
+        std::vector<storm::jani::Property> ToJaniConverter::applyRenaming(std::vector<storm::jani::Property> const& properties) const {
+            std::vector<storm::jani::Property> result;
+            for (auto const& p : properties) {
+                result.push_back(applyRenaming(p));
+            }
+            return result;
+        }
     }
 }

src/storm/storage/prism/ToJaniConverter.h

@@ -6,6 +6,7 @@
 namespace storm {
     namespace jani {
         class Model;
+        class Property;
     }
     
     namespace prism {
@@ -17,10 +18,16 @@ namespace storm {
             storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false);
             
             bool labelsWereRenamed() const;
+            bool rewardModelsWereRenamed() const;
             std::map<std::string, std::string> const& getLabelRenaming() const;
+            std::map<std::string, std::string> const& getRewardModelRenaming() const;
+            
+            storm::jani::Property applyRenaming(storm::jani::Property const& property) const;
+            std::vector<storm::jani::Property> applyRenaming(std::vector<storm::jani::Property> const& property) const;
             
         private:
             std::map<std::string, std::string> labelRenaming;
+            std::map<std::string, std::string> rewardModelRenaming;
         };
         
     }