diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 31606451b..1e769acd0 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -149,7 +149,7 @@ namespace storm { SymbolicModelDescription SymbolicModelDescription::preprocess(std::map const& constantDefinitions) const { if (this->isJaniModel()) { - storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants(); + storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstantsFunctions(); return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas()); diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index e2b03461b..2285bcbaf 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -951,6 +951,12 @@ namespace storm { return result; } + Model Model::substituteConstantsFunctions() const { + auto result = substituteConstants(); + result.substituteFunctions(); + return result; + } + std::map Model::getConstantsSubstitution() const { std::map result; diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 445552cf1..bc32a14c2 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -399,6 +399,12 @@ namespace storm { void substituteFunctions(); void substituteFunctions(std::vector& properties); + /*! + * Substitutes all constants in all expressions of the model. The original model is not modified, but + * instead a new model is created. Afterwards, all function calls are substituted with the defining expression. + */ + Model substituteConstantsFunctions() const; + /*! * Returns true if at least one array variable occurs in the model. */