Browse Source

Grid: Added cli setting to cache subsimplices.

main
Tim Quatmann 5 years ago
parent
commit
b3493b5888
  1. 7
      src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp
  2. 1
      src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h
  3. 1
      src/storm-pomdp-cli/storm-pomdp.cpp
  4. 24
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
  5. 2
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h

7
src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp

@ -18,6 +18,7 @@ namespace storm {
const std::string resolutionOption = "resolution"; const std::string resolutionOption = "resolution";
const std::string limitBeliefExplorationOption = "limit-exploration"; const std::string limitBeliefExplorationOption = "limit-exploration";
const std::string numericPrecisionOption = "numeric-precision"; const std::string numericPrecisionOption = "numeric-precision";
const std::string cacheSimplicesOption = "cache-simplices";
GridApproximationSettings::GridApproximationSettings() : ModuleSettings(moduleName) { GridApproximationSettings::GridApproximationSettings() : ModuleSettings(moduleName) {
@ -32,6 +33,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, numericPrecisionOption, false,"Sets the precision used to determine whether two belief-states are equal.").addArgument( 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()); 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());
} }
bool GridApproximationSettings::isRefineSet() const { bool GridApproximationSettings::isRefineSet() const {
@ -58,6 +61,10 @@ namespace storm {
return this->getOption(numericPrecisionOption).getArgumentByName("value").getValueAsDouble(); return this->getOption(numericPrecisionOption).getArgumentByName("value").getValueAsDouble();
} }
bool GridApproximationSettings::isCacheSimplicesSet() const {
return this->getOption(cacheSimplicesOption).getHasOptionBeenSet();
}
} // namespace modules } // namespace modules
} // namespace settings } // namespace settings
} // namespace storm } // namespace storm

1
src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h

