Moved elimination of non-binary dependencies from builder to the DFT transformator

src/storm-dft-cli/storm-dft.cpp

@@ -13,6 +13,7 @@
 #include "storm/utility/initialize.h"
 #include "storm-cli-utilities/cli.h"
 #include "storm-parsers/api/storm-parsers.h"
+#include "storm-dft/transformations/DftTransformator.h"
 
 
 /*!
@@ -29,6 +30,8 @@ void processOptions() {
     storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
     auto const &debug = storm::settings::getModule<storm::settings::modules::DebugSettings>();
 
+    auto dftTransformator = storm::transformations::dft::DftTransformator<ValueType>();
+
 
     if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given.");
@@ -53,11 +56,8 @@ void processOptions() {
         storm::api::exportDFTToJsonFile<ValueType>(*dft, dftIOSettings.getExportJsonFilename());
     }
 
-    if (dftIOSettings.isExportToSmt()) {
-        // Export to smtlib2
-        storm::api::exportDFTToSMT<ValueType>(*dft, dftIOSettings.getExportSmtFilename(), debug.isTestSet());
-        return;
-    }
+    // Eliminate non-binary dependencies
+    dft = dftTransformator.transformBinaryFDEPs(*dft);
 
     // Check well-formedness of DFT
     std::stringstream stream;
@@ -79,6 +79,12 @@ void processOptions() {
         return;
     }
 
+    // SMT
+    if (dftIOSettings.isExportToSmt()) {
+        // Export to smtlib2
+        storm::api::exportDFTToSMT<ValueType>(*dft, dftIOSettings.getExportSmtFilename(), debug.isTestSet());
+        return;
+    }
 
 #ifdef STORM_HAVE_Z3
     if (faultTreeSettings.solveWithSMT()) {

src/storm-dft/builder/DFTBuilder.cpp

@@ -77,7 +77,6 @@ namespace storm {
                         childElement->addOutgoingDependency(elem.first);
                     }
                 }
-                STORM_LOG_ASSERT(!binaryDependencies || dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element.");
                 for (auto& be : dependencies) {
                     elem.first->addDependentEvent(be);
                     be->addIngoingDependency(elem.first);

src/storm-dft/builder/DFTBuilder.h

@@ -43,7 +43,8 @@ namespace storm {
             std::unordered_map<std::string, storm::storage::DFTLayoutInfo> mLayoutInfo;
             
         public:
-            DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) {
+            DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive),
+                                                       porDefaultInclusive(defaultInclusive) {
                 
             }
             
@@ -107,41 +108,13 @@ namespace storm {
                 std::string trigger = children[0];
 
                 //TODO: collect constraints for SMT solving
-                //0 <= probability <= 1
-                if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) {
-                    // Introduce additional element for first capturing the probabilistic dependency
-                    std::string nameAdditional = name + "_additional";
-                    addBasicElementConst(nameAdditional, false);
-                    // First consider probabilistic dependency
-                    addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability);
-                    // Then consider dependencies to the children if probabilistic dependency failed
-                    std::vector<std::string> newChildren = children;
-                    newChildren[0] = nameAdditional;
-                    addDepElement(name, newChildren, storm::utility::one<ValueType>());
-                    return true;
-                } else {
-                    // Add dependencies
-                    if(binaryDependencies) {
-                        for (size_t i = 1; i < children.size(); ++i) {
-                            std::string nameDep = name + "_" + std::to_string(i);
-                            if (nameInUse(nameDep)) {
-                                STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
-                                return false;
-                            }
-                            STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported.");
-                            DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, nameDep, probability);
-                            mElements[element->name()] = element;
-                            mDependencyChildNames[element] = {trigger, children[i]};
-                            mDependencies.push_back(element);
-                        }
-                    } else {
-                        DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, name, probability);
-                        mElements[element->name()] = element;
-                        mDependencyChildNames[element] = children;
-                        mDependencies.push_back(element);
-                    }
-                    return true;
-                }
+                DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++,
+                                                                                                          name,
+                                                                                                          probability);
+                mElements[element->name()] = element;
+                mDependencyChildNames[element] = children;
+                mDependencies.push_back(element);
+                return true;
             }
 
             bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
@@ -268,8 +241,6 @@ namespace storm {
             bool pandDefaultInclusive;
             // If true, the standard gate adders make a pand inclusive, and exclusive otherwise.
             bool porDefaultInclusive;
-
-            bool binaryDependencies;
             
         };
     }

src/storm-dft/parser/DFTGalileoParser.cpp

@@ -32,8 +32,9 @@ namespace storm {
         }
 
         template<typename ValueType>
-        storm::storage::DFT<ValueType> DFTGalileoParser<ValueType>::parseDFT(const std::string& filename, bool defaultInclusive, bool binaryDependencies) {
-            storm::builder::DFTBuilder<ValueType> builder(defaultInclusive, binaryDependencies);
+        storm::storage::DFT<ValueType>
+        DFTGalileoParser<ValueType>::parseDFT(const std::string &filename, bool defaultInclusive) {
+            storm::builder::DFTBuilder<ValueType> builder(defaultInclusive);
             ValueParser<ValueType> valueParser;
             // Regular expression to detect comments
             // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex

src/storm-dft/parser/DFTGalileoParser.h

@@ -26,11 +26,10 @@ namespace storm {
              *
              * @param filename File.
              * @param defaultInclusive Flag indicating if priority gates are inclusive by default.
-             * @param binaryDependencies Flag indicating if dependencies should be converted to binary dependencies.
              *
              * @return DFT.
              */
