diff --git a/examples/dft/be_nonfail.dft b/examples/dft/be_nonfail.dft
new file mode 100644
index 000000000..d53dca551
--- /dev/null
+++ b/examples/dft/be_nonfail.dft
@@ -0,0 +1,4 @@
+toplevel "A";
+"A" and "B" "C";
+"B" lambda=0 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
diff --git a/examples/dft/pdep4.dft b/examples/dft/pdep4.dft
new file mode 100644
index 000000000..eace91847
--- /dev/null
+++ b/examples/dft/pdep4.dft
@@ -0,0 +1,7 @@
+toplevel "SF";
+"SF" pand "S" "A" "B";
+"PDEP" pdep=0.2 "S" "A" "B";
+
+"S" lambda=0.5 dorm=0;
+"A" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0;
diff --git a/examples/dft/por.dft b/examples/dft/por.dft
new file mode 100644
index 000000000..020687f62
--- /dev/null
+++ b/examples/dft/por.dft
@@ -0,0 +1,5 @@
+toplevel "A";
+"A" por "B" "C" "D";
+"B" lambda=0.4 dorm=0.0;
+"C" lambda=0.2 dorm=0.0;
+"D" lambda=0.2 dorm=0.0;
diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 018e0eb90..fa8be6e1a 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -160,7 +160,7 @@ namespace storm {
transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
// Add self loop for target states
- if (mDft.hasFailed(state) || mDft.isFailsafe(state)) {
+ if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, state->getId(), storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << state->getId());
exitRates.push_back(storm::utility::one<ValueType>());
@@ -168,8 +168,6 @@ namespace storm {
markovianStates.push_back(state->getId());
// No further exploration required
continue;
- } else {
- STORM_LOG_THROW(state->nrFailableBEs() > 0, storm::exceptions::UnexpectedException, "State " << state->getId() << " is no target state but behaves like one");
}
// Let BE fail
@@ -267,6 +265,7 @@ namespace storm {
isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
}
ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
+ assert(!storm::utility::isZero(rate));
auto resultFind = outgoingTransitions.find(newStateId);
if (resultFind != outgoingTransitions.end()) {
// Add to existing transition
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index d82c45dfa..071a7e56a 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -130,7 +130,7 @@ namespace storm {
std::vector<size_t> nonColdBEs() const {
std::vector<size_t> result;
for(DFTElementPointer elem : mElements) {
- if(elem->isBasicElement() && !elem->isColdBasicElement()) {
+ if(elem->isBasicElement() && std::static_pointer_cast<DFTBE<ValueType>>(elem)->canFail() && !elem->isColdBasicElement()) {
result.push_back(elem->id());
}
}
diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp
index 8241ea70a..6998529f8 100644
--- a/src/storage/dft/DFTBuilder.cpp
+++ b/src/storage/dft/DFTBuilder.cpp
@@ -225,7 +225,7 @@ namespace storm {
{
std::shared_ptr<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(element);
ValueType dormancyFactor = storm::utility::zero<ValueType>();
- if (!storm::utility::isZero(be->passiveFailureRate())) {
+ if (be->canFail()) {
dormancyFactor = be->passiveFailureRate() / be->activeFailureRate();
}
addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor);
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index d630c24fb..168b27755 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -85,24 +85,32 @@ namespace storm {
//TODO Matthias: collect constraints for SMT solving
//0 <= probability <= 1
if (!storm::utility::isOne(probability) && children.size() > 2) {
- //TODO Matthias: introduce additional element for probability and then add pdeps with probability 1 to children
- STORM_LOG_ERROR("Probability != 1 for more than one child currently not supported.");
- return false;
- }
-
- for (size_t i = 1; i < children.size(); ++i) {
- std::string nameDep = name + "_" + std::to_string(i);
- if(mElements.count(nameDep) != 0) {
- // Element with that name already exists.
- STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
- return false;
+ // Introduce additional element for first capturing the proabilistic dependency
+ std::string nameAdditional = name + "_additional";
+ addBasicElement(nameAdditional, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
+ // First consider probabilistic dependency
+ addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability);
+ // Then consider dependencies to the children if probabilistic dependency failed
+ std::vector<std::string> newChildren = children;
+ newChildren[0] = nameAdditional;
+ addDepElement(name, newChildren, storm::utility::one<ValueType>());
+ return true;
+ } else {
+ // Add dependencies
+ for (size_t i = 1; i < children.size(); ++i) {
+ std::string nameDep = name + "_" + std::to_string(i);
+ if(mElements.count(nameDep) != 0) {
+ // Element with that name already exists.
+ STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
+ return false;
+ }
+ assert(storm::utility::isOne(probability) || children.size() == 2);
+ DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameDep, trigger, children[i], probability);
+ mElements[element->name()] = element;
+ mDependencies.push_back(element);
}
- assert(storm::utility::isOne(probability) || children.size() == 2);
- DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameDep, trigger, children[i], probability);
- mElements[element->name()] = element;
- mDependencies.push_back(element);
+ return true;
}
- return true;
}
bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 1468a36ff..4d603e501 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -29,7 +29,8 @@ namespace storm {
for(size_t index = 0; index < mDft.nrElements(); ++index) {
// Initialize currently failable BE
if (mDft.isBasicElement(index) && isOperational(index)) {
- if (!mDft.getBasicElement(index)->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)->id())) {
+ std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(index);
+ if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)->id())) {
mIsCurrentlyFailableBE.push_back(index);
STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString());
}
@@ -212,6 +213,7 @@ namespace storm {
// Consider "normal" failure
assert(index < nrFailableBEs());
std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
+ assert(res.first->canFail());
mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
setFailed(res.first->id());
return res;
@@ -244,7 +246,7 @@ namespace storm {
activate(representativeId);
}
for(size_t elem : mDft.module(representativeId)) {
- if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
+ if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem) && mDft.getBasicElement(elem)->canFail()) {
mIsCurrentlyFailableBE.push_back(elem);
} else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
propagateActivation(uses(elem));
diff --git a/src/storage/dft/elements/DFTBE.h b/src/storage/dft/elements/DFTBE.h
index 58e580262..e7f912fd4 100644
--- a/src/storage/dft/elements/DFTBE.h
+++ b/src/storage/dft/elements/DFTBE.h
@@ -33,6 +33,10 @@ namespace storm {
return mPassiveFailureRate;
}
+ bool canFail() const {
+ return !storm::utility::isZero(mActiveFailureRate);
+ }
+
bool addIngoingDependency(DFTDependencyPointer const& e) {
assert(e->dependentEvent()->id() == this->id());
if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
@@ -72,7 +76,9 @@ namespace storm {
}
virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
- if(elemsInSubtree.count(this->id())) return;
+ if(elemsInSubtree.count(this->id())) {
+ return;
+ }
DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
if(elemsInSubtree.empty()) {
// Parent in the subdft, ie it is *not* a subdft