diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index dbd64088b..75556a06f 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -8,31 +8,36 @@ namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(depth) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(0), probability(storm::utility::zero()) { + // Intentionally left empty + } + + template + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(predecessor.depth + 1) { STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); - rateRatio = rate/exitRate; + probability = predecessor.probability * rate/exitRate; } template<> - bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, double rate, double exitRate) { + bool DFTExplorationHeuristicProbability::updateHeuristicValues(DFTExplorationHeuristic const& predecessor, double rate, double exitRate) { STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0"); - rateRatio += rate/exitRate; + probability += predecessor.getProbability() * rate/exitRate; return true; } template<> - bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, storm::RationalFunction rate, storm::RationalFunction exitRate) { + 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 DFTExplorationHeuristicRateRatio::getPriority() const { - return rateRatio; + double DFTExplorationHeuristicProbability::getPriority() const { + return probability; } template<> - double DFTExplorationHeuristicRateRatio::getPriority() const { + double DFTExplorationHeuristicProbability::getPriority() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); } @@ -41,13 +46,13 @@ namespace storm { template class DFTExplorationHeuristic; template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; - template class DFTExplorationHeuristicRateRatio; + template class DFTExplorationHeuristicProbability; #ifdef STORM_HAVE_CARL template class DFTExplorationHeuristic; template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; - template class DFTExplorationHeuristicRateRatio; + template class DFTExplorationHeuristicProbability; #endif } } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index d23c673fc..f24d7defb 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, RATERATIO }; + enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY }; /*! @@ -20,9 +20,11 @@ namespace storm { class DFTExplorationHeuristic { public: - DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate); + DFTExplorationHeuristic(size_t id); - virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0; + DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); + + virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0; virtual double getPriority() const = 0; @@ -40,21 +42,29 @@ namespace storm { return depth; } + ValueType getProbability() const { + return probability; + } + protected: size_t id; bool expand; size_t depth; - ValueType rateRatio; + ValueType probability; }; template class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicNone(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { + DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } - bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override { + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override { return false; } @@ -74,13 +84,17 @@ namespace storm { template class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicDepth(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { + DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic(id) { // Intentionally left empty } - bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override { - if (depth < this->depth) { - this->depth = depth; + DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + // Intentionally left empty + } + + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override { + if (predecessor.getDepth() < this->depth) { + this->depth = predecessor.getDepth(); return true; } return false; @@ -101,13 +115,17 @@ namespace storm { }; template - class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic { + class DFTExplorationHeuristicProbability : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicRateRatio(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { + DFTExplorationHeuristicProbability(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } - bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override; + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override; double getPriority() const override; @@ -115,7 +133,7 @@ namespace storm { return !this->expand && this->getPriority() < approximationThreshold; } - bool operator<(DFTExplorationHeuristicRateRatio const& other) const { + bool operator<(DFTExplorationHeuristicProbability const& other) const { return this->getPriority() < other.getPriority(); } }; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 78272238c..6b35344cd 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -37,7 +37,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::NONE; + heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; } template @@ -79,7 +79,7 @@ namespace storm { STORM_LOG_TRACE("Initial state: " << initialStateIndex); // Initialize heuristic values for inital state STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); - ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex, 0, storm::utility::zero(), storm::utility::one()); + ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex); heuristic->markExpand(); statesNotExplored[initialStateIndex].second = heuristic; explorationQueue.push(heuristic); @@ -95,8 +95,9 @@ namespace storm { case storm::builder::ApproximationHeuristic::DEPTH: approximationThreshold = iteration; break; - case storm::builder::ApproximationHeuristic::RATERATIO: - approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; + case storm::builder::ApproximationHeuristic::PROBABILITY: + //approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; + approximationThreshold = 10 * std::pow(2, iteration); break; } exploreStateSpace(approximationThreshold); @@ -298,12 +299,12 @@ namespace storm { DFTStatePointer state = iter->second.first; if (!iter->second.second) { // Initialize heuristic values - ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); iter->second.second = heuristic; explorationQueue.push(heuristic); } else { double oldPriority = iter->second.second->getPriority(); - if (iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass())) { + if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) { // Update priority queue ++fix; explorationQueue.update(iter->second.second, oldPriority); diff --git a/src/settings/modules/DFTSettings.cpp b/src/settings/modules/DFTSettings.cpp index 0dcb49f1d..ab707b5a4 100644 --- a/src/settings/modules/DFTSettings.cpp +++ b/src/settings/modules/DFTSettings.cpp @@ -40,7 +40,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorIncluding(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, rateratio}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build()); @@ -87,8 +87,8 @@ namespace storm { std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); if (heuristicAsString == "depth") { return storm::builder::ApproximationHeuristic::DEPTH; - } else if (heuristicAsString == "rateratio") { - return storm::builder::ApproximationHeuristic::RATERATIO; + } else if (heuristicAsString == "probability") { + return storm::builder::ApproximationHeuristic::PROBABILITY; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); }