From c7e7722af6963df204d19c4b74fe473c43a9d065 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Feb 2017 19:17:01 +0100 Subject: [PATCH] Avoid whitespace in element names --- src/storm-dft/parser/DFTJsonParser.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 774f2cef8..7d4a64a64 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -75,9 +75,12 @@ namespace storm { json data = element.at("data"); std::string id = data.at("id"); // Append to id to distinguish elements with the same name + std::string name = data.at("name"); + std::replace(name.begin(), name.end(), ' ', '_'); std::stringstream stream; - stream << data.at("name").get() << "-" << id; - std::string name = stream.str(); + stream << name << "_" << data.at("id").get(); + name = stream.str(); + nameMapping[id] = name; } } @@ -90,9 +93,11 @@ namespace storm { continue; } json data = element.at("data"); + std::string name = data.at("name"); + std::replace(name.begin(), name.end(), ' ', '_'); std::stringstream stream; - stream << data.at("name").get() << "-" << data.at("id").get(); - std::string name = stream.str(); + stream << name << "_" << data.at("id").get(); + name = stream.str(); if (data.count("toplevel") > 0) { STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); toplevelName = name;