-            static storm::storage::DFT<ValueType> parseDFT(std::string const& filename, bool defaultInclusive = true, bool binaryDependencies = true);
+            static storm::storage::DFT<ValueType> parseDFT(std::string const &filename, bool defaultInclusive = true);
             
         private:
             /*!

src/storm-dft/transformations/DftTransformator.cpp

@@ -5,16 +5,18 @@ namespace storm {
     namespace transformations {
         namespace dft {
             template<typename ValueType>
-            DftTransformator<ValueType>::DftTransformator(storm::storage::DFT<ValueType> const &dft) : mDft(dft) {}
+            DftTransformator<ValueType>::DftTransformator() {
+            }
 
             template<typename ValueType>
-            storm::storage::DFT<ValueType> DftTransformator<ValueType>::transformUniqueFailedBe() {
-                storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true, false);
+            std::shared_ptr<storm::storage::DFT<ValueType>>
+            DftTransformator<ValueType>::transformUniqueFailedBe(storm::storage::DFT<ValueType> const &dft) {
+                storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true);
                 // NOTE: if probabilities for constant BEs are introduced, change this to vector of tuples (name, prob)
                 std::vector<std::string> failedBEs;
 
-                for (size_t i = 0; i < mDft.nrElements(); ++i) {
-                    std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = mDft.getElement(i);
+                for (size_t i = 0; i < dft.nrElements(); ++i) {
+                    std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
                     switch (element->type()) {
                         case storm::storage::DFTElementType::BE_EXP: {
                             STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]");
@@ -75,13 +77,17 @@ namespace storm {
                             } else {
                                 STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]");
                             }
-                            builder.addDepElement(dep->name(), getChildrenVector(element), dep->probability());
+                            builder.addDepElement(dep->name(), getChildrenVector(dep), dep->probability());
                             break;
                         }
                         case storm::storage::DFTElementType::SEQ:
                             STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]");
                             builder.addSequenceEnforcer(element->name(), getChildrenVector(element));
                             break;
+                        case storm::storage::DFTElementType::MUTEX:
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [MUTEX]");
+                            builder.addMutex(element->name(), getChildrenVector(element));
+                            break;
                         default:
                             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
                                             "DFT type '" << element->type() << "' not known.");
@@ -96,10 +102,135 @@ namespace storm {
                     builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one<ValueType>());
                 }
 
-                builder.setTopLevel(mDft.getTopLevelGate()->name());
+                builder.setTopLevel(dft.getTopLevelGate()->name());
+
+                STORM_LOG_DEBUG("Transformation complete!");
+                return std::make_shared<storm::storage::DFT<ValueType>>(builder.build());
+            }
+
+            template<typename ValueType>
+            std::shared_ptr<storm::storage::DFT<ValueType>>
+            DftTransformator<ValueType>::transformBinaryFDEPs(storm::storage::DFT<ValueType> const &dft) {
+                storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true);
+
+                for (size_t i = 0; i < dft.nrElements(); ++i) {
+                    std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
+                    switch (element->type()) {
+                        case storm::storage::DFTElementType::BE_EXP: {
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]");
+                            auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(
+                                    element);
+                            builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(),
+                                                               be_exp->dormancyFactor());
+                            break;
+                        }
+                        case storm::storage::DFTElementType::BE_CONST: {
+                            auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(
+                                    element);
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const)]");
+                            // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element
+                            builder.addBasicElementConst(be_const->name(), be_const->canFail());
+                            break;
+                        }
+                        case storm::storage::DFTElementType::AND:
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [AND]");
+                            builder.addAndElement(element->name(), getChildrenVector(element));
+                            break;
+                        case storm::storage::DFTElementType::OR:
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [OR]");
+                            builder.addOrElement(element->name(), getChildrenVector(element));
+                            break;
+                        case storm::storage::DFTElementType::VOT: {
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [VOT]");
+                            auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element);
+                            builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot));
+                            break;
+                        }
+                        case storm::storage::DFTElementType::PAND: {
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [PAND]");
+                            auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element);
+                            builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive());
+                            break;
+                        }
+                        case storm::storage::DFTElementType::POR: {
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [POR]");
+                            auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element);
+                            builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive());
+                            break;
+                        }
+                        case storm::storage::DFTElementType::SPARE:
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [SPARE]");
+                            builder.addSpareElement(element->name(), getChildrenVector(element));
+                            break;
+                        case storm::storage::DFTElementType::PDEP: {
+                            auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(
+                                    element);
+                            auto children = getChildrenVector(dep);
+                            if (!storm::utility::isOne(dep->probability())) {
+                                STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]");
+                                if (children.size() > 2) {
+                                    // Introduce additional element for first capturing the probabilistic dependency
+                                    std::string nameAdditional = dep->name() + "_additional";
+                                    builder.addBasicElementConst(nameAdditional, false);
+                                    // First consider probabilistic dependency
+                                    builder.addDepElement(dep->name() + "_pdep", {children.front(), nameAdditional},
+                                                          dep->probability());
+                                    // Then consider dependencies to the children if probabilistic dependency failed
+                                    children.erase(children.begin());
+                                    size_t i = 1;
+                                    for (auto const &child : children) {
+                                        std::string nameDep = dep->name() + "_" + std::to_string(i);
+                                        if (builder.nameInUse(nameDep)) {
+                                            STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists.");
+                                        }
+                                        builder.addDepElement(nameDep, {dep->name() + "_additional", child},
+                                                              storm::utility::one<ValueType>());
+                                        ++i;
+                                    }
+                                } else {
+                                    builder.addDepElement(dep->name(), children, dep->probability());
+                                }
+                            } else {
+                                STORM_LOG_DEBUG("Transform " + element->name() + " [FDEP]");
+                                // Add dependencies
+                                for (size_t i = 1; i < children.size(); ++i) {
+                                    std::string nameDep;
+                                    if (children.size() == 2) {
+                                        nameDep = dep->name();
+                                    } else {
+                                        nameDep = dep->name() + "_" + std::to_string(i);
+                                    }
+                                    if (builder.nameInUse(nameDep)) {
+                                        STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists.");
+                                    }
+                                    STORM_LOG_ASSERT(storm::utility::isOne(dep->probability()) || children.size() == 2,
+                                                     "PDEP with multiple children supported.");
+                                    builder.addDepElement(nameDep, {children[0], children[i]},
+                                                          storm::utility::one<ValueType>());
+                                }
+                            }
+                            break;
+                        }
+                        case storm::storage::DFTElementType::SEQ:
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]");
+                            builder.addSequenceEnforcer(element->name(), getChildrenVector(element));
+                            break;
+                        case storm::storage::DFTElementType::MUTEX:
+                            STORM_LOG_DEBUG("Transform " + element->name() + " [MUTEX]");
+                            builder.addMutex(element->name(), getChildrenVector(element));
+                            break;
+                        default:
+                            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
+                                            "DFT type '" << element->type() << "' not known.");
+                            break;
+                    }
+
+                }
+
+                builder.setTopLevel(dft.getTopLevelGate()->name());
 
                 STORM_LOG_DEBUG("Transformation complete!");
-                return builder.build();
+                return std::make_shared<storm::storage::DFT<ValueType>>(builder.build());
             }
 
             template<typename ValueType>

src/storm-dft/transformations/DftTransformator.h

@@ -18,15 +18,17 @@ namespace storm {
                  *
                  * @param dft DFT
                  */
