Fixed computing rates for lower and upper bound

Former-commit-id: 89846a9788

src/builder/ExplicitDFTModelBuilder.cpp

@@ -290,7 +290,7 @@ namespace storm {
                     if (mDft.hasRepresentant(nextBE->id())) {
                         // Active must be checked for the state we are coming from as this state is responsible for the
                         // rate and not the new state we are going to
-                        isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
+                        isActive = state->isActive(mDft.getRepresentant(nextBE->id()));
                     }
                     ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
                     STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -414,9 +414,15 @@ namespace storm {
             for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
                 auto matrixEntry = matrix.getRow(it->first, 0).begin();
                 STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
-                // Get the lower bound by considering the failure of the BE with the highest rate
-                // The list is sorted by rate, therefore we consider the first BE for the highest failure rate
-                matrixEntry->setValue(it->second->getFailableBERate(0));
+                // Get the lower bound by considering the failure of all possible BEs
+                ValueType newRate = storm::utility::zero<ValueType>();
+                for (size_t index = 0; index < it->second->nrFailableBEs(); ++index) {
+                    newRate += it->second->getFailableBERate(index);
+                }
+                for (size_t index = 0; index < it->second->nrNotFailableBEs(); ++index) {
+                    newRate += it->second->getNotFailableBERate(index);
+                }
+                matrixEntry->setValue(newRate);
             }
         }
 
@@ -433,6 +439,9 @@ namespace storm {
                 for (size_t index = 0; index < it->second->nrFailableBEs(); ++index) {
                     newRate += storm::utility::one<ValueType>() / it->second->getFailableBERate(index);
                 }
+                for (size_t index = 0; index < it->second->nrNotFailableBEs(); ++index) {
+                    newRate += storm::utility::one<ValueType>() / it->second->getNotFailableBERate(index);
+                }
                 newRate = storm::utility::one<ValueType>() / newRate;
                 matrixEntry->setValue(newRate);
             }

src/generator/DftNextStateGenerator.cpp

@@ -168,7 +168,7 @@ namespace storm {
                     bool isActive = true;
                     if (mDft.hasRepresentant(nextBE->id())) {
                         // Active must be checked for the state we are coming from as this state is responsible for the rate
-                        isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
+                        isActive = state->isActive(mDft.getRepresentant(nextBE->id()));
                     }
                     ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
                     STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");

src/modelchecker/dft/DFTModelChecker.cpp

@@ -147,6 +147,8 @@ namespace storm {
             buildingTime += buildingEnd - buildingStart;
 
             if (approximationError > 0.0) {
+                // Comparator for checking the error of the approximation
+                storm::utility::ConstantsComparator<ValueType> comparator;
                 // Build approximate Markov Automata for lower and upper bound
                 double currentApproximationError = approximationError;
                 approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
@@ -173,7 +175,9 @@ namespace storm {
                     // Check lower bound
                     std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-                    approxResult.first = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+                    ValueType newResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+                    STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult, approxResult.first), "New under-approximation " << newResult << " is smaller than old result " << approxResult.first);
+                    approxResult.first = newResult;
 
                     // Build model for upper bound
                     STORM_LOG_INFO("Getting model for upper bound...");
@@ -183,7 +187,9 @@ namespace storm {
                     // Check upper bound
                     result = checkModel(model, formula);
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-                    approxResult.second = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+                    newResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+                    STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult), "New over-approximation " << newResult << " is greater than old result " << approxResult.second);
+                    approxResult.second = newResult;
 
                     ++iteration;
                     STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");

src/storage/dft/DFT.h

@@ -216,9 +216,9 @@ namespace storm {
                 return mRepresentants.find(id) != mRepresentants.end();
             }
 
-            DFTElementCPointer getRepresentant(size_t id) const {
+            size_t getRepresentant(size_t id) const {
                 STORM_LOG_ASSERT(hasRepresentant(id), "Element has no representant.");
-                return getElement(mRepresentants.find(id)->second);
+                return mRepresentants.find(id)->second;
             }
 
             bool hasFailed(DFTStatePointer const& state) const {

src/storage/dft/DFTState.cpp

@@ -9,18 +9,29 @@ namespace storm {
         DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic()  {
             
             // Initialize uses
-            for(size_t spareId  : mDft.getSpareIndices()) {
+            for(size_t spareId : mDft.getSpareIndices()) {
                 std::shared_ptr<DFTGate<ValueType> const> elem = mDft.getGate(spareId);
                 STORM_LOG_ASSERT(elem->isSpareGate(), "Element is no spare gate.");
                 STORM_LOG_ASSERT(elem->nrChildren() > 0, "Element has no child.");
                 this->setUses(spareId, elem->children()[0]->id());
             }
-            
+
+            for (auto elem : mDft.getBasicElements()) {
+                mCurrentlyNotFailableBE.push_back(elem->id());
+            }
+
             // Initialize activation
             propagateActivation(mDft.getTopLevelIndex());
 
-            std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs();
-            mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
+            std::vector<size_t> alwaysActiveBEs = mDft.nonColdBEs();
+            mCurrentlyFailableBE.insert(mCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
+            // Remove always active BEs from currently not failable BEs
+            for (size_t id : alwaysActiveBEs) {
+                auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id);
+                STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Id not found.");
+                mCurrentlyNotFailableBE.erase(it);
+            }
+
             sortFailableBEs();
         }
         
@@ -31,9 +42,13 @@ namespace storm {
                 // Initialize currently failable BE
                 if (mDft.isBasicElement(index) && isOperational(index)) {
                     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);
+                    if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) {
+                        mCurrentlyFailableBE.push_back(index);
                         STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString());
+                    } else {
+                        // BE currently is not failable
+                        mCurrentlyNotFailableBE.push_back(index);
+                        STORM_LOG_TRACE("Currently not failable: " << mDft.getBasicElement(index)->toString());
                     }
                 } else if (mDft.getElement(index)->isSpareGate()) {
                     // Initialize used representants
@@ -176,9 +191,9 @@ namespace storm {
 
         template<typename ValueType>
         void DFTState<ValueType>::beNoLongerFailable(size_t id) {
-            auto it = std::find(mIsCurrentlyFailableBE.begin(), mIsCurrentlyFailableBE.end(), id);
-            if(it != mIsCurrentlyFailableBE.end()) {
-                mIsCurrentlyFailableBE.erase(it);
+            auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id);
+            if(it != mCurrentlyFailableBE.end()) {
+                mCurrentlyFailableBE.erase(it);
             }
         }
 
@@ -210,11 +225,29 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        ValueType DFTState<ValueType>::getBERate(size_t id, bool considerPassive) const {
+            STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE.");
+            if (considerPassive && mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) {
+                return mDft.getBasicElement(id)->passiveFailureRate();
+            } else {
+                return mDft.getBasicElement(id)->activeFailureRate();
+            }
+        }
+
         template<typename ValueType>
         ValueType DFTState<ValueType>::getFailableBERate(size_t index) const {
             STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid.");
-            // TODO Matthias: get passive failure rate when applicable
-            return mDft.getBasicElement(mIsCurrentlyFailableBE[index])->activeFailureRate();
+            return getBERate(mCurrentlyFailableBE[index], true);
+        }
+
+        template<typename ValueType>
+        ValueType DFTState<ValueType>::getNotFailableBERate(size_t index) const {
+            STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid.");
+            STORM_LOG_ASSERT(storm::utility::isZero<ValueType>(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) ||
+                             (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail");
+            // Use active failure rate as passive failure rate is 0.
+            return getBERate(mCurrentlyNotFailableBE[index], false);
         }
 
         template<typename ValueType>
@@ -232,9 +265,9 @@ namespace storm {
             } else {
                 // Consider "normal" failure
                 STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid.");
-                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
+                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(mCurrentlyFailableBE[index]), false);
                 STORM_LOG_ASSERT(res.first->canFail(), "Element cannot fail.");
-                mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
+                mCurrentlyFailableBE.erase(mCurrentlyFailableBE.begin() + index);
                 setFailed(res.first->id());
                 return res;
             }
@@ -269,7 +302,12 @@ namespace storm {
                 if(mDft.isBasicElement(elem) && isOperational(elem)) {
                     std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(elem);
                     if (be->isColdBasicElement() && be->canFail()) {
-                        mIsCurrentlyFailableBE.push_back(elem);
+                        // Add to failable BEs
+                        mCurrentlyFailableBE.push_back(elem);
+                        // Remove from not failable BEs
+                        auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem);
+                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element not found.");
+                        mCurrentlyNotFailableBE.erase(it);
                     }
                 } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
                     propagateActivation(uses(elem));
@@ -373,11 +411,9 @@ namespace storm {
         
         template<typename ValueType>
         void DFTState<ValueType>::sortFailableBEs() {
-            std::sort( mIsCurrentlyFailableBE.begin( ), mIsCurrentlyFailableBE.end( ), [&](size_t const& lhs, size_t const& rhs) {
-                ValueType leftRate = mDft.getBasicElement(lhs)->activeFailureRate();
-                ValueType rightRate = mDft.getBasicElement(rhs)->activeFailureRate();
+            std::sort(mCurrentlyFailableBE.begin( ), mCurrentlyFailableBE.end( ), [&](size_t const& lhs, size_t const& rhs) {
                 // Sort decreasing
-                return rightRate < leftRate;
+                return getBERate(rhs, true) < getBERate(lhs, true);
             });
         }
 

src/storage/dft/DFTState.h

@@ -26,7 +26,8 @@ namespace storm {
             // Status is bitvector where each element has two bits with the meaning according to DFTElementState
             storm::storage::BitVector mStatus;
             size_t mId;
-            std::vector<size_t> mIsCurrentlyFailableBE;
+            std::vector<size_t> mCurrentlyFailableBE;
+            std::vector<size_t> mCurrentlyNotFailableBE;
             std::vector<size_t> mFailableDependencies;
             std::vector<size_t> mUsedRepresentants;
             bool mValid = true;
@@ -158,25 +159,58 @@ namespace storm {
              * @param spareId Id of the spare
              */
             void finalizeUses(size_t spareId);
-            
+
+            /**
+             * Claim a new spare child for the given spare gate.
+             *
+             * @param spareId       Id of the spare gate.
+             * @param currentlyUses Id of the currently used spare child.
+             * @param children      List of children of this spare.
+             *
+             * @return True, if claiming was successful.
+             */
             bool claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children);
             
-            bool hasOutgoingEdges() const {
-                return !mIsCurrentlyFailableBE.empty();
-            }
-            
+            /**
+             * Get number of currently failable BEs.
+             *
+             * @return Number of failable BEs.
+             */
             size_t nrFailableBEs() const {
-                return mIsCurrentlyFailableBE.size();
+                return mCurrentlyFailableBE.size();
+            }
+
+            /**
+             * Get number of currently not failable BEs. These are cold BE which can fail in the future.
+             *
+             * @return Number of not failable BEs.
+             */
+            size_t nrNotFailableBEs() const {
+                return mCurrentlyNotFailableBE.size();
             }
 
-            /** Get the failure rate of the currently failable BE on the given index.
+            /**
+             * Get the failure rate of the currently failable BE on the given index.
              *
-             * @param index Index of BE in list of currently failable BEs.
+             * @param index           Index of BE in list of currently failable BEs.
              *
              * @return Failure rate of the BE.
              */
             ValueType getFailableBERate(size_t index) const;
 
+            /**
+             * Get the failure rate of the currently not failable BE on the given index.
+             *
+             * @param index Index of BE in list of currently not failable BEs.
+             *
+             * @return Failure rate of the BE.
+             */
+            ValueType getNotFailableBERate(size_t index) const;
+
+            /** Get number of currently failable dependencies.
+             *
+             * @return Number of failable dependencies.
+             */
             size_t nrFailableDependencies() const {
                 return mFailableDependencies.size();
             }
@@ -245,13 +279,13 @@ namespace storm {
                     }
                     stream << "} ";
                 } else {
-                    auto it = mIsCurrentlyFailableBE.begin();
+                    auto it = mCurrentlyFailableBE.begin();
                     stream << "{";
-                    if(it != mIsCurrentlyFailableBE.end()) {
+                    if(it != mCurrentlyFailableBE.end()) {
                         stream << *it;
                     }
                     ++it;
-                    while(it != mIsCurrentlyFailableBE.end()) {
+                    while(it != mCurrentlyFailableBE.end()) {
                         stream << ", " << *it;
                         ++it;
                     }
@@ -266,7 +300,18 @@ namespace storm {
             
         private:
             void propagateActivation(size_t representativeId);
-            
+
+            /**
+             * Get the failure rate of the given BE.
+             *
+             * @param id              Id of BE.
+             * @param considerPassive Flag indicating if the passive failure rate should be returned if
+             *                        the BE currently is passive.
+             *
+             * @return Failure rate of the BE.
+             */
+            ValueType getBERate(size_t id, bool considerPassive) const;
+
             /*!
              * Sort failable BEs in decreasing order of their active failure rate.
              */