@ -26,6 +26,7 @@ namespace storm {
double getExplorationThreshold() const; double getExplorationThreshold() const;
bool isNumericPrecisionSetFromDefault() const; bool isNumericPrecisionSetFromDefault() const;
double getNumericPrecision() const; double getNumericPrecision() const;
bool isCacheSimplicesSet() const;
// The name of the module. // The name of the module.
static const std::string moduleName; static const std::string moduleName;

1
src/storm-pomdp-cli/storm-pomdp.cpp

@ -92,6 +92,7 @@ namespace storm {
options.doRefinement = gridSettings.isRefineSet(); options.doRefinement = gridSettings.isRefineSet();
options.refinementPrecision = gridSettings.getRefinementPrecision(); options.refinementPrecision = gridSettings.getRefinementPrecision();
options.numericPrecision = gridSettings.getNumericPrecision(); options.numericPrecision = gridSettings.getNumericPrecision();
options.cacheSubsimplices = gridSettings.isCacheSimplicesSet();
if (storm::NumberTraits<ValueType>::IsExact) { if (storm::NumberTraits<ValueType>::IsExact) {
if (gridSettings.isNumericPrecisionSetFromDefault()) { if (gridSettings.isNumericPrecisionSetFromDefault()) {
STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used."); STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used.");

24
src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp

@ -34,6 +34,7 @@ namespace storm {
doRefinement = true; doRefinement = true;
refinementPrecision = storm::utility::convertNumber<ValueType>(1e-4); refinementPrecision = storm::utility::convertNumber<ValueType>(1e-4);
numericPrecision = storm::NumberTraits<ValueType>::IsExact ? storm::utility::zero<ValueType>() : storm::utility::convertNumber<ValueType>(1e-9); numericPrecision = storm::NumberTraits<ValueType>::IsExact ? storm::utility::zero<ValueType>() : storm::utility::convertNumber<ValueType>(1e-9);
cacheSubsimplices = false;
} }
template<typename ValueType, typename RewardModelType> template<typename ValueType, typename RewardModelType>
@ -41,7 +42,6 @@ namespace storm {
cc = storm::utility::ConstantsComparator<ValueType>(storm::utility::convertNumber<ValueType>(this->options.numericPrecision), false); cc = storm::utility::ConstantsComparator<ValueType>(storm::utility::convertNumber<ValueType>(this->options.numericPrecision), false);
useMdp = true; useMdp = true;
maxIterations = 1000; maxIterations = 1000;
cacheSubsimplices = false;
} }
template<typename ValueType, typename RewardModelType> template<typename ValueType, typename RewardModelType>
@ -299,7 +299,7 @@ namespace storm {
auto initTemp = computeSubSimplexAndLambdas(initialBelief.probabilities, observationResolutionVector[initialBelief.observation], pomdp.getNumberOfStates()); auto initTemp = computeSubSimplexAndLambdas(initialBelief.probabilities, observationResolutionVector[initialBelief.observation], pomdp.getNumberOfStates());
auto initSubSimplex = initTemp.first; auto initSubSimplex = initTemp.first;
auto initLambdas = initTemp.second; auto initLambdas = initTemp.second;
if (cacheSubsimplices) {
if (options.cacheSubsimplices) {
subSimplexCache[0] = initSubSimplex; subSimplexCache[0] = initSubSimplex;
lambdaCache[0] = initLambdas; lambdaCache[0] = initLambdas;
} }
@ -406,7 +406,7 @@ namespace storm {
//Triangulate here and put the possibly resulting belief in the grid //Triangulate here and put the possibly resulting belief in the grid
std::vector<std::map<uint64_t, ValueType>> subSimplex; std::vector<std::map<uint64_t, ValueType>> subSimplex;
std::vector<ValueType> lambdas; std::vector<ValueType> lambdas;
if (cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) {
if (options.cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) {
subSimplex = subSimplexCache[idNextBelief]; subSimplex = subSimplexCache[idNextBelief];
lambdas = lambdaCache[idNextBelief]; lambdas = lambdaCache[idNextBelief];
} else { } else {
@ -414,7 +414,7 @@ namespace storm {
observationResolutionVector[beliefList[idNextBelief].observation], pomdp.getNumberOfStates()); observationResolutionVector[beliefList[idNextBelief].observation], pomdp.getNumberOfStates());
subSimplex = temp.first; subSimplex = temp.first;
lambdas = temp.second; lambdas = temp.second;
if (cacheSubsimplices) {
if (options.cacheSubsimplices) {
subSimplexCache[idNextBelief] = subSimplex; subSimplexCache[idNextBelief] = subSimplex;
lambdaCache[idNextBelief] = lambdas; lambdaCache[idNextBelief] = lambdas;
} }
@ -600,7 +600,7 @@ namespace storm {
std::vector<std::map<uint64_t, ValueType>> subSimplex; std::vector<std::map<uint64_t, ValueType>> subSimplex;
std::vector<ValueType> lambdas; std::vector<ValueType> lambdas;
//TODO add caching //TODO add caching
if (cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) {
if (options.cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) {
subSimplex = subSimplexCache[idNextBelief]; subSimplex = subSimplexCache[idNextBelief];
lambdas = lambdaCache[idNextBelief]; lambdas = lambdaCache[idNextBelief];
} else { } else {
@ -609,7 +609,7 @@ namespace storm {
pomdp.getNumberOfStates()); pomdp.getNumberOfStates());
subSimplex = temp.first; subSimplex = temp.first;
lambdas = temp.second; lambdas = temp.second;
if (cacheSubsimplices) {
if (options.cacheSubsimplices) {
subSimplexCache[idNextBelief] = subSimplex; subSimplexCache[idNextBelief] = subSimplex;
lambdaCache[idNextBelief] = lambdas; lambdaCache[idNextBelief] = lambdas;
} }
@ -693,7 +693,7 @@ namespace storm {
std::vector<std::map<uint64_t, ValueType>> subSimplex; std::vector<std::map<uint64_t, ValueType>> subSimplex;
std::vector<ValueType> lambdas; std::vector<ValueType> lambdas;
/* TODO Caching /* TODO Caching
if (cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) {
if (options.cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) {
subSimplex = subSimplexCache[idNextBelief]; subSimplex = subSimplexCache[idNextBelief];
lambdas = lambdaCache[idNextBelief]; lambdas = lambdaCache[idNextBelief];
} else { */ } else { */
@ -702,7 +702,7 @@ namespace storm {
pomdp.getNumberOfStates()); pomdp.getNumberOfStates());
subSimplex = temp.first; subSimplex = temp.first;
lambdas = temp.second; lambdas = temp.second;
/*if (cacheSubsimplices) {
/*if (options.cacheSubsimplices) {
subSimplexCache[idNextBelief] = subSimplex; subSimplexCache[idNextBelief] = subSimplex;
lambdaCache[idNextBelief] = lambdas; lambdaCache[idNextBelief] = lambdas;
} }
@ -882,14 +882,14 @@ namespace storm {
// cache the values to not always re-calculate // cache the values to not always re-calculate
std::vector<std::map<uint64_t, ValueType>> subSimplex; std::vector<std::map<uint64_t, ValueType>> subSimplex;
std::vector<ValueType> lambdas; std::vector<ValueType> lambdas;
if (cacheSubsimplices && subSimplexCache.count(nextBelief.id) > 0) {
if (options.cacheSubsimplices && subSimplexCache.count(nextBelief.id) > 0) {
subSimplex = subSimplexCache[nextBelief.id]; subSimplex = subSimplexCache[nextBelief.id];
lambdas = lambdaCache[nextBelief.id]; lambdas = lambdaCache[nextBelief.id];
} else { } else {
auto temp = computeSubSimplexAndLambdas(nextBelief.probabilities, gridResolution, pomdp.getNumberOfStates()); auto temp = computeSubSimplexAndLambdas(nextBelief.probabilities, gridResolution, pomdp.getNumberOfStates());
subSimplex = temp.first; subSimplex = temp.first;
lambdas = temp.second; lambdas = temp.second;
if (cacheSubsimplices) {
if (options.cacheSubsimplices) {
subSimplexCache[nextBelief.id] = subSimplex; subSimplexCache[nextBelief.id] = subSimplex;
lambdaCache[nextBelief.id] = lambdas; lambdaCache[nextBelief.id] = lambdas;
} }
@ -937,7 +937,7 @@ namespace storm {
std::vector<ValueType> initialLambda; std::vector<ValueType> initialLambda;
std::vector<std::map<uint64_t, ValueType>> initialSubsimplex; std::vector<std::map<uint64_t, ValueType>> initialSubsimplex;
if (cacheSubsimplices) {
if (options.cacheSubsimplices) {
initialLambda = lambdaCache[0]; initialLambda = lambdaCache[0];
initialSubsimplex = subSimplexCache[0]; initialSubsimplex = subSimplexCache[0];
} else { } else {
@ -1007,7 +1007,7 @@ namespace storm {
std::map<uint64_t, std::vector<ValueType>> lambdaCache; std::map<uint64_t, std::vector<ValueType>> lambdaCache;
auto temp = computeSubSimplexAndLambdas(initialBelief.probabilities, gridResolution, pomdp.getNumberOfStates()); auto temp = computeSubSimplexAndLambdas(initialBelief.probabilities, gridResolution, pomdp.getNumberOfStates());
if (cacheSubsimplices) {
if (options.cacheSubsimplices) {
subSimplexCache[0] = temp.first; subSimplexCache[0] = temp.first;
lambdaCache[0] = temp.second; lambdaCache[0] = temp.second;
} }

2
src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h

@ -59,6 +59,7 @@ namespace storm {
bool doRefinement; /// Sets whether the bounds should be refined automatically until the refinement precision is reached bool doRefinement; /// Sets whether the bounds should be refined automatically until the refinement precision is reached
ValueType refinementPrecision; /// Used to decide when the refinement should terminate ValueType refinementPrecision; /// Used to decide when the refinement should terminate
ValueType numericPrecision; /// Used to decide whether two values are equal ValueType numericPrecision; /// Used to decide whether two values are equal
bool cacheSubsimplices; /// Enables caching of subsimplices
}; };
ApproximatePOMDPModelchecker(storm::models::sparse::Pomdp<ValueType, RewardModelType> const& pomdp, Options options = Options()); ApproximatePOMDPModelchecker(storm::models::sparse::Pomdp<ValueType, RewardModelType> const& pomdp, Options options = Options());
@ -349,7 +350,6 @@ namespace storm {
storm::utility::ConstantsComparator<ValueType> cc; storm::utility::ConstantsComparator<ValueType> cc;
// TODO: these should be obsolete, right? // TODO: these should be obsolete, right?
bool useMdp; bool useMdp;
bool cacheSubsimplices;
uint64_t maxIterations; uint64_t maxIterations;
}; };

Loading…
Cancel
Save