From 743ce2b023079a6dd678b46660a9b858a960f7bf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 22 Dec 2016 12:21:00 +0100 Subject: [PATCH] Export DFT to Cytoscape JSON format --- src/storm-dft-cli/storm-dyftee.cpp | 12 +- .../settings/modules/DFTSettings.cpp | 12 +- src/storm-dft/settings/modules/DFTSettings.h | 15 +++ src/storm-dft/storage/dft/DFTElementType.h | 2 +- src/storm-dft/storage/dft/DftJsonExporter.cpp | 122 ++++++++++++++++++ src/storm-dft/storage/dft/DftJsonExporter.h | 47 +++++++ 6 files changed, 207 insertions(+), 3 deletions(-) create mode 100644 src/storm-dft/storage/dft/DftJsonExporter.cpp create mode 100644 src/storm-dft/storage/dft/DftJsonExporter.h diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index f246438fe..78e411df8 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -19,7 +19,7 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" - +#include "storm-dft/storage/dft/DftJsonExporter.h" #include "storm-dft/settings/modules/DFTSettings.h" @@ -129,6 +129,16 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } + if (dftSettings.isExportToJson()) { + STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); + storm::parser::DFTGalileoParser parser; + storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + // Export to json + storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); + storm::utility::cleanUp(); + return 0; + } + if (dftSettings.isTransformToGspn()) { std::shared_ptr> dft; diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index 898360c4b..6af1d9678 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -32,6 +32,7 @@ namespace storm { const std::string DFTSettings::minValueOptionName = "min"; const std::string DFTSettings::maxValueOptionName = "max"; const std::string DFTSettings::transformToGspnOptionName = "gspn"; + const std::string DFTSettings::exportToJsonOptionName = "export-json"; #ifdef STORM_HAVE_Z3 const std::string DFTSettings::solveWithSmtOptionName = "smt"; #endif @@ -55,8 +56,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); } - + bool DFTSettings::isDftFileSet() const { return this->getOption(dftFileOptionName).getHasOptionBeenSet(); } @@ -141,6 +143,14 @@ namespace storm { return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); } + bool DFTSettings::isExportToJson() const { + return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); + } + + std::string DFTSettings::getExportJsonFilename() const { + return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); + } + void DFTSettings::finalize() { } diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h index c1a9df7e5..0d8695e2a 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DFTSettings.h @@ -138,6 +138,20 @@ namespace storm { * @return True iff the option was set. */ bool isTransformToGspn() const; + + /*! + * Retrieves whether the export to Json file option was set. + * + * @return True if the export to json file option was set. + */ + bool isExportToJson() const; + + /*! + * Retrieves the name of the json file to export to. + * + * @return The name of the json file to export to. + */ + std::string getExportJsonFilename() const; #ifdef STORM_HAVE_Z3 /*! @@ -177,6 +191,7 @@ namespace storm { static const std::string solveWithSmtOptionName; #endif static const std::string transformToGspnOptionName; + static const std::string exportToJsonOptionName; }; diff --git a/src/storm-dft/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h index 800da161f..1527efe25 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -75,7 +75,7 @@ namespace storm { } inline std::ostream& operator<<(std::ostream& os, DFTElementType const& tp) { - return os << toString(tp) << std::endl; + return os << toString(tp); } diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp new file mode 100644 index 000000000..89cb07287 --- /dev/null +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -0,0 +1,122 @@ +#include "DftJsonExporter.h" + +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/FileIOException.h" + +#include +#include + +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); + } + } + + 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) { + 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); + } + } + } + + 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["name"] = element->name(); + + 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(child->id()); + } + nodeData["children"] = children; + } else if (element->isBasicElement()) { + // Set rates for BE + 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(); + } + + 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; + nodeData["id"] = currentId; + ++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 new file mode 100644 index 000000000..ef04750ba --- /dev/null +++ b/src/storm-dft/storage/dft/DftJsonExporter.h @@ -0,0 +1,47 @@ +#pragma once + +#include "storm/utility/macros.h" + +#include "storm-dft/storage/dft/DFT.h" + +// JSON parser +#include "json.hpp" +namespace modernjson { + using json = nlohmann::basic_json; +} + +namespace storm { + namespace storage { + + /** + * Exports a DFT into the JSON format for visualizing it. + */ + template + class DftJsonExporter { + + using DFTElementPointer = std::shared_ptr>; + using DFTElementCPointer = std::shared_ptr const>; + using DFTGatePointer = std::shared_ptr>; + + public: + + static void toFile(storm::storage::DFT const& dft, std::string const& filepath); + + 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 translateNode(DFTElementCPointer const& element); + + static modernjson::json translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index); + + + }; + + } +}