From 159890844e6a8fef56b930c2297e034c947fcca2 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 15 Dec 2016 09:57:27 +0100
Subject: [PATCH] Layout for AND and BE

---
 src/storm-dft/parser/DFTJsonParser.cpp        |  7 +++--
 .../DftToGspnTransformator.cpp                | 27 ++++++++++++++-----
 2 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp
index 4bedbe7ac..2a1f3f1ac 100644
--- a/src/storm-dft/parser/DFTJsonParser.cpp
+++ b/src/storm-dft/parser/DFTJsonParser.cpp
@@ -49,7 +49,7 @@ namespace storm {
 
         template<typename ValueType>
         void DFTJsonParser<ValueType>::readFile(const std::string& filename) {
-            std::cout << "Parsing from JSON" << std::endl;
+            STORM_LOG_DEBUG("Parsing from JSON");
 
             std::ifstream file;
             file.exceptions ( std::ifstream::failbit );
@@ -81,8 +81,6 @@ namespace storm {
             std::string toplevelId = nameMapping["1"];
 
             for (auto& element : parsedJson) {
-                std::cout << element << std::endl;
-
                 bool success = true;
                 if (element.at("classes") == "") {
                     continue;
@@ -124,10 +122,11 @@ namespace storm {
                     success = false;
                 }
 
+                // Set layout positions
                 json position = element.at("position");
                 double x = position.at("x");
                 double y = position.at("y");
-                builder.addLayoutInfo(name, x, y);
+                builder.addLayoutInfo(name, x / 10, y / 10);
                 STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'.");
             }
 
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 868ab652c..176ed3254 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -90,9 +90,7 @@ namespace storm {
             
             template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative) {
-                double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
-                double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y;
-				uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
+                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);
                 
@@ -127,7 +125,10 @@ namespace storm {
                     builder.addOutputArc(tActive, unavailableNode);
                     builder.addOutputArc(tPassive, unavailableNode);
                 }
-                
+
+                double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
+                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));
                 builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
@@ -137,8 +138,6 @@ namespace storm {
 			
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative) {
-                double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
-                double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
                 uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED);
                 assert(failedNodes.size() == dftAnd->id());
                 failedNodes.push_back(nodeFailed);
@@ -160,7 +159,10 @@ namespace storm {
                     builder.addInputArc(failedNodes[child->id()], tAndFailed);
                     builder.addOutputArc(tAndFailed, failedNodes[child->id()]);
                 }
-                
+
+                double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
+                double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
+
                 builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
                 builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0));
                 
@@ -171,6 +173,11 @@ namespace storm {
                 uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED);
                 assert(failedNodes.size() == dftOr->id());
                 failedNodes.push_back(nodeFailed);
+
+                double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x;
+                double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y;
+                builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
+
                 uint64_t unavailableNode = 0;
                 if (isRepresentative) {
                     unavailableNode = addUnavailableNode(dftOr);
@@ -188,6 +195,7 @@ namespace storm {
                     builder.addInputArc(failedNodes[child->id()], tNodeFailed);
                     builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
                     ++i;
+                    builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5+i*3, ycenter+3.0));
                 }
 			}
 			
@@ -228,6 +236,11 @@ namespace storm {
                 uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name()  + STR_FAILED);
                 assert(failedNodes.size() == dftPand->id());
                 failedNodes.push_back(nodeFailed);
+
+                double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x;
+                double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y;
+                builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
+
                 uint64_t unavailableNode = 0;
                 if (!smart || isRepresentative) {
                     unavailableNode = addUnavailableNode(dftPand);