diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 117ee9c43..01271e2c5 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -32,7 +32,6 @@ void processOptions() { auto dftTransformator = storm::transformations::dft::DftTransformator(); - 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 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()) { diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index f4af34ed1..bfbc870ba 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -76,14 +76,8 @@ namespace storm { Choice choice(0, !exploreDependencies); // Let BE fail - bool isFirst = true; while (!state->getFailableElements().isEnd()) { //TODO outside - if (storm::settings::getModule().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); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 611a9c5d9..65beab71b 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/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)); } } diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 2133a54ab..c06af7da4 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -68,6 +68,7 @@ namespace storm { std::vector> mSymmetries; std::map mLayoutInfo; std::vector mDynamicBehavior; + std::map mDependencyInConflict; public: DFT(DFTElementVector const &elements, DFTElementPointer const &tle); @@ -131,6 +132,17 @@ namespace storm { return mSpareModules.find(representativeId)->second; } } + + 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 const& getDependencies() const { return mDependencies; diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index be66bc2a0..887446a1d 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/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; } diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index fd911b355..2800ed6c8 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/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 mFailableDependencies; + std::vector mFailableConflictingDependencies; + std::vector mFailableNonconflictingDependencies; std::set remainingRelevantEvents; mutable storm::storage::BitVector::const_iterator it;