From ea1a1d97efd956a55a20041028f5bc7d8b008f0c Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 20 Sep 2018 09:59:27 +0200
Subject: [PATCH] fixed export of jani functions to json. Remove output to cout
 when writing the jani file

---
 src/storm/storage/jani/JSONExporter.cpp | 8 +++++++-
 src/storm/utility/file.h                | 6 ++++--
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 97f811e9f..7be7799fa 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -742,7 +742,7 @@ namespace storm {
         
         void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid, bool compact) {
             std::ofstream stream;
-            storm::utility::openFile(filepath, stream);
+            storm::utility::openFile(filepath, stream, true);
             toStream(janiModel, formulas, stream, checkValid, compact);
             storm::utility::closeFile(stream);
         }
@@ -1015,6 +1015,9 @@ namespace storm {
                 modernjson::json autoEntry;
                 autoEntry["name"] = automaton.getName();
                 autoEntry["variables"] = buildVariablesArray(automaton.getVariables(), constants, globalVariables, automaton.getVariables());
+                if (!automaton.getFunctionDefinitions().empty()) {
+                    autoEntry["functions"] = buildFunctionsArray(automaton.getFunctionDefinitions(), constants, globalVariables, automaton.getVariables());
+                }
                 if(automaton.hasRestrictedInitialStates()) {
                     autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction(), constants, globalVariables, automaton.getVariables());
                 }
@@ -1034,6 +1037,9 @@ namespace storm {
             jsonStruct["actions"] = buildActionArray(janiModel.getActions());
             jsonStruct["constants"] = buildConstantsArray(janiModel.getConstants());
             jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables(), janiModel.getConstants(), janiModel.getGlobalVariables());
+            if (!janiModel.getGlobalFunctionDefinitions().empty()) {
+                jsonStruct["functions"] = buildFunctionsArray(janiModel.getGlobalFunctionDefinitions(), janiModel.getConstants(), janiModel.getGlobalVariables());
+            }
             jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction(), janiModel.getConstants(), janiModel.getGlobalVariables());
             jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions);
             jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
diff --git a/src/storm/utility/file.h b/src/storm/utility/file.h
index 97201e4a2..c089eb45a 100644
--- a/src/storm/utility/file.h
+++ b/src/storm/utility/file.h
@@ -15,14 +15,16 @@ namespace storm {
          * @param filestream Contains the file handler afterwards.
          * @param append If true, the new content is appended instead of clearing the existing content.
          */
-        inline void openFile(std::string const& filepath, std::ofstream& filestream, bool append = false) {
+        inline void openFile(std::string const& filepath, std::ofstream& filestream, bool append = false, bool silent = false) {
             if (append) {
                 filestream.open(filepath, std::ios::app);
             } else {
                 filestream.open(filepath);
             }
             STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
-            STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl);
+            if (!silent) {
+                STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl);
+            }
         }
 
         /*!