diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 1e0de68b5..f9ed51ef3 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -124,14 +124,18 @@ namespace storm { Scope scope(name); // Parse constants - size_t constantsCount = parsedStructure.count("constants"); ConstantsMap constants; scope.constants = &constants; + size_t constantsCount = parsedStructure.count("constants"); STORM_LOG_THROW(constantsCount < 2, storm::exceptions::InvalidJaniException, "Constant-declarations can be given at most once."); if (constantsCount == 1) { for (auto const &constStructure : parsedStructure.at("constants")) { std::shared_ptr constant = parseConstant(constStructure, scope.refine("constants[" + std::to_string(constants.size()) + "]")); - constants.emplace(constant->getName(), &model.addConstant(*constant)); + model.addConstant(*constant); + } + // Insert references after adding all constants to make sure that they remain valid + for (auto const& constant : model.getConstants()) { + constants.emplace(constant.getName(), &constant); } } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 11255bf12..3aa65516f 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -604,12 +604,12 @@ namespace storm { return nonsilentActionIndices; } - Constant const& Model::addConstant(Constant const& constant) { + void Model::addConstant(Constant const& constant) { auto it = constantToIndex.find(constant.getName()); STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists."); constantToIndex.emplace(constant.getName(), constants.size()); constants.push_back(constant); - return constants.back(); + // Note that we should not return a reference to the inserted constant as it might get invalidated when more constants are added. } bool Model::hasConstant(std::string const& name) const { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 3824398e5..36e2ee99b 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -157,7 +157,7 @@ namespace storm { /*! * Adds the given constant to the model. */ - Constant const& addConstant(Constant const& constant); + void addConstant(Constant const& constant); /*! * Retrieves whether the model has a constant with the given name. @@ -176,6 +176,7 @@ namespace storm { /*! * Retrieves the constant with the given name (if any). + * @note the reference to the constant is invalidated whenever a new constant is added. */ Constant const& getConstant(std::string const& name) const;