From ce91fa7d5b42b7f992167a50f65b4a7b7a7c9a24 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 7 Apr 2016 16:58:48 +0200 Subject: [PATCH] started to work on local EC-detection Former-commit-id: 0f36a1bf786b6ed48e99f84e54c8acc3520ffa09 --- .../SparseMdpLearningModelChecker.cpp | 26 +++++--- .../SparseMdpLearningModelChecker.h | 11 +++- src/settings/SettingsManager.cpp | 5 ++ src/settings/SettingsManager.h | 7 +++ src/settings/modules/LearningSettings.cpp | 52 ++++++++++++++++ src/settings/modules/LearningSettings.h | 59 +++++++++++++++++++ 6 files changed, 152 insertions(+), 8 deletions(-) create mode 100644 src/settings/modules/LearningSettings.cpp create mode 100644 src/settings/modules/LearningSettings.h diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp index f8adee32e..d76638997 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp @@ -13,6 +13,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/LearningSettings.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" @@ -42,7 +43,7 @@ namespace storm { StateGeneration stateGeneration(program, variableInformation, getTargetStateExpression(subformula)); - ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true)); + ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().isLocalECDetectionSet()); explorationInformation.optimizationDirection = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; // The first row group starts at action 0. @@ -361,18 +362,29 @@ namespace storm { // Outline: // 1. construct a sparse transition matrix of the relevant part of the state space. // 2. use this matrix to compute an MEC decomposition. - // 3. if non-empty analyze the decomposition for accepting/rejecting MECs. + // 3. if non-empty, analyze the decomposition for accepting/rejecting MECs. // Start with 1. storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true, 0); // Determine the set of states that was expanded. std::vector relevantStates; - for (StateType state = 0; state < explorationInformation.stateStorage.numberOfStates; ++state) { - // Add the state to the relevant states if it's unexplored. Additionally, if we are computing minimal - // probabilities, we only consider it relevant if it's not a target state. - if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) { - relevantStates.push_back(state); + if (explorationInformation.useLocalECDetection()) { + for (auto const& stateActionPair : stack) { + if (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) { + relevantStates.push_back(stateActionPair.first); + } + } + std::sort(relevantStates.begin(), relevantStates.end()); + auto newEnd = std::unique(relevantStates.begin(), relevantStates.end()); + relevantStates.resize(std::distance(relevantStates.begin(), newEnd)); + } else { + for (StateType state = 0; state < explorationInformation.stateStorage.numberOfStates; ++state) { + // Add the state to the relevant states if it's unexplored. Additionally, if we are computing minimal + // probabilities, we only consider it relevant if it's not a target state. + if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) { + relevantStates.push_back(state); + } } } StateType sink = relevantStates.size(); diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h index b0a09e343..df7c0ad92 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h @@ -87,7 +87,7 @@ namespace storm { // A structure containing the data assembled during exploration. struct ExplorationInformation { - ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker) { + ExplorationInformation(uint_fast64_t bitsPerBucket, bool localECDetection, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localECDetection(localECDetection) { // Intentionally left empty. } @@ -104,6 +104,7 @@ namespace storm { StateSet terminalStates; std::unordered_map stateToLeavingActionsOfEndComponent; + bool localECDetection; void setInitialStates(std::vector const& initialStates) { stateStorage.initialStateIndices = initialStates; @@ -199,6 +200,14 @@ namespace storm { bool minimize() const { return !maximize(); } + + bool useLocalECDetection() const { + return localECDetection; + } + + bool useGlobalECDetection() const { + return !useLocalECDetection(); + } }; // A struct containg the lower and upper bounds per state and action. diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index fffb10366..65ab09d2a 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -26,6 +26,7 @@ #include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" +#include "src/settings/modules/LearningSettings.h" #include "src/utility/macros.h" #include "src/settings/Option.h" @@ -547,5 +548,9 @@ namespace storm { storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName)); } + + storm::settings::modules::LearningSettings const& learningSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::LearningSettings::moduleName)); + } } } \ No newline at end of file diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 8d6f79964..52bc470d3 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -25,6 +25,7 @@ namespace storm { class TopologicalValueIterationEquationSolverSettings; class ParametricSettings; class SparseDtmcEliminationModelCheckerSettings; + class LearningSettings; class ModuleSettings; } class Option; @@ -330,6 +331,12 @@ namespace storm { * @return An object that allows accessing the settings of the elimination-based DTMC model checker. */ storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings(); + + /* Retrieves the settings of the learning engine. + * + * @return An object that allows accessing the settings of the learning engine. + */ + storm::settings::modules::LearningSettings const& learningSettings(); } // namespace settings } // namespace storm diff --git a/src/settings/modules/LearningSettings.cpp b/src/settings/modules/LearningSettings.cpp new file mode 100644 index 000000000..f393751f0 --- /dev/null +++ b/src/settings/modules/LearningSettings.cpp @@ -0,0 +1,52 @@ +#include "src/settings/modules/LearningSettings.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string LearningSettings::moduleName = "learning"; + const std::string LearningSettings::ecDetectionTypeOptionName = "ecdetection"; + + LearningSettings::LearningSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + std::vector types = { "local", "global" }; + this->addOption(storm::settings::OptionBuilder(moduleName, ecDetectionTypeOptionName, true, "Sets the kind of EC-detection used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("local").build()).build()); + } + + bool LearningSettings::isLocalECDetectionSet() const { + if (this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString() == "local") { + return true; + } + return false; + } + + bool LearningSettings::isGlobalECDetectionSet() const { + if (this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString() == "global") { + return true; + } + return false; + } + + LearningSettings::ECDetectionType LearningSettings::getECDetectionType() const { + std::string typeAsString = this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString(); + if (typeAsString == "local") { + return LearningSettings::ECDetectionType::Local; + } else if (typeAsString == "global") { + return LearningSettings::ECDetectionType::Global; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown EC-detection type '" << typeAsString << "'."); + } + + bool LearningSettings::check() const { + bool optionsSet = this->getOption(ecDetectionTypeOptionName).getHasOptionBeenSet(); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect."); + return true; + } + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/LearningSettings.h b/src/settings/modules/LearningSettings.h new file mode 100644 index 000000000..d95b9fe98 --- /dev/null +++ b/src/settings/modules/LearningSettings.h @@ -0,0 +1,59 @@ +#ifndef STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ +#define STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ + +#include "src/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the learning settings. + */ + class LearningSettings : public ModuleSettings { + public: + // An enumeration of all available EC-detection types. + enum class ECDetectionType { Local, Global }; + + /*! + * Creates a new set of learning settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ + LearningSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether local EC-detection is to be used. + * + * @return True iff local EC-detection is to be used. + */ + bool isLocalECDetectionSet() const; + + /*! + * Retrieves whether global EC-detection is to be used. + * + * @return True iff global EC-detection is to be used. + */ + bool isGlobalECDetectionSet() const; + + /*! + * Retrieves the selected EC-detection type. + * + * @return The selected EC-detection type. + */ + ECDetectionType getECDetectionType() const; + + virtual bool check() const override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string ecDetectionTypeOptionName; + }; + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ */