From c3770504287a9b46b488a61bafeb7a52d5e96f47 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 8 Dec 2016 13:00:57 +0100
Subject: [PATCH] initial support for partitions

---
 src/storm-gspn/storage/gspn/GSPN.cpp          |  4 +--
 src/storm-gspn/storage/gspn/GSPN.h            |  7 ++--
 src/storm-gspn/storage/gspn/GspnBuilder.cpp   | 36 +++++++++++++++++--
 src/storm-gspn/storage/gspn/GspnBuilder.h     |  2 ++
 .../storage/gspn/TransitionPartition.h        | 18 ++++++++++
 5 files changed, 61 insertions(+), 6 deletions(-)
 create mode 100644 src/storm-gspn/storage/gspn/TransitionPartition.h

diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index 8377f2f8e..6cae21e99 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -27,8 +27,8 @@ namespace storm {
             return tId;
         }
         
-        GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions)
-        : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions)
+        GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions)
+        : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions)
         {
             
         }
diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h
index 17448bc8b..06ee0e788 100644
--- a/src/storm-gspn/storage/gspn/GSPN.h
+++ b/src/storm-gspn/storage/gspn/GSPN.h
@@ -10,6 +10,7 @@
 #include "storm-gspn/storage/gspn/Marking.h"
 #include "storm-gspn/storage/gspn/Place.h"
 #include "storm-gspn/storage/gspn/TimedTransition.h"
+#include "storm-gspn/storage/gspn/TransitionPartition.h"
 
 namespace storm {
     namespace gspn {
@@ -27,7 +28,8 @@ namespace storm {
             typedef double WeightType;
             
             
-            GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions);
+            GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions,
+                 std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions);
             
             /*!
              * Returns the number of places in this gspn.
@@ -176,7 +178,8 @@ namespace storm {
             // set containing all timed transitions
             std::vector<storm::gspn::TimedTransition<RateType>> timedTransitions;
 
-
+            std::vector<storm::gspn::TransitionPartition> partitions;
+            
         };
     }
 }
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
index cbea96b6a..d634c00e9 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
@@ -29,8 +29,27 @@ namespace storm {
             auto newId = GSPN::immediateTransitionIdToTransitionId(immediateTransitions.size());
             trans.setName(name);
             trans.setPriority(priority);
-            trans.setWeight(weight);
             trans.setID(newId);
+            
+            // ensure that the first partition is for the 'general/weighted' transitions
+            if(partitions.count(priority) == 0) {
+                TransitionPartition newPart;
+                newPart.priority = priority;
+                partitions.at(priority).push_back(newPart);
+            }
+            
+            if(storm::utility::isZero(weight)) {
+                trans.setWeight(storm::utility::one<double>());
+                TransitionPartition newPart;
+                newPart.priority = priority;
+                newPart.transitions = {newId};
+                partitions.at(priority).push_back(newPart);
+            } else {
+                trans.setWeight(weight);
+                partitions.at(priority).front().transitions.push_back(newId);
+                
+                
+            }
             immediateTransitions.push_back(trans);
             return newId;
             
@@ -131,7 +150,20 @@ namespace storm {
         
 
         storm::gspn::GSPN* GspnBuilder::buildGspn() const {
-            return new GSPN(gspnName, places, immediateTransitions, timedTransitions);
+            std::vector<TransitionPartition> orderedPartitions;
+            for(auto const& priorityPartitions : partitions) {
+                for (auto const& partition : priorityPartitions.second) {
+                    // sanity check
+                    assert(partition.priority == priorityPartitions.first);
+                    
+                    if(partition.nrTransitions() > 0) {
+                        orderedPartitions.push_back(partition);
+                    }
+                }
+                
+            }
+            
+            return new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions);
         }
     }
 }
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h
index 59f098a82..2f63ba719 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.h
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.h
@@ -102,6 +102,8 @@ namespace storm {
             
             std::string gspnName = "_gspn_";
             
+            std::map<uint64_t, std::vector<storm::gspn::TransitionPartition>> partitions;
+            
             // set containing all immediate transitions
             std::vector<storm::gspn::ImmediateTransition<WeightType>> immediateTransitions;
             
diff --git a/src/storm-gspn/storage/gspn/TransitionPartition.h b/src/storm-gspn/storage/gspn/TransitionPartition.h
new file mode 100644
index 000000000..128a87641
--- /dev/null
+++ b/src/storm-gspn/storage/gspn/TransitionPartition.h
@@ -0,0 +1,18 @@
+#pragma once
+#include <vector>
+
+namespace storm {
+    namespace gspn {
+        
+        struct TransitionPartition {
+            std::vector<uint64_t> transitions;
+            uint64_t priority;
+            
+            
+            uint64_t nrTransitions() const {
+                return transitions.size();
+            }
+        };
+        
+    }
+}
\ No newline at end of file