Parsing and exporting of jani-functions

src/storm-parsers/parser/JaniParser.h

@@ -1,5 +1,6 @@
 #pragma once
 #include "storm/storage/jani/Constant.h"
+#include "storm/storage/jani/FunctionDefinition.h"
 #include "storm/storage/jani/LValue.h"
 #include "storm/logic/Formula.h"
 #include "storm/logic/Bound.h"
@@ -32,8 +33,6 @@ namespace storm {
         /*
          * The JANI format parser.
          * Parses Models and Properties
-         *
-         * TODO some parts are copy-heavy, a bit of cleaning is good as soon as the format is stable.
          */
         class JaniParser {
 
@@ -41,48 +40,75 @@ namespace storm {
             typedef std::vector<storm::jani::Property> PropertyVector;
             typedef std::unordered_map<std::string, storm::jani::Variable const*> VariablesMap;
             typedef std::unordered_map<std::string, storm::jani::Constant const*> ConstantsMap;
+            typedef std::unordered_map<std::string, storm::jani::FunctionDefinition const*> FunctionsMap;
 
             JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {}
             JaniParser(std::string const& jsonstring);
             static std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parse(std::string const& path);
 
-
         protected:
             void readFile(std::string const& path);
+            
+            struct Scope {
+                Scope(std::string description = "global", ConstantsMap const* constants = nullptr, VariablesMap const* globalVars = nullptr, FunctionsMap const* globalFunctions = nullptr, VariablesMap const* localVars = nullptr, FunctionsMap const* localFunctions = nullptr) : description(description) , constants(constants), globalVars(globalVars), globalFunctions(globalFunctions), localVars(localVars), localFunctions(localFunctions) {};
+                
+                Scope(Scope const& other) = default;
+                std::string description;
+                ConstantsMap const* constants;
+                VariablesMap const* globalVars;
+                FunctionsMap const* globalFunctions;
+                VariablesMap const* localVars;
+                FunctionsMap const* localFunctions;
+                Scope refine(std::string const& prependedDescription = "") const {
+                    Scope res(*this);
+                    if (prependedDescription != "") {
+                        res.description = "'" + prependedDescription + "' at " + res.description;
+                    }
+                    return res;
+                }
+                
+                Scope& clearVariables() {
+                    this->globalVars = nullptr;
+                    this->localVars = nullptr;
+                    return *this;
+                }
+            };
+
             std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseModel(bool parseProperties = true);
-            storm::jani::Property parseProperty(json const& propertyStructure, VariablesMap const& globalVars, ConstantsMap const& constants);
-            storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, VariablesMap const& globalVars, ConstantsMap const& constants);
+            storm::jani::Property parseProperty(json const& propertyStructure, Scope const& scope);
+            storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, Scope const& scope);
             struct ParsedType {
                 enum class BasicType {Bool, Int, Real};
                 boost::optional<BasicType> basicType;
                 boost::optional<std::pair<storm::expressions::Expression, storm::expressions::Expression>> bounds;
                 std::unique_ptr<ParsedType> arrayBase;
+                storm::expressions::Type expressionType;
             };
-            void parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars);
-            storm::jani::LValue parseLValue(json const& lValueStructure, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars = {});
-            std::shared_ptr<storm::jani::Variable>  parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars = {}, bool prefWithScope = false);
-            storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
+            void parseType(ParsedType& result, json const& typeStructure, std::string variableName, Scope const& scope);
+            storm::jani::LValue parseLValue(json const& lValueStructure, Scope const& scope);
+            std::shared_ptr<storm::jani::Variable>  parseVariable(json const& variableStructure, bool requireInitialValues, Scope const& scope, std::string const& namePrefix = "");
+            storm::expressions::Expression parseExpression(json const& expressionStructure, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
             
         private:
-            std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure,  ConstantsMap const& constants, std::string const& scopeDescription = "global");
+            std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure, Scope const& scope);
+            storm::jani::FunctionDefinition parseFunctionDefinition(json const& functionDefinitionStructure, Scope const& scope, std::string const& parameterNamePrefix = "");
 
             /**
              * Helper for parsing the actions of a model.
              */
             void parseActions(json const& actionStructure, storm::jani::Model& parentModel);
