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

Introduced new settings for controlling the refinement strategy and whether to produce only upper and/or lower bounds

main
Tim Quatmann 5 years ago
parent
2d94e77f2a
commit
fa624d2a20
9 changed files with 280 additions and 205 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. 4
      src/storm-pomdp-cli/settings/PomdpSettings.cpp
  2. 150
      src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp
  3. 71
      src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h
  4. 80
      src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp
  5. 42
      src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h
  6. 27
      src/storm-pomdp-cli/storm-pomdp.cpp
  7. 43
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h
  8. 33
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
  9. 35
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h

4
src/storm-pomdp-cli/settings/PomdpSettings.cpp
View File

@ -31,7 +31,7 @@
#include "storm/settings/modules/HintSettings.h"
#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
#include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h"
#include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
namespace storm {
namespace settings {
@ -45,7 +45,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::BuildSettings>();
storm::settings::addModule<storm::settings::modules::POMDPSettings>();
storm::settings::addModule<storm::settings::modules::GridApproximationSettings>();
storm::settings::addModule<storm::settings::modules::BeliefExplorationSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();

150
src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp
View File

@ -0,0 +1,150 @@
#include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/SettingMemento.h"
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/ArgumentBuilder.h"
#include "storm/utility/NumberTraits.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace settings {
namespace modules {
const std::string BeliefExplorationSettings::moduleName = "belexpl";
const std::string refineOption = "refine";
const std::string resolutionOption = "resolution";
const std::string sizeThresholdOption = "size-threshold";
const std::string gapThresholdOption = "gap-threshold";
const std::string schedulerThresholdOption = "scheduler-threshold";
const std::string observationThresholdOption = "obs-threshold";
const std::string numericPrecisionOption = "numeric-precision";
BeliefExplorationSettings::BeliefExplorationSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, refineOption, false,"Refines the result bounds until reaching either the goal precision or the refinement step limit").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("prec","The goal precision.").setDefaultValueDouble(1e-4).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("steps","The number of allowed refinement steps (0 means no limit).").setDefaultValueUnsignedInteger(0).makeOptional().build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, resolutionOption, false,"Sets the resolution of the discretization and how it is increased in case of refinement").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("init","the initial resolution (higher means more precise)").setDefaultValueUnsignedInteger(12).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor","Multiplied to the resolution of refined observations (higher means more precise).").setDefaultValueDouble(2).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterValidator(1)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, observationThresholdOption, false,"Only observations whose score is below this threshold will be refined.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("init","initial threshold (higher means more precise").setDefaultValueDouble(0.1).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0,1)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor","Controlls how fast the threshold is increased in each refinement step (higher means more precise).").setDefaultValueDouble(0.1).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0,1)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, sizeThresholdOption, false,"Sets how many new states are explored or rewired in a refinement step and how this value is increased in case of refinement.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("init","initial limit (higher means more precise, 0 means automatic choice)").setDefaultValueUnsignedInteger(0).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor","Before each step the new threshold is set to the current state count times this number (higher means more precise).").setDefaultValueDouble(4).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(1)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, gapThresholdOption, false,"Sets how large the gap between known lower- and upper bounds at a beliefstate needs to be in order to explore").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("init","initial threshold (higher means less precise").setDefaultValueDouble(0.1).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor","Multiplied to the gap in each refinement step (higher means less precise).").setDefaultValueDouble(0.25).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0,1)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, schedulerThresholdOption, false,"Sets how much worse a sub-optimal choice can be in order to be included in the relevant explored fragment").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("init","initial threshold (higher means more precise").setDefaultValueDouble(1e-3).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor","Multiplied to the threshold in each refinement step (higher means more precise).").setDefaultValueDouble(1).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(1)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, numericPrecisionOption, false,"Sets the precision used to determine whether two belief-states are equal.").setIsAdvanced().addArgument(
storm::settings::ArgumentBuilder::createDoubleArgument("value","the precision").setDefaultValueDouble(1e-9).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0, 1)).build()).build());
}
bool BeliefExplorationSettings::isRefineSet() const {
return this->getOption(refineOption).getHasOptionBeenSet();
}
double BeliefExplorationSettings::getRefinePrecision() const {
return this->getOption(refineOption).getArgumentByName("prec").getValueAsDouble();
}
bool BeliefExplorationSettings::isRefineStepLimitSet() const {
return this->getOption(refineOption).getArgumentByName("steps").getValueAsUnsignedInteger() != 0;
}
uint64_t BeliefExplorationSettings::getRefineStepLimit() const {
assert(isRefineStepLimitSet());
return this->getOption(refineOption).getArgumentByName("steps").getValueAsUnsignedInteger();
}
uint64_t BeliefExplorationSettings::getResolutionInit() const {
return this->getOption(resolutionOption).getArgumentByName("init").getValueAsUnsignedInteger();
}
double BeliefExplorationSettings::getResolutionFactor() const {
return this->getOption(resolutionOption).getArgumentByName("factor").getValueAsDouble();
}
uint64_t BeliefExplorationSettings::getSizeThresholdInit() const {
return this->getOption(sizeThresholdOption).getArgumentByName("init").getValueAsUnsignedInteger();
}
double BeliefExplorationSettings::getSizeThresholdFactor() const {
return this->getOption(sizeThresholdOption).getArgumentByName("factor").getValueAsDouble();
}
double BeliefExplorationSettings::getGapThresholdInit() const {
return this->getOption(gapThresholdOption).getArgumentByName("init").getValueAsDouble();
}
double BeliefExplorationSettings::getGapThresholdFactor() const {
return this->getOption(gapThresholdOption).getArgumentByName("factor").getValueAsDouble();
}
double BeliefExplorationSettings::getOptimalChoiceValueThresholdInit() const {
return this->getOption(schedulerThresholdOption).getArgumentByName("init").getValueAsDouble();
}
double BeliefExplorationSettings::getOptimalChoiceValueThresholdFactor() const {
return this->getOption(schedulerThresholdOption).getArgumentByName("factor").getValueAsDouble();
}
double BeliefExplorationSettings::getObservationScoreThresholdInit() const {
return this->getOption(observationThresholdOption).getArgumentByName("init").getValueAsDouble();
}
double BeliefExplorationSettings::getObservationScoreThresholdFactor() const {
return this->getOption(observationThresholdOption).getArgumentByName("factor").getValueAsDouble();
}
bool BeliefExplorationSettings::isNumericPrecisionSetFromDefault() const {
return !this->getOption(numericPrecisionOption).getHasOptionBeenSet() || this->getOption(numericPrecisionOption).getArgumentByName("value").wasSetFromDefaultValue();
}
double BeliefExplorationSettings::getNumericPrecision() const {
return this->getOption(numericPrecisionOption).getArgumentByName("value").getValueAsDouble();
}
template<typename ValueType>
void BeliefExplorationSettings::setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) const {
options.refine = isRefineSet();
options.refinePrecision = getRefinePrecision();
if (isRefineStepLimitSet()) {
options.refineStepLimit = getRefineStepLimit();
}
options.resolutionInit = getResolutionInit();
options.resolutionFactor = storm::utility::convertNumber<ValueType>(getResolutionFactor());
options.sizeThresholdInit = getSizeThresholdInit();
options.sizeThresholdFactor = storm::utility::convertNumber<ValueType>(getSizeThresholdFactor());
options.gapThresholdInit = storm::utility::convertNumber<ValueType>(getGapThresholdInit());
options.gapThresholdFactor = storm::utility::convertNumber<ValueType>(getGapThresholdFactor());
options.optimalChoiceValueThresholdInit = storm::utility::convertNumber<ValueType>(getOptimalChoiceValueThresholdInit());
options.optimalChoiceValueThresholdFactor = storm::utility::convertNumber<ValueType>(getOptimalChoiceValueThresholdFactor());
options.obsThresholdInit = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdInit());
options.obsThresholdIncrementFactor = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdFactor());
options.numericPrecision = getNumericPrecision();
if (storm::NumberTraits<ValueType>::IsExact) {
if (isNumericPrecisionSetFromDefault()) {
STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used.");
options.numericPrecision = storm::utility::zero<ValueType>();
} else {
STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "A non-zero numeric precision was set although exact arithmethic is used. Results might be inexact.");
}
}
}
template void BeliefExplorationSettings::setValuesInOptionsStruct<double>(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<double>& options) const;
template void BeliefExplorationSettings::setValuesInOptionsStruct<storm::RationalNumber>(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<storm::RationalNumber>& options) const;
} // namespace modules
} // namespace settings
} // namespace storm

