diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 1e9a53045..253e0e0a2 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -105,6 +105,7 @@ namespace storm {
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
+ newState->updateFailableInRestrictions(next->id());
}
// Check restrictions
@@ -116,6 +117,7 @@ namespace storm {
DFTRestrictionPointer next = queues.nextRestrictionCheck();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
+ newState->updateFailableInRestrictions(next->id());
}
bool transient = false;
@@ -153,6 +155,7 @@ namespace storm {
// Update failable dependencies
newState->updateFailableDependencies(nextBE->id());
newState->updateDontCareDependencies(nextBE->id());
+ newState->updateFailableInRestrictions(nextBE->id());
// Add new state
newStateId = stateToIdCallback(newState);
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 8ae059104..1aa04eaa6 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -89,11 +89,12 @@ namespace storm {
DFTStateGenerationInfo DFT<ValueType>::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const {
DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount);
- // Generate Pre and Post info for restrictions
+ // Generate Pre and Post info for restrictions, and mutexes
for(auto const& elem : mElements) {
if(!elem->isDependency() && !elem->isRestriction()) {
generationInfo.setRestrictionPreElements(elem->id(), elem->seqRestrictionPres());
generationInfo.setRestrictionPostElements(elem->id(), elem->seqRestrictionPosts());
+ generationInfo.setMutexElements(elem->id(), elem->mutexRestrictionElements());
}
}
diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
index 804068576..778c571b8 100644
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -1,6 +1,7 @@
#include "DFTState.h"
#include "storm-dft/storage/dft/DFTElements.h"
#include "storm-dft/storage/dft/DFT.h"
+#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace storage {
@@ -22,7 +23,12 @@ namespace storm {
// Initialize currently failable BEs
for (size_t id : mDft.nonColdBEs()) {
- failableElements.addBE(id);
+ // Check if restriction might prevent failure
+ if (!isEventDisabledViaRestriction(id)) {
+ failableElements.addBE(id);
+ } else {
+ STORM_LOG_TRACE("BE " << id << " is disabled due to a restriction.");
+ }
}
}
@@ -40,7 +46,7 @@ namespace storm {
STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed.");
for(size_t index = 0; index < mDft.nrElements(); ++index) {
// Initialize currently failable BE
- if (mDft.isBasicElement(index) && isOperational(index)) {
+ if (mDft.isBasicElement(index) && isOperational(index) && !isEventDisabledViaRestriction(index)) {
std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(index);
if (be->canFail()) {
switch (be->type()) {
@@ -215,16 +221,69 @@ namespace storm {
bool addedFailableDependency = false;
for (auto dependency : mDft.getElement(id)->outgoingDependencies()) {
STORM_LOG_ASSERT(dependency->triggerEvent()->id() == id, "Ids do not match.");
- assert(dependency->dependentEvents().size() == 1);
+ STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "Only one dependent event is allowed.");
if (getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe.");
- failableElements.addDependency(dependency->id());
- STORM_LOG_TRACE("New dependency failure: " << *dependency);
- addedFailableDependency = true;
+ // By assertion we have only one dependent event
+ // Check if restriction prevents failure of dependent event
+ if (!isEventDisabledViaRestriction(dependency->dependentEvents()[0]->id())) {
+ // Add dependency as possible failure
+ failableElements.addDependency(dependency->id());
+ STORM_LOG_TRACE("New dependency failure: " << *dependency);
+ addedFailableDependency = true;
+ }
}
}
return addedFailableDependency;
}
+
+ template<typename ValueType>
+ bool DFTState<ValueType>::updateFailableInRestrictions(size_t id) {
+ if (!hasFailed(id)) {
+ // Non-failure does not change anything in a restriction
+ return false;
+ }
+
+ bool addedFailableEvent = false;
+ for (auto restriction : mDft.getElement(id)->restrictions()) {
+ STORM_LOG_ASSERT(restriction->containsChild(id), "Ids do not match.");
+ if (restriction->isSeqEnforcer()) {
+ for (auto it = restriction->children().cbegin(); it != restriction->children().cend(); ++it) {
+ if ((*it)->isBasicElement()) {
+ if ((*it)->id() != id) {
+ if (!hasFailed((*it)->id())) {
+ // Failure should be prevented later on
+ STORM_LOG_TRACE("Child " << (*it)->id() << " should have failed.");
+ }
+ } else {
+ // Current event has failed
+ ++it;
+ if (it != restriction->children().cend()) {
+ // Enable next event
+ failableElements.addBE((*it)->id());
+ STORM_LOG_TRACE("Added possible BE failure: " << *(*it));
+ addedFailableEvent = true;
+ }
+ break;
+ }
+ }
+ }
+ } else if (restriction->isMutex()) {
+ // Current element has failed and disables all other children
+ for (auto const& child : restriction->children()) {
+ if (child->isBasicElement() && child->id() != id && getElementState(child->id()) == DFTElementState::Operational) {
+ // Disable child
+ failableElements.removeBE(child->id());
+ STORM_LOG_TRACE("Disabled child: " << *child);
+ addedFailableEvent = true;
+ }
+ }
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Restriction must be SEQ or MUTEX");
+ }
+ }
+ return addedFailableEvent;
+ }
template<typename ValueType>
void DFTState<ValueType>::updateDontCareDependencies(size_t id) {
@@ -304,7 +363,7 @@ namespace storm {
activate(representativeId);
}
for(size_t elem : mDft.module(representativeId)) {
- if(mDft.isBasicElement(elem) && isOperational(elem)) {
+ if(mDft.isBasicElement(elem) && isOperational(elem) && !isEventDisabledViaRestriction(elem)) {
std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(elem);
if (be->canFail()) {
switch (be->type()) {
@@ -361,6 +420,28 @@ namespace storm {
STORM_LOG_ASSERT(hasFailed(spareId), "Spare has not failed.");
mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount());
}
+
+ template<typename ValueType>
+ bool DFTState<ValueType>::isEventDisabledViaRestriction(size_t id) const {
+ STORM_LOG_ASSERT(!mDft.isDependency(id), "Event " << id << " is dependency.");
+ STORM_LOG_ASSERT(!mDft.isRestriction(id), "Event " << id << " is restriction.");
+ // First check sequence enforcer
+ auto const& preIds = mStateGenerationInfo.seqRestrictionPreElements(id);
+ for (size_t id : preIds) {
+ if (isOperational(id)) {
+ return true;
+ }
+ }
+
+ // Second check mutexes
+ auto const& mutexIds = mStateGenerationInfo.mutexRestrictionElements(id);
+ for (size_t id : mutexIds) {
+ if (!isOperational(id)) {
+ return true;
+ }
+ }
+ return false;
+ }
template<typename ValueType>
bool DFTState<ValueType>::hasOperationalPostSeqElements(size_t id) const {
diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h
index e569e8d49..97048fd2d 100644
--- a/src/storm-dft/storage/dft/DFTState.h
+++ b/src/storm-dft/storage/dft/DFTState.h
@@ -289,6 +289,13 @@ namespace storm {
* @return true if failable dependent events exist
*/
bool updateFailableDependencies(size_t id);
+
+ /**
+ * Sets all failable BEs due to restrictions from newly failed element.
+ * @param id Id of the newly failed element
+ * @return true if newly failable events exist
+ */
+ bool updateFailableInRestrictions(size_t id);
/**
* Sets all dependencies dont care whose dependent event is the newly failed BE.
@@ -315,6 +322,13 @@ namespace storm {
* @return True, if elements were swapped, false if nothing changed.
*/
bool orderBySymmetry();
+
+ /*!
+ * Check whether the event cannot fail at the moment due to a restriction.
+ * @param id Event id.
+ * @return True iff a restriction prevents the failure of the event.
+ */
+ bool isEventDisabledViaRestriction(size_t id) const;
/**
* Checks whether operational post seq elements are present
diff --git a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h
index bc7e56140..ec2ed993a 100644
--- a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h
+++ b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h
@@ -8,8 +8,9 @@ namespace storm {
std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
- std::map<size_t, std::vector<size_t>> mSeqRestrictionPreElements; // id -> list of restriction pre elements;
- std::map<size_t, std::vector<size_t>> mSeqRestrictionPostElements; // id -> list of restriction post elements;
+ std::map<size_t, std::vector<size_t>> mSeqRestrictionPreElements; // id -> list of restriction pre elements
+ std::map<size_t, std::vector<size_t>> mSeqRestrictionPostElements; // id -> list of restriction post elements
+ std::map<size_t, std::vector<size_t>> mMutexRestrictionElements; // id -> list of elments in the same mutexes
std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (length of symmetry group, vector indicating the starting points of the symmetry groups)
public:
@@ -37,12 +38,25 @@ namespace storm {
void setRestrictionPostElements(size_t id, std::vector<size_t> const& elems) {
mSeqRestrictionPostElements[id] = elems;
}
+
+ void setMutexElements(size_t id, std::vector<size_t> const& elems) {
+ mMutexRestrictionElements[id] = elems;
+ }
+
+ std::vector<size_t> const& seqRestrictionPreElements(size_t index) const {
+ STORM_LOG_ASSERT(mSeqRestrictionPreElements.count(index) > 0, "Index invalid.");
+ return mSeqRestrictionPreElements.at(index);
+ }
std::vector<size_t> const& seqRestrictionPostElements(size_t index) const {
STORM_LOG_ASSERT(mSeqRestrictionPostElements.count(index) > 0, "Index invalid.");
return mSeqRestrictionPostElements.at(index);
}
-
+
+ std::vector<size_t> const& mutexRestrictionElements(size_t index) const {
+ STORM_LOG_ASSERT(mMutexRestrictionElements.count(index) > 0, "Index invalid.");
+ return mMutexRestrictionElements.at(index);
+ }
void addSpareActivationIndex(size_t id, size_t index) {
mSpareActivationIndex[id] = index;
diff --git a/src/storm-dft/storage/dft/elements/DFTChildren.h b/src/storm-dft/storage/dft/elements/DFTChildren.h
index a9d0c7290..8aeb1381f 100644
--- a/src/storm-dft/storage/dft/elements/DFTChildren.h
+++ b/src/storm-dft/storage/dft/elements/DFTChildren.h
@@ -52,6 +52,18 @@ namespace storm {
return mChildren.size();
}
+ /*!
+ * Check whether the given element is contained in the list of children.
+ * @param id Id of element to search for.
+ * @return True iff element was found in list of children.
+ */
+ bool containsChild(size_t id) {
+ auto it = std::find_if(this->mChildren.begin(), this->mChildren.end(), [&id](DFTElementPointer element) -> bool {
+ return element->id() == id;
+ });
+ return it != this->mChildren.end();
+ }
+
virtual std::vector<size_t> independentUnit() const override {
std::set<size_t> unit = {this->mId};
for (auto const& child : mChildren) {
diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h
index a7cca4f36..955d3b9be 100644
--- a/src/storm-dft/storage/dft/elements/DFTDependency.h
+++ b/src/storm-dft/storage/dft/elements/DFTDependency.h
@@ -113,7 +113,6 @@ namespace storm {
return it != this->mDependentEvents.end();
}
-
virtual size_t nrChildren() const override {
return 1;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h
index b287ae863..80fff512c 100644
--- a/src/storm-dft/storage/dft/elements/DFTElement.h
+++ b/src/storm-dft/storage/dft/elements/DFTElement.h
@@ -338,6 +338,29 @@ namespace storm {
return res;
}
+ /**
+ * Obtains ids of elements which are under the same mutex.
+ * @return A vector of ids
+ */
+ std::vector<size_t> mutexRestrictionElements() const {
+ std::vector<size_t> res;
+ for (auto const& restr : mRestrictions) {
+ if (!restr->isMutex()) {
+ continue;
+ }
+ bool found = false;
+ for (auto it = restr->children().cbegin(); it != restr->children().cend(); ++it) {
+ if ((*it)->id() != mId) {
+ res.push_back((*it)->id());
+ } else {
+ found = true;
+ }
+ }
+ STORM_LOG_ASSERT(found, "Child " << mId << " is not included in restriction " << *restr);
+ }
+ return res;
+ }
+
virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
// virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
diff --git a/src/storm-dft/storage/dft/elements/DFTMutex.h b/src/storm-dft/storage/dft/elements/DFTMutex.h
index cbc18a69b..ff50d0f9f 100644
--- a/src/storm-dft/storage/dft/elements/DFTMutex.h
+++ b/src/storm-dft/storage/dft/elements/DFTMutex.h
@@ -28,7 +28,7 @@ namespace storm {
return DFTElementType::MUTEX;
}
- bool isSeqEnforcer() const override {
+ bool isMutex() const override {
return true;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h
index 92c9a69ec..54421d556 100644
--- a/src/storm-dft/storage/dft/elements/DFTRestriction.h
+++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h
@@ -44,6 +44,14 @@ namespace storm {
return false;
}
+ /*!
+ * Return whether the restriction is a mutex.
+ * @return True iff the restriction is a MUTEX.
+ */
+ virtual bool isMutex() const {
+ return false;
+ }
+
/*!
* Returns whether all children are BEs.
* @return True iff all children are BEs.