From 44082fbc37ba9d0a514c8c8fa485a89bc5178f9a Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 15 Dec 2016 00:08:00 +0100
Subject: [PATCH] pand-ex support

---
 .../DftToGspnTransformator.cpp                | 40 +++++++++++++++----
 1 file changed, 32 insertions(+), 8 deletions(-)

diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 6d22c8184..9028db24c 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -229,20 +229,22 @@ namespace storm {
                 assert(failedNodes.size() == dftPand->id());
                 failedNodes.push_back(nodeFailed);
                 uint64_t unavailableNode = 0;
-                if (isRepresentative) {
+                if (!smart || isRepresentative) {
                     unavailableNode = addUnavailableNode(dftPand);
                 }
                 
+                uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0,  dftPand->name() + STR_FAILING);
+                builder.addInhibitionArc(nodeFailed, tNodeFailed);
+                builder.addOutputArc(tNodeFailed, nodeFailed);
+                if (!smart || isRepresentative) {
+                    builder.addOutputArc(tNodeFailed, nodeFailed);
+                }
+                
+                
                 if(dftPand->isInclusive()) {
                     
                     uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
-                    uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0,  dftPand->name() + STR_FAILING);
-                    builder.addInhibitionArc(nodeFailed, tNodeFailed);
                     builder.addInhibitionArc(nodeFS, tNodeFailed);
-                    builder.addOutputArc(tNodeFailed, nodeFailed);
-                    if (isRepresentative) {
-                        builder.addOutputArc(tNodeFailed, nodeFailed);
-                    }
                     for(auto const& child : dftPand->children()) {
                         builder.addInputArc(failedNodes[child->id()], tNodeFailed);
                         builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
@@ -257,7 +259,29 @@ namespace storm {
                         
                     }
                 } else {
-                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NOt yet implemented");
+                    uint64_t fi = 0;
+                    uint64_t tn = 0;
+                    for(uint64_t j = 0; j < dftPand->nrChildren(); ++j) {
+                        auto const& child = dftPand->children()[j];
+                        if (j > 0) {
+                            builder.addInhibitionArc(failedNodes.at(child->id()), tn);
+                        }
+                        if (j != dftPand->nrChildren() - 1) {
+                            tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j));
+                        } else {
+                            tn = tNodeFailed;
+                        }
+                        builder.addInputArc(failedNodes.at(child->id()), tn);
+                        builder.addOutputArc(tn, failedNodes.at(child->id()));
+                        if (j > 0) {
+                            builder.addInputArc(fi, tn);
+                        }
+                        if (j != dftPand->nrChildren() - 1) {
+                            fi = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(j));
+                            builder.addOutputArc(tn, fi);
+                        }
+                        
+                    }
                 }
             }
 //