jani parser parses array variables

src/storm-parsers/parser/JaniParser.cpp

@@ -10,6 +10,7 @@
 #include "storm/storage/jani/AutomatonComposition.h"
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/CompositionInformationVisitor.h"
+#include "storm/storage/jani/expressions/JaniExpressions.h"
 #include "storm/exceptions/FileIoException.h"
 #include "storm/exceptions/InvalidJaniException.h"
 
@@ -23,6 +24,7 @@
 #include <sstream>
 #include <fstream>
 #include <boost/lexical_cast.hpp>
+#include <storm/storage/jani/ArrayVariable.h>
 
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
@@ -109,8 +111,9 @@ namespace storm {
             STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables.");
             std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> globalVars;
             if (variablesCount == 1) {
+                bool requireInitialValues = parsedStructure.count("restrict-initial") == 0;
                 for (auto const& varStructure : parsedStructure.at("variables")) {
-                    std::shared_ptr<storm::jani::Variable> variable = parseVariable(varStructure, "global", globalVars, constants);
+                    std::shared_ptr<storm::jani::Variable> variable = parseVariable(varStructure, requireInitialValues, "global", globalVars, constants);
                     globalVars.emplace(variable->getName(), variable);
                     model.addVariable(*variable);
                 }
@@ -626,8 +629,52 @@ namespace storm {
 
             STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << constantStructure.at("type").dump()  << " for Variable '" << name << "' (scope: " << scopeDescription << ")");
         }
-
-        std::shared_ptr<storm::jani::Variable> JaniParser::parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool prefWithScope) {
+        
+        void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
+            if (typeStructure.is_string()) {
+                if (typeStructure == "real") {
+                    result.basicType = ParsedType::BasicType::Real;
+                } else if (typeStructure == "bool") {
+                    result.basicType = ParsedType::BasicType::Bool;
+                } else if (typeStructure == "int") {
+                    result.basicType = ParsedType::BasicType::Int;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")");
+                }
+            } else if (typeStructure.is_object()) {
+                STORM_LOG_THROW(typeStructure.count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << variableName << "(scope: " << scopeDescription << ")  kind must be given");
+                std::string kind = getString(typeStructure.at("kind"), "kind for complex type as in variable " + variableName  + "(scope: " + scopeDescription + ") ");
+                if (kind == "bounded") {
+                    STORM_LOG_THROW(typeStructure.count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scopeDescription << ") lower-bound must be given");
+                    storm::expressions::Expression lowerboundExpr = parseExpression(typeStructure.at("lower-bound"), "Lower bound for variable " + variableName + " (scope: " + scopeDescription + ")", globalVars, constants, localVars);
+                    assert(lowerboundExpr.isInitialized());
+                    STORM_LOG_THROW(typeStructure.count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scopeDescription << ") upper-bound must be given");
+                    storm::expressions::Expression upperboundExpr = parseExpression(typeStructure.at("upper-bound"), "Upper bound for variable "+ variableName + " (scope: " + scopeDescription + ")", globalVars, constants, localVars);
+                    assert(upperboundExpr.isInitialized());
+                    STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scopeDescription << ") base must be given");
+                    std::string basictype = getString(typeStructure.at("base"), "base for bounded type as in variable " + variableName  + "(scope: " + scopeDescription + ") ");
+                    if (basictype == "int") {
+                        STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << variableName << "(scope: " << scopeDescription << ") must be integer-typed");
+                        STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << variableName << "(scope: " << scopeDescription << ") must be integer-typed");
+                        if (!lowerboundExpr.containsVariables() && !upperboundExpr.containsVariables()) {
+                            STORM_LOG_THROW(lowerboundExpr.evaluateAsInt() <= upperboundExpr.evaluateAsInt(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable "  << variableName << "(scope: " << scopeDescription << ")");
+                        }
+                        result.basicType = ParsedType::BasicType::Int;
+                        result.bounds = std::make_pair(lowerboundExpr, upperboundExpr);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scopeDescription << ") ");
+                    }
+                } else if (kind == "array") {
+                    STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For array type as in variable " << variableName << "(scope: " << scopeDescription << ") base must be given");
+                    result.arrayBase = ParsedType();
+                    parseType(result.arrayBase.get(), typeStructure.at("base"), variableName, scopeDescription, globalVars, constants, localVars);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") ");
+                }
+            }
+        }
+        
+        std::shared_ptr<storm::jani::Variable> JaniParser::parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool prefWithScope) {
             STORM_LOG_THROW(variableStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scopeDescription + ") must have a name");
             std::string pref = prefWithScope  ? scopeDescription + VARIABLE_AUTOMATON_DELIMITER : "";
             std::string name = getString(variableStructure.at("name"), "variable-name in " + scopeDescription + "-scope");
@@ -640,101 +687,103 @@ namespace storm {
             if(tvarcount == 1) {
                 transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name  + "' (scope: " + scopeDescription + ")  ");
             }
+            STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration.");
+            ParsedType type;
+            parseType(type, variableStructure.at("type"), name, scopeDescription, globalVars, constants, localVars);
+
             size_t initvalcount = variableStructure.count("initial-value");
             if(transientVar) {
                 STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scopeDescription + ")  "+ name + "' (scope: " + scopeDescription + ")  ");
             } else {
                 STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scopeDescription + ")");
             }
