From 71489a24f56582a8e3b3d80ca4a92d4599ef5372 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Sep 2018 22:58:33 +0200
Subject: [PATCH] The model builders now substitute jani functions (if still
 present)

---
 src/storm/builder/DdJaniModelBuilder.cpp              | 1 +
 src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp | 2 +-
 src/storm/generator/JaniNextStateGenerator.cpp        | 4 +++-
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index 47cd321db..449e60781 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -1991,6 +1991,7 @@ namespace storm {
             STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The dd jani model builder does not support the following model feature(s): " << features.toString() << ".");
 
             storm::jani::Model preparedModel = model;
+            preparedModel.substituteFunctions();
             
             // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
             if (preparedModel.hasTransientEdgeDestinationAssignments()) {
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index d34a6c9f1..63566089a 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -56,7 +56,7 @@ namespace storm {
 #endif
             
             template <typename ValueType, typename RewardModelType>
-            ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model.substituteConstants()), modelComponentsBuilder(model.getModelType()) {
+            ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model.substituteConstantsFunctions()), modelComponentsBuilder(model.getModelType()) {
                 
                 // Load all options from the settings module.
                 storm::settings::modules::JitBuilderSettings const& settings = storm::settings::getModule<storm::settings::modules::JitBuilderSettings>();
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 21b796683..5abd8ccbc 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -33,7 +33,7 @@ namespace storm {
     namespace generator {
         
         template<typename ValueType, typename StateType>
-        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : JaniNextStateGenerator(model.substituteConstants(), options, false) {
+        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : JaniNextStateGenerator(model.substituteConstantsFunctions(), options, false) {
             // Intentionally left empty.
         }
         
@@ -765,6 +765,8 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         void JaniNextStateGenerator<ValueType, StateType>::checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const {
+            // Todo: this also throws if the writes are on different assignment level
+            // Todo: this also throws if the writes are on different elements of the same array
             std::map<storm::expressions::Variable, uint64_t> writtenGlobalVariables;
             for (auto edgeSetIt = enabledEdges.begin(), edgeSetIte = enabledEdges.end(); edgeSetIt != edgeSetIte; ++edgeSetIt) {
                 for (auto const& indexAndEdge : edgeSetIt->second) {