From 1f5d3b9479f81cc70fe33e6c0e65c25abb64af17 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 24 Mar 2019 18:05:21 +0100
Subject: [PATCH] Correct initialization of priority queue
---
.../generator/DftNextStateGenerator.cpp | 32 ++++++++++++-------
.../generator/DftNextStateGenerator.h | 4 ++-
src/storm-dft/storage/dft/DFTState.cpp | 10 +++---
src/storm-dft/storage/dft/DFTState.h | 3 +-
4 files changed, 32 insertions(+), 17 deletions(-)
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 2a3502c5e..69751ea62 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -46,16 +46,19 @@ namespace storm {
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state));
+ // Initialization
+ bool hasDependencies = state->getFailableElements().hasDependencies();
+ return exploreState(stateToIdCallback, hasDependencies);
+ }
+ template<typename ValueType, typename StateType>
+ StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies) {
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;
- // Initialization
- bool hasDependencies = state->getFailableElements().hasDependencies();
//size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
//size_t currentFailable = 0;
- state->getFailableElements().init(hasDependencies);
-
+ state->getFailableElements().init(exploreDependencies);
// Check for absorbing state
if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->getFailableElements().isEnd()) {
Choice<ValueType, StateType> choice(0, true);
@@ -68,12 +71,12 @@ namespace storm {
return result;
}
- Choice<ValueType, StateType> choice(0, !hasDependencies);
+ Choice<ValueType, StateType> choice(0, !exploreDependencies);
// Let BE fail
bool isFirst = true;
while (!state->getFailableElements().isEnd()) {
- if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && hasDependencies && !isFirst) {
+ if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && exploreDependencies && !isFirst) {
// We discard further exploration as we already chose one dependent event
break;
}
@@ -82,10 +85,10 @@ namespace storm {
// Construct new state as copy from original one
DFTStatePointer newState = state->copy();
- std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get());
+ std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get(), exploreDependencies);
std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
STORM_LOG_ASSERT(nextBE, "NextBE is null.");
- STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
+ STORM_LOG_ASSERT(nextBEPair.second == exploreDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
// Propagate
@@ -149,7 +152,7 @@ namespace storm {
}
// Set transitions
- if (hasDependencies) {
+ if (exploreDependencies) {
// Failure is due to dependency -> add non-deterministic choice
ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability();
choice.addProbability(newStateId, probability);
@@ -184,8 +187,15 @@ namespace storm {
state->getFailableElements().next();
} // end while failing BE
-
- if (!hasDependencies) {
+
+ if (exploreDependencies) {
+ if (result.empty()) {
+ // Dependencies might have been prevented from sequence enforcer
+ // -> explore BEs now
+ return exploreState(stateToIdCallback, false);
+ }
+ } else {
+ STORM_LOG_ASSERT(choice.size() > 0, "No transitions were generated");
// Add all rates as one choice
result.addChoice(std::move(choice));
}
diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h
index 2f614afe6..08aa3739e 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.h
+++ b/src/storm-dft/generator/DftNextStateGenerator.h
@@ -43,7 +43,9 @@ namespace storm {
StateBehavior<ValueType, StateType> createMergeFailedState(StateToIdCallback const& stateToIdCallback);
private:
-
+
+ StateBehavior<ValueType, StateType> exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies);
+
// The dft used for the generation of next states.
storm::storage::DFT<ValueType> const& mDft;
diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
index 2bbc2dfed..18b0559a0 100644
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -195,7 +195,8 @@ namespace storm {
if (!hasFailed(id)) {
return false;
}
-
+
+ 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);
@@ -203,9 +204,10 @@ namespace storm {
STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe.");
failableElements.addDependency(dependency->id());
STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
+ addedFailableDependency = true;
}
}
- return failableElements.hasDependencies();
+ return addedFailableDependency;
}
template<typename ValueType>
@@ -235,9 +237,9 @@ namespace storm {
}
template<typename ValueType>
- std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> DFTState<ValueType>::letNextBEFail(size_t id) {
+ std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> DFTState<ValueType>::letNextBEFail(size_t id, bool dueToDependency) {
STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
- if (failableElements.hasDependencies()) {
+ if (dueToDependency) {
// Consider failure due to dependency
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(id);
STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event");
diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h
index 427115de4..e569e8d49 100644
--- a/src/storm-dft/storage/dft/DFTState.h
+++ b/src/storm-dft/storage/dft/DFTState.h
@@ -299,9 +299,10 @@ namespace storm {
/**
* Sets the next BE as failed
* @param index Index in currentlyFailableBE of BE to fail
+ * @param dueToDependency Whether the failure is due to a dependency.
* @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies
*/
- std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> letNextBEFail(size_t index = 0);
+ std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> letNextBEFail(size_t index, bool dueToDependency);
/**
* Sets the dependency as unsuccesful meaning no BE will fail.