sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added some statistics and options 

Former-commit-id: 1b6a9c20f6
tempestpy_adaptions
dehnert 9 years ago
parent
6d421a6fbe
commit
07e97e1977
4 changed files with 203 additions and 68 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 53
      src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
  2. 157
      src/modelchecker/reachability/SparseMdpLearningModelChecker.h
  3. 35
      src/settings/modules/LearningSettings.cpp
  4. 26
      src/settings/modules/LearningSettings.h

53
src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
View File

@ -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 ValueType>
typename SparseMdpLearningModelChecker<ValueType>::StateType SparseMdpLearningModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
// TODO: precompute this?
std::vector<ValueType> probabilities(explorationInformation.getRowOfMatrix(chosenAction).size());
std::transform(explorationInformation.getRowOfMatrix(chosenAction).begin(), explorationInformation.getRowOfMatrix(chosenAction).end(), probabilities.begin(), [&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) { return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation) ; } );
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
// if (row.size() == 1) {
// return row.front().getColumn();
// }
std::vector<ValueType> 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<StateType, ValueType> 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<StateType, ValueType> const& entry) {
return entry.getValue();
});
}
// Now sample according to the probabilities.
std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end());
StateType offset = distribution(randomGenerator);
return explorationInformation.getRowOfMatrix(chosenAction)[offset].getColumn();
return row[offset].getColumn();
}
template<typename ValueType>
bool SparseMdpLearningModelChecker<ValueType>::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).

157
src/modelchecker/reachability/SparseMdpLearningModelChecker.h
View File

@ -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<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> 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<StateType> getInitialStates() {
return generator.getInitialStates(stateToIdCallback);
}
storm::generator::StateBehavior<ValueType, StateType> expand() {
return generator.expand(stateToIdCallback);
}
bool isTargetState() const {
return generator.satisfies(targetStateExpression);
}
storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
std::function<StateType (storm::generator::CompressedState const&)> 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<ActionType>::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(localPrecomputation), numberOfExplorationStepsUntilPrecomputation(numberOfExplorationStepsUntilPrecomputation) {
// Intentionally left empty.
ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::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<StateType> stateStorage;
@ -108,6 +81,9 @@ namespace storm {
bool localPrecomputation;
uint_fast64_t numberOfExplorationStepsUntilPrecomputation;
boost::optional<uint_fast64_t> numberOfSampledPathsUntilPrecomputation;
storm::settings::modules::LearningSettings::NextStateHeuristic nextStateHeuristic;
void setInitialStates(std::vector<StateType> 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<StateType> getInitialStates() {
return generator.getInitialStates(stateToIdCallback);
}
storm::generator::StateBehavior<ValueType, StateType> expand() {
return generator.expand(stateToIdCallback);
}
bool isTargetState() const {
return generator.satisfies(targetStateExpression);
}
storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback;
storm::expressions::Expression targetStateExpression;
};
// A struct containg the lower and upper bounds per state and action.

35
src/settings/modules/LearningSettings.cpp
View File

@ -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<std::string> 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<std::string> 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;
}

26
src/settings/modules/LearningSettings.h
View File

@ -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

Write Preview
Loading…
Cancel
Save