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

Added timing and caching of subsimplex computation results

tempestpy_adaptions
Alexander Bork 5 years ago
parent
d814942997
commit
3bd910f42b
5 changed files with 117 additions and 41 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. 17
      src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
  2. 4
      src/storm-pomdp-cli/settings/modules/POMDPSettings.h
  3. 42
      src/storm-pomdp-cli/storm-pomdp.cpp
  4. 85
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
  5. 10
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h

17
src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
View File

@ -14,6 +14,7 @@ namespace storm {
const std::string POMDPSettings::moduleName = "pomdp";
const std::string exportAsParametricModelOption = "parametric-drn";
const std::string gridApproximationOption = "gridapproximation";
const std::string qualitativeReductionOption = "qualitativereduction";
const std::string analyzeUniqueObservationsOption = "uniqueobservations";
const std::string mecReductionOption = "mecreduction";
@ -37,6 +38,13 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, gridApproximationOption, false,
"Analyze the POMDP using grid approximation.").addArgument(
storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("resolution",
"the resolution of the grid").setDefaultValueUnsignedInteger(
10).addValidatorUnsignedInteger(
storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(
0)).build()).build());
}
bool POMDPSettings::isExportToParametricSet() const {
@ -62,6 +70,15 @@ namespace storm {
bool POMDPSettings::isSelfloopReductionSet() const {
return this->getOption(selfloopReductionOption).getHasOptionBeenSet();
}
bool POMDPSettings::isGridApproximationSet() const {
return this->getOption(gridApproximationOption).getHasOptionBeenSet();
}
uint64_t POMDPSettings::getGridResolution() const {
return this->getOption(gridApproximationOption).getArgumentByName(
"resolution").getValueAsUnsignedInteger();
}
uint64_t POMDPSettings::getMemoryBound() const {
return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger();

4
src/storm-pomdp-cli/settings/modules/POMDPSettings.h
View File

@ -25,6 +25,8 @@ namespace storm {
std::string getExportToParametricFilename() const;
bool isQualitativeReductionSet() const;
bool isGridApproximationSet() const;
bool isAnalyzeUniqueObservationsSet() const;
bool isMecReductionSet() const;
bool isSelfloopReductionSet() const;
@ -32,6 +34,8 @@ namespace storm {
bool isTransformBinarySet() const;
std::string getFscApplicationTypeString() const;
uint64_t getMemoryBound() const;
uint64_t getGridResolution() const;
storm::storage::PomdpMemoryPattern getMemoryPattern() const;
bool check() const override;

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

@ -42,6 +42,8 @@
#include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h"
#include "storm/api/storm.h"
#include <typeinfo>
/*!
* Initialize the settings manager.
*/
@ -113,10 +115,6 @@ int main(const int argc, const char** argv) {
STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP.");
std::shared_ptr<storm::models::sparse::Pomdp<storm::RationalNumber>> pomdp = model->template as<storm::models::sparse::Pomdp<storm::RationalNumber>>();
// For ease of testing
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::RationalNumber> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::RationalNumber>();
checker.computeReachabilityProbability(*pomdp, std::set<uint32_t>({7}), false, 10);
std::shared_ptr<storm::logic::Formula const> formula;
if (!symbolicInput.properties.empty()) {
formula = symbolicInput.properties.front().getRawFormula();
@ -149,6 +147,42 @@ int main(const int argc, const char** argv) {
STORM_PRINT_AND_LOG(" done." << std::endl);
std::cout << "actual reduction not yet implemented..." << std::endl;
}
if (pomdpSettings.isGridApproximationSet()) {
storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula();
storm::logic::Formula const &subformula1 = probFormula.getSubformula();
std::set<uint32_t> targetObservationSet;
//TODO refactor
bool validFormula = false;
if (subformula1.isEventuallyFormula()) {
storm::logic::EventuallyFormula const &eventuallyFormula = subformula1.asEventuallyFormula();
storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
}
}
}
}
STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
"The formula is not supported by the grid approximation");
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::RationalNumber> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::RationalNumber>();
storm::RationalNumber overRes = storm::utility::one<storm::RationalNumber>();
storm::RationalNumber underRes = storm::utility::zero<storm::RationalNumber>();
std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<storm::RationalNumber>> result;
result = checker.computeReachabilityProbability(*pomdp, targetObservationSet,
probFormula.getOptimalityType() ==
storm::OptimizationDirection::Minimize,
pomdpSettings.getGridResolution() + gridIncrease);
overRes = result->OverapproximationValue;
underRes = result->UnderapproximationValue;
}
} else if (formula->isRewardOperatorFormula()) {
if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) {
STORM_PRINT_AND_LOG("Eliminating self-loop choices ...");

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

@ -22,11 +22,11 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
/*std::unique_ptr<POMDPCheckResult>*/ void
std::unique_ptr<POMDPCheckResult<ValueType>>
ApproximatePOMDPModelchecker<ValueType, RewardModelType>::computeReachabilityProbability(
storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
std::set<uint32_t> targetObservations, bool min, uint64_t gridResolution) {
//TODO add timing
storm::utility::Stopwatch beliefGridTimer(true);
uint64_t maxIterations = 100;
bool finished = false;
uint64_t iteration = 0;
@ -46,7 +46,9 @@ namespace storm {
constructBeliefGrid(pomdp, targetObservations, gridResolution, beliefList, beliefGrid, beliefIsTarget,
nextId);
nextId = beliefList.size();
beliefGridTimer.stop();
storm::utility::Stopwatch overApproxTimer(true);
// ID -> Value
std::map<uint64_t, ValueType> result;
std::map<uint64_t, ValueType> result_backup;
@ -58,6 +60,7 @@ namespace storm {
// current ID -> action -> next ID
std::map<uint64_t, std::vector<std::map<uint32_t, uint64_t>>> nextBelieves;
storm::utility::Stopwatch nextBeliefGeneration(true);
for (size_t i = 0; i < beliefGrid.size(); ++i) {
auto currentBelief = beliefGrid[i];
bool isTarget = beliefIsTarget[currentBelief.id];
@ -68,6 +71,7 @@ namespace storm {
result.emplace(std::make_pair(currentBelief.id, storm::utility::zero<ValueType>()));
result_backup.emplace(std::make_pair(currentBelief.id, storm::utility::zero<ValueType>()));
//TODO put this in extra function
std::vector<std::map<uint32_t, ValueType>> observationProbabilitiesInAction;
std::vector<std::map<uint32_t, uint64_t>> nextBelievesInAction;
@ -98,9 +102,17 @@ namespace storm {
nextBelieves.emplace(std::make_pair(currentBelief.id, nextBelievesInAction));
}
}
nextBeliefGeneration.stop();
//Use chaching to avoid multiple computation of the subsimplices and lambdas
std::map<uint64_t, std::vector<std::vector<ValueType>>> subSimplexCache;
std::map<uint64_t, std::vector<ValueType>> lambdaCache;
STORM_PRINT("Time generation of next believes: " << nextBeliefGeneration << std::endl)
// Value Iteration
auto cc = storm::utility::ConstantsComparator<ValueType>();
while (!finished && iteration < maxIterations) {
storm::utility::Stopwatch iterationTimer(true);
STORM_LOG_DEBUG("Iteration " << iteration + 1);
bool improvement = false;
for (size_t i = 0; i < beliefGrid.size(); ++i) {
@ -123,10 +135,20 @@ namespace storm {
uint32_t observation = iter->first;
storm::pomdp::Belief<ValueType> nextBelief = beliefList[nextBelieves[currentBelief.id][action][observation]];
// compute subsimplex and lambdas according to the Lovejoy paper to approximate the next belief
std::pair<std::vector<std::vector<ValueType>>, std::vector<ValueType>> temp = computeSubSimplexAndLambdas(
nextBelief.probabilities, gridResolution);
std::vector<std::vector<ValueType>> subSimplex = temp.first;
std::vector<ValueType> lambdas = temp.second;
// cache the values to not always re-calculate
std::vector<std::vector<ValueType>> subSimplex;
std::vector<ValueType> lambdas;
if (subSimplexCache.count(nextBelief.id) > 0) {
subSimplex = subSimplexCache[nextBelief.id];
lambdas = lambdaCache[nextBelief.id];
} else {
std::pair<std::vector<std::vector<ValueType>>, std::vector<ValueType>> temp = computeSubSimplexAndLambdas(
nextBelief.probabilities, gridResolution);
subSimplex = temp.first;
lambdas = temp.second;
subSimplexCache[nextBelief.id] = subSimplex;
lambdaCache[nextBelief.id] = lambdas;
}
auto sum = storm::utility::zero<ValueType>();
for (size_t j = 0; j < lambdas.size(); ++j) {
@ -138,17 +160,11 @@ namespace storm {
currentValue += iter->second * sum;
}
// Update the selected actions TODO make this nicer
// Update the selected actions
if ((min && cc.isLess(storm::utility::zero<ValueType>(), chosenValue - currentValue)) ||
(!min &&
cc.isLess(storm::utility::zero<ValueType>(), currentValue - chosenValue))) {
chosenValue = currentValue;
chosenActionIndex = action;
} else if ((min && cc.isEqual(storm::utility::zero<ValueType>(),
chosenValue - currentValue)) ||
(!min &&
cc.isEqual(storm::utility::zero<ValueType>(),
currentValue - chosenValue))) {
cc.isLess(storm::utility::zero<ValueType>(), currentValue - chosenValue)) ||
cc.isEqual(storm::utility::zero<ValueType>(), chosenValue - currentValue)) {
chosenValue = currentValue;
chosenActionIndex = action;
}
@ -171,9 +187,11 @@ namespace storm {
result_backup[iter->first] = result[iter->first];
}
++iteration;
iterationTimer.stop();
STORM_PRINT("Iteration " << iteration << ": " << iterationTimer << std::endl);
}
STORM_PRINT("Grid approximation took " << iteration << " iterations" << std::endl);
STORM_PRINT("Overapproximation took " << iteration << " iterations" << std::endl);
beliefGrid.push_back(initialBelief);
beliefIsTarget.push_back(
@ -192,9 +210,10 @@ namespace storm {
initSubSimplex[j])];
}
}
overApproxTimer.stop();
// Now onto the under-approximation
storm::utility::Stopwatch underApproxTimer(true);
std::set<uint64_t> visitedBelieves;
std::deque<uint64_t> believesToBeExpanded;
std::map<uint64_t, uint64_t> beliefStateMap;
@ -243,12 +262,6 @@ namespace storm {
believesToBeExpanded.pop_front();
}
for (size_t i = 0; i < transitions.size(); ++i) {
for (auto const &transition : transitions[i]) {
STORM_LOG_DEBUG(
"Transition: " << i << " -- " << transition.second << "--> " << transition.first);
}
}
storm::models::sparse::StateLabeling labeling(transitions.size());
labeling.addLabel("init");
labeling.addLabel("target");
@ -276,8 +289,17 @@ namespace storm {
ValueType resultValue = res->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
STORM_PRINT("Time Belief Grid Generation: " << beliefGridTimer << std::endl
<< "Time Overapproximation: " << overApproxTimer
<< std::endl
<< "Time Underapproximation: " << underApproxTimer
<< std::endl);
STORM_PRINT("Over-Approximation Result: " << overApprox << std::endl);
STORM_PRINT("Under-Approximation Result: " << resultValue << std::endl);
return std::make_unique<POMDPCheckResult<ValueType>>(
POMDPCheckResult<ValueType>{overApprox, resultValue});
}
template<typename ValueType, typename RewardModelType>
@ -311,9 +333,10 @@ namespace storm {
uint64_t gridResolution, uint64_t currentBeliefId, uint64_t nextId, bool min) {
auto cc = storm::utility::ConstantsComparator<ValueType>();
storm::pomdp::Belief<ValueType> currentBelief = beliefList[currentBeliefId];
//TODO put this in extra function
std::vector<std::map<uint32_t, ValueType>> observationProbabilitiesInAction;
std::vector<std::map<uint32_t, uint64_t>> nextBelievesInAction;
uint64_t numChoices = pomdp.getNumberOfChoices(
pomdp.getStatesWithObservation(currentBelief.observation).front());
for (uint64_t action = 0; action < numChoices; ++action) {
@ -354,8 +377,7 @@ namespace storm {
storm::pomdp::Belief<ValueType> nextBelief = beliefList[nextBelieves[currentBelief.id][action][observation]];
// compute subsimplex and lambdas according to the Lovejoy paper to approximate the next belief
auto temp = computeSubSimplexAndLambdas(
nextBelief.probabilities, gridResolution);
auto temp = computeSubSimplexAndLambdas(nextBelief.probabilities, gridResolution);
std::vector<std::vector<ValueType>> subSimplex = temp.first;
std::vector<ValueType> lambdas = temp.second;
@ -369,15 +391,11 @@ namespace storm {
currentValue += iter->second * sum;
}
// Update the selected actions TODO make this nicer
// Update the selected actions
if ((min && cc.isLess(storm::utility::zero<ValueType>(), chosenValue - currentValue)) ||
(!min &&
cc.isLess(storm::utility::zero<ValueType>(), currentValue - chosenValue))) {
chosenValue = currentValue;
chosenActionIndex = action;
} else if ((min && cc.isEqual(storm::utility::zero<ValueType>(), chosenValue - currentValue)) ||
(!min &&
cc.isEqual(storm::utility::zero<ValueType>(), currentValue - chosenValue))) {
cc.isLess(storm::utility::zero<ValueType>(), currentValue - chosenValue)) ||
cc.isEqual(storm::utility::zero<ValueType>(), chosenValue - currentValue)) {
chosenValue = currentValue;
chosenActionIndex = action;
}
@ -561,7 +579,6 @@ namespace storm {
}
lambdas[0] = storm::utility::one<ValueType>() - sum;
//TODO add assertion that we are close enough
return std::make_pair(subSimplex, lambdas);
}

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

@ -9,19 +9,23 @@
namespace storm {
namespace pomdp {
namespace modelchecker {
class POMDPCheckResult;
template<class ValueType>
struct POMDPCheckResult {
ValueType OverapproximationValue;
ValueType UnderapproximationValue;
};
template<class ValueType, typename RewardModelType = models::sparse::StandardRewardModel<ValueType>>
class ApproximatePOMDPModelchecker {
public:
explicit ApproximatePOMDPModelchecker();
/*std::unique_ptr<POMDPCheckResult>*/ void
std::unique_ptr<POMDPCheckResult<ValueType>>
computeReachabilityProbability(storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
std::set<uint32_t> targetObservations, bool min,
uint64_t gridResolution);
std::unique_ptr<POMDPCheckResult>
std::unique_ptr<POMDPCheckResult<ValueType>>
computeReachabilityReward(storm::models::sparse::Pomdp<ValueType, RewardModelType> const &pomdp,
std::set<uint32_t> target_observations, uint64_t gridResolution);

Write Preview
Loading…
Cancel
Save