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

Former-commit-id: 8b34e3ef59

examples/dft/spare8.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" wsp "I" "B";
+"B" wsp "J" "K";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+

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/builder/ExplicitDFTModelBuilder.cpp

@@ -256,7 +256,7 @@ namespace storm {
                             if (mStates.contains(unsuccessfulState->status())) {
                                 // Unsuccessful state already exists
                                 unsuccessfulStateId = mStates.getValue(unsuccessfulState->status());
-                                STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists");
+                                STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " with id " << unsuccessfulStateId << " already exists");
                             } else {
                                 // New unsuccessful state
                                 unsuccessfulState->setId(newIndex++);
@@ -277,16 +277,15 @@ namespace storm {
                         ++rowOffset;
 
                     } else {
-                        // Set failure rate according to usage
-                        bool isUsed = true;
+                        // Set failure rate according to activation
+                        bool isActive = true;
                         if (mDft.hasRepresentant(nextBE->id())) {
-                            DFTElementCPointer representant = mDft.getRepresentant(nextBE->id());
-                            // Used must be checked for the state we are coming from as this state is responsible for the
+                            // Active must be checked for the state we are coming from as this state is responsible for the
                             // rate and not the new state we are going to
-                            isUsed = state->isUsed(representant->id());
+                            isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
                         }
-                        STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
-                        ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
+                        STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isActive ? "active" : "not active"));
+                        ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
                         auto resultFind = outgoingTransitions.find(newStateId);
                         if (resultFind != outgoingTransitions.end()) {
                             // Add to existing transition

src/storage/dft/DFT.cpp

@@ -80,12 +80,6 @@ namespace storm {
             std::queue<size_t> visitQueue;
             std::set<size_t> visited;
             visitQueue.push(subTreeRoots[0]);
-            bool consideredDependencies = false;
-            while (true) {
-                if (consideredDependencies) {
-                    break;
-                }
-                
             stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
             
             // Consider dependencies
@@ -95,8 +89,8 @@ namespace storm {
                 visitQueue.push(dependency->triggerEvent()->id());
                 visitQueue.push(dependency->dependentEvent()->id());
             }
-                consideredDependencies = true;
-            }
+            stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
+            
             assert(stateIndex = mStateVectorSize);
 
             STORM_LOG_TRACE(generationInfo);
@@ -197,10 +191,11 @@ namespace storm {
                 } else {
                     stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id()));
                     if(elem->isSpareGate()) {
-                        if(state->isActiveSpare(elem->id())) {
+                        size_t useId = state->uses(elem->id());
+                        if(state->isActive(useId)) {
                             stream << " actively ";
                         }
-                        stream << " using " << state->uses(elem->id());
+                        stream << " using " << useId;
                     }
                 }
                 stream << std::endl;
@@ -220,10 +215,11 @@ namespace storm {
                     stream << storm::storage::toChar(state->getElementState(elem->id()));
                     if(elem->isSpareGate()) {
                         stream << "[";
-                        if(state->isActiveSpare(elem->id())) {
+                        size_t useId = state->uses(elem->id());
+                        if(state->isActive(useId)) {
                             stream << " actively ";
                         }
-                        stream << "using " << state->uses(elem->id()) << "]";
+                        stream << "using " << useId << "]";
                     }
                 }
             }

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.cpp

@@ -7,18 +7,24 @@ namespace storm {
 
         template<typename ValueType>
         bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
-            if(!state.dontCare(mId) && !hasOutgoingDependencies())
-            {
+            if (state.dontCare(mId)) {
+                return false;
+            }
+            // Check that no outgoing dependencies can be triggered anymore
+            for (DFTDependencyPointer dependency : mOutgoingDependencies) {
+                if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) {
+                    return false;
+                }
+            }
+            // Check that no parent can fail anymore
             for(DFTGatePointer const& parent : mParents) {
                 if(state.isOperational(parent->id())) {
                     return false;
                 }
             }
+
             state.setDontCare(mId);
             return true;
-
-            }
-            return false;
         }
 
         template<typename ValueType>

src/storage/dft/DFTElements.h

@@ -259,6 +259,7 @@ namespace storm {
             virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
             
             virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+                if (!this->isSpareGate()) {
                     DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
                     for( auto const& child : mChildren) {
                         if(elementsInSpareModule.count(child->id()) == 0) {
@@ -267,6 +268,7 @@ namespace storm {
                         }
                     }
                 }
+            }
             
             virtual std::vector<size_t> independentUnit() const override {
                 std::set<size_t> unit = {this->mId};
@@ -350,6 +352,10 @@ namespace storm {
                     }
                 }
                 state.setFailed(this->mId);
+                if (this->isSpareGate()) {
+                    this->finalizeSpare(state);
+                }
+                this->childrenDontCare(state, queues);
             }
 
             void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
