Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft

Former-commit-id: a02c42a89c

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

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

src/storage/dft/DFTElements.h

@@ -728,60 +728,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> {

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> {
+            
+        };
+        
+    }
+}