From 096d532aa02d3832b8bdcaec9d8a1640157e0d51 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 15 Jan 2018 14:04:57 +0100 Subject: [PATCH] Small changes --- .../DftToGspnTransformator.cpp | 27 ++++----- src/storm-gspn/storage/gspn/GSPN.cpp | 9 +++ src/storm-gspn/storage/gspn/GSPN.h | 5 +- .../storage/gspn/GspnJsonExporter.cpp | 58 +++++++++++++++++-- .../storage/gspn/GspnJsonExporter.h | 6 +- 5 files changed, 78 insertions(+), 27 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 1cb6673c7..c948f297f 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -98,7 +98,6 @@ namespace storm { double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); - uint64_t disabledNode = 0; if (!smart || dftBE->nrRestrictions() > 0) { @@ -146,7 +145,7 @@ namespace storm { builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); uint64_t unavailableNode = 0; - if (isRepresentative) { + if (!smart || isRepresentative) { unavailableNode = addUnavailableNode(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); } @@ -155,10 +154,10 @@ namespace storm { builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); builder.addInhibitionArc(nodeFailed, tAndFailed); builder.addOutputArc(tAndFailed, nodeFailed); - if (isRepresentative) { + if (!smart || isRepresentative) { builder.addOutputArc(tAndFailed, unavailableNode); } - for(auto const& child : dftAnd->children()) { + for (auto const& child : dftAnd->children()) { assert(failedNodes.size() > child->id()); builder.addInputArc(failedNodes[child->id()], tAndFailed); builder.addOutputArc(tAndFailed, failedNodes[child->id()]); @@ -176,7 +175,7 @@ namespace storm { builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); uint64_t unavailableNode = 0; - if (isRepresentative) { + if (!smart || isRepresentative) { unavailableNode = addUnavailableNode(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); } @@ -186,7 +185,7 @@ namespace storm { builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0)); builder.addInhibitionArc(nodeFailed, tNodeFailed); builder.addOutputArc(tNodeFailed, nodeFailed); - if (isRepresentative) { + if (!smart || isRepresentative) { builder.addOutputArc(tNodeFailed, unavailableNode); } assert(failedNodes.size() > child->id()); @@ -265,10 +264,12 @@ namespace storm { builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); builder.addInhibitionArc(nodeFS, tNodeFailed); - for(auto const& child : dftPand->children()) { + // Transition for failed + for (auto const& child : dftPand->children()) { builder.addInputArc(failedNodes[child->id()], tNodeFailed); builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); } + // Transitions for fail-safe for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) { uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j)); builder.setTransitionLayoutInfo(tfs, storm::gspn::LayoutInfo(xcenter-6.0+j*3.0, ycenter+3.0)); @@ -290,9 +291,11 @@ namespace storm { builder.addInhibitionArc(failedNodes.at(child->id()), tn); } if (j != dftPand->nrChildren() - 1) { + // Not last child tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j)); builder.setTransitionLayoutInfo(tn, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0)); } else { + // Last child tn = tNodeFailed; } builder.addInputArc(failedNodes.at(child->id()), tn); @@ -353,7 +356,6 @@ namespace storm { builder.addInhibitionArc(nodeFS, tfailsf); builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); } - ++j; } } else { @@ -448,9 +450,6 @@ namespace storm { builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); builder.addOutputArc(nextclTransitions.back(), unavailableNode); } - - - } template @@ -515,13 +514,7 @@ namespace storm { if (!smart || mDft.isRepresentative(depEv->id())) { builder.addOutputArc(tx, unavailableNodes.at(depEv->id())); } - } - - - - - } template diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 3a603cb8b..f26c71540 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -395,6 +395,15 @@ namespace storm { this->transitionLayout = transitionLayout; } + std::map const& GSPN::getPlaceLayoutInfos() const { + return this->placeLayout; + } + + std::map const& GSPN::getTransitionLayoutInfos() const { + return this->transitionLayout; + } + + void GSPN::toPnpro(std::ostream &stream) const { auto space = " "; auto space2 = " "; diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h index 6a0d58143..7b37ed5cb 100644 --- a/src/storm-gspn/storage/gspn/GSPN.h +++ b/src/storm-gspn/storage/gspn/GSPN.h @@ -154,7 +154,10 @@ namespace storm { void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layout) const; void setPlaceLayoutInfo(std::map const& placeLayout) const; void setTransitionLayoutInfo(std::map const& transitionLayout) const; - + + std::map const& getPlaceLayoutInfos() const; + + std::map const& getTransitionLayoutInfos() const; /*! * Performe some checks diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp index 5432074ee..4e451d094 100644 --- a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp +++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp @@ -9,6 +9,10 @@ namespace storm { namespace gspn { + // Prevent some magic constants + static constexpr const uint64_t scaleFactor = 50; + + void GspnJsonExporter::toStream(storm::gspn::GSPN const& gspn, std::ostream& os) { os << translate(gspn).dump(4) << std::endl; } @@ -16,21 +20,48 @@ namespace storm { modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) { modernjson::json jsonGspn; + // Layouts + std::map placeLayout = gspn.getPlaceLayoutInfos(); + std::map transitionLayout = gspn.getTransitionLayoutInfos(); + double tmpX = 0; + double tmpY = 10; + // Export places for (const auto &place : gspn.getPlaces()) { - modernjson::json jsonPlace = translatePlace(place); + double x = tmpX; + double y = tmpY; + if (placeLayout.count(place.getID()) > 0) { + x = placeLayout.at(place.getID()).x; + y = placeLayout.at(place.getID()).y; + } + tmpX += 3; + modernjson::json jsonPlace = translatePlace(place, x, y); jsonGspn.push_back(jsonPlace); } // Export immediate transitions for (const auto &transition : gspn.getImmediateTransitions()) { - modernjson::json jsonImmediateTransition = translateImmediateTransition(transition); + double x = tmpX; + double y = tmpY; + if (transitionLayout.count(transition.getID()) > 0) { + x = transitionLayout.at(transition.getID()).x; + y = transitionLayout.at(transition.getID()).y; + } + tmpX += 3; + modernjson::json jsonImmediateTransition = translateImmediateTransition(transition, x, y); jsonGspn.push_back(jsonImmediateTransition); } // Export timed transitions for (const auto &transition : gspn.getTimedTransitions()) { - modernjson::json jsonTimedTransition = translateTimedTransition(transition); + double x = tmpX; + double y = tmpY; + if (transitionLayout.count(transition.getID()) > 0) { + x = transitionLayout.at(transition.getID()).x; + y = transitionLayout.at(transition.getID()).y; + } + tmpX += 3; + modernjson::json jsonTimedTransition = translateTimedTransition(transition, x, y); jsonGspn.push_back(jsonTimedTransition); } @@ -86,42 +117,57 @@ namespace storm { } - modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place) { + modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) { modernjson::json data; data["id"] = toJsonString(place); data["name"] = place.getName(); data["marking"] = place.getNumberOfInitialTokens(); + modernjson::json position; + position["x"] = x * scaleFactor; + position["y"] = y * scaleFactor; + modernjson::json jsonPlace; jsonPlace["data"] = data; + jsonPlace["position"] = position; jsonPlace["group"] = "nodes"; jsonPlace["classes"] = "place"; return jsonPlace; } - modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition const& transition) { + modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition const& transition, double x, double y) { modernjson::json data; data["id"] = toJsonString(transition, true); data["name"] = transition.getName(); data["priority"] = transition.getPriority(); data["weight"] = transition.getWeight(); + modernjson::json position; + position["x"] = x * scaleFactor; + position["y"] = y * scaleFactor; + modernjson::json jsonTrans; jsonTrans["data"] = data; + jsonTrans["position"] = position; jsonTrans["group"] = "nodes"; jsonTrans["classes"] = "trans_im"; return jsonTrans; } - modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition const& transition) { + modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition const& transition, double x, double y) { modernjson::json data; data["id"] = toJsonString(transition, false); data["name"] = transition.getName(); data["rate"] = transition.getRate(); data["priority"] = transition.getPriority(); + modernjson::json position; + position["x"] = x * scaleFactor; + position["y"] = y * scaleFactor; + modernjson::json jsonTrans; jsonTrans["data"] = data; + jsonTrans["position"] = position; jsonTrans["group"] = "nodes"; jsonTrans["classes"] = "trans_time"; return jsonTrans; diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.h b/src/storm-gspn/storage/gspn/GspnJsonExporter.h index c49a5a872..9c225434d 100644 --- a/src/storm-gspn/storage/gspn/GspnJsonExporter.h +++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.h @@ -26,11 +26,11 @@ namespace storm { private: enum ArcType { INPUT, OUTPUT, INHIBITOR }; - static modernjson::json translatePlace(storm::gspn::Place const& place); + static modernjson::json translatePlace(storm::gspn::Place const& place, double x, double y); - static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition const& transition); + static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition const& transition, double x, double y); - static modernjson::json translateTimedTransition(storm::gspn::TimedTransition const& transition); + static modernjson::json translateTimedTransition(storm::gspn::TimedTransition const& transition, double x, double y); static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype);