diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 30e0d2eec..cdae727c5 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -9,9 +9,6 @@ namespace storm { namespace storage { - template - size_t DftJsonExporter::currentId = 0; - template void DftJsonExporter::toFile(storm::storage::DFT const& dft, std::string const& filepath) { std::ofstream ofs; @@ -31,46 +28,34 @@ namespace storm { template modernjson::json DftJsonExporter::translate(storm::storage::DFT const& dft) { - modernjson::json jsonDft; - currentId = 0; - // Nodes modernjson::json jsonNodes; for (size_t i = 0; i < dft.nrElements(); ++i) { modernjson::json jsonNode = translateNode(dft.getElement(i)); - jsonDft.push_back(jsonNode); - } - - // Edges - modernjson::json jsonEdges; - for (size_t i = 0; i < dft.nrElements(); ++i) { - if (dft.isGate(i)) { - std::shared_ptr const> gate = dft.getGate(i); - for (size_t index = 0; index < gate->nrChildren(); ++index) { - DFTElementPointer child = gate->children()[index]; - modernjson::json jsonEdge = translateEdge(gate, child, index); - jsonDft.push_back(jsonEdge); - } - } + jsonNodes.push_back(jsonNode); } + modernjson::json jsonDft; + jsonDft["toplevel"] = std::to_string(dft.getTopLevelIndex()); + jsonDft["nodes"] = jsonNodes; return jsonDft; } template modernjson::json DftJsonExporter::translateNode(DFTElementCPointer const& element) { modernjson::json nodeData; - nodeData["id"] = element->id(); - ++currentId; - STORM_LOG_ASSERT(element->id() == currentId-1, "Ids do not correspond"); + nodeData["id"] = std::to_string(element->id()); nodeData["name"] = element->name(); + std::string type = storm::storage::toString(element->type()); + std::transform(type.begin(), type.end(), type.begin(), ::tolower); + nodeData["type"] = type; if (element->isGate()) { // Set children for gate std::shared_ptr const> gate = std::static_pointer_cast const>(element); - std::vector children; + std::vector children; for (DFTElementPointer const& child : gate->children()) { - children.push_back(child->id()); + children.push_back(std::to_string(child->id())); } nodeData["children"] = children; } else if (element->isBasicElement()) { @@ -86,39 +71,14 @@ namespace storm { modernjson::json jsonNode; jsonNode["data"] = nodeData; - jsonNode["group"] = "nodes"; - std::string type = storm::storage::toString(element->type()); - std::transform(type.begin(), type.end(), type.begin(), ::tolower); jsonNode["classes"] = type; return jsonNode; } - template - modernjson::json DftJsonExporter::translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index) { - modernjson::json nodeData; - std::stringstream stream; - stream << gate->id() << "e" << child->id(); - nodeData["id"] = stream.str(); - ++currentId; - nodeData["source"] = gate->id(); - nodeData["target"] = child->id(); - nodeData["index"] = index; - - modernjson::json jsonNode; - jsonNode["data"] = nodeData; - - jsonNode["group"] = "edges"; - jsonNode["classes"] = ""; - return jsonNode; - } - // Explicitly instantiate the class. template class DftJsonExporter; - -#ifdef STORM_HAVE_CARL template class DftJsonExporter; -#endif } } diff --git a/src/storm-dft/storage/dft/DftJsonExporter.h b/src/storm-dft/storage/dft/DftJsonExporter.h index ef04750ba..646821bb6 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.h +++ b/src/storm-dft/storage/dft/DftJsonExporter.h @@ -29,19 +29,12 @@ namespace storm { static void toStream(storm::storage::DFT const& dft, std::ostream& os); - static modernjson::json translate(storm::storage::DFT const& dft); - - private: - static size_t currentId; + static modernjson::json translate(storm::storage::DFT const& dft); static modernjson::json translateNode(DFTElementCPointer const& element); - static modernjson::json translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index); - - }; - } }