From ad8350c68426bd2b4e1cb6d608b5dfc960110645 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 8 May 2018 09:31:07 +0200
Subject: [PATCH] Make elements for DC propagation choosable in GSPN
 transformation

---
 src/storm-dft/api/storm-dft.cpp                | 18 ++++++++++++++++--
 .../transformations/DftToGspnTransformator.cpp |  3 ++-
 .../transformations/DftToGspnTransformator.h   | 13 ++++++++++---
 3 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp
index 91632739e..e05b13210 100644
--- a/src/storm-dft/api/storm-dft.cpp
+++ b/src/storm-dft/api/storm-dft.cpp
@@ -1,5 +1,7 @@
 #include "storm-dft/api/storm-dft.h"
 
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
+
 namespace storm {
     namespace api {
 
@@ -27,13 +29,25 @@ namespace storm {
 
         template<>
         void transformToGSPN(storm::storage::DFT<double> const& dft) {
+            bool smart = true;
+
+            // Set Don't Care elements
+            std::set<uint64_t> dontCareElements;
+            storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
+            if (!ftSettings.isDisableDC()) {
+                // Insert all elements as Don't Care elements
+                for (std::size_t i = 0; i < dft.nrElements(); i++) {
+                    dontCareElements.insert(dft.getElement(i)->id());
+                }
+            }
+
             // Transform to GSPN
             storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
-            bool smart = true;
-            gspnTransformator.transform(smart);
+            gspnTransformator.transform(dontCareElements, smart);
             storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
             uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
 
+            // Export
             storm::api::handleGSPNExportSettings(*gspn);
 
             std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 7a2b0f360..a9b761c52 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -16,7 +16,8 @@ namespace storm {
             }
 
             template <typename ValueType>
-            void DftToGspnTransformator<ValueType>::transform(bool smart) {
+            void DftToGspnTransformator<ValueType>::transform(std::set<uint64_t> const& dontCareElements, bool smart) {
+                this->dontCareElements = dontCareElements;
                 this->smart = smart;
                 builder.setGspnName("DftToGspnTransformation");
 				
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h
index 3d49505c9..22ba384c7 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.h
+++ b/src/storm-dft/transformations/DftToGspnTransformator.h
@@ -24,8 +24,12 @@ namespace storm {
 
                 /*!
                  * Transform the DFT to a GSPN.
+                 *
+                 * @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.
                  */
-                void transform(bool smart = true);
+                void transform(std::set<uint64_t> const& dontCareElements, bool smart = true);
 
                 /*!
                  * Extract Gspn by building
@@ -188,13 +192,16 @@ namespace storm {
                 storm::storage::DFT<ValueType> const& mDft;
                 storm::gspn::GspnBuilder builder;
 
+                // Options
+                bool smart;
+                std::set<uint64_t> dontCareElements;
+
                 // Interface places for DFT elements
                 std::vector<uint64_t> failedPlaces;
                 std::map<uint64_t, uint64_t> unavailablePlaces;
                 std::map<uint64_t, uint64_t> activePlaces;
                 std::map<uint64_t, uint64_t> disabledPlaces;
-                bool smart;
-                
+
                 static constexpr const char* STR_FAILING = "_failing";			// Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.
                 static constexpr const char* STR_FAILED = "_failed";			// Name standard for place which indicates the failure of a gate.
                 static constexpr const char* STR_FAILSAVING = "_failsaving";	// Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate.