From 4fb3f68a948a85b8005adade0993ffed1806ab1e Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 28 Sep 2018 11:52:57 +0200
Subject: [PATCH] Added inhibitor arcs for spare, fixing boundedness with
 merged places + TODO Dependency priority fixing

---
 src/storm-dft/transformations/DftToGspnTransformator.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 243f69938..51a20dc03 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -92,7 +92,7 @@ namespace storm {
                     // Define a running variable for the current priority
                     // Initialize it with an offset for the DC priorities + first interval length as prios give upper interval limit
                     u_int64_t currentPrio = mDft.nrElements() + priorityIntervalLength;
-
+                    //TODO Dependencies have to have same priority
                     for (std::list<size_t>::iterator it = elementList.begin(); it != elementList.end(); ++it) {
                         priorities[*it] = currentPrio;
                         currentPrio += priorityIntervalLength;
@@ -963,6 +963,8 @@ namespace storm {
                 // Set arcs to failed
                 builder.addOutputArc(tNextConsiders.back(), failedPlace);
                 builder.addOutputArc(tNextClaims.back(), failedPlace);
+                builder.addInhibitionArc(failedPlace, tNextConsiders.back());
+                builder.addInhibitionArc(failedPlace, tNextClaims.back());
 
                 // Don't Care Mechanism
                 if (dontCareElements.count(dftSpare->id())) {