diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3aa121a0a..60fbadab9 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -38,6 +38,7 @@ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SO
file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp)
file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp)
+file(GLOB STORM_STORAGE_DFT_ELEMENTS_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp)
@@ -94,6 +95,7 @@ source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES})
source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES})
source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES})
source_group(storage\\dft FILES ${STORM_STORAGE_DFT_FILES})
+source_group(storage\\dft\\elements FILES ${STORM_STORAGE_DFT_ELEMENTS_FILES})
source_group(utility FILES ${STORM_UTILITY_FILES})
# Add custom additional include or link directories
diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h
index a32745cdf..d4bf3bfc2 100644
--- a/src/storage/dft/DFTElementType.h
+++ b/src/storage/dft/DFTElementType.h
@@ -4,20 +4,20 @@
namespace storm {
namespace storage {
- enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQAND = 11};
+ enum class DFTElementType : int {AND = 0, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQ = 11, MUTEX=12};
inline bool isGateType(DFTElementType const& tp) {
switch(tp) {
case DFTElementType::AND:
- case DFTElementType::COUNTING:
case DFTElementType::OR:
case DFTElementType::VOT:
case DFTElementType::PAND:
case DFTElementType::SPARE:
case DFTElementType::POR:
- case DFTElementType::SEQAND:
return true;
+ case DFTElementType::SEQ:
+ case DFTElementType::MUTEX:
case DFTElementType::BE:
case DFTElementType::CONSTF:
case DFTElementType::CONSTS:
@@ -40,7 +40,6 @@ namespace storm {
case DFTElementType::POR:
case DFTElementType::SPARE:
case DFTElementType::PAND:
- case DFTElementType::SEQAND:
return false;
default:
assert(false);
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 11fc31948..c51e180c7 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -726,60 +726,6 @@ namespace storm {
- template<typename ValueType>
- class DFTSeqAnd : public DFTGate<ValueType> {
-
- public:
- DFTSeqAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- if(!state.hasFailed(this->mId)) {
- bool childOperationalBefore = false;
- for(auto const& child : this->mChildren)
- {
- if(!state.hasFailed(child->id())) {
- childOperationalBefore = true;
- }
- else {
- if(childOperationalBefore) {
- state.markAsInvalid();
- return;
- }
- }
- }
- if(!childOperationalBefore) {
- fail(state, queues);
- }
-
- }
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
- assert(hasFailsafeChild(state));
- if(state.isOperational(this->mId)) {
- failsafe(state, queues);
- //return true;
- }
- //return false;
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::SEQAND;
- }
-
- std::string typestring() const override {
- return "SEQAND";
- }
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd<ValueType> const& gate) {
- return os << gate.toString();
- }
-
-
template<typename ValueType>
class DFTPand : public DFTGate<ValueType> {
diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h
new file mode 100644
index 000000000..8bd586deb
--- /dev/null
+++ b/src/storage/dft/elements/DFTRestriction.h
@@ -0,0 +1,13 @@
+#pragma once
+
+#include "../DFTElements.h"
+
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTRestriction : public DFTElement<ValueType> {
+
+ };
+
+ }
+}
\ No newline at end of file