diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 2eb418dab..617cebf36 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -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(); diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 5b1d6cd9b..1e68871e8 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -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; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 8d33fc2d2..18f446d20 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -42,6 +42,8 @@ #include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h" #include "storm/api/storm.h" +#include + /*! * 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> pomdp = model->template as>(); - // For ease of testing - storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - checker.computeReachabilityProbability(*pomdp, std::set({7}), false, 10); - std::shared_ptr 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 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 checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); + storm::RationalNumber overRes = storm::utility::one(); + storm::RationalNumber underRes = storm::utility::zero(); + std::unique_ptr> 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 ..."); diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 24d312c7f..f8c9709aa 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -22,11 +22,11 @@ namespace storm { } template - /*std::unique_ptr*/ void + std::unique_ptr> ApproximatePOMDPModelchecker::computeReachabilityProbability( storm::models::sparse::Pomdp const &pomdp, std::set 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 result; std::map result_backup; @@ -58,6 +60,7 @@ namespace storm { // current ID -> action -> next ID std::map>> 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())); result_backup.emplace(std::make_pair(currentBelief.id, storm::utility::zero())); + //TODO put this in extra function std::vector> observationProbabilitiesInAction; std::vector> 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>> subSimplexCache; + std::map> lambdaCache; + + STORM_PRINT("Time generation of next believes: " << nextBeliefGeneration << std::endl) // Value Iteration auto cc = storm::utility::ConstantsComparator(); 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 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> temp = computeSubSimplexAndLambdas( - nextBelief.probabilities, gridResolution); - std::vector> subSimplex = temp.first; - std::vector lambdas = temp.second; + // cache the values to not always re-calculate + std::vector> subSimplex; + std::vector lambdas; + if (subSimplexCache.count(nextBelief.id) > 0) { + subSimplex = subSimplexCache[nextBelief.id]; + lambdas = lambdaCache[nextBelief.id]; + } else { + std::pair>, std::vector> temp = computeSubSimplexAndLambdas( + nextBelief.probabilities, gridResolution); + subSimplex = temp.first; + lambdas = temp.second; + subSimplexCache[nextBelief.id] = subSimplex; + lambdaCache[nextBelief.id] = lambdas; + } auto sum = storm::utility::zero(); 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(), chosenValue - currentValue)) || (!min && - cc.isLess(storm::utility::zero(), currentValue - chosenValue))) { - chosenValue = currentValue; - chosenActionIndex = action; - } else if ((min && cc.isEqual(storm::utility::zero(), - chosenValue - currentValue)) || - (!min && - cc.isEqual(storm::utility::zero(), - currentValue - chosenValue))) { + cc.isLess(storm::utility::zero(), currentValue - chosenValue)) || + cc.isEqual(storm::utility::zero(), 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 visitedBelieves; std::deque believesToBeExpanded; std::map 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().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{overApprox, resultValue}); } template @@ -311,9 +333,10 @@ namespace storm { uint64_t gridResolution, uint64_t currentBeliefId, uint64_t nextId, bool min) { auto cc = storm::utility::ConstantsComparator(); storm::pomdp::Belief currentBelief = beliefList[currentBeliefId]; + + //TODO put this in extra function std::vector> observationProbabilitiesInAction; std::vector> 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 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> subSimplex = temp.first; std::vector 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(), chosenValue - currentValue)) || (!min && - cc.isLess(storm::utility::zero(), currentValue - chosenValue))) { - chosenValue = currentValue; - chosenActionIndex = action; - } else if ((min && cc.isEqual(storm::utility::zero(), chosenValue - currentValue)) || - (!min && - cc.isEqual(storm::utility::zero(), currentValue - chosenValue))) { + cc.isLess(storm::utility::zero(), currentValue - chosenValue)) || + cc.isEqual(storm::utility::zero(), chosenValue - currentValue)) { chosenValue = currentValue; chosenActionIndex = action; } @@ -561,7 +579,6 @@ namespace storm { } lambdas[0] = storm::utility::one() - sum; - //TODO add assertion that we are close enough return std::make_pair(subSimplex, lambdas); } diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index 46b5ee1e4..896435bce 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h @@ -9,19 +9,23 @@ namespace storm { namespace pomdp { namespace modelchecker { - class POMDPCheckResult; + template + struct POMDPCheckResult { + ValueType OverapproximationValue; + ValueType UnderapproximationValue; + }; template> class ApproximatePOMDPModelchecker { public: explicit ApproximatePOMDPModelchecker(); - /*std::unique_ptr*/ void + std::unique_ptr> computeReachabilityProbability(storm::models::sparse::Pomdp const &pomdp, std::set targetObservations, bool min, uint64_t gridResolution); - std::unique_ptr + std::unique_ptr> computeReachabilityReward(storm::models::sparse::Pomdp const &pomdp, std::set target_observations, uint64_t gridResolution);