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 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); + } } /*!