diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp
index 3c856407b..fce5d7962 100644
--- a/src/storm-dft/builder/DFTBuilder.cpp
+++ b/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.");
diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp
index bf1dced78..8d44637f9 100644
--- a/src/storm-dft/parser/DFTGalileoParser.cpp
+++ b/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>());
diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp
index 7975a0d5b..96eeeb762 100644
--- a/src/storm-dft/parser/DFTJsonParser.cpp
+++ b/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") {
diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h
index 3173446fb..36d671703 100644
--- a/src/storm-dft/storage/dft/DFTElements.h
+++ b/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"
diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp
index 2eb811095..9ff66615e 100644
--- a/src/storm-dft/storage/dft/DftJsonExporter.cpp
+++ b/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;
diff --git a/src/storm-dft/storage/dft/elements/DFTMutex.h b/src/storm-dft/storage/dft/elements/DFTMutex.h
new file mode 100644
index 000000000..cbc18a69b
--- /dev/null
+++ b/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;
+ }
+ };
+
+ }
+}
diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h
index b83ba44f7..92c9a69ec 100644
--- a/src/storm-dft/storage/dft/elements/DFTRestriction.h
+++ b/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;
- }
- };
-
}
}
diff --git a/src/storm-dft/storage/dft/elements/DFTSeq.h b/src/storm-dft/storage/dft/elements/DFTSeq.h
new file mode 100644
index 000000000..8cef64e21
--- /dev/null
+++ b/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;
+ }
+ };
+
+ }
+}