diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 27cbdb2bc..3939913c6 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -24,6 +24,7 @@ namespace storm { cc = storm::utility::ConstantsComparator(storm::utility::convertNumber(precision), false); useMdp = true; maxIterations = 1000; + cacheSubsimplices = false; } template @@ -81,6 +82,7 @@ namespace storm { initPropString += "=? [F \"goal\"]"; std::vector propVector = storm::api::parseProperties(initPropString); std::shared_ptr underlyingProperty = storm::api::extractFormulasFromProperties(propVector).front(); + STORM_PRINT("Underlying MDP" << std::endl) underlyingMdp.printModelInformationToStream(std::cout); std::unique_ptr underlyingRes( @@ -90,6 +92,7 @@ namespace storm { auto mdpResultMap = underlyingRes->asExplicitQuantitativeCheckResult().getValueMap(); auto underApproxModel = underlyingMdp.applyScheduler(pomdpScheduler, false); + STORM_PRINT("Random Positional Scheduler" << std::endl) underApproxModel->printModelInformationToStream(std::cout); std::unique_ptr underapproxRes( storm::api::verifyWithSparseEngine(underApproxModel, storm::api::createTask(underlyingProperty, false))); @@ -138,13 +141,15 @@ namespace storm { std::pair>, std::vector> initTemp = computeSubSimplexAndLambdas(initialBelief.probabilities, gridResolution); std::vector> initSubSimplex = initTemp.first; std::vector initLambdas = initTemp.second; - subSimplexCache[0] = initSubSimplex; - lambdaCache[0] = initLambdas; - bool initInserted = false; + if(cacheSubsimplices){ + subSimplexCache[0] = initSubSimplex; + lambdaCache[0] = initLambdas; + } + std::vector> initTransitionsInBelief; std::map initTransitionInActionBelief; - + bool initInserted = false; for (size_t j = 0; j < initLambdas.size(); ++j) { if (!cc.isEqual(initLambdas[j], storm::utility::zero())) { uint64_t searchResult = getBeliefIdInVector(beliefList, initialBelief.observation, initSubSimplex[j]); @@ -183,13 +188,14 @@ namespace storm { mdpTransitions.push_back(initTransitionsInBelief); } - //beliefsToBeExpanded.push_back(initialBelief.id); TODO I'm curious what happens if we do this instead of first triangulating. Should do nothing special if belief is on grid, otherwise it gets interesting + //beliefsToBeExpanded.push_back(initialBelief.id); I'm curious what happens if we do this instead of first triangulating. Should do nothing special if belief is on grid, otherwise it gets interesting std::map weightedSumOverMap; std::map weightedSumUnderMap; // Expand the beliefs to generate the grid on-the-fly to avoid unreachable grid points while (!beliefsToBeExpanded.empty()) { + // TODO add direct generation of transition matrix uint64_t currId = beliefsToBeExpanded.front(); beliefsToBeExpanded.pop_front(); bool isTarget = beliefIsTarget[currId]; @@ -230,8 +236,7 @@ namespace storm { //Triangulate here and put the possibly resulting belief in the grid std::vector> subSimplex; std::vector lambdas; - if (subSimplexCache.count(idNextBelief) > 0) { - // TODO is this necessary here? Think later + if (cacheSubsimplices && subSimplexCache.count(idNextBelief) > 0) { subSimplex = subSimplexCache[idNextBelief]; lambdas = lambdaCache[idNextBelief]; } else { @@ -239,8 +244,10 @@ namespace storm { beliefList[idNextBelief].probabilities, gridResolution); subSimplex = temp.first; lambdas = temp.second; - subSimplexCache[idNextBelief] = subSimplex; - lambdaCache[idNextBelief] = lambdas; + if(cacheSubsimplices){ + subSimplexCache[idNextBelief] = subSimplex; + lambdaCache[idNextBelief] = lambdas; + } } for (size_t j = 0; j < lambdas.size(); ++j) { @@ -307,6 +314,8 @@ namespace storm { STORM_PRINT("#Believes in List: " << beliefList.size() << std::endl) STORM_PRINT("Belief space expansion took " << expansionTimer << std::endl) + //auto overApprox = overApproximationValueIteration(pomdp, beliefList, beliefGrid, beliefIsTarget, observationProbabilities, nextBelieves, beliefActionRewards, subSimplexCache, lambdaCache,result, chosenActions, gridResolution, min, computeRewards); + storm::models::sparse::StateLabeling mdpLabeling(mdpTransitions.size()); mdpLabeling.addLabel("init"); mdpLabeling.addLabel("target"); @@ -334,29 +343,6 @@ namespace storm { } overApproxMdp.printModelInformationToStream(std::cout); - /* - storm::utility::Stopwatch overApproxTimer(true); - auto overApprox = overApproximationValueIteration(pomdp, beliefList, beliefGrid, beliefIsTarget, observationProbabilities, nextBelieves, beliefActionRewards, - subSimplexCache, lambdaCache, - result, chosenActions, gridResolution, min, computeRewards); - overApproxTimer.stop();*/ - - auto underApprox = storm::utility::zero(); - auto overApprox = storm::utility::one(); - /* - storm::utility::Stopwatch underApproxTimer(true); - ValueType underApprox = computeUnderapproximationWithMDP(pomdp, beliefList, beliefIsTarget, targetObservations, observationProbabilities, nextBelieves, - result, chosenActions, gridResolution, initialBelief.id, min, computeRewards); - underApproxTimer.stop(); - - STORM_PRINT("Time Overapproximation: " << overApproxTimer - << std::endl - << "Time Underapproximation: " << underApproxTimer - << std::endl); - - STORM_PRINT("Over-Approximation Result: " << overApprox << std::endl); - STORM_PRINT("Under-Approximation Result: " << underApprox << std::endl);*/ - auto model = std::make_shared>(overApproxMdp); auto modelPtr = std::static_pointer_cast>(model); std::vector parameterNames; @@ -367,17 +353,26 @@ namespace storm { propertyString += "=? [F \"target\"]"; std::vector propertyVector = storm::api::parseProperties(propertyString); std::shared_ptr property = storm::api::extractFormulasFromProperties(propertyVector).front(); - - auto task = storm::api::createTask(property, true); auto hint = storm::modelchecker::ExplicitModelCheckerHint(); hint.setResultHint(hintVector); auto hintPtr = std::make_shared>(hint); task.setHint(hintPtr); + storm::utility::Stopwatch overApproxTimer(true); std::unique_ptr res(storm::api::verifyWithSparseEngine(model, task)); + overApproxTimer.stop(); STORM_LOG_ASSERT(res, "Result not exist."); res->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - STORM_PRINT("OverApprox MDP: " << (res->asExplicitQuantitativeCheckResult().getValueMap().begin()->second) << std::endl); + auto overApprox = res->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + /* storm::utility::Stopwatch underApproxTimer(true); + ValueType underApprox = computeUnderapproximationWithMDP(pomdp, beliefList, beliefIsTarget, targetObservations, observationProbabilities, nextBelieves, + result, chosenActions, gridResolution, initialBelief.id, min, computeRewards); + underApproxTimer.stop();*/ + + STORM_PRINT("Time Overapproximation: " << overApproxTimer << std::endl) + auto underApprox = storm::utility::zero(); + STORM_PRINT("Over-Approximation Result: " << overApprox << std::endl); + STORM_PRINT("Under-Approximation Result: " << underApprox << std::endl); return std::make_unique>(POMDPCheckResult{overApprox, underApprox}); } @@ -425,7 +420,7 @@ namespace storm { // cache the values to not always re-calculate std::vector> subSimplex; std::vector lambdas; - if (subSimplexCache.count(nextBelief.id) > 0) { + if (cacheSubsimplices && subSimplexCache.count(nextBelief.id) > 0) { subSimplex = subSimplexCache[nextBelief.id]; lambdas = lambdaCache[nextBelief.id]; } else { @@ -433,8 +428,10 @@ namespace storm { gridResolution); subSimplex = temp.first; lambdas = temp.second; - subSimplexCache[nextBelief.id] = subSimplex; - lambdaCache[nextBelief.id] = lambdas; + if(cacheSubsimplices) { + subSimplexCache[nextBelief.id] = subSimplex; + lambdaCache[nextBelief.id] = lambdas; + } } auto sum = storm::utility::zero(); for (size_t j = 0; j < lambdas.size(); ++j) { @@ -477,11 +474,21 @@ namespace storm { STORM_PRINT("Overapproximation took " << iteration << " iterations" << std::endl); + std::vector initialLambda; + std::vector> initialSubsimplex; + if(cacheSubsimplices){ + initialLambda = lambdaCache[0]; + initialSubsimplex = subSimplexCache[0]; + } else { + auto temp = computeSubSimplexAndLambdas(beliefList[0].probabilities, gridResolution); + initialSubsimplex= temp.first; + initialLambda = temp.second; + } auto overApprox = storm::utility::zero(); - for (size_t j = 0; j < lambdaCache[0].size(); ++j) { - if (lambdaCache[0][j] != storm::utility::zero()) { - overApprox += lambdaCache[0][j] * result_backup[getBeliefIdInVector(beliefGrid, beliefList[0].observation, subSimplexCache[0][j])]; + for (size_t j = 0; j < initialLambda.size(); ++j) { + if (initialLambda[j] != storm::utility::zero()) { + overApprox += initialLambda[j] * result_backup[getBeliefIdInVector(beliefGrid, beliefList[0].observation, initialSubsimplex[j])]; } } return overApprox; @@ -541,8 +548,10 @@ namespace storm { std::map> lambdaCache; std::pair>, std::vector> temp = computeSubSimplexAndLambdas(initialBelief.probabilities, gridResolution); - subSimplexCache[0] = temp.first; - lambdaCache[0] = temp.second; + if(cacheSubsimplices) { + subSimplexCache[0] = temp.first; + lambdaCache[0] = temp.second; + } storm::utility::Stopwatch nextBeliefGeneration(true); for (size_t i = 0; i < beliefGrid.size(); ++i) { @@ -553,6 +562,7 @@ namespace storm { } else { result.emplace(std::make_pair(currentBelief.id, storm::utility::zero())); //TODO put this in extra function + // As we need to grab some parameters which are the same for all states with the same observation, we simply select some state as the representative uint64_t representativeState = pomdp.getStatesWithObservation(currentBelief.observation).front(); uint64_t numChoices = pomdp.getNumberOfChoices(representativeState); diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index aada759d2..e6f935a72 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h @@ -253,6 +253,7 @@ namespace storm { storm::utility::ConstantsComparator cc; double precision; bool useMdp; + bool cacheSubsimplices; uint64_t maxIterations; };