-            std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure,   storm::logic::FormulaContext formulaContext, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context,  boost::optional<storm::logic::Bound> bound = boost::none);
-            std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars= {}, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
-            std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
+            std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure,   storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional<storm::logic::Bound> bound = boost::none);
+            std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
+            std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
 
 
-            std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext,  std::string const& opstring, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context);
-            std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context);
-            storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, ConstantsMap const& constants);
+            std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext,  std::string const& opstring, Scope const& scope);
+            std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope);
+            storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, Scope const& scope);
             storm::logic::RewardAccumulation parseRewardAccumulation(json const& accStructure, std::string const& context);
             
-            
             std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
-            storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants,  VariablesMap const& localVars = {}, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
+            storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, Scope const& scope, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
 
 
             

src/storm/storage/jani/Automaton.cpp

@@ -85,6 +85,20 @@ namespace storm {
             return variables.hasTransientVariable();
         }
         
+        FunctionDefinition const& Automaton::addFunctionDefinition(FunctionDefinition const& functionDefinition) {
+            auto insertionRes = functionDefinitions.emplace(functionDefinition.getName(), functionDefinition);
+            STORM_LOG_THROW(insertionRes.second, storm::exceptions::InvalidArgumentException, " a function with the name " << functionDefinition.getName() << " already exists in this automaton (" << this->getName() << ")");
+            return insertionRes.first->second;
+        }
+        
+        std::unordered_map<std::string, FunctionDefinition> const& Automaton::getFunctionDefinitions() const {
+            return functionDefinitions;
+        }
+        
+        std::unordered_map<std::string, FunctionDefinition> Automaton::getFunctionDefinitions() {
+            return functionDefinitions;
+        }
+        
         bool Automaton::hasLocation(std::string const& name) const {
             return locationToIndex.find(name) != locationToIndex.end();
         }
