Fixed problem with gate as trigger events for dependencies

Former-commit-id: 87cd1115bb

src/builder/ExplicitDFTModelBuilder.cpp

@@ -196,12 +196,14 @@ namespace storm {
                     while (!queues.failurePropagationDone()) {
                         DFTGatePointer next = queues.nextFailurePropagation();
                         next->checkFails(*newState, queues);
+                        newState->updateFailableDependencies(next->id());
                     }
                     
                     while(!queues.restrictionChecksDone()) {
                         DFTRestrictionPointer next = queues.nextRestrictionCheck();
                         next->checkFails(*newState, queues);
-                    } 
+                        newState->updateFailableDependencies(next->id());
+                    }
                     
                     if(newState->isInvalid()) {
                         continue;

src/storage/dft/DFT.cpp

@@ -56,14 +56,24 @@ namespace storm {
                     topModuleSet.insert(elem->id());
                 }
             }
-
+            // Erase spare modules
             for(auto const& module : mSpareModules) {
                 for(auto const& index : module.second) {
                     topModuleSet.erase(index);
                 }
             }
+            // Extend top module and insert those elements which are part of the top module and a spare module
+            mElements[mTopLevelIndex]->extendSpareModule(topModuleSet);
             mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end());
-            
+            // Clear all spare modules where at least one element is also in the top module
+            if (!mTopModule.empty()) {
+                for (auto& module : mSpareModules) {
+                    if (std::find(module.second.begin(), module.second.end(), mTopModule.front()) != module.second.end()) {
+                        module.second.clear();
+                    }
+                }
+            }
+
             //Reserve space for failed spares
             ++mMaxSpareChildCount;
             size_t usageInfoBits = storm::utility::math::uint64_log2(mMaxSpareChildCount) + 1;
@@ -240,6 +250,10 @@ namespace storm {
             std::stringstream stream;
             stream << "[" << mElements[mTopLevelIndex]->id() << "] {";
             std::vector<size_t>::const_iterator it = mTopModule.begin();
+            if (it == mTopModule.end()) {
+                stream << "}" << std::endl;
+                return stream.str();
+            }
             assert(it != mTopModule.end());
             stream << mElements[(*it)]->name();
             ++it;
@@ -251,13 +265,15 @@ namespace storm {
 
             for(auto const& spareModule : mSpareModules) {
                 stream << "[" << mElements[spareModule.first]->name() << "] = {";
-                std::vector<size_t>::const_iterator it = spareModule.second.begin();
+                if (!spareModule.second.empty()) {
-                assert(it != spareModule.second.end());
+                    std::vector<size_t>::const_iterator it = spareModule.second.begin();
-                stream << mElements[(*it)]->name();
+                    assert(it != spareModule.second.end());
-                ++it;
+                    stream << mElements[(*it)]->name();
-                while(it != spareModule.second.end()) {
-                    stream <<  ", " << mElements[(*it)]->name();
                     ++it;
+                    while(it != spareModule.second.end()) {
+                        stream <<  ", " << mElements[(*it)]->name();
+                        ++it;
+                    }
                 }
                 stream << "}" << std::endl;
             }

src/storage/dft/DFTState.cpp

@@ -129,15 +129,16 @@ namespace storm {
 
         template<typename ValueType>
         bool DFTState<ValueType>::updateFailableDependencies(size_t id) {
-            assert(hasFailed(id));
+            if (!hasFailed(id)) {
-            for (size_t i = 0; i < mDft.getDependencies().size(); ++i) {
+                return false;
-                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mDft.getDependencies()[i]);
+            }
-                if (dependency->triggerEvent()->id() == id) {
+            for (auto dependency : mDft.getElement(id)->outgoingDependencies()) {
-                    if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
+                assert(dependency->triggerEvent()->id() == id);
-                        assert(!isFailsafe(dependency->dependentEvent()->id()));
+                if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
-                        mFailableDependencies.push_back(dependency->id());
+                    assert(!isFailsafe(dependency->dependentEvent()->id()));
-                        STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
+                    mFailableDependencies.push_back(dependency->id());
-                    }
+                    STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
                 }
             }
             return nrFailableDependencies() > 0;