From 8b1fbca27195110919d4e2a5f31a61628d6d4a6f Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 24 Jan 2018 18:04:53 +0100
Subject: [PATCH] Set priority to 1 for all GSPN transitions

---
 .../transformations/DftToGspnTransformator.cpp       | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 047ce44af..bd8fe53b9 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -433,7 +433,7 @@ namespace storm {
                     // Activate all nodes in spare module
                     uint64_t l = 0;
                     for (uint64_t k : mDft.module(child->id())) {
-                        uint64_t tactive = builder.addImmediateTransition(defaultPriority+1, 0.0, dftSpare->name() + "_activate_" + std::to_string(j) + "_" +  std::to_string(k));
+                        uint64_t tactive = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(j) + "_" +  std::to_string(k));
                         builder.setTransitionLayoutInfo(tactive, storm::gspn::LayoutInfo(xcenter-18.0+(j+l)*3, ycenter-12.0));
                         builder.addInhibitionArc(activeNodes.at(k), tactive);
                         builder.addInputArc(nodeCUC, tactive);
@@ -502,11 +502,11 @@ namespace storm {
                     builder.addOutputArc(t1, flipPlace);
                     
                     builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0));
-                    uint64_t t2 = builder.addImmediateTransition(defaultPriority + 1, dftDependency->probability(), "_win_flip");
+                    uint64_t t2 = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip");
                     builder.addInputArc(flipPlace, t2);
                     builder.addOutputArc(t2, forwardPlace);
                     if (dftDependency->probability() < 1.0) {
-                        uint64_t t3 = builder.addImmediateTransition(defaultPriority + 1, 1 - dftDependency->probability(), "_loose_flip");
+                        uint64_t t3 = builder.addImmediateTransition(defaultPriority, 1 - dftDependency->probability(), "_loose_flip");
                         builder.addInputArc(flipPlace, t3);
                     }
                 } else {
@@ -549,7 +549,7 @@ namespace storm {
                     if (j>0) {
                         builder.addOutputArc(tEnable, nextPlace);
                     }
-                    tEnable = builder.addImmediateTransition(defaultPriority + 1, 0.0, dftSeq->name() + "_unblock_" +child->name());
+                    tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" +child->name());
                     builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter-5.0+j*3.0, ycenter+3.0));
 
                     builder.addInputArc(nextPlace, tEnable);
@@ -589,7 +589,9 @@ namespace storm {
 			template <typename ValueType>
             uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
 			{
-                return mDft.maxRank() - dftElement->rank() + 2;
+                // Temporariliy use one priority for all
+                return defaultPriority;
+                //return mDft.maxRank() - dftElement->rank() + 2;
 			}