@@ -385,6 +399,9 @@ namespace storm {
             for (auto& variable : this->getVariables().getBoundedIntegerVariables()) {
                 variable.substitute(substitution);
             }
+            for (auto& variable : this->getVariables().getArrayVariables()) {
+                variable.substitute(substitution);
+            }
             
             for (auto& location : this->getLocations()) {
                 location.substitute(substitution);

src/storm/storage/jani/Automaton.h

@@ -9,7 +9,7 @@
 #include "storm/storage/jani/VariableSet.h"
 #include "storm/storage/jani/TemplateEdgeContainer.h"
 #include "storm/storage/jani/EdgeContainer.h"
-
+#include "storm/storage/jani/FunctionDefinition.h"
 
 namespace storm {
     namespace jani {
@@ -99,6 +99,21 @@ namespace storm {
              */
             bool hasTransientVariable() const;
             
+            /*!
+             * Adds the given function definition
+             */
+            FunctionDefinition const& addFunctionDefinition(FunctionDefinition const& functionDefinition);
+            
+            /*!
+             * Retrieves all function definitions of this automaton
+             */
+            std::unordered_map<std::string, FunctionDefinition> const& getFunctionDefinitions() const;
+            
+            /*!
+             * Retrieves all function definitions of this automaton
+             */
+            std::unordered_map<std::string, FunctionDefinition> getFunctionDefinitions();
+
             /*!
              * Retrieves whether the automaton has a location with the given name.
              */
@@ -356,6 +371,9 @@ namespace storm {
             /// The set of variables of this automaton.
             VariableSet variables;
             
+            /// A mapping from names to function definitions
+            std::unordered_map<std::string, FunctionDefinition> functionDefinitions;
+            
             /// The locations of the automaton.
             std::vector<Location> locations;
             

src/storm/storage/jani/FunctionDefinition.cpp

@@ -0,0 +1,30 @@
+#include "storm/storage/jani/FunctionDefinition.h"
+
+namespace storm {
+    namespace jani {
+        
+        FunctionDefinition::FunctionDefinition(std::string const& name, storm::expressions::Type const& type, std::vector<storm::expressions::Variable> const& parameters, storm::expressions::Expression const& functionBody) : name(name), type(type), parameters(parameters), functionBody(functionBody) {
+            // Intentionally left empty.
+        }
+        
+        std::string const& FunctionDefinition::getName() const {
+            return name;
+        }
+        
+        storm::expressions::Type const& FunctionDefinition::getType() const {
+            return type;
+        }
+        
+        std::vector<storm::expressions::Variable> const& FunctionDefinition::getParameters() const {
+            return parameters;
+        }
+        
+        storm::expressions::Expression const& FunctionDefinition::getFunctionBody() const {
+            return functionBody;
+        }
+        
+        void FunctionDefinition::setFunctionBody(storm::expressions::Expression const& body) {
+            functionBody = body;
+        }
+    }
+}

src/storm/storage/jani/FunctionDefinition.h

@@ -0,0 +1,61 @@
+#pragma once
+
+#include <string>
+#include <vector>
+
+#include <boost/optional.hpp>
+
+#include "storm/storage/expressions/Variable.h"
+#include "storm/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace jani {
+        
+        class FunctionDefinition {
+        public:
+            /*!
+             * Creates a functionDefinition.
+             */
+            FunctionDefinition(std::string const& name, storm::expressions::Type const& type, std::vector<storm::expressions::Variable> const& parameters, storm::expressions::Expression const& functionBody);
+            
+            /*!
+             * Retrieves the name of the function.
+             */
+            std::string const& getName() const;
+            
+            /*!
+             * Retrieves the type of the function.
+             */
+            storm::expressions::Type const& getType() const;
+            
+            /*!
+             * Retrieves the parameters of the function
+             */
+            std::vector<storm::expressions::Variable> const& getParameters() const;
+            
+            /*!
+             * Retrieves the expression that defines the function
+             */
+            storm::expressions::Expression const& getFunctionBody() const;
+            
+            /*!
+             * sets the expression that defines the function
+             */
+            void setFunctionBody(storm::expressions::Expression const& body);
+            
+        private:
+            // The name of the function.
+            std::string name;
+            
+            // The type of the function
+            storm::expressions::Type type;
+
+            // The parameters
+            std::vector<storm::expressions::Variable> parameters;
+            
+            // The body of the function
+            storm::expressions::Expression functionBody;
+        };
+        
+    }
+}

src/storm/storage/jani/JSONExporter.cpp

@@ -36,9 +36,9 @@ namespace storm {
     namespace jani {
 
 
-        modernjson::json buildExpression(storm::expressions::Expression const& exp,  std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) {
+        modernjson::json buildExpression(storm::expressions::Expression const& exp,  std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set<std::string> const& auxiliaryVariables = {}) {
             STORM_LOG_TRACE("Exporting " << exp);
-            return ExpressionToJson::translate(exp,  constants, globalVariables, localVariables);
+            return ExpressionToJson::translate(exp,  constants, globalVariables, localVariables, auxiliaryVariables);
         }
 
         class CompositionJsonExporter : public CompositionVisitor {
@@ -616,13 +616,13 @@ namespace storm {
             }
         }
         
-        modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) {
+        modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) {
             
             // Simplify the expression first and reduce the nesting
             auto simplifiedExpr = expr.simplify().reduceNesting();
             
             
-            ExpressionToJson visitor(constants, globalVariables, localVariables);
+            ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables);
             return boost::any_cast<modernjson::json>(simplifiedExpr.accept(visitor, boost::none));
         }
         
@@ -657,7 +657,9 @@ namespace storm {
             return opDecl;
         }
         boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
-            if (globalVariables.hasVariable(expression.getVariable())) {
+            if (auxiliaryVariables.count(expression.getVariableName())) {
+                return modernjson::json(expression.getVariableName());
+            } else if (globalVariables.hasVariable(expression.getVariable())) {
                 return modernjson::json(globalVariables.getVariable(expression.getVariable()).getName());
             } else if (localVariables.hasVariable(expression.getVariable())) {
                 return modernjson::json(localVariables.getVariable(expression.getVariable()).getName());
@@ -701,7 +703,7 @@ namespace storm {
             for (uint64_t i = 0; i < size; ++i) {
                 elements.push_back(boost::any_cast<modernjson::json>(expression.at(i)->accept(*this, data)));
             }
-            opDecl["elements"] = elements;
+            opDecl["elements"] = std::move(elements);
             return opDecl;
         }
         
@@ -710,7 +712,11 @@ namespace storm {
             opDecl["op"] = "ac";
             opDecl["var"] = expression.getIndexVar().getName();
             opDecl["length"] = boost::any_cast<modernjson::json>(expression.size()->accept(*this, data));
+            bool inserted = auxiliaryVariables.insert(expression.getIndexVar().getName()).second;
             opDecl["exp"] = boost::any_cast<modernjson::json>(expression.getElementExpression()->accept(*this, data));
+            if (inserted) {
+                auxiliaryVariables.erase(expression.getIndexVar().getName());
+            }
             return opDecl;
         }
         
@@ -722,6 +728,18 @@ namespace storm {
             return opDecl;
         }
         
+        boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = "call";
+            opDecl["function"] = expression.getIdentifier();
+            std::vector<modernjson::json> arguments;
+            for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
+                arguments.push_back(boost::any_cast<modernjson::json>(expression.getArgument(i)->accept(*this, data)));
+            }
+            opDecl["args"] = std::move(arguments);
+            return opDecl;
+        }
+        
         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);
@@ -832,16 +850,54 @@ namespace storm {
                             }
                             break;
                     }
-                    typeDesc["base"] = "int";
                 }
                 varEntry["type"] = typeDesc;
-                if(variable.hasInitExpression()) {
+                if (variable.hasInitExpression()) {
                     varEntry["initial-value"] = buildExpression(variable.getInitExpression(), constants, globalVariables, localVariables);
                 }
                 variableDeclarations.push_back(varEntry);
             }
             return modernjson::json(variableDeclarations);
+        }
         
+        modernjson::json buildTypeDescription(storm::expressions::Type const& type) {
+            modernjson::json typeDescr;
+            if (type.isIntegerType()) {
+                typeDescr = "int";
+            } else if (type.isRationalType()) {
+                typeDescr = "real";
+            } else if (type.isBooleanType()) {
+                typeDescr = "bool";
+            } else if (type.isArrayType()) {
+                typeDescr["kind"] = "array";
+                typeDescr["base"] = buildTypeDescription(type.getElementType());
+            } else {
+                assert(false);
+            }
+            return typeDescr;
+        }
+        
+        modernjson::json buildFunctionsArray(std::unordered_map<std::string, FunctionDefinition> const& functionDefinitions, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
+            std::vector<modernjson::json> functionDeclarations;
+            for (auto const& nameFunDef : functionDefinitions) {
+                storm::jani::FunctionDefinition const& funDef = nameFunDef.second;
+                modernjson::json funDefJson;
+                funDefJson["name"] = nameFunDef.first;
+                funDefJson["type"] = buildTypeDescription(funDef.getType());
+                std::vector<modernjson::json> parameterDeclarations;
+                std::unordered_set<std::string> parameterNames;
+                for (auto const& p : funDef.getParameters()) {
+                    modernjson::json parDefJson;
+                    parDefJson["name"] = p.getName();
+                    parameterNames.insert(p.getName());
+                    parDefJson["type"] = buildTypeDescription(p.getType());
+                    parameterDeclarations.push_back(parDefJson);
+                }
+                funDefJson["parameters"] = parameterDeclarations;
+                funDefJson["body"] = buildExpression(funDef.getFunctionBody(), constants, globalVariables, localVariables, parameterNames);
+                functionDeclarations.push_back(funDefJson);
+            }
+            return modernjson::json(functionDeclarations);
         }
         
         modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
@@ -868,7 +924,7 @@ namespace storm {
                     assignmentEntry["comment"] = assignment.getVariable().getName() + " <- " + assignment.getAssignedExpression().toString();
                 }
             }