@@ -359,12 +365,30 @@ namespace storm {
                     }
                 }
                 state.setFailsafe(this->mId);
+                if (this->isSpareGate()) {
+                    this->finalizeSpare(state);
+                }
+                this->childrenDontCare(state, queues);
             }
 
             void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
                 queues.propagateDontCare(mChildren);
             }
 
+            /**
+             * Finish failed/failsafe spare gate by activating the children and setting the useIndex to zero.
+             * This prevents multiple fail states with different usages or activations.
+             * @param state The current state.
+             */
+            void finalizeSpare(DFTState<ValueType>& state) const {
+                state.setUses(this->mId, 0);
+                for (auto child : this->children()) {
+                    if (!state.isActive(child->id())) {
+                        state.activate(child->id());
+                    }
+                }
+            }
+
             bool hasFailsafeChild(DFTState<ValueType>& state) const {
                 for(auto const& child : mChildren) {
                     if(state.isFailsafe(child->id()))
@@ -726,60 +750,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/DFTState.cpp

@@ -7,7 +7,6 @@ namespace storm {
 
         template<typename ValueType>
         DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo)  {
-            mInactiveSpares = dft.getSpareIndices();
             
             // Initialize uses
             for(size_t id  : mDft.getSpareIndices()) {
@@ -18,12 +17,7 @@ namespace storm {
             }
             
             // Initialize activation
-            this->activate(mDft.getTopLevelIndex());
-            for(auto const& id : mDft.module(mDft.getTopLevelIndex())) {
-                if(mDft.getElement(id)->isSpareGate()) {
-                    propagateActivation(uses(id));
-                }
-            }
+            propagateActivation(mDft.getTopLevelIndex());
 
             std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs();
             mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
@@ -182,29 +176,25 @@ namespace storm {
 
         template<typename ValueType>
         void DFTState<ValueType>::activate(size_t repr) {
-            for(size_t elem : mDft.module(repr)) {
-                if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
-                    mIsCurrentlyFailableBE.push_back(elem);
-                }
-                else if(mDft.getElement(elem)->isSpareGate()) {
-                    assert(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem) != mInactiveSpares.end());
-                    mInactiveSpares.erase(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem));
-                }
-            }
+            size_t activationIndex = mStateGenerationInfo.getSpareActivationIndex(repr);
+            assert(!mStatus[activationIndex]);
+            mStatus.set(activationIndex);
+            propagateActivation(repr);
         }
 
         template<typename ValueType>
-        bool DFTState<ValueType>::isActiveSpare(size_t id) const {
-            assert(mDft.getElement(id)->isSpareGate());
-            return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end());
+        bool DFTState<ValueType>::isActive(size_t id) const {
+            assert(mDft.isRepresentative(id));
+            return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)];
         }
             
         template<typename ValueType>
         void DFTState<ValueType>::propagateActivation(size_t representativeId) {
-            activate(representativeId);
-            for(size_t id : mDft.module(representativeId)) {
-                if(mDft.getElement(id)->isSpareGate()) {
-                    propagateActivation(uses(id));
+            for(size_t elem : mDft.module(representativeId)) {
+                if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
+                    mIsCurrentlyFailableBE.push_back(elem);
+                } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
+                    activate(uses(elem));
                 }
             }
         }
@@ -243,8 +233,8 @@ namespace storm {
                 size_t childId = (*it)->id();
                 if(!hasFailed(childId) && !isUsed(childId)) {
                     setUses(spareId, childId);
-                    if(isActiveSpare(spareId)) {
-                        propagateActivation(childId);
+                    if(isActive(currentlyUses)) {
+                        activate(childId);
                     }
                     return true;
                 }

src/storage/dft/DFTState.h

@@ -26,7 +26,6 @@ namespace storm {
             // Status is bitvector where each element has two bits with the meaning according to DFTElementState
             storm::storage::BitVector mStatus;
             size_t mId;
-            std::vector<size_t> mInactiveSpares;
             std::vector<size_t> mIsCurrentlyFailableBE;
             std::vector<size_t> mFailableDependencies;
             std::vector<size_t> mUsedRepresentants;
@@ -79,9 +78,7 @@ namespace storm {
             
             void activate(size_t repr);
             
-            bool isActiveSpare(size_t id) const;
-            
-            void propagateActivation(size_t representativeId);
+            bool isActive(size_t id) const;
             
             void markAsInvalid() {
                 mValid = false;
@@ -200,6 +197,10 @@ namespace storm {
             friend bool operator==(DFTState const& a, DFTState const& b) {
                 return a.mStatus == b.mStatus;
             }
+            
+        private:
+            void propagateActivation(size_t representativeId);
+
         };
 
     }

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