started to include array support

src/storm/storage/SymbolicModelDescription.cpp

@@ -144,18 +144,15 @@ namespace storm {
         
         SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
             std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = parseConstantDefinitions(constantDefinitionString);
-            if (this->isJaniModel()) {
-                storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants();
-                return SymbolicModelDescription(preparedModel);
-            } else if (this->isPrismProgram()) {
-                return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants());
-            }
-            return *this;
+            return preprocess(substitution);
         }
         
         SymbolicModelDescription SymbolicModelDescription::preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
             if (this->isJaniModel()) {
                 storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants();
+                if (preparedModel.hasArrayVariables()) {
+                    preparedModel = preparedModel.convertArrays();
+                }
                 return SymbolicModelDescription(preparedModel);
             } else if (this->isPrismProgram()) {
                 return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants());

src/storm/storage/jani/Model.cpp

@@ -923,6 +923,14 @@ namespace storm {
             return result;
         }
         
+        bool Model::hasArrayVariables() const {
+            return true;
+        }
+        
+        Model Model::convertArrays() const {
+            return *this;
+        }
+        
         void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
             this->initialStatesRestriction = initialStatesRestriction;
         }

src/storm/storage/jani/Model.h

@@ -352,6 +352,16 @@ namespace storm {
              */
             std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
             
+            /*!
+             * Returns true if at least one array variable occurs in the model.
+             */
+            bool hasArrayVariables() const;
+            
+            /*!
+             * Converts occurring (fixed size) arrays into multiple variables.
+             */
+            Model convertArrays() const;
+            
             /*!
              * Retrieves whether there is an expression restricting the legal initial values of the global variables.
              */