jani/Automaton: Implemented possibility to clone an automaton.

src/storm/storage/jani/Automaton.cpp

@@ -4,6 +4,7 @@
 #include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/Location.h"
 #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
+#include "storm/storage/expressions/ExpressionManager.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/WrongFormatException.h"
@@ -21,6 +22,24 @@ namespace storm {
             locationToStartingIndex.push_back(0);
         }
         
+        storm::expressions::Variable cloneVariable(storm::expressions::ExpressionManager& manager, storm::expressions::Variable const& var, std::string const& variablePrefix) {
+            STORM_LOG_ASSERT(var.getManager() == manager, "expected same manager.");
+            return manager.declareVariable(variablePrefix + var.getName(), var.getType());
+        }
+        
+        Automaton Automaton::clone(storm::expressions::ExpressionManager& manager, std::string const& nameOfClone, std::string const& variablePrefix) const {
+            Automaton result(*this);
+            result.name = nameOfClone;
+            result.locationExpressionVariable = cloneVariable(manager, result.locationExpressionVariable, variablePrefix);
+            auto allVars = result.getAllExpressionVariables();
+            std::map<storm::expressions::Variable, storm::expressions::Expression> oldToNewVarMap;
+            for (auto const& v : allVars) {
+                oldToNewVarMap[v] = cloneVariable(manager, v, variablePrefix).getExpression();
+            }
+            result.variables.substituteExpressionVariables(oldToNewVarMap);
+            result.substitute(oldToNewVarMap);
+        }
+        
         std::string const& Automaton::getName() const {
             return name;
         }

src/storm/storage/jani/Automaton.h

@@ -40,6 +40,8 @@ namespace storm {
             Automaton(Automaton&& other) = default;
             Automaton& operator=(Automaton&& other) = default;
             
+            Automaton clone(storm::expressions::ExpressionManager& manager, std::string const& nameOfClone, std::string const& variablePrefix) const;
+            
             /*!
              * Retrieves the name of the automaton.
              */

src/storm/storage/jani/Variable.cpp

@@ -26,6 +26,10 @@ namespace storm {
         storm::expressions::Variable const& Variable::getExpressionVariable() const {
             return variable;
         }
+        
+        void Variable::setExpressionVariable(storm::expressions::Variable const& newVariable) {
+            variable = newVariable;
+        }
 
         std::string const& Variable::getName() const {
             return name;

src/storm/storage/jani/Variable.h

@@ -41,6 +41,11 @@ namespace storm {
              */
             storm::expressions::Variable const& getExpressionVariable() const;
             
+            /*!
+             * Sets the associated expression variable.
+             */
+            void setExpressionVariable(storm::expressions::Variable const& newVariable);
+            
             /*!
              * Retrieves the name of the variable.
              */

src/storm/storage/jani/VariableSet.cpp

@@ -1,5 +1,6 @@
 #include "storm/storage/jani/VariableSet.h"
 
+#include "storm/storage/expressions/Expressions.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -439,5 +440,15 @@ namespace storm {
                 variable->substitute(substitution);
             }
         }
+        
+        void VariableSet::substituteExpressionVariables(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            for (auto& variable : variables) {
+                auto varIt = substitution.find(variable->getExpressionVariable());
+                if (varIt != substitution.end()) {
+                    STORM_LOG_ASSERT(varIt->second.isVariable(), "Expected that variables are only substituted by other variables. However, we substitute " << varIt->first.getName() << " by " << varIt->second << ".");
+                    variable->setExpressionVariable(varIt->second.getBaseExpression().asVariableExpression().getVariable());
+                }
+            }
+        }
     }
 }

src/storm/storage/jani/VariableSet.h

@@ -282,6 +282,14 @@ namespace storm {
              */
             void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
             
+            /*!
+             * Substitutes the actual variables according to the given substitution.
+             * @param substitution The substitution. Assumed to only map variables to VariableExpressions.
+             * @note does not substitute variables in initial expressions, variable bounds, ...
+             */
+            void substituteExpressionVariables(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
+            
         private:
             /// The vector of all variables.
             std::vector<std::shared_ptr<Variable>> variables;