Integrated results of FDEP conflict search in DFT state space generation

src/storm-dft-cli/storm-dft.cpp

@@ -32,7 +32,6 @@ void processOptions() {
 
     auto dftTransformator = storm::transformations::dft::DftTransformator<ValueType>();
 
-
     if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given.");
     }
@@ -92,17 +91,6 @@ void processOptions() {
     }
 
 #ifdef STORM_HAVE_Z3
-    if(debug.isTestSet()){
-        dft->setDynamicBehaviorInfo();
-        for(size_t i = 0; i < dft->nrElements(); ++i){
-            if(dft->getDynamicBehavior()[i]) {
-                STORM_LOG_DEBUG("Element " << dft->getElement(i)->name() << " has dynamic behavior");
-            } else {
-                STORM_LOG_DEBUG("Element " << dft->getElement(i)->name() << " has static behavior");
-            }
-        }
-    }
-
     if (faultTreeSettings.solveWithSMT()) {
         dft = dftTransformator.transformUniqueFailedBe(*dft);
         if (dft->getDependencies().size() > 0) {
@@ -113,8 +101,18 @@ void processOptions() {
         STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
         // Set dynamic behavior vector
         dft->setDynamicBehaviorInfo();
-        storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet());
-        return;
+        auto smtResults = storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet());
+        // Set the conflict map of the dft
+        std::set<size_t> conflict_set;
+        for (auto conflict : smtResults.fdepConflicts) {
+            conflict_set.insert(size_t(conflict.first));
+            conflict_set.insert(size_t(conflict.second));
+        }
+        for (size_t depId : dft->getDependencies()) {
+            if (!conflict_set.count(depId)) {
+                dft->setDependencyNotInConflict(depId);
+            }
+        }
     }
 #endif
 
@@ -215,7 +213,6 @@ void processOptions() {
         }
     }
 
-
     // Analyze DFT
     // TODO allow building of state space even without properties
     if (props.empty()) {

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -76,14 +76,8 @@ namespace storm {
             Choice<ValueType, StateType> choice(0, !exploreDependencies);
 
             // Let BE fail
-            bool isFirst = true;
             while (!state->getFailableElements().isEnd()) {
                 //TODO outside
-                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && exploreDependencies && !isFirst) {
-                    // We discard further exploration as we already chose one dependent event
-                    break;
-                }
-                isFirst = false;
 
                 // Construct new state as copy from original one
                 DFTStatePointer newState = state->copy();
@@ -167,7 +161,7 @@ namespace storm {
 
                 // Set transitions
                 if (exploreDependencies) {
-                    // Failure is due to dependency -> add non-deterministic choice
+                    // Failure is due to dependency -> add non-deterministic choice if necessary
                     ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability();
                     choice.addProbability(newStateId, probability);
                     STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability);

src/storm-dft/storage/dft/DFT.cpp

@@ -53,6 +53,7 @@ namespace storm {
                     }
                 } else if (elem->isDependency()) {
                     mDependencies.push_back(elem->id());
+                    mDependencyInConflict.insert(std::make_pair(elem->id(), true));
                 }
             }
 

src/storm-dft/storage/dft/DFT.h

@@ -68,6 +68,7 @@ namespace storm {
             std::vector<std::vector<size_t>> mSymmetries;
             std::map<size_t, DFTLayoutInfo> mLayoutInfo;
             std::vector<bool> mDynamicBehavior;
+            std::map<size_t, bool> mDependencyInConflict;
 
         public:
             DFT(DFTElementVector const &elements, DFTElementPointer const &tle);
@@ -132,6 +133,17 @@ namespace storm {
                 }
             }
 
+            bool isDependencyInConflict(size_t id) const {
+                STORM_LOG_ASSERT(isDependency(id), "Not a dependency.");
+                return mDependencyInConflict.at(id);
+            }
+
+
+            void setDependencyNotInConflict(size_t id) {
+                STORM_LOG_ASSERT(isDependency(id), "Not a dependency.");
+                mDependencyInConflict.at(id) = false;
+            }
+            
             std::vector<size_t> const& getDependencies() const {
                 return mDependencies;
             }

src/storm-dft/storage/dft/DFTState.cpp

@@ -82,7 +82,7 @@ namespace storm {
                 STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match.");
                 assert(dependency->dependentEvents().size() == 1);
                 if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
-                    failableElements.addDependency(dependencyId);
+                    failableElements.addDependency(dependency->id(), mDft.isDependencyInConflict(dependency->id()));
                     STORM_LOG_TRACE("New dependency failure: " << *dependency);
                 }
             }
