#include "DftJsonExporter.h" #include "storm/utility/file.h" #include "storm/exceptions/NotSupportedException.h" #include #include namespace storm { namespace storage { template void DftJsonExporter::toFile(storm::storage::DFT const& dft, std::string const& filepath) { std::ofstream stream; storm::utility::openFile(filepath, stream); toStream(dft, stream); storm::utility::closeFile(stream); } template void DftJsonExporter::toStream(storm::storage::DFT const& dft, std::ostream& os) { os << translate(dft).dump(4) << std::endl; } template modernjson::json DftJsonExporter::translate(storm::storage::DFT const& dft) { // Nodes modernjson::json jsonNodes; for (size_t i = 0; i < dft.nrElements(); ++i) { modernjson::json jsonNode = translateNode(dft.getElement(i)); 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"] = 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; for (DFTElementPointer const& child : gate->children()) { children.push_back(std::to_string(child->id())); } nodeData["children"] = children; // Set threshold for voting gate if (element->type() == storm::storage::DFTElementType::VOT) { nodeData["voting"] = std::static_pointer_cast const>(element)->threshold(); } } else if (element->isRestriction()) { // Set children for restriction auto seq = std::static_pointer_cast const>(element); std::vector children; for (DFTElementPointer const& child : seq->children()) { children.push_back(std::to_string(child->id())); } nodeData["children"] = children; } else if (element->isDependency()) { // Set children for dependency auto dependency = std::static_pointer_cast const>(element); std::vector children; children.push_back(std::to_string(dependency->triggerEvent()->id())); for (DFTElementPointer const& child : dependency->dependentEvents()) { children.push_back(std::to_string(child->id())); } nodeData["children"] = children; if (!storm::utility::isOne(dependency->probability())) { std::stringstream stream; stream << dependency->probability(); nodeData["prob"] = stream.str(); } } else if (element->isBasicElement()) { // 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.str(std::string()); // Clear stringstream ValueType dormancy = be->passiveFailureRate() / be->activeFailureRate(); stream << dormancy; nodeData["dorm"] = stream.str(); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Element of type '" << element->type() << "' is not supported."); } modernjson::json jsonNode; jsonNode["data"] = nodeData; jsonNode["group"] = "nodes"; jsonNode["classes"] = type; return jsonNode; } // Explicitly instantiate the class. template class DftJsonExporter; template class DftJsonExporter; } }