From ca0d76e502d3755e52b251e3229726135a16ac21 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 15 Jan 2018 11:34:59 +0100 Subject: [PATCH] Finished JSON export for GSPNs --- .../storage/gspn/GspnJsonExporter.cpp | 86 +++++++++++++++++-- .../storage/gspn/GspnJsonExporter.h | 36 ++++++++ 2 files changed, 113 insertions(+), 9 deletions(-) diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp index aee23cf00..5432074ee 100644 --- a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp +++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp @@ -34,15 +34,61 @@ namespace storm { jsonGspn.push_back(jsonTimedTransition); } + // Export arcs + std::vector places = gspn.getPlaces(); + // Export arcs for immediate transitions + for (const auto &transition : gspn.getImmediateTransitions()) { + // Export input arcs + for (auto const& entry : transition.getInputPlaces()) { + storm::gspn::Place place = places.at(entry.first); + modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INPUT); + jsonGspn.push_back(jsonInputArc); + } + + // Export inhibitor arcs + for (auto const& entry : transition.getInhibitionPlaces()) { + storm::gspn::Place place = places.at(entry.first); + modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INHIBITOR); + jsonGspn.push_back(jsonInputArc); + } + + // Export output arcs + for (auto const& entry : transition.getOutputPlaces()) { + storm::gspn::Place place = places.at(entry.first); + modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::OUTPUT); + jsonGspn.push_back(jsonInputArc); + } + } + // Export arcs for timed transitions + for (const auto &transition : gspn.getTimedTransitions()) { + // Export input arcs + for (auto const& entry : transition.getInputPlaces()) { + storm::gspn::Place place = places.at(entry.first); + modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INPUT); + jsonGspn.push_back(jsonInputArc); + } + + // Export inhibitor arcs + for (auto const& entry : transition.getInhibitionPlaces()) { + storm::gspn::Place place = places.at(entry.first); + modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INHIBITOR); + jsonGspn.push_back(jsonInputArc); + } + + // Export output arcs + for (auto const& entry : transition.getOutputPlaces()) { + storm::gspn::Place place = places.at(entry.first); + modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::OUTPUT); + jsonGspn.push_back(jsonInputArc); + } + } return jsonGspn; } modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place) { modernjson::json data; - std::stringstream stream; - stream << "p" << place.getID(); - data["id"] = stream.str(); + data["id"] = toJsonString(place); data["name"] = place.getName(); data["marking"] = place.getNumberOfInitialTokens(); @@ -55,9 +101,7 @@ namespace storm { modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition const& transition) { modernjson::json data; - std::stringstream stream; - stream << "i" << transition.getID(); - data["id"] = stream.str(); + data["id"] = toJsonString(transition, true); data["name"] = transition.getName(); data["priority"] = transition.getPriority(); data["weight"] = transition.getWeight(); @@ -71,9 +115,7 @@ namespace storm { modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition const& transition) { modernjson::json data; - std::stringstream stream; - stream << "t" << transition.getID(); - data["id"] = stream.str(); + data["id"] = toJsonString(transition, false); data["name"] = transition.getName(); data["rate"] = transition.getRate(); data["priority"] = transition.getPriority(); @@ -85,5 +127,31 @@ namespace storm { return jsonTrans; } + modernjson::json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) { + modernjson::json data; + data["id"] = toJsonString(transition, place, arctype); + data["source"] = toJsonString(place); + data["target"] = toJsonString(transition, immediate); + data["mult"] = multiplicity; + + modernjson::json jsonArc; + jsonArc["data"] = data; + //jsonTrans["group"] = "nodes"; + switch (arctype) { + case INPUT: + jsonArc["classes"] = "input"; + break; + case OUTPUT: + jsonArc["classes"] = "output"; + break; + case INHIBITOR: + jsonArc["classes"] = "inhibit"; + break; + default: + STORM_LOG_ASSERT(false, "Unknown type " << arctype << " used."); + } + return jsonArc; + } + } } diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.h b/src/storm-gspn/storage/gspn/GspnJsonExporter.h index 00b3f19a4..c49a5a872 100644 --- a/src/storm-gspn/storage/gspn/GspnJsonExporter.h +++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.h @@ -24,11 +24,47 @@ namespace storm { static modernjson::json translate(storm::gspn::GSPN const& gspn); private: + enum ArcType { INPUT, OUTPUT, INHIBITOR }; + static modernjson::json translatePlace(storm::gspn::Place const& place); static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition const& transition); static modernjson::json translateTimedTransition(storm::gspn::TimedTransition const& transition); + + static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype); + + std::string static inline toJsonString(storm::gspn::Place const& place) { + std::stringstream stream; + stream << "p" << place.getID(); + return stream.str(); + } + + std::string static inline toJsonString(storm::gspn::Transition const& transition, bool immediate) { + std::stringstream stream; + stream << (immediate ? "i" : "t") << transition.getID(); + return stream.str(); + } + + std::string static inline toJsonString(storm::gspn::Transition const& transition, storm::gspn::Place const& place, ArcType arctype) { + std::stringstream stream; + stream << place.getID(); + switch (arctype) { + case INPUT: + stream << "i"; + break; + case OUTPUT: + stream << "o"; + break; + case INHIBITOR: + stream << "h"; + break; + default: + STORM_LOG_ASSERT(false, "Unknown type " << arctype << " used."); + } + stream << transition.getID(); + return stream.str(); + } }; }