diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index b0fd73a66..f71f60dcc 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -22,7 +22,7 @@ namespace storm { class DFTExplorationHeuristic { public: - explicit DFTExplorationHeuristic(size_t id) : id(id), expand(true), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { + explicit DFTExplorationHeuristic(size_t id) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { // Intentionally left empty } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index efc51d89f..e71f8e4b9 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -383,7 +383,7 @@ namespace storm { setMarkovian(true); // Add transition to target state with temporary value 0 // TODO: what to do when there is no unique target state? - STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state"); + //STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state"); matrixBuilder.addTransition(0, storm::utility::zero()); // Remember skipped state skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); @@ -425,8 +425,9 @@ namespace storm { } iter->second.second = heuristic; - if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) { - // Do not skip absorbing state or if reached by dependencies + //if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) { + if (state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) { + // Do not skip absorbing state or if reached by dependencies iter->second.second->markExpand(); } if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) { diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 4edd26b4b..f4af34ed1 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -78,6 +78,7 @@ namespace storm { // Let BE fail bool isFirst = true; while (!state->getFailableElements().isEnd()) { + //TODO outside if (storm::settings::getModule().isTakeFirstDependency() && exploreDependencies && !isFirst) { // We discard further exploration as we already chose one dependent event break;