From 53821d3d84a50419f1ed8566fa8bfec64c6bc6ff Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 11 Oct 2016 22:58:00 +0200 Subject: [PATCH] Added settings for approximation heuristic Former-commit-id: 40267add31426b65c1232ad11a82b12d0e1a0e0d --- src/builder/DftExplorationHeuristic.cpp | 25 ++++++++++++++----- src/builder/DftExplorationHeuristic.h | 10 +++++++- src/builder/ExplicitDFTModelBuilderApprox.cpp | 5 ++-- src/builder/ExplicitDFTModelBuilderApprox.h | 3 +++ src/settings/modules/DFTSettings.cpp | 18 +++++++++++-- src/settings/modules/DFTSettings.h | 9 +++++++ src/storage/dft/DFTState.h | 4 +++ 7 files changed, 63 insertions(+), 11 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 1364026a1..74937d4b1 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -16,10 +16,27 @@ namespace storm { } template - bool DFTExplorationHeuristic::isSkip() const { - return skip; + bool DFTExplorationHeuristic::isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const { + if (!skip) { + return false; + } + switch (heuristic) { + case ApproximationHeuristic::NONE: + return false; + case ApproximationHeuristic::DEPTH: + return depth > approximationThreshold; + case ApproximationHeuristic::RATERATIO: + // TODO Matthias: implement + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work."); + } } + template + void DFTExplorationHeuristic::setNotSkip() { + skip = false; + } + + template size_t DFTExplorationHeuristic::getDepth() const { return depth; @@ -42,10 +59,6 @@ namespace storm { template<> double DFTExplorationHeuristic::getPriority() const { // TODO Matthias: change according to heuristic - if (!skip) { - // TODO Matthias: change to non-magic number - return 0; - } //return rate/exitRate; return depth; } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 59c35f812..a9958443a 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -14,6 +14,11 @@ namespace storm { namespace builder { + /*! + * Enum representing the heuristic used for deciding which states to expand. + */ + enum class ApproximationHeuristic { NONE, DEPTH, RATERATIO }; + template class DFTExplorationHeuristic { @@ -22,13 +27,16 @@ namespace storm { void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate); - bool isSkip() const; + bool isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const; + + void setNotSkip(); size_t getDepth() const; double getPriority() const; private: + bool skip; size_t depth; ValueType rate; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 3dedfd01d..9ed09eccb 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -26,6 +26,8 @@ namespace storm { ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64) { // stateVectorSize is bound for size of bitvector + heuristic = storm::settings::getModule().getApproximationHeuristic(); + // Compare states by their distance from the initial state // TODO Matthias: customize statesToExplore = std::priority_queue, std::function>(&storm::builder::compareDepth); @@ -229,8 +231,7 @@ namespace storm { // Try to explore the next state generator.load(currentState); - STORM_LOG_TRACE("Priority of state " <getId() << ": " << currentState->getPriority()); - if (currentState->getPriority() > approximationThreshold) { + if (currentState->isSkip(approximationThreshold, heuristic)) { // Skip the current state STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); setMarkovian(true); diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 65575735f..cb9a444af 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -258,6 +258,9 @@ namespace storm { //TODO Matthias: make changeable const bool mergeFailedStates = true; + // Heuristic used for approximation + storm::builder::ApproximationHeuristic heuristic; + // Current id for new state size_t newIndex = 0; diff --git a/src/settings/modules/DFTSettings.cpp b/src/settings/modules/DFTSettings.cpp index c27009a85..1b3f0bae2 100644 --- a/src/settings/modules/DFTSettings.cpp +++ b/src/settings/modules/DFTSettings.cpp @@ -9,7 +9,6 @@ #include "src/exceptions/InvalidSettingsException.h" - namespace storm { namespace settings { namespace modules { @@ -23,6 +22,7 @@ namespace storm { const std::string DFTSettings::disableDCOptionName = "disabledc"; const std::string DFTSettings::approximationErrorOptionName = "approximation"; const std::string DFTSettings::approximationErrorOptionShortName = "approx"; + const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic"; const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; const std::string DFTSettings::propProbabilityOptionName = "probability"; @@ -40,6 +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 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, 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()); @@ -78,6 +79,20 @@ namespace storm { return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); } + storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const { + if (!isApproximationErrorSet() || getApproximationError() == 0.0) { + // No approximation is done + return storm::builder::ApproximationHeuristic::NONE; + } + 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; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); + } + bool DFTSettings::usePropExpectedTime() const { return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); } @@ -109,7 +124,6 @@ namespace storm { #endif void DFTSettings::finalize() { - } bool DFTSettings::check() const { diff --git a/src/settings/modules/DFTSettings.h b/src/settings/modules/DFTSettings.h index bb83a7475..2aa418538 100644 --- a/src/settings/modules/DFTSettings.h +++ b/src/settings/modules/DFTSettings.h @@ -3,6 +3,7 @@ #include "storm-config.h" #include "src/settings/modules/ModuleSettings.h" +#include "src/builder/DftExplorationHeuristic.h" namespace storm { namespace settings { @@ -68,6 +69,13 @@ namespace storm { */ double getApproximationError() const; + /*! + * Retrieves the heuristic used for approximation. + * + * @return The heuristic to use. + */ + storm::builder::ApproximationHeuristic getApproximationHeuristic() const; + /*! * Retrieves whether the property expected time should be used. * @@ -135,6 +143,7 @@ namespace storm { static const std::string disableDCOptionName; static const std::string approximationErrorOptionName; static const std::string approximationErrorOptionShortName; + static const std::string approximationHeuristicOptionName; static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionShortName; static const std::string propProbabilityOptionName; diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index cd2b9eb0f..b49727313 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -112,6 +112,10 @@ namespace storm { exploreHeuristic.setHeuristicValues(oldState->exploreHeuristic.getDepth() + 1, rate, exitRate); } + bool isSkip(double approximationThreshold, storm::builder::ApproximationHeuristic heuristic) { + return exploreHeuristic.isSkip(approximationThreshold, heuristic); + } + double getPriority() const { return exploreHeuristic.getPriority(); }