diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index cdae727c5..8c76959b5 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -58,6 +58,24 @@ 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; + } } else if (element->isBasicElement()) { // Set rates for BE std::shared_ptr const> be = std::static_pointer_cast const>(element);