diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 79a12f8b1..77c1a897d 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -144,18 +144,15 @@ namespace storm { SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const { std::map 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 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()); diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index c74d049a2..040f73eba 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/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; } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 644f90f20..2bcf13504 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -352,6 +352,16 @@ namespace storm { */ std::map 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. */