From 07e97e19774c7b1206574e47cd48d5384a7ff23d Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 11 Apr 2016 14:37:46 +0200 Subject: [PATCH] added some statistics and options Former-commit-id: 1b6a9c20f6f88babeff3e63e53cf7b078347606c --- .../SparseMdpLearningModelChecker.cpp | 53 ++++-- .../SparseMdpLearningModelChecker.h | 157 +++++++++++++----- src/settings/modules/LearningSettings.cpp | 35 +++- src/settings/modules/LearningSettings.h | 26 +++ 4 files changed, 203 insertions(+), 68 deletions(-) diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp index 2e3b6c601..f526ea27c 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp @@ -12,13 +12,10 @@ #include "src/models/sparse/StandardRewardModel.h" -#include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/LearningSettings.h" #include "src/utility/graph.h" -#include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotSupportedException.h" @@ -45,7 +42,7 @@ namespace storm { StateGeneration stateGeneration(program, variableInformation, getTargetStateExpression(subformula)); - ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().isLocalPrecomputationSet(), storm::settings::learningSettings().getNumberOfExplorationStepsUntilPrecomputation()); + ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().getNumberOfExplorationStepsUntilPrecomputation()); explorationInformation.optimizationDirection = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; // The first row group starts at action 0. @@ -107,6 +104,9 @@ namespace storm { while (!convergenceCriterionMet) { bool result = samplePathFromInitialState(stateGeneration, explorationInformation, stack, bounds, stats); + stats.sampledPath(); + stats.updateMaxPathLength(stack.size()); + // If a terminal state was found, we update the probabilities along the path contained in the stack. if (result) { // Update the bounds along the path to the terminal state. @@ -124,15 +124,15 @@ namespace storm { STORM_LOG_DEBUG("Difference after iteration " << stats.pathsSampled << " is " << difference << "."); convergenceCriterionMet = comparator.isZero(difference); - ++stats.pathsSampled; + // If the number of sampled paths exceeds a certain threshold, do a precomputation. + if (!convergenceCriterionMet && explorationInformation.performPrecomputationExcessiveSampledPaths(stats.pathsSampledSinceLastPrecomputation)) { + performPrecomputation(stack, explorationInformation, bounds, stats); + } } + // Show statistics if required. if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::cout << std::endl << "Learning summary -------------------------" << std::endl; - std::cout << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << stats.numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << stats.numberOfTargetStates << " target)" << std::endl; - std::cout << "Sampled paths: " << stats.pathsSampled << std::endl; - std::cout << "Maximal path length: " << stats.maxPathLength << std::endl; - std::cout << "EC detections: " << stats.ecDetections << " (" << stats.failedEcDetections << " failed, " << stats.totalNumberOfEcDetected << " EC(s) detected)" << std::endl; + stats.printToStream(std::cout, explorationInformation); } return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation)); @@ -169,8 +169,8 @@ namespace storm { } } - // Increase the number of exploration steps to eventually trigger the precomputation. - ++stats.explorationSteps; + // Notify the stats about the performed exploration step. + stats.explorationStep(); // If the state was not a terminal state, we continue the path search and sample the next state. if (!foundTerminalState) { @@ -185,10 +185,9 @@ namespace storm { // Put the successor state and a dummy action on top of the stack. stack.emplace_back(successor, 0); - stats.maxPathLength = std::max(stats.maxPathLength, stack.size()); // If the number of exploration steps exceeds a certain threshold, do a precomputation. - if (explorationInformation.performPrecomputation(stats.explorationSteps)) { + if (explorationInformation.performPrecomputationExcessiveExplorationSteps(stats.explorationStepsSinceLastPrecomputation)) { performPrecomputation(stack, explorationInformation, bounds, stats); STORM_LOG_TRACE("Aborting the search after precomputation."); @@ -338,18 +337,36 @@ namespace storm { template typename SparseMdpLearningModelChecker::StateType SparseMdpLearningModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { - // TODO: precompute this? - std::vector probabilities(explorationInformation.getRowOfMatrix(chosenAction).size()); - std::transform(explorationInformation.getRowOfMatrix(chosenAction).begin(), explorationInformation.getRowOfMatrix(chosenAction).end(), probabilities.begin(), [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation) ; } ); + std::vector> const& row = explorationInformation.getRowOfMatrix(chosenAction); +// if (row.size() == 1) { +// return row.front().getColumn(); +// } + + std::vector probabilities(row.size()); + + // Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen. + if (explorationInformation.useDifferenceWeightedProbabilityHeuristic()) { + std::transform(row.begin(), row.end(), probabilities.begin(), + [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { + return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation); + }); + } else if (explorationInformation.useProbabilityHeuristic()) { + std::transform(row.begin(), row.end(), probabilities.begin(), + [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { + return entry.getValue(); + }); + } // Now sample according to the probabilities. std::discrete_distribution distribution(probabilities.begin(), probabilities.end()); StateType offset = distribution(randomGenerator); - return explorationInformation.getRowOfMatrix(chosenAction)[offset].getColumn(); + return row[offset].getColumn(); } template bool SparseMdpLearningModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { + ++stats.numberOfPrecomputations; + // Outline: // 1. construct a sparse transition matrix of the relevant part of the state space. // 2. use this matrix to compute states with probability 0/1 and an MEC decomposition (in the max case). diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h index d9a4baf7f..2e43ad582 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h @@ -12,6 +12,10 @@ #include "src/generator/CompressedState.h" #include "src/generator/VariableInformation.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/LearningSettings.h" + +#include "src/utility/macros.h" #include "src/utility/ConstantsComparator.h" #include "src/utility/constants.h" @@ -49,49 +53,18 @@ namespace storm { virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; private: - // A struct that keeps track of certain statistics during the computation. - struct Statistics { - Statistics() : pathsSampled(0), explorationSteps(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) { - // Intentionally left empty. - } - - std::size_t pathsSampled; - std::size_t explorationSteps; - std::size_t maxPathLength; - std::size_t numberOfTargetStates; - std::size_t numberOfExploredStates; - std::size_t ecDetections; - std::size_t failedEcDetections; - std::size_t totalNumberOfEcDetected; - }; - - // A struct containing the data required for state exploration. - struct StateGeneration { - StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), targetStateExpression(targetStateExpression) { - // Intentionally left empty. - } - - std::vector getInitialStates() { - return generator.getInitialStates(stateToIdCallback); - } - - storm::generator::StateBehavior expand() { - return generator.expand(stateToIdCallback); - } - - bool isTargetState() const { - return generator.satisfies(targetStateExpression); - } - - storm::generator::PrismNextStateGenerator generator; - std::function stateToIdCallback; - storm::expressions::Expression targetStateExpression; - }; - // A structure containing the data assembled during exploration. struct ExplorationInformation { - ExplorationInformation(uint_fast64_t bitsPerBucket, bool localPrecomputation, uint_fast64_t numberOfExplorationStepsUntilPrecomputation, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(localPrecomputation), numberOfExplorationStepsUntilPrecomputation(numberOfExplorationStepsUntilPrecomputation) { - // Intentionally left empty. + ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::LearningSettings::NextStateHeuristic::DifferenceWeightedProbability) { + + storm::settings::modules::LearningSettings const& settings = storm::settings::learningSettings(); + localPrecomputation = settings.isLocalPrecomputationSet(); + if (settings.isNumberOfSampledPathsUntilPrecomputationSet()) { + numberOfSampledPathsUntilPrecomputation = settings.getNumberOfSampledPathsUntilPrecomputation(); + } + + nextStateHeuristic = settings.getNextStateHeuristic(); + STORM_LOG_ASSERT(useDifferenceWeightedProbabilityHeuristic() || useProbabilityHeuristic(), "Illegal next-state heuristic."); } storm::storage::sparse::StateStorage stateStorage; @@ -108,6 +81,9 @@ namespace storm { bool localPrecomputation; uint_fast64_t numberOfExplorationStepsUntilPrecomputation; + boost::optional numberOfSampledPathsUntilPrecomputation; + + storm::settings::modules::LearningSettings::NextStateHeuristic nextStateHeuristic; void setInitialStates(std::vector const& initialStates) { stateStorage.initialStateIndices = initialStates; @@ -208,22 +184,111 @@ namespace storm { return !maximize(); } - bool performPrecomputation(std::size_t& performedExplorationSteps) const { - bool result = performedExplorationSteps > numberOfExplorationStepsUntilPrecomputation; + bool performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const { + bool result = numberExplorationStepsSinceLastPrecomputation > numberOfExplorationStepsUntilPrecomputation; if (result) { - std::cout << "triggering precomp" << std::endl; - performedExplorationSteps = 0; + numberExplorationStepsSinceLastPrecomputation = 0; } return result; } + bool performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const { + if (!numberOfSampledPathsUntilPrecomputation) { + return false; + } else { + bool result = numberOfSampledPathsSinceLastPrecomputation > numberOfSampledPathsUntilPrecomputation.get(); + if (result) { + numberOfSampledPathsSinceLastPrecomputation = 0; + } + return result; + } + } + bool useLocalPrecomputation() const { return localPrecomputation; } - + bool useGlobalPrecomputation() const { return !useLocalPrecomputation(); } + + storm::settings::modules::LearningSettings::NextStateHeuristic const& getNextStateHeuristic() const { + return nextStateHeuristic; + } + + bool useDifferenceWeightedProbabilityHeuristic() const { + return nextStateHeuristic == storm::settings::modules::LearningSettings::NextStateHeuristic::DifferenceWeightedProbability; + } + + bool useProbabilityHeuristic() const { + return nextStateHeuristic == storm::settings::modules::LearningSettings::NextStateHeuristic::Probability; + } + }; + + // A struct that keeps track of certain statistics during the computation. + struct Statistics { + Statistics() : pathsSampled(0), pathsSampledSinceLastPrecomputation(0), explorationSteps(0), explorationStepsSinceLastPrecomputation(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), numberOfPrecomputations(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) { + // Intentionally left empty. + } + + void explorationStep() { + ++explorationSteps; + ++explorationStepsSinceLastPrecomputation; + } + + void sampledPath() { + ++pathsSampled; + ++pathsSampledSinceLastPrecomputation; + } + + void updateMaxPathLength(std::size_t const& currentPathLength) { + maxPathLength = std::max(maxPathLength, currentPathLength); + } + + std::size_t pathsSampled; + std::size_t pathsSampledSinceLastPrecomputation; + std::size_t explorationSteps; + std::size_t explorationStepsSinceLastPrecomputation; + std::size_t maxPathLength; + std::size_t numberOfTargetStates; + std::size_t numberOfExploredStates; + std::size_t numberOfPrecomputations; + std::size_t ecDetections; + std::size_t failedEcDetections; + std::size_t totalNumberOfEcDetected; + + void printToStream(std::ostream& out, ExplorationInformation const& explorationInformation) const { + out << std::endl << "Learning statistics:" << std::endl; + out << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << numberOfTargetStates << " target)" << std::endl; + out << "Exploration steps: " << explorationSteps << std::endl; + out << "Sampled paths: " << pathsSampled << std::endl; + out << "Maximal path length: " << maxPathLength << std::endl; + out << "Precomputations: " << numberOfPrecomputations << std::endl; + out << "EC detections: " << ecDetections << " (" << failedEcDetections << " failed, " << totalNumberOfEcDetected << " EC(s) detected)" << std::endl; + } + }; + + // A struct containing the data required for state exploration. + struct StateGeneration { + StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), targetStateExpression(targetStateExpression) { + // Intentionally left empty. + } + + std::vector getInitialStates() { + return generator.getInitialStates(stateToIdCallback); + } + + storm::generator::StateBehavior expand() { + return generator.expand(stateToIdCallback); + } + + bool isTargetState() const { + return generator.satisfies(targetStateExpression); + } + + storm::generator::PrismNextStateGenerator generator; + std::function stateToIdCallback; + storm::expressions::Expression targetStateExpression; }; // A struct containg the lower and upper bounds per state and action. diff --git a/src/settings/modules/LearningSettings.cpp b/src/settings/modules/LearningSettings.cpp index fdddd1672..0ce44a8e4 100644 --- a/src/settings/modules/LearningSettings.cpp +++ b/src/settings/modules/LearningSettings.cpp @@ -13,11 +13,17 @@ namespace storm { const std::string LearningSettings::moduleName = "learning"; const std::string LearningSettings::precomputationTypeOptionName = "precomp"; const std::string LearningSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp"; + const std::string LearningSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp"; + const std::string LearningSettings::nextStateHeuristicOptionName = "nextstate"; LearningSettings::LearningSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector types = { "local", "global" }; - this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation 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()); - this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, false, "Sets the number of exploration steps until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation 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("global").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, false, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, false, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build()); + + std::vector nextStateHeuristics = { "probdiff", "prob" }; + this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiff, prob } where 'prob' samples according to the probabilities in the system and 'probdiff' weights the probabilities with the differences between the current bounds.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiff").build()).build()); } bool LearningSettings::isLocalPrecomputationSet() const { @@ -41,15 +47,36 @@ namespace storm { } else if (typeAsString == "global") { return LearningSettings::PrecomputationType::Global; } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown EC-detection type '" << typeAsString << "'."); + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown precomputation type '" << typeAsString << "'."); } uint_fast64_t LearningSettings::getNumberOfExplorationStepsUntilPrecomputation() const { return this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); } + bool LearningSettings::isNumberOfSampledPathsUntilPrecomputationSet() const { + return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet(); + } + + uint_fast64_t LearningSettings::getNumberOfSampledPathsUntilPrecomputation() const { + return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); + } + + LearningSettings::NextStateHeuristic LearningSettings::getNextStateHeuristic() const { + std::string nextStateHeuristicAsString = this->getOption(nextStateHeuristicOptionName).getArgumentByName("name").getValueAsString(); + if (nextStateHeuristicAsString == "probdiff") { + return LearningSettings::NextStateHeuristic::DifferenceWeightedProbability; + } else if (nextStateHeuristicAsString == "prob") { + return LearningSettings::NextStateHeuristic::Probability; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'."); + } + bool LearningSettings::check() const { - bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() || this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet(); + bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() || + this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || + this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() || + this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning || !optionsSet, "Learning engine is not selected, so setting options for it has no effect."); return true; } diff --git a/src/settings/modules/LearningSettings.h b/src/settings/modules/LearningSettings.h index 8db1fe44a..2aa0d61a7 100644 --- a/src/settings/modules/LearningSettings.h +++ b/src/settings/modules/LearningSettings.h @@ -15,6 +15,9 @@ namespace storm { // An enumeration of all available precomputation types. enum class PrecomputationType { Local, Global }; + // The available heuristics to choose the next state. + enum class NextStateHeuristic { DifferenceWeightedProbability, Probability }; + /*! * Creates a new set of learning settings that is managed by the given manager. * @@ -49,6 +52,27 @@ namespace storm { * @return The number of exploration steps to perform until a precomputation is triggered. */ uint_fast64_t getNumberOfExplorationStepsUntilPrecomputation() const; + + /* + * Retrieves whether the option to perform a precomputation after a given number of sampled paths was set. + * + * @return True iff a precomputation after a given number of sampled paths is to be performed. + */ + bool isNumberOfSampledPathsUntilPrecomputationSet() const; + + /*! + * Retrieves the number of paths to sample until a precomputation is triggered. + * + * @return The the number of paths to sample until a precomputation is triggered. + */ + uint_fast64_t getNumberOfSampledPathsUntilPrecomputation() const; + + /*! + * Retrieves the selected next-state heuristic. + * + * @return The selected next-state heuristic. + */ + NextStateHeuristic getNextStateHeuristic() const; virtual bool check() const override; @@ -59,6 +83,8 @@ namespace storm { // Define the string names of the options as constants. static const std::string precomputationTypeOptionName; static const std::string numberOfExplorationStepsUntilPrecomputationOptionName; + static const std::string numberOfSampledPathsUntilPrecomputationOptionName; + static const std::string nextStateHeuristicOptionName; }; } // namespace modules } // namespace settings