diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index db26fc60d..40d00115f 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -8,12 +8,12 @@ namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(true), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { // Intentionally left empty } template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : id(id), expand(false), lowerBound(lowerBound), upperBound(upperBound), depth(predecessor.depth + 1) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::zero()), depth(predecessor.depth + 1) { STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); probability = predecessor.probability * rate/exitRate; } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 12f178f25..8feb0fefa 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -22,7 +22,7 @@ namespace storm { public: DFTExplorationHeuristic(size_t id); - DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound); + DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); void setBounds(ValueType lowerBound, ValueType upperBound); @@ -76,7 +76,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -85,7 +85,7 @@ namespace storm { } double getPriority() const override { - return this->id; + return 0; } bool isSkip(double approximationThreshold) const override { @@ -104,7 +104,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -137,7 +137,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -161,7 +161,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 6a6474ad8..432636161 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -255,9 +255,6 @@ namespace storm { if (currentState->isPseudoState()) { // Create concrete state from pseudo state currentState->construct(); - ValueType lowerBound = getLowerBound(currentState); - ValueType upperBound = getUpperBound(currentState); - currentExplorationHeuristic->setBounds(lowerBound, upperBound); } STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); @@ -301,17 +298,8 @@ namespace storm { // Update heuristic values DFTStatePointer state = iter->second.first; if (!iter->second.second) { - ValueType lowerBound; - ValueType upperBound; - if (state->isPseudoState()) { - lowerBound = storm::utility::infinity(); - upperBound = storm::utility::infinity(); - } else { - lowerBound = getLowerBound(state); - upperBound = getUpperBound(state); - } // Initialize heuristic values - ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass(), lowerBound, upperBound); + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); iter->second.second = heuristic; if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { // Do not skip absorbing state or if reached by dependencies @@ -453,6 +441,16 @@ namespace storm { auto matrixEntry = matrix.getRow(it->first, 0).begin(); STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); + + ExplorationHeuristicPointer heuristic = it->second.second; + if (storm::utility::isZero(heuristic->getUpperBound())) { + // Initialize bounds + ValueType lowerBound = getLowerBound(it->second.first); + ValueType upperBound = getUpperBound(it->second.first); + heuristic->setBounds(lowerBound, upperBound); + } + + // Change bound if (lowerBound) { matrixEntry->setValue(it->second.second->getLowerBound()); } else { @@ -489,6 +487,7 @@ namespace storm { for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { rates[index + state->nrFailableBEs()] = state->getNotFailableBERate(index); } + STORM_LOG_ASSERT(rates.size() > 0, "State is absorbing"); // TODO Matthias: works only for <64 BEs! for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {