diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 30e0d2eec..1a4cd7019 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -1,7 +1,7 @@ #include "DftJsonExporter.h" +#include "storm/utility/file.h" #include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/FileIoException.h" #include #include @@ -9,19 +9,12 @@ 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; - ofs.open(filepath, std::ofstream::out); - if(ofs.is_open()) { - toStream(dft, ofs); - ofs.close(); - } else { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); - } + std::ofstream stream; + storm::utility::openFile(filepath, stream); + toStream(dft, stream); + storm::utility::closeFile(stream); } template @@ -32,27 +25,19 @@ namespace storm { template modernjson::json DftJsonExporter::translate(storm::storage::DFT const& dft) { modernjson::json jsonDft; - currentId = 0; + jsonDft["toplevel"] = dft.getTopLevelIndex(); + + // Parameters + modernjson::json jsonParameters; + jsonDft["parameters"] = jsonParameters; // 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); } + jsonDft["nodes"] = jsonNodes; return jsonDft; } @@ -61,9 +46,10 @@ namespace storm { 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["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 @@ -73,52 +59,43 @@ namespace storm { children.push_back(child->id()); } nodeData["children"] = children; + // Set gate specific data + switch (element->type()) { + case storm::storage::DFTElementType::VOT: + nodeData["voting"] = std::static_pointer_cast const>(element)->threshold(); + break; + default: + break; + } } else if (element->isBasicElement()) { - // Set rates for BE + // Set BE specific data std::shared_ptr const> be = std::static_pointer_cast const>(element); - std::stringstream stream; - stream << be->activeFailureRate(); - nodeData["rate"] = stream.str(); - stream.clear(); - stream << (be->passiveFailureRate() / be->activeFailureRate()); - nodeData["dorm"] = stream.str(); + nodeData["rate"] = storm::utility::to_string(be->activeFailureRate()); + nodeData["dorm"] = storm::utility::to_string(be->passiveFailureRate() / be->activeFailureRate()); + nodeData["repair"] = 0; + nodeData["transient"] = be->isTransient(); + } else if (element->isDependency()) { + std::shared_ptr const> dependency = std::static_pointer_cast const>(element); + std::vector children = { dependency->triggerEvent()->id() }; + for (DFTElementPointer const& child : dependency->dependentEvents()) { + children.push_back(child->id()); + } + nodeData["children"] = children; + nodeData["prob"] = storm::utility::to_string(dependency->probability()); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Type name: " << type << " not supported for export."); } 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..e7650614c 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.h +++ b/src/storm-dft/storage/dft/DftJsonExporter.h @@ -34,14 +34,9 @@ namespace storm { private: - static size_t currentId; - static modernjson::json translateNode(DFTElementCPointer const& element); - static modernjson::json translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index); - - }; - + } }