71
src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h
View File

@ -0,0 +1,71 @@
#pragma once
#include "storm-config.h"
#include "storm/settings/modules/ModuleSettings.h"
namespace storm {
namespace pomdp {
namespace modelchecker {
template<typename ValueType>
struct ApproximatePOMDPModelCheckerOptions;
}
}
namespace settings {
namespace modules {
/*!
* This class represents the settings for POMDP model checking.
*/
class BeliefExplorationSettings : public ModuleSettings {
public:
/*!
* Creates a new set of POMDP settings.
*/
BeliefExplorationSettings();
virtual ~BeliefExplorationSettings() = default;
bool isRefineSet() const;
double getRefinePrecision() const;
bool isRefineStepLimitSet() const;
uint64_t getRefineStepLimit() const;
/// Discretization Resolution
uint64_t getResolutionInit() const;
double getResolutionFactor() const;
/// The maximal number of newly expanded MDP states in a refinement step
uint64_t getSizeThresholdInit() const;
double getSizeThresholdFactor() const;
/// Controls how large the gap between known lower- and upper bounds at a beliefstate needs to be in order to explore
double getGapThresholdInit() const;
double getGapThresholdFactor() const;
/// Controls whether "almost optimal" choices will be considered optimal
double getOptimalChoiceValueThresholdInit() const;
double getOptimalChoiceValueThresholdFactor() const;
/// Controls which observations are refined.
double getObservationScoreThresholdInit() const;
double getObservationScoreThresholdFactor() const;
/// Used to determine whether two beliefs are equal
bool isNumericPrecisionSetFromDefault() const;
double getNumericPrecision() const;
template<typename ValueType>
void setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) const;
// The name of the module.
static const std::string moduleName;
private:
};
} // namespace modules
} // namespace settings
} // namespace storm

