diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 40d00115f..527513134 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -47,9 +47,29 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); } + template<> + bool DFTExplorationHeuristicBoundDifference::updateHeuristicValues(DFTExplorationHeuristic const& predecessor, double rate, double exitRate) { + STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0"); + probability += predecessor.getProbability() * rate/exitRate; + return true; + } + + template<> + bool DFTExplorationHeuristicBoundDifference::updateHeuristicValues(DFTExplorationHeuristic const& predecessor, storm::RationalFunction rate, storm::RationalFunction exitRate) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); + return false; + } + + template + void DFTExplorationHeuristicBoundDifference::setBounds(ValueType lowerBound, ValueType upperBound) { + this->lowerBound = lowerBound; + this->upperBound = upperBound; + difference = (storm::utility::one() / upperBound) - (storm::utility::one() / lowerBound); + } + template<> double DFTExplorationHeuristicBoundDifference::getPriority() const { - return upperBound / lowerBound; + return probability * difference; } template<> diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 8feb0fefa..44931dfbf 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -10,7 +10,7 @@ namespace storm { /*! * Enum representing the heuristic used for deciding which states to expand. */ - enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY }; + enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY, BOUNDDIFFERENCE }; /*! @@ -165,9 +165,9 @@ namespace storm { // Intentionally left empty } - bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override { - return false; - } + void setBounds(ValueType lowerBound, ValueType upperBound); + + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override; double getPriority() const override; @@ -180,8 +180,7 @@ namespace storm { } private: - ValueType lowerBound; - ValueType upperBound; + ValueType difference; }; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index c6c584e86..2f302b0db 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -28,7 +28,7 @@ namespace storm { dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), - heuristic(storm::settings::getModule().getApproximationHeuristic()), + usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), @@ -38,7 +38,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; + usedHeuristic = storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE; // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { @@ -144,7 +144,7 @@ namespace storm { } if (approximationThreshold > 0) { - switch (heuristic) { + switch (usedHeuristic) { case storm::builder::ApproximationHeuristic::NONE: // Do not change anything approximationThreshold = dft.nrElements()+10; @@ -153,6 +153,7 @@ namespace storm { approximationThreshold = iteration; break; case storm::builder::ApproximationHeuristic::PROBABILITY: + case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: approximationThreshold = 10 * std::pow(2, iteration); break; } @@ -360,6 +361,20 @@ namespace storm { // Do not skip absorbing state or if reached by dependencies iter->second.second->markExpand(); } + if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) { + // Compute bounds for heuristic now + if (state->isPseudoState()) { + // Create concrete state from pseudo state + state->construct(); + } + STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); + + // Initialize bounds + ValueType lowerBound = getLowerBound(state); + ValueType upperBound = getUpperBound(state); + heuristic->setBounds(lowerBound, upperBound); + } + explorationQueue.push(heuristic); } else if (!iter->second.second->isExpand()) { double oldPriority = iter->second.second->getPriority(); @@ -567,9 +582,11 @@ namespace storm { for (size_t i = 0; i < rates.size(); ++i) { // Cold BEs cannot fail in the first step if (!coldBEs.get(i) && rateCount[i] > 0) { + std::iter_swap(rates.begin() + i, rates.end() - 1); // Compute AND MTTF of subtree without current rate and scale with current rate upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1); - // Swap here to avoid swapping back + // Swap back + // TODO try to avoid swapping back std::iter_swap(rates.begin() + i, rates.end() - 1); } } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 933cd3277..0e9b9dc57 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicProbability; + using ExplorationHeuristic = DFTExplorationHeuristicBoundDifference; using ExplorationHeuristicPointer = std::shared_ptr; @@ -289,7 +289,7 @@ namespace storm { const bool mergeFailedStates = true; // Heuristic used for approximation - storm::builder::ApproximationHeuristic heuristic; + storm::builder::ApproximationHeuristic usedHeuristic; // Current id for new state size_t newIndex = 0; diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index 224b14cf6..7870888f0 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -153,7 +153,16 @@ namespace storm { template size_t BucketPriorityQueue::getBucket(double priority) const { STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low"); - size_t newBucket = std::log(priority - lowerValue) / logBase; + + // For possible values greater 1 + double tmpBucket = std::log(priority - lowerValue) / logBase; + tmpBucket += buckets.size() / 2; + if (tmpBucket < 0) { + tmpBucket = 0; + } + size_t newBucket = tmpBucket; + // For values ensured to be lower 1 + //size_t newBucket = std::log(priority - lowerValue) / logBase; if (newBucket >= nrBuckets) { newBucket = nrBuckets - 1; } diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 1719c7124..75f065bdc 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio);