From 4453eb4134b153856695b71ebb207cb7dec963ce Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Sep 2018 15:34:18 +0200
Subject: [PATCH] substitute jani-functions during preprocessing (analogous to
 prism program preprocessing)

---
 src/storm/storage/SymbolicModelDescription.cpp | 2 +-
 src/storm/storage/jani/Model.cpp               | 6 ++++++
 src/storm/storage/jani/Model.h                 | 6 ++++++
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp
index 31606451b..1e769acd0 100644
--- a/src/storm/storage/SymbolicModelDescription.cpp
+++ b/src/storm/storage/SymbolicModelDescription.cpp
@@ -149,7 +149,7 @@ namespace storm {
         
         SymbolicModelDescription SymbolicModelDescription::preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
             if (this->isJaniModel()) {
-                storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants();
+                storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstantsFunctions();
                 return SymbolicModelDescription(preparedModel);
             } else if (this->isPrismProgram()) {
                 return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas());
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index e2b03461b..2285bcbaf 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -951,6 +951,12 @@ namespace storm {
             return result;
         }
         
+        Model Model::substituteConstantsFunctions() const {
+            auto result = substituteConstants();
+            result.substituteFunctions();
+            return result;
+        }
+        
         std::map<storm::expressions::Variable, storm::expressions::Expression> Model::getConstantsSubstitution() const {
             std::map<storm::expressions::Variable, storm::expressions::Expression> result;
             
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 445552cf1..bc32a14c2 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -399,6 +399,12 @@ namespace storm {
             void substituteFunctions();
             void substituteFunctions(std::vector<Property>& properties);
             
+            /*!
+             * Substitutes all constants in all expressions of the model. The original model is not modified, but
+             * instead a new model is created. Afterwards, all function calls are substituted with the defining expression.
+             */
+            Model substituteConstantsFunctions() const;
+
             /*!
              * Returns true if at least one array variable occurs in the model.
              */