80
src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp
View File

@ -1,80 +0,0 @@
#include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/SettingMemento.h"
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/ArgumentBuilder.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace settings {
namespace modules {
const std::string GridApproximationSettings::moduleName = "grid";
const std::string refineOption = "refine";
const std::string resolutionOption = "resolution";
const std::string limitBeliefExplorationOption = "limit-exploration";
const std::string numericPrecisionOption = "numeric-precision";
const std::string cacheSimplicesOption = "cache-simplices";
const std::string unfoldBeliefMdpOption = "unfold-belief-mdp";
GridApproximationSettings::GridApproximationSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, refineOption, false,"Enables automatic refinement of the grid until the goal precision is reached").addArgument(
storm::settings::ArgumentBuilder::createDoubleArgument("precision","Allowed difference between upper and lower bound of the result.").setDefaultValueDouble(1e-6).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, resolutionOption, false,"Sets the (initial-) resolution of the grid (higher means more precise results)").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value","the resolution").setDefaultValueUnsignedInteger(10).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, limitBeliefExplorationOption, false,"Sets whether the belief space exploration is stopped if upper and lower bound are close").addArgument(
storm::settings::ArgumentBuilder::createDoubleArgument("threshold","the difference between upper and lower bound when to stop").setDefaultValueDouble(0.0).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, numericPrecisionOption, false,"Sets the precision used to determine whether two belief-states are equal.").addArgument(
storm::settings::ArgumentBuilder::createDoubleArgument("value","the precision").setDefaultValueDouble(1e-9).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0, 1)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, cacheSimplicesOption, false,"Enables caching of simplices which requires more memory but can be faster.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, unfoldBeliefMdpOption, false,"Sets the (initial-) size threshold of the unfolded belief MDP (higher means more precise results, 0 means automatic choice)").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value","the maximal number of states").setDefaultValueUnsignedInteger(0).build()).build());
}
bool GridApproximationSettings::isRefineSet() const {
return this->getOption(refineOption).getHasOptionBeenSet();
}
double GridApproximationSettings::getRefinementPrecision() const {
return this->getOption(refineOption).getArgumentByName("precision").getValueAsDouble();
}
uint64_t GridApproximationSettings::getGridResolution() const {
return this->getOption(resolutionOption).getArgumentByName("value").getValueAsUnsignedInteger();
}
double GridApproximationSettings::getExplorationThreshold() const {
return this->getOption(limitBeliefExplorationOption).getArgumentByName("threshold").getValueAsDouble();
}
bool GridApproximationSettings::isNumericPrecisionSetFromDefault() const {
return !this->getOption(numericPrecisionOption).getHasOptionBeenSet() || this->getOption(numericPrecisionOption).getArgumentByName("value").wasSetFromDefaultValue();
}
double GridApproximationSettings::getNumericPrecision() const {
return this->getOption(numericPrecisionOption).getArgumentByName("value").getValueAsDouble();
}
bool GridApproximationSettings::isCacheSimplicesSet() const {
return this->getOption(cacheSimplicesOption).getHasOptionBeenSet();
}
bool GridApproximationSettings::isUnfoldBeliefMdpSizeThresholdSet() const {
return this->getOption(unfoldBeliefMdpOption).getHasOptionBeenSet();
}
uint64_t GridApproximationSettings::getUnfoldBeliefMdpSizeThreshold() const {
return this->getOption(unfoldBeliefMdpOption).getArgumentByName("value").getValueAsUnsignedInteger();
}
} // namespace modules
} // namespace settings
} // namespace storm