-            return modernjson::json(assignmentDeclarations);
+            return modernjson::json(std::move(assignmentDeclarations));
         }
         
         modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
@@ -882,7 +938,7 @@ namespace storm {
                 }
                 locationDeclarations.push_back(locEntry);
             }
-            return modernjson::json(locationDeclarations);
+            return modernjson::json(std::move(locationDeclarations));
         }
         
         modernjson::json buildInitialLocations(storm::jani::Automaton const& automaton) {
@@ -916,7 +972,7 @@ namespace storm {
                 }
                 destDeclarations.push_back(destEntry);
             }
-            return modernjson::json(destDeclarations);
+            return modernjson::json(std::move(destDeclarations));
         }
         
         modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
@@ -950,7 +1006,7 @@ namespace storm {
                 
                 edgeDeclarations.push_back(edgeEntry);
             }
-            return modernjson::json(edgeDeclarations);
+            return modernjson::json(std::move(edgeDeclarations));
         }
         
         modernjson::json buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, bool commentExpressions) {
@@ -967,7 +1023,7 @@ namespace storm {
                 autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap(), constants, globalVariables, automaton.getVariables(), commentExpressions);
                 automataDeclarations.push_back(autoEntry);
             }
-            return modernjson::json(automataDeclarations);
+            return modernjson::json(std::move(automataDeclarations));
         }
         
         void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) {

src/storm/storage/jani/JSONExporter.h

@@ -19,7 +19,7 @@ namespace storm {
         class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {
             
         public:
-            static modernjson::json translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables);
+            static modernjson::json translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables);
             
             virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data);
             virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data);