-            STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration.");
             boost::optional<storm::expressions::Expression> initVal;
-            if(variableStructure.at("type").is_string()) {
-                if(variableStructure.at("type") == "real") {
-                    if(initvalcount == 1) {
-                        if(variableStructure.at("initial-value").is_null()) {
+            if (initvalcount == 1 && !variableStructure.at("initial-value").is_null()) {
+                initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
+            } else {
+                assert(!transientVar);
+            }
+            
+            bool setInitValFromDefault = !initVal.is_initialized() && requireInitialValues;
+            if (type.basicType) {
+                switch (type.basicType.get()) {
+                    case ParsedType::BasicType::Real:
+                        if (setInitValFromDefault) {
                             initVal = expressionManager->rational(defaultRationalInitialValue);
-                        } else {
-                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
-                            STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational");
                         }
-                        return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar);
-                        
-                    }
-                    assert(!transientVar);
-                    return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName));
-                } else if(variableStructure.at("type") == "bool") {
-                    if(initvalcount == 1) {
-                        if(variableStructure.at("initial-value").is_null()) {
-                            initVal = expressionManager->boolean(defaultBooleanInitialValue);
+                        if (initVal) {
+                            STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational");
+                            return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar);
                         } else {
-                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
-                            STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
+                            return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName));
                         }
-                        if(transientVar) {
-                            labels.insert(name);
+                    case ParsedType::BasicType::Int:
+                        if (setInitValFromDefault) {
+                            if (type.bounds) {
+                                initVal = storm::expressions::ite(type.bounds->first < 0 && type.bounds->second > 0, expressionManager->integer(defaultIntegerInitialValue), type.bounds->first);
+                                // TODO as soon as we support half-open intervals, we have to change this.
+                            } else {
+                                initVal = expressionManager->integer(defaultIntegerInitialValue);
+                            }
                         }
-                        return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar);
-                    }
-                    assert(!transientVar);
-                    return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName));
-                } else if(variableStructure.at("type") == "int") {
-                    if(initvalcount == 1) {
-                        if(variableStructure.at("initial-value").is_null()) {
-                            initVal = expressionManager->integer(defaultIntegerInitialValue);
-                        } else {
-                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
+                        if (initVal) {
                             STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
-                        }
-                        return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
-                    }
-                    assert(!transientVar); // Checked earlier.
-                    return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName));
-                } else if(variableStructure.at("type") == "clock") {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'clock' for variable '" << name << "' (scope: " << scopeDescription << ")");
-                } else if(variableStructure.at("type") == "continuous") {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'continuous' for variable ''" << name << "' (scope: " << scopeDescription << ")");
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump()  << " for variable '" << name << "' (scope: " << scopeDescription << ")");
-                }
-            } else if(variableStructure.at("type").is_object()) {
-                STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ")  kind must be given");
-                std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name  + "(scope: " + scopeDescription + ") ");
-                if(kind == "bounded") {
-                    // First do the bounds, that makes the code a bit more streamlined
-                    STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given");
-                    storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars);
-                    assert(lowerboundExpr.isInitialized());
-                    STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given");
-                    storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars);
-                    assert(upperboundExpr.isInitialized());
-                    STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given");
-                    if(initvalcount == 1) {
-                        if(variableStructure.at("initial-value").is_null()) {
-                            initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr);
-                            // TODO as soon as we support half-open intervals, we have to change this.
+                            if (type.bounds) {
+                                return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, type.bounds->first, type.bounds->second);
+                            } else {
+                                return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
+                            }
                         } else {
-                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
+                            if (type.bounds) {
+                                return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
+                            } else {
+                                return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), boost::none, false, type.bounds->first, type.bounds->second);
+                            }
                         }
