Added support for MUTEX (but without DC support)

src/storm-dft/builder/DFTBuilder.cpp

@@ -137,7 +137,7 @@ namespace storm {
         template<typename ValueType>
         bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
             if (children.size() <= 1) {
-                STORM_LOG_ERROR("Sequence enforcers require at least two children");
+                STORM_LOG_ERROR("Restrictions require at least two children");
             }
             if (nameInUse(name)) {
                 STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
@@ -149,8 +149,7 @@ namespace storm {
                     restr = std::make_shared<storm::storage::DFTSeq<ValueType>>(mNextId++, name);
                     break;
                 case storm::storage::DFTElementType::MUTEX:
-                    // TODO notice that mutex state generation support is lacking anyway, as DONT CARE propagation would be broken for this.
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
+                    restr = std::make_shared<storm::storage::DFTMutex<ValueType>>(mNextId++, name);
                     break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known.");

src/storm-dft/parser/DFTGalileoParser.cpp

@@ -137,6 +137,8 @@ namespace storm {
                             success = builder.addSpareElement(name, childNames);
                         } else if (type == "seq") {
                             success = builder.addSequenceEnforcer(name, childNames);
+                        } else if (type == "mutex") {
+                            success = builder.addMutex(name, childNames);
                         } else if (type == "fdep") {
                             STORM_LOG_THROW(childNames.size() >= 2, storm::exceptions::WrongFormatException, "FDEP gate needs at least two children in line " << lineNo << ".");
                             success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>());

src/storm-dft/parser/DFTJsonParser.cpp

@@ -88,6 +88,8 @@ namespace storm {
                     success = builder.addSpareElement(name, childNames);
                 } else if (type == "seq") {
                     success = builder.addSequenceEnforcer(name, childNames);
+                } else if (type == "mutex") {
+                    success = builder.addMutex(name, childNames);
                 } else if (type == "fdep") {
                     success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>());
                 } else if (type == "pdep") {

src/storm-dft/storage/dft/DFTElements.h

@@ -4,9 +4,10 @@
 #include "storm-dft/storage/dft/elements/BEConst.h"
 #include "storm-dft/storage/dft/elements/DFTAnd.h"
 #include "storm-dft/storage/dft/elements/DFTDependency.h"
+#include "storm-dft/storage/dft/elements/DFTMutex.h"
 #include "storm-dft/storage/dft/elements/DFTOr.h"
 #include "storm-dft/storage/dft/elements/DFTPand.h"
 #include "storm-dft/storage/dft/elements/DFTPor.h"
-#include "storm-dft/storage/dft/elements/DFTRestriction.h"
+#include "storm-dft/storage/dft/elements/DFTSeq.h"
 #include "storm-dft/storage/dft/elements/DFTSpare.h"
 #include "storm-dft/storage/dft/elements/DFTVot.h"

src/storm-dft/storage/dft/DftJsonExporter.cpp

@@ -61,10 +61,11 @@ namespace storm {
                     nodeData["voting"] = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element)->threshold();
                 }
             } else if (element->isRestriction()) {
+                // TODO use same method for gates and restrictions
                 // Set children for restriction
-                auto seq = std::static_pointer_cast<storm::storage::DFTRestriction<ValueType> const>(element);
+                auto restriction = std::static_pointer_cast<storm::storage::DFTRestriction<ValueType> const>(element);
                 std::vector<std::string> children;
-                for (DFTElementPointer const& child : seq->children()) {
+                for (DFTElementPointer const& child : restriction->children()) {
                     children.push_back(std::to_string(child->id()));
                 }
                 nodeData["children"] = children;

src/storm-dft/storage/dft/elements/DFTMutex.h

@@ -0,0 +1,61 @@
+#pragma once
+
+#include "DFTRestriction.h"
+
+namespace storm {
+    namespace storage {
+
+        /*!
+         * Mutex restriction (MUTEX).
+         * Only one of the children can fail.
+         * A child which has failed prevents the failure of all other children.
+         */
+        template<typename ValueType>
+        class DFTMutex : public DFTRestriction<ValueType> {
+
+        public:
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param children Children.
+             */
+            DFTMutex(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTRestriction<ValueType>(id, name, children) {
+                // Intentionally left empty.
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::MUTEX;
+            }
+
+            bool isSeqEnforcer() const override {
+                return true;
+            }
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished.");
+                bool childFailed = false;
+                for (auto const& child : this->children()) {
+                    if (state.hasFailed(child->id())) {
+                        if (childFailed) {
+                            // Two children have failed
+                            this->fail(state, queues);
+                            return;
+                        } else {
+                            childFailed = true;
+                        }
+                    }
+                }
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+            }
+
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                // Actually, it doesnt matter what we return here..
+                return false;
+            }
+        };
+
+    }
+}

src/storm-dft/storage/dft/elements/DFTRestriction.h

@@ -61,70 +61,20 @@ namespace storm {
                 // Do nothing
             }
 
-            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 return false;
             }
 
 
         protected:
-            void fail(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+            void fail(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 state.markAsInvalid();
             }
 
-            void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+            void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 // Do nothing
             }
         };
 
-
-        /*!
-         * Sequence enforcer (SEQ).
-         * All children can only fail in order from first to last child.
-         * A child which has not failed yet prevents the failure of all children to the right of it.
-         */
-        template<typename ValueType>
-        class DFTSeq : public DFTRestriction<ValueType> {
-
-        public:
-            /*!
-             * Constructor.
-             * @param id Id.
-             * @param name Name.
-             * @param children Children.
-             */
-            DFTSeq(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const&children = {}) : DFTRestriction<ValueType>(id, name, children) {
-                // Intentionally left empty.
-            }
-
-            DFTElementType type() const override {
-                return DFTElementType::SEQ;
-            }
-
-            bool isSeqEnforcer() const override {
-                return true;
-            }
-
-            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
-                STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished.");
-                bool childOperationalBefore = false;
-                for (auto const& child : this->children()) {
-                    if (!state.hasFailed(child->id())) {
-                        childOperationalBefore = true;
-                    } else if (childOperationalBefore && state.hasFailed(child->id())) {
-                        this->fail(state, queues);
-                        return;
-                    }
-                }
-            }
-
-            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
-            }
-
-            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
-                // Actually, it doesnt matter what we return here..
-                return false;
-            }
-        };
-
     }
 }

src/storm-dft/storage/dft/elements/DFTSeq.h

@@ -0,0 +1,59 @@
+#pragma once
+
+#include "DFTRestriction.h"
+
+namespace storm {
+    namespace storage {
+
+        /*!
+         * Sequence enforcer (SEQ).
+         * All children can only fail in order from first to last child.
+         * A child which has not failed yet prevents the failure of all children to the right of it.
+         */
+        template<typename ValueType>
+        class DFTSeq : public DFTRestriction<ValueType> {
+
+        public:
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param children Children.
+             */
+            DFTSeq(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTRestriction<ValueType>(id, name, children) {
+                // Intentionally left empty.
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::SEQ;
+            }
+
+            bool isSeqEnforcer() const override {
+                return true;
+            }
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished.");
+                bool childOperationalBefore = false;
+                for (auto const& child : this->children()) {
+                    if (!state.hasFailed(child->id())) {
+                        childOperationalBefore = true;
+                    } else if (childOperationalBefore && state.hasFailed(child->id())) {
+                        // Child has failed before left sibling.
+                        this->fail(state, queues);
+                        return;
+                    }
+                }
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+            }
+
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                // Actually, it doesnt matter what we return here..
+                return false;
+            }
+        };
+
+    }
+}