Support for pdeps with more than one child

Former-commit-id: f3de8f2abd

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;

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;

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;

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

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());
                     }
                 }

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);

src/storage/dft/DFTBuilder.h

@@ -85,11 +85,18 @@ 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;
-                }
-
+                    // 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) {
@@ -104,6 +111,7 @@ namespace storm {
                     }
                     return true;
                 }
+            }
 
             bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
                 assert(children.size() > 0);

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));

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