diff --git a/src/storm-dft/builder/DftExplorationHeuristic.cpp b/src/storm-dft/builder/DftExplorationHeuristic.cpp index a8a11ae18..d46736268 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.cpp +++ b/src/storm-dft/builder/DftExplorationHeuristic.cpp @@ -1,81 +1,30 @@ #include "DftExplorationHeuristic.h" #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/utility/macros.h" -#include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" namespace storm { namespace builder { - template - 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) : 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; - } - - template - void DFTExplorationHeuristic::setBounds(ValueType lowerBound, ValueType upperBound) { - this->lowerBound = lowerBound; - this->upperBound = upperBound; - } - - template<> - bool DFTExplorationHeuristicProbability::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 DFTExplorationHeuristicProbability::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<> double DFTExplorationHeuristicProbability::getPriority() const { return probability; } - template<> - double DFTExplorationHeuristicProbability::getPriority() const { - 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); + double DFTExplorationHeuristicProbability::getPriority() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic 'probability' does not work for this data type."); } template<> double DFTExplorationHeuristicBoundDifference::getPriority() const { + double difference = (storm::utility::one() / upperBound) - (storm::utility::one() / lowerBound); return probability * difference; } - template<> - double DFTExplorationHeuristicBoundDifference::getPriority() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic bound difference does not work for rational functions."); + template + double DFTExplorationHeuristicBoundDifference::getPriority() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic 'bound difference' does not work for this data type."); } // Instantiate templates. diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index 2de704e29..f49f5925a 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -1,6 +1,10 @@ #pragma once #include +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + + namespace storm { namespace builder { @@ -12,25 +16,32 @@ namespace storm { /*! - * General super class for appoximation heuristics. + * General super class for approximation heuristics. */ template class DFTExplorationHeuristic { public: - DFTExplorationHeuristic(size_t id); + explicit 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 + } - DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); + 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), probability(storm::utility::one()) { + this->updateHeuristicValues(predecessor, rate, exitRate); + } virtual ~DFTExplorationHeuristic() = default; - void setBounds(ValueType lowerBound, ValueType upperBound); - - virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0; - - virtual double getPriority() const = 0; + void setBounds(ValueType lowerBound, ValueType upperBound) { + this->lowerBound = lowerBound; + this->upperBound = upperBound; + } - virtual bool isSkip(double approximationThreshold) const = 0; + virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) { + STORM_LOG_ASSERT(!storm::utility::isZero(exitRate), "Exit rate is 0"); + probability += predecessor.getProbability() * rate/exitRate; + return true; + } void markExpand() { expand = true; @@ -40,7 +51,7 @@ namespace storm { return id; } - bool isExpand() { + bool isExpand() const { return expand; } @@ -60,6 +71,16 @@ namespace storm { return upperBound; } + virtual double getPriority() const = 0; + + virtual bool isSkip(double approximationThreshold) const { + return !this->isExpand() && this->getPriority() < approximationThreshold; + } + + virtual bool operator<(DFTExplorationHeuristic const& other) const { + return this->getPriority() < other.getPriority(); + } + protected: size_t id; bool expand; @@ -76,7 +97,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -91,10 +112,6 @@ namespace storm { bool isSkip(double) const override { return false; } - - bool operator<(DFTExplorationHeuristicNone const& other) const { - return this->id > other.id; - } }; template @@ -104,7 +121,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -116,17 +133,16 @@ namespace storm { return false; } - double getPriority() const override { return this->depth; } bool isSkip(double approximationThreshold) const override { - return !this->expand && this->depth > approximationThreshold; + return !this->expand && this->getPriority() > approximationThreshold; } - bool operator<(DFTExplorationHeuristicDepth const& other) const { - return this->depth > other.depth; + bool operator<(DFTExplorationHeuristic const& other) const override { + return this->getPriority() > other.getPriority(); } }; @@ -137,21 +153,11 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } - bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override; - double getPriority() const override; - - bool isSkip(double approximationThreshold) const override { - return !this->expand && this->getPriority() < approximationThreshold; - } - - bool operator<(DFTExplorationHeuristicProbability const& other) const { - return this->getPriority() < other.getPriority(); - } }; template @@ -161,28 +167,12 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } - void setBounds(ValueType lowerBound, ValueType upperBound); - - bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override; - double getPriority() const override; - - bool isSkip(double approximationThreshold) const override { - return !this->expand && this->getPriority() < approximationThreshold; - } - - bool operator<(DFTExplorationHeuristicBoundDifference const& other) const { - return this->getPriority() < other.getPriority(); - } - - private: - ValueType difference; }; - } }