@@ -34,13 +34,15 @@ namespace storm {
             virtual boost::any visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data);
             virtual boost::any visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data);
             virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data);
 
         private:
 
-            ExpressionToJson(std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) : constants(constants), globalVariables(globalVariables), localVariables(localVariables) {}
+            ExpressionToJson(std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) : constants(constants), globalVariables(globalVariables), localVariables(localVariables), auxiliaryVariables(auxiliaryVariables) {}
             std::vector<storm::jani::Constant> const& constants;
             VariableSet const& globalVariables;
             VariableSet const& localVariables;
+            std::unordered_set<std::string> auxiliaryVariables;
         };
         
         class FormulaToJaniJson : public storm::logic::FormulaVisitor {

src/storm/storage/jani/Model.cpp

@@ -82,6 +82,7 @@ namespace storm {
                 this->automatonToIndex = other.automatonToIndex;
                 this->composition = other.composition;
                 this->initialStatesRestriction = other.initialStatesRestriction;
+                this->globalFunctions = other.globalFunctions;
                 
                 // Now that we have copied all the data, we need to fix all assignments as they contain references to the old model.
                 std::map<Variable const*, std::reference_wrapper<Variable const>> remapping;
@@ -725,6 +726,20 @@ namespace storm {
             return false;
         }
         
+        FunctionDefinition const& Model::addFunctionDefinition(FunctionDefinition const& functionDefinition) {
+            auto insertionRes = globalFunctions.emplace(functionDefinition.getName(), functionDefinition);
+            STORM_LOG_THROW(insertionRes.second, storm::exceptions::InvalidOperationException, " a function with the name " << functionDefinition.getName() << " already exists in this model.");
+            return insertionRes.first->second;
+        }
+        
+        std::unordered_map<std::string, FunctionDefinition> const& Model::getGlobalFunctionDefinitions() const {
+            return globalFunctions;
+        }
+        
+        std::unordered_map<std::string, FunctionDefinition> Model::getGlobalFunctionDefinitions() {
+            return globalFunctions;
+        }
+        
         storm::expressions::ExpressionManager& Model::getExpressionManager() const {
             return *expressionManager;
         }

src/storm/storage/jani/Model.h

@@ -12,6 +12,7 @@
 #include "storm/storage/jani/Constant.h"
 #include "storm/storage/jani/Composition.h"
 #include "storm/storage/jani/Edge.h"
+#include "storm/storage/jani/FunctionDefinition.h"
 #include "storm/storage/jani/Location.h"
 #include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/ModelFeatures.h"
@@ -248,6 +249,21 @@ namespace storm {
              */
             bool hasNonGlobalTransientVariable() const;
             
+            /*!
+             * Adds the given function definition
+             */
+            FunctionDefinition const& addFunctionDefinition(FunctionDefinition const& functionDefinition);
+            
+            /*!
+             * Retrieves all global function definitions
+             */
+            std::unordered_map<std::string, FunctionDefinition> const& getGlobalFunctionDefinitions() const;
+            
+            /*!
+             * Retrieves all global function definitions
+             */
+            std::unordered_map<std::string, FunctionDefinition> getGlobalFunctionDefinitions();
+            
             /*!
              * Retrieves the manager responsible for the expressions in the JANI model.
              */
@@ -564,6 +580,9 @@ namespace storm {
             /// The global variables of the model.
             VariableSet globalVariables;
             
+            /// A mapping from names to function definitions
+            std::unordered_map<std::string, FunctionDefinition> globalFunctions;
+            
             /// The list of automata.
             std::vector<Automaton> automata;
             

src/storm/storage/jani/ModelFeatures.cpp

@@ -11,6 +11,8 @@ namespace storm {
                     return "arrays";
                 case ModelFeature::DerivedOperators:
                     return "derived-operators";
+                case ModelFeature::Functions:
+                    return "functions";
                 case ModelFeature::StateExitRewards:
                     return "state-exit-rewards";
             }
@@ -40,6 +42,10 @@ namespace storm {
             return features.count(ModelFeature::DerivedOperators) > 0;
         }
         
+        bool ModelFeatures::hasFunctions() const {
+            return features.count(ModelFeature::Functions) > 0;
+        }
+        
         bool ModelFeatures::hasStateExitRewards() const {
             return features.count(ModelFeature::StateExitRewards) > 0;
         }

src/storm/storage/jani/ModelFeatures.h

@@ -6,7 +6,7 @@
 namespace storm {
     namespace jani {
 
-        enum class ModelFeature {Arrays, DerivedOperators, StateExitRewards};
+        enum class ModelFeature {Arrays, DerivedOperators, Functions, StateExitRewards};
 
         std::string toString(ModelFeature const& modelFeature);
         
@@ -16,6 +16,7 @@ namespace storm {
             std::string toString() const;
             
             bool hasArrays() const;
+            bool hasFunctions() const;
             bool hasDerivedOperators() const;
             bool hasStateExitRewards() const;
             

src/storm/storage/jani/expressions/FunctionCallExpression.cpp

@@ -0,0 +1,75 @@
+#include "storm/storage/jani/expressions/FunctionCallExpression.h"
+
+#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/UnexpectedException.h"
+
+namespace storm {
+    namespace expressions {
+        
+        FunctionCallExpression::FunctionCallExpression(ExpressionManager const& manager, Type const& type, std::string const& functionIdentifier, std::vector<std::shared_ptr<BaseExpression const>> const& arguments) : BaseExpression(manager, type), identifier(functionIdentifier), arguments(arguments) {
+            // Intentionally left empty
+        }
+        
+        void FunctionCallExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
+            for (auto const& a : arguments) {
+                a->gatherVariables(variables);
+            }
+        }
+        
+        bool FunctionCallExpression::containsVariables() const {
+            for (auto const& a : arguments) {
+                if (a->containsVariables()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
+        std::shared_ptr<BaseExpression const> FunctionCallExpression::simplify() const {
+            std::vector<std::shared_ptr<BaseExpression const>> simplifiedArguments;
+            simplifiedArguments.reserve(arguments.size());
+            for (auto const& a : arguments) {
+                simplifiedArguments.push_back(a->simplify());
+            }
+            return std::shared_ptr<BaseExpression const>(new FunctionCallExpression(getManager(), getType(), identifier, simplifiedArguments));
+        }
+        
+        boost::any FunctionCallExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
+            auto janiVisitor = dynamic_cast<JaniExpressionVisitor*>(&visitor);
+            STORM_LOG_THROW(janiVisitor != nullptr, storm::exceptions::UnexpectedException, "Visitor of jani expression should be of type JaniVisitor.");
+            return janiVisitor->visit(*this, data);
+        }
+        
+        void FunctionCallExpression::printToStream(std::ostream& stream) const {
+            stream << identifier;
+            if (getNumberOfArguments() > 0) {
+                stream << "(";
+                bool first = true;
+                for (auto const& a : arguments) {
+                    stream << *a;
+                    if (!first) {
+                        stream << ", ";
+                    }
+                    first = false;
+                }
+                stream << ")";
+            }
+        }
+        
+        std::string const& FunctionCallExpression::getFunctionIdentifier() const {
+            return identifier;
+        }
+        
+        uint64_t FunctionCallExpression::getNumberOfArguments() const {
+            return arguments.size();
+        }
+        
+        std::shared_ptr<BaseExpression const> FunctionCallExpression::getArgument(uint64_t i) const {
+            STORM_LOG_THROW(i < arguments.size(), storm::exceptions::InvalidArgumentException, "Tried to access the argument with index " << i << " of a function call with " << arguments.size() << " arguments.");
+            return arguments[i];
+        }
+    }
+}

src/storm/storage/jani/expressions/FunctionCallExpression.h

@@ -0,0 +1,42 @@
+#pragma once
+
+#include "storm/storage/expressions/BaseExpression.h"
+
+namespace storm {
+    namespace expressions {
+        /*!
+         * Represents an array with a given list of elements.
+         */
+        class FunctionCallExpression : public BaseExpression {
+        public:
+            
+            FunctionCallExpression(ExpressionManager const& manager, Type const& type, std::string const& functionIdentifier, std::vector<std::shared_ptr<BaseExpression const>> const& arguments);
+            
+            
+            // Instantiate constructors and assignments with their default implementations.
+            FunctionCallExpression(FunctionCallExpression const& other) = default;
+            FunctionCallExpression& operator=(FunctionCallExpression const& other) = delete;
+            FunctionCallExpression(FunctionCallExpression&&) = default;
+            FunctionCallExpression& operator=(FunctionCallExpression&&) = delete;
+
+            virtual ~FunctionCallExpression() = default;
+
+            virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
+            virtual bool containsVariables() const override;
+            virtual std::shared_ptr<BaseExpression const> simplify() const override;
+            virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            
+            std::string const& getFunctionIdentifier() const;
+            uint64_t getNumberOfArguments() const;
+            std::shared_ptr<BaseExpression const> getArgument(uint64_t i) const;
+
+
+        protected:
+            virtual void printToStream(std::ostream& stream) const override;
+            
+        private:
+            std::string identifier;
+            std::vector<std::shared_ptr<BaseExpression const>> arguments;
+        };
+    }
+}

src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp

@@ -60,6 +60,15 @@ namespace storm {
             }
         }
 
+        template<typename MapType>
+        boost::any JaniExpressionSubstitutionVisitor<MapType>::visit(FunctionCallExpression const& expression, boost::any const& data) {
+            std::vector<std::shared_ptr<BaseExpression const>> newArguments;
+            newArguments.reserve(expression.getNumberOfArguments());
+            for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
+                newArguments.push_back(boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getArgument(i)->accept(*this, data)));
+            }
+            return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new FunctionCallExpression(expression.getManager(), expression.getType(), expression.getIdentifier(), newArguments)));
+        }
 
         // Explicitly instantiate the class with map and unordered_map.
 		template class JaniExpressionSubstitutionVisitor<std::map<Variable, Expression>>;

src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h

@@ -25,6 +25,7 @@ namespace storm {
             virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(FunctionCallExpression const& expression, boost::any const& data) override;
         };
     }
 }

src/storm/storage/jani/expressions/JaniExpressionVisitor.h

@@ -11,6 +11,7 @@ namespace storm {
             virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) = 0;
             virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) = 0;
             virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) = 0;
+            virtual boost::any visit(FunctionCallExpression const& expression, boost::any const& data) = 0;
         };
     }
 }

src/storm/storage/jani/expressions/JaniExpressions.h

@@ -2,3 +2,4 @@
 #include "storm/storage/jani/expressions/ArrayAccessExpression.h"
 #include "storm/storage/jani/expressions/ConstructorArrayExpression.h"
 #include "storm/storage/jani/expressions/ValueArrayExpression.h"
+#include "storm/storage/jani/expressions/FunctionCallExpression.h"

src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp

@@ -71,6 +71,15 @@ namespace storm {
                 virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) override {
                     return true;
                 }
+                
+                virtual boost::any visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) override {
+                    for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
+                        if (boost::any_cast<bool>(expression.getArgument(i)->accept(*this, data))) {
+                            return true;
+                        }
+                    }
+                    return false;
+                }
             };
             
             class ArrayExpressionFinderTraverser : public ConstJaniTraverser {