diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 699490984..608d01aca 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/NotSupportedException.h" #include #include @@ -54,23 +54,32 @@ namespace storm { children.push_back(std::to_string(child->id())); } nodeData["children"] = children; - // Gate dependent export - switch (element->type()) { - case storm::storage::DFTElementType::VOT: - nodeData["voting"] = std::static_pointer_cast const>(element)->threshold(); - break; - case storm::storage::DFTElementType::PDEP: - { - ValueType probability = std::static_pointer_cast const>(element)->probability(); - if (!storm::utility::isOne(probability)) { - std::stringstream stream; - stream << probability; - nodeData["prob"] = stream.str(); - } - break; - } - default: - break; + + // 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 @@ -82,6 +91,8 @@ namespace storm { 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;