Browse Source

JaniParser: Making result field optional (fixes #83)

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
75b6ac27e8
  1. 7
      src/storm-parsers/parser/JaniParser.cpp

7
src/storm-parsers/parser/JaniParser.cpp

@ -1564,7 +1564,12 @@ namespace storm {
inputs.push_back(syncInput);
}
}
std::string syncResult = syncEntry.at("result");
std::string syncResult;
if (syncEntry.count("result")) {
syncResult = syncEntry.at("result");
} else {
syncResult = storm::jani::Model::SILENT_ACTION_NAME;
}
syncVectors.emplace_back(inputs, syncResult);
}
return syncVectors;

Loading…
Cancel
Save