Browse Source

fixed incorrect parsing of jani constants

tempestpy_adaptions
TimQu 6 years ago
parent
commit
0bacb6f5eb
  1. 8
      src/storm-parsers/parser/JaniParser.cpp
  2. 4
      src/storm/storage/jani/Model.cpp
  3. 3
      src/storm/storage/jani/Model.h

8
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<storm::jani::Constant> 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);
}
}

4
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 {

3
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;

Loading…
Cancel
Save