diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 80ccdec45..4c4dc0a3c 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -24,27 +24,11 @@ namespace storm { } template - std::string DFTJsonParser::stripQuotsFromName(std::string const& name) { - size_t firstQuots = name.find("\""); - size_t secondQuots = name.find("\"", firstQuots+1); - - if(firstQuots == std::string::npos) { - return name; - } else { - STORM_LOG_THROW(secondQuots != std::string::npos, storm::exceptions::FileIoException, "No ending quotation mark found in " << name); - return name.substr(firstQuots+1,secondQuots-1); - } - } - - template - std::string DFTJsonParser::getString(json const& structure, std::string const& errorInfo) { - STORM_LOG_THROW(structure.is_string(), storm::exceptions::FileIoException, "Expected a string in " << errorInfo << ", got '" << structure.dump() << "'"); - return structure.front(); - } - - template - std::string DFTJsonParser::parseNodeIdentifier(std::string const& name) { - return boost::replace_all_copy(name, "'", "__prime__"); + std::string DFTJsonParser::generateUniqueName(std::string const& id, std::string const& name) { + std::string newId = name; + std::replace(newId.begin(), newId.end(), ' ', '_'); + std::replace(newId.begin(), newId.end(), '-', '_'); + return newId + "_" + id; } template @@ -66,52 +50,33 @@ namespace storm { parsedJson << file; file.close(); - std::string toplevelName = ""; + storm::expressions::Variable var = manager->declareRationalVariable("x"); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + + json nodes = parsedJson.at("nodes"); - // Start by building mapping from ids to names + // Start by building mapping from ids to their unique names std::map nameMapping; - for (auto& element: parsedJson) { - if (element.at("classes") != "") { - 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::replace(name.begin(), name.end(), '-', '_'); - std::stringstream stream; - stream << name << "_" << data.at("id").get(); - name = stream.str(); - - nameMapping[id] = name; - } + for (auto& element: nodes) { + json data = element.at("data"); + std::string id = data.at("id"); + nameMapping[id] = generateUniqueName(id, data.at("name")); } - std::cout << toplevelName << std::endl; - for (auto& element : parsedJson) { + for (auto& element : nodes) { STORM_LOG_TRACE("Parsing: " << element); bool success = true; - if (element.at("classes") == "") { - continue; - } json data = element.at("data"); - std::string name = data.at("name"); - std::replace(name.begin(), name.end(), ' ', '_'); - std::replace(name.begin(), name.end(), '-', '_'); - std::stringstream stream; - 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; - } + std::string name = generateUniqueName(data.at("id"), data.at("name")); std::vector childNames; if (data.count("children") > 0) { - for (json& child : data.at("children")) { - childNames.push_back(nameMapping[child.get()]); + for (std::string const& child : data.at("children")) { + childNames.push_back(nameMapping[child]); } } - std::string type = getString(element.at("classes"), "classes"); + std::string type = data.at("type"); if(type == "and") { success = builder.addAndElement(name, childNames); @@ -152,6 +117,7 @@ namespace storm { STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } + std::string toplevelName = nameMapping[parsedJson.at("toplevel")]; if(!builder.setTopLevel(toplevelName)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index cf2e83826..d23baf58e 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -38,9 +38,7 @@ namespace storm { private: void readFile(std::string const& filename); - std::string stripQuotsFromName(std::string const& name); - std::string parseNodeIdentifier(std::string const& name); - std::string getString(json const& structure, std::string const& errorInfo); + std::string generateUniqueName(std::string const& id, std::string const& name); ValueType parseRationalExpression(std::string const& expr); };