From 49537a83d35fbb1ee19261aa4074f69f88ab5559 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 20:04:32 +0100 Subject: [PATCH] added layout info to gspn - dft to gspn builds some layout in be and and --- .../DftToGspnTransformator.cpp | 15 ++++++- src/storm-gspn/storage/gspn/GSPN.cpp | 43 ++++++++++++++++--- src/storm-gspn/storage/gspn/GSPN.h | 13 +++++- src/storm-gspn/storage/gspn/GspnBuilder.cpp | 14 +++++- src/storm-gspn/storage/gspn/GspnBuilder.h | 14 ++++-- src/storm-gspn/storage/gspn/PlacementInfo.h | 17 ++++++++ src/storm-gspn/storage/gspn/Transition.h | 3 ++ 7 files changed, 106 insertions(+), 13 deletions(-) create mode 100644 src/storm-gspn/storage/gspn/PlacementInfo.h diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 355c6f440..9ab52f28c 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -90,11 +90,13 @@ namespace storm { template void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE, bool isRepresentative) { - + double xcenter = 10.0; + double ycenter = 10.0; uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); activeNodes.emplace(dftBE->id(), beActive); uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); + uint64_t unavailableNode = 0; if (isRepresentative) { unavailableNode = addUnavailableNode(dftBE); @@ -116,10 +118,18 @@ namespace storm { builder.addOutputArc(tActive, unavailableNode); builder.addOutputArc(tPassive, unavailableNode); } + + builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); + builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); + builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); + builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); + } template void DftToGspnTransformator::drawAND(std::shared_ptr const> dftAnd, bool isRepresentative) { + double xcenter = 10.0; + double ycenter = 20.0; uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED); assert(failedNodes.size() == dftAnd->id()); failedNodes.push_back(nodeFailed); @@ -142,6 +152,9 @@ namespace storm { builder.addOutputArc(tAndFailed, failedNodes[child->id()]); } + builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); + builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); + } template diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 19f598c17..ce0d47d44 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -376,6 +376,20 @@ namespace storm { return result; } + + void GSPN::setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layout) const { + placeLayout[placeId] = layout; + } + void GSPN::setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layout) const { + transitionLayout[transitionId] = layout; + } + + void GSPN::setPlaceLayoutInfo(std::map const& placeLayout) const { + this->placeLayout = placeLayout; + } + void GSPN::setTransitionLayoutInfo(std::map const& transitionLayout) const { + this->transitionLayout = transitionLayout; + } void GSPN::toPnpro(std::ostream &stream) const { auto space = " "; @@ -390,8 +404,14 @@ namespace storm { for (auto& place : places) { stream << space3 << " 0) { + stream << "x=\"" << placeLayout.at(place.getID()).x << "\" "; + stream << "y=\"" << placeLayout.at(place.getID()).y << "\" "; + } else { + stream << "x=\"" << x << "\" "; + stream << "y=\"1\" "; + + } stream << "/>" << std::endl; x = x + 3; } @@ -400,8 +420,14 @@ namespace storm { stream << space3 << " 0) { + stream << "x=\"" << transitionLayout.at(trans.getID()).x << "\" "; + stream << "y=\"" << transitionLayout.at(trans.getID()).y << "\" "; + } else { + stream << "x=\"" << x << "\" "; + stream << "y=\"4\" "; + + } stream << "/>" << std::endl; x = x + 3; } @@ -409,8 +435,13 @@ namespace storm { stream << space3 << " 0) { + stream << "x=\"" << transitionLayout.at(trans.getID()).x << "\" "; + stream << "y=\"" << transitionLayout.at(trans.getID()).y << "\" "; + } else { + stream << "x=\"" << x << "\" "; + stream << "y=\"4\" "; + } stream << "/>" << std::endl; x = x + 3; } diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h index b58a6adc5..947769af3 100644 --- a/src/storm-gspn/storage/gspn/GSPN.h +++ b/src/storm-gspn/storage/gspn/GSPN.h @@ -11,6 +11,7 @@ #include "storm-gspn/storage/gspn/Place.h" #include "storm-gspn/storage/gspn/TimedTransition.h" #include "storm-gspn/storage/gspn/TransitionPartition.h" +#include "storm-gspn/storage/gspn/PlacementInfo.h" namespace storm { namespace gspn { @@ -140,7 +141,13 @@ namespace storm { * Set Capacities according to name->capacity map. */ void setCapacities(std::unordered_map const& mapping); - + + void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layout) const; + void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layout) const; + void setPlaceLayoutInfo(std::map const& placeLayout) const; + void setTransitionLayoutInfo(std::map const& transitionLayout) const; + + /*! * Performe some checks * - testPlaces() @@ -191,6 +198,10 @@ namespace storm { std::vector partitions; + mutable std::map placeLayout; + mutable std::map transitionLayout; + + }; } } diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index fa81444c3..e0bbd76fd 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -23,6 +23,15 @@ namespace storm { places.push_back(place); return newId; } + + + void GspnBuilder::setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layoutInfo) { + placeLayout[placeId] = layoutInfo; + } + + void GspnBuilder::setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo) { + transitionLayout[transitionId] = layoutInfo; + } uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight, std::string const& name) { auto trans = storm::gspn::ImmediateTransition(); @@ -164,7 +173,10 @@ namespace storm { } std::reverse(orderedPartitions.begin(), orderedPartitions.end()); - return new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions); + GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions); + result->setTransitionLayoutInfo(transitionLayout); + result->setPlaceLayoutInfo(placeLayout); + return result; } } } diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h index 2f63ba719..79fb2e712 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.h +++ b/src/storm-gspn/storage/gspn/GspnBuilder.h @@ -20,29 +20,32 @@ namespace storm { /** * Add a place to the gspn. - * @param id The id must be unique for the gspn. * @param name The name must be unique for the gspn. * @param capacity The capacity is the limit of tokens in the place. * A capacity of -1 indicates an unbounded place. * @param initialTokens The number of inital tokens in the place. */ uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0, std::string const& name = ""); + + void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layoutInfo); /** * Adds an immediate transition to the gspn. - * @param id The id must be unique for the gspn. * @param priority The priority for the transtion. * @param weight The weight for the transition. */ uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, WeightType const& weight = 0, std::string const& name = ""); - + + /** * Adds an timed transition to the gspn. - * @param id The name id be unique for the gspn. * @param priority The priority for the transtion. * @param weight The weight for the transition. */ uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, std::string const& name = ""); + + void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo); + /** * Adds an new input arc from a place to an transition. @@ -112,6 +115,9 @@ namespace storm { // set containing all places std::vector places; + + std::map placeLayout; + std::map transitionLayout; }; } } diff --git a/src/storm-gspn/storage/gspn/PlacementInfo.h b/src/storm-gspn/storage/gspn/PlacementInfo.h new file mode 100644 index 000000000..e59218686 --- /dev/null +++ b/src/storm-gspn/storage/gspn/PlacementInfo.h @@ -0,0 +1,17 @@ +#pragma once + +namespace storm { + namespace gspn { + struct LayoutInfo { + LayoutInfo() {}; + LayoutInfo(double x, double y, double rotation = 0.0) : x(x), y(y), rotation(rotation) {}; + + // x location + double x = 0.0; + // y location + double y = 0.0; + // degrees + double rotation = 0.0; + }; + } +} \ No newline at end of file diff --git a/src/storm-gspn/storage/gspn/Transition.h b/src/storm-gspn/storage/gspn/Transition.h index d61affaea..9deab2fb0 100644 --- a/src/storm-gspn/storage/gspn/Transition.h +++ b/src/storm-gspn/storage/gspn/Transition.h @@ -168,6 +168,9 @@ namespace storm { void setID(uint64_t const& id) { this->id = id; } + + + uint64_t getID() const { return id; } private: // maps place ids connected to this transition with an input arc to the corresponding multiplicity