-                    }
-                    std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name  + "(scope: " + scopeDescription + ") ");
-                    if(basictype == "int") {
-                        if(initVal) {
-                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
+                        break;
+                    case ParsedType::BasicType::Bool:
+                        if (setInitValFromDefault) {
+                            initVal = expressionManager->boolean(defaultBooleanInitialValue);
                         }
-                        STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
-                        STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
-                        if(!lowerboundExpr.containsVariables() && !upperboundExpr.containsVariables()) {
-                            STORM_LOG_THROW(lowerboundExpr.evaluateAsInt() <= upperboundExpr.evaluateAsInt(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable "  << name << "(scope: " << scopeDescription << ")");
+                        if (initVal) {
+                            STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
+                            if (transientVar) {
+                                labels.insert(name);
+                            }
+                            return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar);
+                        } else {
+                            return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName));
                         }
-                        return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr);
-                    } else {
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") ");
-                    }
+                }
+            } else if (type.arrayBase) {
+                STORM_LOG_THROW(type.arrayBase->basicType, storm::exceptions::InvalidJaniException, "Array base type for variable " + name + "(scope " + scopeDescription + ") should be a BasicType or a BoundedType.");
+                storm::jani::ArrayVariable::ElementType elementType;
+                storm::expressions::Type* exprVariableType;
+                switch (type.arrayBase->basicType.get()) {
+                    case ParsedType::BasicType::Real:
+                        elementType = storm::jani::ArrayVariable::ElementType::Real;
+                        exprVariableType = &expressionManager->getArrayType(expressionManager->getRationalType());
+                        break;
+                    case ParsedType::BasicType::Bool:
+                        elementType = storm::jani::ArrayVariable::ElementType::Bool;
+                        exprVariableType = &expressionManager->getArrayType(expressionManager->getBooleanType());
+                        break;
+                    case ParsedType::BasicType::Int:
+                        elementType = storm::jani::ArrayVariable::ElementType::Int;
+                        exprVariableType = &expressionManager->getArrayType(expressionManager->getIntegerType());
+                        break;
+                }
+                if (setInitValFromDefault) {
+                    initVal = storm::expressions::ValueArrayExpression(expressionManager, *exprVariableType, {});
+                }
+                if (initVal) {
+                    STORM_LOG_THROW(initVal.get().hasArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array");
+                    return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType, initVal.get(), transientVar);
                 } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") ");
+                    return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType);
                 }
             }
-
+            
             STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump()  << " for variable '" << name << "' (scope: " << scopeDescription << ")");
         }
 
@@ -1050,8 +1099,9 @@ namespace storm {
             STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables");
             std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> localVars;
             if(varDeclCount > 0) {
+                bool requireInitialValues = automatonStructure.count("restrict-initial") == 0;
                 for(auto const& varStructure : automatonStructure.at("variables")) {
-                    std::shared_ptr<storm::jani::Variable> var = parseVariable(varStructure, name, globalVars, constants, localVars, true);
+                    std::shared_ptr<storm::jani::Variable> var = parseVariable(varStructure, requireInitialValues, name, globalVars, constants, localVars, true);
                     assert(localVars.count(var->getName()) == 0);
                     automaton.addVariable(*var);
                     localVars.emplace(var->getName(), var);

src/storm-parsers/parser/JaniParser.h

@@ -48,7 +48,15 @@ namespace storm {
             std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseModel(bool parseProperties = true);
             storm::jani::Property parseProperty(json const& propertyStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants);
             storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants);
-            std::shared_ptr<storm::jani::Variable>  parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool prefWithScope = false);
+            struct ParsedType {
+                enum class BasicType {Bool, Int, Real};
+    
+                boost::optional<BasicType> basicType;
+                boost::optional<std::pair<storm::expressions::Expression, storm::expressions::Expression>> bounds;
+                boost::optional<ParsedType> arrayBase;
+            };
+            void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars);
+            std::shared_ptr<storm::jani::Variable>  parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool prefWithScope = false);
             storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants,  std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
             
         private:

src/storm/storage/jani/ArrayVariable.cpp

@@ -0,0 +1,57 @@
+#include "storm/storage/jani/ArrayVariable.h"
+
+namespace storm {
+    namespace jani {
+        
+        ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
+            // Intentionally left empty.
+        }
+        
+        ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue) : Variable(name, variable, initValue, transient) {
+            // Intentionally left empty.
+        }
+        
+        void ArrayVariable::setElementTypeBounds(storm::expressions::Expression lowerBound, storm::expressions::Expression upperBound) {
+            elementTypeBounds = std::make_pair(lowerBound, upperBound);
+        }
+        
+        bool ArrayVariable::hasElementTypeBounds() const {
+            return elementTypeBounds.is_initialized();
+        }
+        
+        std::pair<storm::expressions::Expression, storm::expressions::Expression> const& ArrayVariable::getElementTypeBounds() const {
+            return elementTypeBounds.get();
+        }
+        
+        void ArrayVariable::setMaxSize(uint64_t size) {
+            maxSize = size;
+        }
+        
+        bool ArrayVariable::hasMaxSize() const {
+            return maxSize.is_initialized();
+        }
+        
+        uint64_t ArrayVariable::getMaxSize() const {
+            return maxSize.get();
+        }
+        
+        ElementType ArrayVariable::getElementType() const {
+            return elementType;
+        }
+        
+        std::unique_ptr<Variable> ArrayVariable::clone() const {
+            return std::make_unique<ArrayVariable>(*this);
+        }
+        
+        bool ArrayVariable::isArrayVariable() const {
+            return true;
+        }
+        
+        void ArrayVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            Variable::substitute(substitution);
+            if (hasElementTypeBounds()) {
+                setElementTypeBounds(elementTypeBounds->first.substitute(substitution), elementTypeBounds->second.substitute(substitution));
+            }
+        }
+    }
+}

src/storm/storage/jani/ArrayVariable.h

@@ -0,0 +1,52 @@
+#pragma once
+
+#include "storm/storage/jani/Variable.h"
+
+namespace storm {
+    namespace jani {
+        
+        class ArrayVariable : public Variable {
+        public:
+            
+            enum class ElementType {Bool, Int, Real};
+            
+            /*!
+             * Creates an Array variable
+             */
+            ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType elementType);
+            
+            /*!
+             * Creates an Array variable with initial value
+             */
+            ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType elementType, storm::expressions::Expression const& initialValue, bool transient);
+            
+            /*!
+             * Sets/Gets bounds to the values stored in this array
+             */
+            void setElementTypeBounds(storm::expressions::Expression lowerBound, storm::expressions::Expression upperBound);
+            bool hasElementTypeBounds() const;
+            std::pair<storm::expressions::Expression, storm::expressions::Expression> const& getElementTypeBounds() const;
+            
+            /*!
+             * Sets/Gets the maximum size of the array
+             */
+            void setMaxSize(uint64_t size);
+            bool hasMaxSize() const;
+            uint64_t getMaxSize() const;
+            
+            ElementType getElementType() const;
+            
+            virtual std::unique_ptr<Variable> clone() const override;
+            virtual bool isArrayVariable() const override;
+            virtual void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) override;
+
+
+        private:
+            ElementType elementType;
+            boost::optional<std::pair<storm::expressions::Expression, storm::expressions::Expression>> elementTypeBounds;
+            boost::optional<uint64_t> maxSize;
+        };
+        
+        
+    }
+}

src/storm/storage/jani/Model.cpp

@@ -924,10 +924,11 @@ namespace storm {
         }
         
         bool Model::hasArrayVariables() const {
-            return true;
+            return getExpressionManager().getNumberOfArrayVariables() != 0;
         }
         
         Model Model::convertArrays() const {
+            std::cout << "TODO";
             return *this;
         }
         

src/storm/storage/jani/Variable.cpp

@@ -4,6 +4,7 @@
 #include "storm/storage/jani/BoundedIntegerVariable.h"
 #include "storm/storage/jani/UnboundedIntegerVariable.h"
 #include "storm/storage/jani/RealVariable.h"
+#include "storm/storage/jani/ArrayVariable.h"
 
 namespace storm {
     namespace jani {
@@ -48,6 +49,10 @@ namespace storm {
             return false;
         }
         
+        bool Variable::isArrayVariable() const {
+            return false;
+        }
+        
         bool Variable::isTransient() const {
             return transient;
         }
@@ -96,6 +101,14 @@ namespace storm {
             return static_cast<RealVariable const&>(*this);
         }
         
+        ArrayVariable& Variable::asArrayVariable() {
+            return static_cast<ArrayVariable&>(*this);
+        }
+        
+        ArrayVariable const& Variable::asArrayVariable() const {
+            return static_cast<ArrayVariable const&>(*this);
+        }
+        
         void Variable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             if (this->hasInitExpression()) {
                 this->setInitExpression(this->getInitExpression().substitute(substitution));

src/storm/storage/jani/Variable.h

@@ -14,6 +14,7 @@ namespace storm {
         class BoundedIntegerVariable;
         class UnboundedIntegerVariable;
         class RealVariable;
+        class ArrayVariable;
         
         class Variable {
         public:
@@ -72,6 +73,7 @@ namespace storm {
             virtual bool isBoundedIntegerVariable() const;
             virtual bool isUnboundedIntegerVariable() const;
             virtual bool isRealVariable() const;
+            virtual bool isArrayVariable() const;
 
             virtual bool isTransient() const;
             
@@ -84,6 +86,8 @@ namespace storm {
             UnboundedIntegerVariable const& asUnboundedIntegerVariable() const;
             RealVariable& asRealVariable();
             RealVariable const& asRealVariable() const;
+            RealVariable& asArrayVariable();
+            RealVariable const& asArrayVariable() const;
             
             /*!
              * Substitutes all variables in all expressions according to the given substitution.