Make elements for DC propagation choosable in GSPN transformation

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();

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");
 				

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.