diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 46797aa23..9481e3392 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/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.");
diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 0bf848838..1f702d270 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/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);
}
diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp
index 31d17fbe0..e61e8e331 100644
--- a/src/generator/DftNextStateGenerator.cpp
+++ b/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.");
diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp
index 692f61735..26f2033d6 100644
--- a/src/modelchecker/dft/DFTModelChecker.cpp
+++ b/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 << ")");
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index c12204e06..7620a059a 100644
--- a/src/storage/dft/DFT.h
+++ b/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 {
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 5e84b0c56..b292e322d 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/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);
});
}
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 617d40a7d..a6644f349 100644
--- a/src/storage/dft/DFTState.h
+++ b/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.
*/