@@ -243,7 +243,7 @@ namespace storm {
                     // Check if restriction prevents failure of dependent event
                     if (!isEventDisabledViaRestriction(dependency->dependentEvents()[0]->id())) {
                         // Add dependency as possible failure
-                        failableElements.addDependency(dependency->id());
+                        failableElements.addDependency(dependency->id(), mDft.isDependencyInConflict(dependency->id()));
                         STORM_LOG_TRACE("New dependency failure: " << *dependency);
                         addedFailableDependency = true;
                     }

src/storm-dft/storage/dft/DFTState.h

@@ -33,9 +33,18 @@ namespace storm {
                     currentlyFailableBE.set(id);
                 }
 
-                void addDependency(size_t id) {
-                    if (std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id) == mFailableDependencies.end()) {
-                        mFailableDependencies.push_back(id);
+                void addDependency(size_t id, bool isConflicting) {
+                    if (isConflicting) {
+                        if (std::find(mFailableConflictingDependencies.begin(), mFailableConflictingDependencies.end(),
+                                      id) == mFailableConflictingDependencies.end()) {
+                            mFailableConflictingDependencies.push_back(id);
+                        }
+                    } else {
+                        if (std::find(mFailableNonconflictingDependencies.begin(),
+                                      mFailableNonconflictingDependencies.end(), id) ==
+                            mFailableNonconflictingDependencies.end()) {
+                            mFailableNonconflictingDependencies.push_back(id);
+                        }
                     }
                 }
 
@@ -44,21 +53,36 @@ namespace storm {
                 }
 
                 void removeDependency(size_t id) {
-                    auto it = std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id);
-                    if (it != mFailableDependencies.end()) {
-                        mFailableDependencies.erase(it);
+                    auto it1 = std::find(mFailableConflictingDependencies.begin(),
+                                         mFailableConflictingDependencies.end(), id);
+                    if (it1 != mFailableConflictingDependencies.end()) {
+                        mFailableConflictingDependencies.erase(it1);
+                        return;
+                    }
+                    auto it2 = std::find(mFailableNonconflictingDependencies.begin(),
+                                         mFailableNonconflictingDependencies.end(), id);
+                    if (it2 != mFailableNonconflictingDependencies.end()) {
+                        mFailableNonconflictingDependencies.erase(it2);
+                        return;
                     }
                 }
 
                 void clear() {
                     currentlyFailableBE.clear();
-                    mFailableDependencies.clear();
+                    mFailableConflictingDependencies.clear();
+                    mFailableNonconflictingDependencies.clear();
                 }
 
                 void init(bool dependency) const {
                     this->dependency = dependency;
                     if (this->dependency) {
-                        itDep = mFailableDependencies.begin();
+                        if (!mFailableNonconflictingDependencies.empty()) {
+                            itDep = mFailableNonconflictingDependencies.begin();
+                            conflicting = false;
+                        } else {
+                            itDep = mFailableConflictingDependencies.begin();
+                            conflicting = true;
+                        }
                     } else {
                         it = currentlyFailableBE.begin();
                     }
@@ -77,7 +101,12 @@ namespace storm {
 
                 bool isEnd() const {
                     if (dependency) {
-                        return itDep == mFailableDependencies.end();
+                        if (!conflicting) {
+                            // If we are handling the non-conflicting FDEPs, end after the first element
+                            return itDep != mFailableNonconflictingDependencies.begin();
+                        } else {
+                            return itDep == mFailableConflictingDependencies.end();
+                        }
                     } else {
                         return it == currentlyFailableBE.end();
                     }
@@ -96,7 +125,7 @@ namespace storm {
                 };
 
                 bool hasDependencies() const {
-                    return !mFailableDependencies.empty();
+                    return !mFailableConflictingDependencies.empty() || !mFailableNonconflictingDependencies.empty();
                 }
 
                 bool hasBEs() const {
@@ -112,9 +141,11 @@ namespace storm {
                 }
 
                 mutable bool dependency;
+                mutable bool conflicting;
 
                 storm::storage::BitVector currentlyFailableBE;
-                std::vector<size_t> mFailableDependencies;
+                std::vector<size_t> mFailableConflictingDependencies;
+                std::vector<size_t> mFailableNonconflictingDependencies;
                 std::set<size_t> remainingRelevantEvents;
 
                 mutable storm::storage::BitVector::const_iterator it;