From bc32853c281547bebb157686850f4d4af05dd25e Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 18 Mar 2019 14:51:10 +0100
Subject: [PATCH] Jani: Fixed an issue where initial expressions for unbounded
 variables have not been substituted correctly.

---
 src/storm/storage/jani/Automaton.cpp   | 11 ++---------
 src/storm/storage/jani/Model.cpp       | 10 +---------
 src/storm/storage/jani/VariableSet.cpp |  6 ++++++
 src/storm/storage/jani/VariableSet.h   |  7 +++++++
 4 files changed, 16 insertions(+), 18 deletions(-)

diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index beba4b92e..bc3d68efa 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -440,15 +440,8 @@ namespace storm {
             for (auto& functionDefinition : this->getFunctionDefinitions()) {
                 functionDefinition.second.substitute(substitution);
             }
-            for (auto& variable : this->getVariables().getBoundedIntegerVariables()) {
-                variable.substitute(substitution);
-            }
-            for (auto& variable : this->getVariables().getArrayVariables()) {
-                variable.substitute(substitution);
-            }
-            for (auto& variable : this->getVariables().getClockVariables()) {
-                variable.substitute(substitution);
-            }
+            
+            this->getVariables().substitute(substitution);
             
             for (auto& location : this->getLocations()) {
                 location.substitute(substitution);
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 792abf98a..3aa05a20c 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -1036,15 +1036,7 @@ namespace storm {
             }
             
             // Substitute constants in all global variables.
-            for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
-                variable.substitute(constantSubstitution);
-            }
-            for (auto& variable : result.getGlobalVariables().getArrayVariables()) {
-                variable.substitute(constantSubstitution);
-            }
-            for (auto& variable : result.getGlobalVariables().getClockVariables()) {
-                variable.substitute(constantSubstitution);
-            }
+            result.getGlobalVariables().substitute(constantSubstitution);
             
             // Substitute constants in initial states expression.
             result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution));
diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp
index 65725888c..a3701dbae 100644
--- a/src/storm/storage/jani/VariableSet.cpp
+++ b/src/storm/storage/jani/VariableSet.cpp
@@ -423,5 +423,11 @@ namespace storm {
             
             return result;
         }
+        
+        void VariableSet::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            for (auto& variable : variables) {
+                variable.substitute(substitution);
+            }
+        }
     }
 }
diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h
index 7a428ba16..612d2e992 100644
--- a/src/storm/storage/jani/VariableSet.h
+++ b/src/storm/storage/jani/VariableSet.h
@@ -265,6 +265,13 @@ namespace storm {
              */
             std::map<std::string, std::reference_wrapper<Variable const>> getNameToVariableMap() const;
             
+            /*!
+             * Applies the given substitution to all variables in this set.
+             * The substitution does not apply to the variables itself, but to initial expressions, variable bounds, ...
+             * @param substitution
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
         private:
             /// The vector of all variables.
             std::vector<std::shared_ptr<Variable>> variables;