42
src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h
View File

@ -1,42 +0,0 @@
#pragma once
#include "storm-config.h"
#include "storm/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for POMDP model checking.
*/
class GridApproximationSettings : public ModuleSettings {
public:
/*!
* Creates a new set of POMDP settings.
*/
GridApproximationSettings();
virtual ~GridApproximationSettings() = default;
bool isRefineSet() const;
double getRefinementPrecision() const;
uint64_t getGridResolution() const;
double getExplorationThreshold() const;
bool isNumericPrecisionSetFromDefault() const;
double getNumericPrecision() const;
bool isCacheSimplicesSet() const;
bool isUnfoldBeliefMdpSizeThresholdSet() const;
uint64_t getUnfoldBeliefMdpSizeThreshold() const;
// The name of the module.
static const std::string moduleName;
private:
};
} // namespace modules
} // namespace settings
} // namespace storm

27
src/storm-pomdp-cli/storm-pomdp.cpp
View File

@ -5,7 +5,7 @@
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
#include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h"
#include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
#include "storm-pomdp-cli/settings/PomdpSettings.h"
#include "storm/analysis/GraphConditions.h"
@ -114,28 +114,9 @@ namespace storm {
bool analysisPerformed = false;
if (pomdpSettings.isBeliefExplorationSet()) {
STORM_PRINT_AND_LOG("Exploring the belief MDP... ");
auto const& gridSettings = storm::settings::getModule<storm::settings::modules::GridApproximationSettings>();
typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::models::sparse::Pomdp<ValueType>>::Options options;
std::cout << "TODO: create and read from new settings!" << std::endl;
// options.initialGridResolution = gridSettings.getGridResolution();
// options.explorationThreshold = storm::utility::convertNumber<ValueType>(gridSettings.getExplorationThreshold());
options.refine = gridSettings.isRefineSet();
options.unfold = pomdpSettings.isBeliefExplorationUnfoldSet();
options.discretize = pomdpSettings.isBeliefExplorationDiscretizeSet();
// options.refinementPrecision = storm::utility::convertNumber<ValueType>(gridSettings.getRefinementPrecision());
// options.numericPrecision = storm::utility::convertNumber<ValueType>(gridSettings.getNumericPrecision());
// options.cacheSubsimplices = gridSettings.isCacheSimplicesSet();
if (gridSettings.isUnfoldBeliefMdpSizeThresholdSet()) {
//options.beliefMdpSizeThreshold = gridSettings.getUnfoldBeliefMdpSizeThreshold();
}
if (storm::NumberTraits<ValueType>::IsExact) {
if (gridSettings.isNumericPrecisionSetFromDefault()) {
STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used.");
options.numericPrecision = storm::utility::zero<ValueType>();
} else {
STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "A non-zero numeric precision was set although exact arithmethic is used. Results might be inexact.");
}
}
auto options = storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>(pomdpSettings.isBeliefExplorationDiscretizeSet(), pomdpSettings.isBeliefExplorationUnfoldSet());
auto const& beliefExplorationSettings = storm::settings::getModule<storm::settings::modules::BeliefExplorationSettings>();
beliefExplorationSettings.setValuesInOptionsStruct(options);
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::models::sparse::Pomdp<ValueType>> checker(*pomdp, options);
auto result = checker.check(formula);
checker.printStatisticsToStream(std::cout);

43
src/storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h
View File

@ -0,0 +1,43 @@
#pragma once
#include <boost/optional.hpp>
#include "storm/utility/constants.h"
#include "storm/utility/NumberTraits.h"
namespace storm {
namespace pomdp {
namespace modelchecker {
template<typename ValueType>
struct ApproximatePOMDPModelCheckerOptions {
ApproximatePOMDPModelCheckerOptions(bool discretize, bool unfold) : discretize(discretize), unfold(unfold) {
// Intentionally left empty
}
bool discretize;
bool unfold;
bool refine = false;
boost::optional<uint64_t> refineStepLimit;
ValueType refinePrecision = storm::utility::zero<ValueType>();
// Controlparameters for the refinement heuristic
// Discretization Resolution
uint64_t resolutionInit = 2;
ValueType resolutionFactor = storm::utility::convertNumber<ValueType, uint64_t>(2);
// The maximal number of newly expanded MDP states in a refinement step
uint64_t sizeThresholdInit = 0;
ValueType sizeThresholdFactor = storm::utility::convertNumber<ValueType,uint64_t>(4);
// Controls how large the gap between known lower- and upper bounds at a beliefstate needs to be in order to explore
ValueType gapThresholdInit = storm::utility::convertNumber<ValueType>(0.1);
ValueType gapThresholdFactor = storm::utility::convertNumber<ValueType>(0.25);
// Controls whether "almost optimal" choices will be considered optimal
ValueType optimalChoiceValueThresholdInit = storm::utility::convertNumber<ValueType>(1e-3);
ValueType optimalChoiceValueThresholdFactor = storm::utility::one<ValueType>();
// Controls which observations are refined.
ValueType obsThresholdInit = storm::utility::convertNumber<ValueType>(0.1);
ValueType obsThresholdIncrementFactor = storm::utility::convertNumber<ValueType>(0.1);
ValueType numericPrecision = storm::NumberTraits<ValueType>::IsExact ? storm::utility::zero<ValueType>() : storm::utility::convertNumber<ValueType>(1e-9); /// Used to decide whether two beliefs are equal
};
}
}
}

33
src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
View File

@ -27,25 +27,6 @@
namespace storm {
namespace pomdp {
namespace modelchecker {
template<typename PomdpModelType, typename BeliefValueType>
ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Options::Options() {
discretize = false;
unfold = false;
refine = false;
resolutionInit = 2;
resolutionFactor = storm::utility::convertNumber<ValueType,uint64_t>(2);
sizeThresholdInit = 0; // automatic
sizeThresholdFactor = 4;
gapThresholdInit = storm::utility::convertNumber<ValueType>(0.1);
gapThresholdFactor = storm::utility::convertNumber<ValueType>(0.25);
optimalChoiceValueThresholdInit = storm::utility::convertNumber<ValueType>(1e-3);
optimalChoiceValueThresholdFactor = storm::utility::one<ValueType>();
obsThresholdInit = storm::utility::convertNumber<ValueType>(0.1);
obsThresholdIncrementFactor = storm::utility::convertNumber<ValueType>(0.1);
numericPrecision = storm::NumberTraits<ValueType>::IsExact ? storm::utility::zero<ValueType>() : storm::utility::convertNumber<ValueType>(1e-9);
}
template<typename PomdpModelType, typename BeliefValueType>
ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result::Result(ValueType lower, ValueType upper) : lowerBound(lower), upperBound(upper) {
@ -278,9 +259,9 @@ namespace storm {
// Start refinement
statistics.refinementSteps = 0;
STORM_LOG_WARN_COND(options.refineStepLimit.is_initialized() || options.refinePrecision.is_initialized(), "No termination criterion for refinement given. Consider to specify a steplimit, precisionlimit or timeout");
STORM_LOG_WARN_COND(!options.refinePrecision.is_initialized() || (options.unfold && options.discretize), "Refinement goal precision is given, but only one bound is going to be refined.");
while ((!options.refineStepLimit.is_initialized() || statistics.refinementSteps < options.refineStepLimit.get()) && (!options.refinePrecision.is_initialized() || result.diff() > options.refinePrecision.get())) {
STORM_LOG_WARN_COND(options.refineStepLimit.is_initialized() || !storm::utility::isZero(options.refinePrecision), "No termination criterion for refinement given. Consider to specify a steplimit, a non-zero precisionlimit, or a timeout");
STORM_LOG_WARN_COND(storm::utility::isZero(options.refinePrecision) || (options.unfold && options.discretize), "Refinement goal precision is given, but only one bound is going to be refined.");
while ((!options.refineStepLimit.is_initialized() || statistics.refinementSteps < options.refineStepLimit.get()) && result.diff() > options.refinePrecision) {
if (storm::utility::resources::isTerminate()) {
break;
}
@ -295,7 +276,7 @@ namespace storm {
overApproximation->takeCurrentValuesAsUpperBounds();
}
overApproxHeuristicPar.gapThreshold *= options.gapThresholdFactor;
overApproxHeuristicPar.sizeThreshold = overApproximation->getExploredMdp()->getNumberOfStates() * options.sizeThresholdFactor;
overApproxHeuristicPar.sizeThreshold = storm::utility::convertNumber<uint64_t, ValueType>(storm::utility::convertNumber<ValueType, uint64_t>(overApproximation->getExploredMdp()->getNumberOfStates()) * options.sizeThresholdFactor);
overApproxHeuristicPar.observationThreshold += options.obsThresholdIncrementFactor * (storm::utility::one<ValueType>() - overApproxHeuristicPar.observationThreshold);
overApproxHeuristicPar.optimalChoiceValueEpsilon *= options.optimalChoiceValueThresholdFactor;
buildOverApproximation(targetObservations, min, rewardModelName.is_initialized(), true, overApproxHeuristicPar, observationResolutionVector, overApproxBeliefManager, overApproximation);
@ -306,10 +287,10 @@ namespace storm {
}
}
if (options.unfold && (!options.refinePrecision.is_initialized() || result.diff() > options.refinePrecision.get())) {
if (options.unfold && result.diff() > options.refinePrecision) {
// Refine under-approximation
overApproxHeuristicPar.gapThreshold *= options.gapThresholdFactor;
underApproxHeuristicPar.sizeThreshold = underApproximation->getExploredMdp()->getNumberOfStates() * options.sizeThresholdFactor;
overApproxHeuristicPar.sizeThreshold = storm::utility::convertNumber<uint64_t, ValueType>(storm::utility::convertNumber<ValueType, uint64_t>(underApproximation->getExploredMdp()->getNumberOfStates()) * options.sizeThresholdFactor);
overApproxHeuristicPar.optimalChoiceValueEpsilon *= options.optimalChoiceValueThresholdFactor;
buildUnderApproximation(targetObservations, min, rewardModelName.is_initialized(), true, underApproxHeuristicPar, underApproxBeliefManager, underApproximation);
if (underApproximation->hasComputedValues()) {
@ -403,7 +384,7 @@ namespace storm {
STORM_LOG_DEBUG("Refining the resolution of " << refinedObservations.getNumberOfSetBits() << "/" << refinedObservations.size() << " observations.");
for (auto const& obs : refinedObservations) {
// Increment the resolution at the refined observations
observationResolutionVector[obs] *= 2;
observationResolutionVector[obs] = storm::utility::convertNumber<uint64_t, ValueType>(storm::utility::convertNumber<ValueType>(observationResolutionVector[obs]) * options.resolutionFactor);
}
overApproximation->restartExploration();
}

35
src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h
View File

@ -1,11 +1,10 @@
#include <cstdlib>
#include "storm/api/storm.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/utility/logging.h"
#include "storm-pomdp/storage/Belief.h"
#include "storm-pomdp/storage/BeliefManager.h"
#include "storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h"
#include "storm-pomdp/builder/BeliefMdpExplorer.h"
#include <boost/bimap.hpp>
#include "storm/storage/jani/Property.h"
@ -16,8 +15,7 @@ namespace storm {
namespace pomdp {
namespace modelchecker {
typedef boost::bimap<uint64_t, uint64_t> bsmap_type;
template<typename PomdpModelType, typename BeliefValueType = typename PomdpModelType::ValueType>
class ApproximatePOMDPModelchecker {
public:
@ -25,34 +23,7 @@ namespace storm {
typedef typename PomdpModelType::RewardModelType RewardModelType;
typedef storm::storage::BeliefManager<PomdpModelType, BeliefValueType> BeliefManagerType;
typedef storm::builder::BeliefMdpExplorer<PomdpModelType, BeliefValueType> ExplorerType;
struct Options {
Options();
bool discretize;
bool unfold;
bool refine;
boost::optional<uint64_t> refineStepLimit;
boost::optional<ValueType> refinePrecision;
// Controlparameters for the refinement heuristic
// Discretization Resolution
uint64_t resolutionInit;
ValueType resolutionFactor;
// The maximal number of newly expanded MDP states in a refinement step
uint64_t sizeThresholdInit;
uint64_t sizeThresholdFactor;
// Controls how large the gap between known lower- and upper bounds at a beliefstate needs to be in order to explore
ValueType gapThresholdInit;
ValueType gapThresholdFactor;
// Controls whether "almost optimal" choices will be considered optimal
ValueType optimalChoiceValueThresholdInit;
ValueType optimalChoiceValueThresholdFactor;
// Controls which observations are refined.
ValueType obsThresholdInit;
ValueType obsThresholdIncrementFactor;
ValueType numericPrecision; /// Used to decide whether two beliefs are equal
};
typedef ApproximatePOMDPModelCheckerOptions<ValueType> Options;
struct Result {
Result(ValueType lower, ValueType upper);

Write Preview
Loading…
Cancel
Save