implemented functionality to rename reward model names

src/storm/logic/Formula.cpp

@@ -6,6 +6,7 @@
 #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 #include "storm/logic/ExpressionSubstitutionVisitor.h"
 #include "storm/logic/LabelSubstitutionVisitor.h"
+#include "storm/logic/RewardModelNameSubstitutionVisitor.h"
 #include "storm/logic/ToExpressionVisitor.h"
 
 namespace storm {
@@ -458,6 +459,11 @@ namespace storm {
             return visitor.substitute(*this);
         }
         
+        std::shared_ptr<Formula> Formula::substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const {
+            RewardModelNameSubstitutionVisitor visitor(rewardModelNameSubstitution);
+            return visitor.substitute(*this);
+        }
+        
         storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) const {
             ToExpressionVisitor visitor;
             if (labelToExpressionMapping.empty()) {

src/storm/logic/Formula.h

@@ -201,6 +201,7 @@ namespace storm {
             std::shared_ptr<Formula> substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& expressionSubstitution) const;
             std::shared_ptr<Formula> substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const;
             std::shared_ptr<Formula> substitute(std::map<std::string, std::string> const& labelSubstitution) const;
+            std::shared_ptr<Formula> substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const;
 
             /*!
              * Takes the formula and converts it to an equivalent expression. The formula may contain atomic labels, but

src/storm/logic/RewardModelNameSubstitutionVisitor.cpp

@@ -0,0 +1,96 @@
+#include "storm/logic/RewardModelNameSubstitutionVisitor.h"
+#include "storm/logic/Formulas.h"
+
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/traverser/AssignmentsFinder.h"
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+
+        RewardModelNameSubstitutionVisitor::RewardModelNameSubstitutionVisitor(std::map<std::string, std::string> const& rewardModelNameMapping) : rewardModelNameMapping(rewardModelNameMapping) {
+            // Intentionally left empty
+        }
+        
+        std::shared_ptr<Formula> RewardModelNameSubstitutionVisitor::substitute(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+        
+        boost::any RewardModelNameSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
+            std::vector<TimeBoundReference> timeBoundReferences;
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                if (f.hasLowerBound(i)) {
+                    lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i)));
+                } else {
+                    lowerBounds.emplace_back();
+                }
+                if (f.hasUpperBound(i)) {
+                    upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i)));
+                } else {
+                    upperBounds.emplace_back();
+                }
+                auto const& tbr = f.getTimeBoundReference(i);
+                if (tbr.isRewardBound()) {
+                    timeBoundReferences.emplace_back(getNewName(tbr.getRewardName()), tbr.getOptionalRewardAccumulation());
+                } else {
+                    timeBoundReferences.push_back(tbr);
+                }
+            }
+            if (f.hasMultiDimensionalSubformulas()) {
+                std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
+                for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                    leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
+                    rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
+                }
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
+            } else {
+                std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+                std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
+            }
+        }
+        
+        boost::any RewardModelNameSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            std::vector<TimeBound> bounds;
+            std::vector<TimeBoundReference> timeBoundReferences;
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i)));
+                storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i);
+                if (tbr.isRewardBound()) {
+                    tbr = storm::logic::TimeBoundReference(getNewName(tbr.getRewardName()), tbr.getOptionalRewardAccumulation());
+                }
+                timeBoundReferences.push_back(std::move(tbr));
+            }
+            if (f.hasRewardAccumulation()) {
+                return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, f.getRewardAccumulation()));
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences));
+            }
+        }
+        
+        boost::any RewardModelNameSubstitutionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            if (f.hasRewardModelName()) {
+                return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, getNewName(f.getRewardModelName()), f.getOperatorInformation()));
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, boost::none, f.getOperatorInformation()));
+            }
+        }
+        
+        std::string const& RewardModelNameSubstitutionVisitor::getNewName(std::string const& oldName) const {
+            auto nameIt = rewardModelNameMapping.find(oldName);
+            if (nameIt == rewardModelNameMapping.end()) {
+                return oldName;
+            } else {
+                return nameIt->second;
+            }
+        }
+
+        
+    }
+}

src/storm/logic/RewardModelNameSubstitutionVisitor.h

@@ -0,0 +1,30 @@
+#pragma once
+
+#include <map>
+
+#include "storm/logic/CloneVisitor.h"
+
+#include "storm/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace logic {
+        
+        class RewardModelNameSubstitutionVisitor : public CloneVisitor {
+        public:
+            RewardModelNameSubstitutionVisitor(std::map<std::string, std::string> const& rewardModelNameMapping);
+            
+            std::shared_ptr<Formula> substitute(Formula const& f) const;
+            
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+            
+        private:
+            
+            std::string const& getNewName(std::string const& oldName) const;
+            
+            std::map<std::string, std::string> const& rewardModelNameMapping;
+        };
+        
+    }
+}

src/storm/logic/TimeBoundType.h

@@ -59,6 +59,11 @@ namespace storm {
                 return rewardAccumulation.get();
             }
             
+            boost::optional<RewardAccumulation> const& getOptionalRewardAccumulation() const {
+                assert(isRewardBound());
+                return rewardAccumulation;
+            }
+            
         };
 
 

src/storm/storage/jani/Property.cpp

@@ -38,6 +38,16 @@ namespace storm {
             return Property(name, filterExpression.substituteLabels(substitution), comment);
         }
         
+        Property Property::substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const {
+            return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), comment);
+        }
+        
+        Property Property::clone() const {
+            return Property(name, filterExpression.clone(), comment);
+        }
+        
+
+        
         FilterExpression const& Property::getFilter() const {
             return this->filterExpression;
         }

src/storm/storage/jani/Property.h

@@ -5,6 +5,7 @@
 #include "storm/modelchecker/results/FilterType.h"
 #include "storm/logic/Formulas.h"
 #include "storm/logic/FragmentSpecification.h"
+#include "storm/logic/CloneVisitor.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -64,6 +65,15 @@ namespace storm {
                 return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution));
             }
             
+            FilterExpression substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const {
+                return FilterExpression(formula->substituteRewardModelNames(rewardModelNameSubstitution), ft, statesFormula->substituteRewardModelNames(rewardModelNameSubstitution));
+            }
+            
+            FilterExpression clone() const {
+                storm::logic::CloneVisitor cv;
+                return FilterExpression(cv.clone(*formula), ft, cv.clone(*statesFormula));
+            }
+            
         private:
             // For now, we assume that the states are always the initial states.
             std::shared_ptr<storm::logic::Formula const> formula;
@@ -111,6 +121,8 @@ namespace storm {
             Property substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             Property substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction) const;
             Property substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const;
+            Property substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const;
+            Property clone() const;
             
             FilterExpression const& getFilter() const;