Added priorities to GSPN transformation

src/storm-dft/api/storm-dft.cpp

@@ -45,7 +45,8 @@ namespace storm {
 
             // Transform to GSPN
             storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
-            gspnTransformator.transform(dontCareElements, smart, mergeDCFailed);
+            auto priorities = gspnTransformator.computePriorities();
+            gspnTransformator.transform(priorities, dontCareElements, smart, mergeDCFailed);
             storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
             uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
 

src/storm-dft/transformations/DftToGspnTransformator.cpp

@@ -17,8 +17,9 @@ namespace storm {
             }
 
             template<typename ValueType>
-            void DftToGspnTransformator<ValueType>::transform(std::set<uint64_t> const &dontCareElements, bool smart,
+            void DftToGspnTransformator<ValueType>::transform(std::map<uint64_t, uint64_t> const &priorities, std::set<uint64_t> const &dontCareElements, bool smart,
                                                               bool mergeDCFailed) {
+                this->priorities = priorities;
                 this->dontCareElements = dontCareElements;
                 this->smart = smart;
                 this->mergedDCFailed = false;//mergeDCFailed;
@@ -31,10 +32,20 @@ namespace storm {
                 // TODO
             }
 
+            template<typename ValueType>
+            std::map<uint64_t, uint64_t> DftToGspnTransformator<ValueType>::computePriorities() {
+                std::map<uint64_t, uint64_t> priorities;
+                for (std::size_t i = 0; i < mDft.nrElements(); i++) {
+                    // Give all elements the same priority
+                    priorities[i] = 1;
+                }
+                return priorities;
+            }
+
+
             template<typename ValueType>
             uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() {
-                STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(),
-                                 "Failed place for top level element does not exist.");
+                STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(), "Failed place for top level element does not exist.");
                 return failedPlaces.at(mDft.getTopLevelIndex());
             }
 

src/storm-dft/transformations/DftToGspnTransformator.h

@@ -25,13 +25,19 @@ namespace storm {
                 /*!
                  * Transform the DFT to a GSPN.
                  *
+                 * @param priorities GSPN transition priorities to use for each DFT element.
                  * @param dontCareElements Set of DFT elements which should have Don't Care propagation.
                  * @param smart Flag indicating if smart semantics should be used.
                  *              Smart semantics will only generate necessary parts of the GSPNs.
                  * @param mergeDCFailed Flag indicating if Don't Care places and Failed places should be merged.
                  */
-                void
-                transform(std::set<uint64_t> const &dontCareElements, bool smart = true, bool mergeDCFailed = true);
+                void transform(std::map<uint64_t, uint64_t> const &priorities, std::set<uint64_t> const &dontCareElements, bool smart = true, bool mergeDCFailed = true);
+
+                /*!
+                 * Compute priorities used for GSPN transformation.
+                 * @return Priority mapping.
+                 */
+                std::map<uint64_t, uint64_t> computePriorities();
 
                 /*!
                  * Extract Gspn by building
@@ -219,6 +225,8 @@ namespace storm {
                 bool mergedDCFailed;
                 // Set of DFT elements which should have Don't Care propagation.
                 std::set<uint64_t> dontCareElements;
+                // Map from DFT elements to their GSPN priorities
+                std::map<uint64_t, uint64_t> priorities;
 
                 // Interface places for DFT elements
                 std::vector<uint64_t> failedPlaces;