diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 2d0ddfe39..774f2cef8 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -74,27 +74,33 @@ namespace storm { if (element.at("classes") != "") { json data = element.at("data"); std::string id = data.at("id"); - std::string name = data.at("name"); + // Append to id to distinguish elements with the same name + std::stringstream stream; + stream << data.at("name").get() << "-" << id; + std::string name = stream.str(); nameMapping[id] = name; - if (data.count("toplevel") > 0) { - STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); - toplevelName = name; - } } } std::cout << toplevelName << std::endl; for (auto& element : parsedJson) { + 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::stringstream stream; + stream << data.at("name").get() << "-" << data.at("id").get(); + std::string name = stream.str(); + if (data.count("toplevel") > 0) { + STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); + toplevelName = name; + } std::vector childNames; if (data.count("children") > 0) { - for (auto& child : data.at("children")) { - childNames.push_back(nameMapping[child]); + for (json& child : data.at("children")) { + childNames.push_back(nameMapping[child.get()]); } } @@ -126,11 +132,16 @@ namespace storm { success = false; } - // Set layout positions - json position = element.at("position"); - double x = position.at("x"); - double y = position.at("y"); - builder.addLayoutInfo(name, x / 7, y / 7); + // Do not set layout for dependencies + // This does not work because dependencies might be splitted + // TODO: do splitting later in rewriting step + if (type != "fdep" && type != "pdep") { + // Set layout positions + json position = element.at("position"); + double x = position.at("x"); + double y = position.at("y"); + builder.addLayoutInfo(name, x / 7, y / 7); + } STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 974ffac8a..db779e3d9 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -159,7 +159,7 @@ namespace storm { template bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp) { - STORM_LOG_ASSERT(children.size() > 0, "No child."); + STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); if(mElements.count(name) != 0) { // Element with that name already exists. return false; diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 636b5e5a1..598c1d765 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -103,7 +103,7 @@ namespace storm { //TODO Matthias: collect constraints for SMT solving //0 <= probability <= 1 if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { - // Introduce additional element for first capturing the proabilistic dependency + // Introduce additional element for first capturing the probabilistic dependency std::string nameAdditional = name + "_additional"; addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero()); // First consider probabilistic dependency