-                DftTransformator(storm::storage::DFT<ValueType> const &dft);
+                DftTransformator();
 
-                storm::storage::DFT<ValueType> transformUniqueFailedBe();
+                std::shared_ptr<storm::storage::DFT<ValueType>>
+                transformUniqueFailedBe(storm::storage::DFT<ValueType> const &dft);
+
+                std::shared_ptr<storm::storage::DFT<ValueType>>
+                transformBinaryFDEPs(storm::storage::DFT<ValueType> const &dft);
 
             private:
                 std::vector<std::string>
                 getChildrenVector(std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
-
-                storm::storage::DFT<ValueType> const &mDft;
             };
         }
     }

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

@@ -2,6 +2,7 @@
 #include "storm-config.h"
 
 #include "storm-dft/api/storm-dft.h"
+#include "storm-dft/transformations/DftTransformator.h"
 #include "storm-parsers/api/storm-parsers.h"
 
 namespace {
@@ -73,7 +74,9 @@ namespace {
         }
 
         double analyzeMTTF(std::string const& file) {
-            std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
+            storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
+            std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(
+                    *(storm::api::loadDFTGalileoFile<double>(file)));
             EXPECT_TRUE(storm::api::isWellFormed(*dft));
             std::string property = "Tmin=? [F \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
@@ -87,7 +90,9 @@ namespace {
         }
 
         double analyzeReliability(std::string const &file, double bound) {
-            std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
+            storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
+            std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(
+                    *(storm::api::loadDFTGalileoFile<double>(file)));
             EXPECT_TRUE(storm::api::isWellFormed(*dft));
             std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(