From c663edbd853f96f05191f5d83204af6e2723b079 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 22 Nov 2019 16:29:29 +0100 Subject: [PATCH] Added generation of an MDP for the over-approximation in the on-the-fly state exploration --- .../ApproximatePOMDPModelchecker.cpp | 96 ++++++++++++++++--- 1 file changed, 82 insertions(+), 14 deletions(-) diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index ff9bb522b..c1ce9449e 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -81,6 +81,15 @@ namespace storm { beliefIsTarget.push_back( targetObservations.find(initialBelief.observation) != targetObservations.end()); + // These are the components to build the MDP from the grid + std::map beliefStateMap; + std::vector>> mdpTransitions; + std::vector targetStates; + uint64_t mdpStateId = 0; + + beliefStateMap[initialBelief.id] = mdpStateId; + ++mdpStateId; + // for the initial belief, add the triangulated initial states std::pair>, std::vector> initTemp = computeSubSimplexAndLambdas( initialBelief.probabilities, gridResolution); @@ -90,6 +99,8 @@ namespace storm { lambdaCache[0] = initLambdas; bool initInserted = false; + std::vector> initTransitionsInBelief; + std::map initTransitionInActionBelief; for (size_t j = 0; j < initLambdas.size(); ++j) { if (!cc.isEqual(initLambdas[j], storm::utility::zero())) { @@ -107,12 +118,21 @@ namespace storm { beliefGrid.push_back(gridBelief); beliefIsTarget.push_back(targetObservations.find(initialBelief.observation) != targetObservations.end()); beliefsToBeExpanded.push_back(nextId); + + beliefStateMap[nextId] = mdpStateId; + initTransitionInActionBelief[mdpStateId] = initLambdas[j]; ++nextId; + ++mdpStateId; } } } } + // If the initial belief is not on the grid, we add the transitions from our initial MDP state to the triangulated beliefs + if (!initTransitionInActionBelief.empty()) { + initTransitionsInBelief.push_back(initTransitionInActionBelief); + 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 @@ -124,6 +144,14 @@ namespace storm { if (isTarget) { result.emplace(std::make_pair(currId, storm::utility::one())); result_backup.emplace(std::make_pair(currId, storm::utility::one())); + + // MDP stuff + std::vector> transitionsInBelief; + targetStates.push_back(beliefStateMap[currId]); + std::map transitionInActionBelief; + transitionInActionBelief[beliefStateMap[currId]] = storm::utility::one(); + transitionsInBelief.push_back(transitionInActionBelief); + mdpTransitions.push_back(transitionsInBelief); } else { result.emplace(std::make_pair(currId, storm::utility::zero())); result_backup.emplace(std::make_pair(currId, storm::utility::zero())); @@ -131,12 +159,14 @@ namespace storm { uint64_t numChoices = pomdp.getNumberOfChoices(pomdp.getStatesWithObservation(beliefList[currId].observation).front()); std::vector> observationProbabilitiesInAction(numChoices); std::vector> nextBelievesInAction(numChoices); + std::vector> transitionsInBelief; for (uint64_t action = 0; action < numChoices; ++action) { std::map actionObservationProbabilities = computeObservationProbabilitiesAfterAction(pomdp, beliefList[currId], action); std::map actionObservationBelieves; - for (auto iter = actionObservationProbabilities.begin(); - iter != actionObservationProbabilities.end(); ++iter) { + std::map transitionInActionBelief; + + for (auto iter = actionObservationProbabilities.begin(); iter != actionObservationProbabilities.end(); ++iter) { uint32_t observation = iter->first; // THIS CALL IS SLOW // TODO speed this up @@ -159,7 +189,6 @@ namespace storm { subSimplexCache[idNextBelief] = subSimplex; lambdaCache[idNextBelief] = lambdas; } - for (size_t j = 0; j < lambdas.size(); ++j) { if (!cc.isEqual(lambdas[j], storm::utility::zero())) { if (getBeliefIdInVector(beliefGrid, observation, subSimplex[j]) == uint64_t(-1)) { @@ -169,17 +198,31 @@ namespace storm { beliefGrid.push_back(gridBelief); beliefIsTarget.push_back(targetObservations.find(observation) != targetObservations.end()); beliefsToBeExpanded.push_back(nextId); + + beliefStateMap[nextId] = mdpStateId; + transitionInActionBelief[mdpStateId] = iter->second * lambdas[j]; ++nextId; + ++mdpStateId; + } else { + transitionInActionBelief[beliefStateMap[getBeliefIdInVector(beliefGrid, observation, subSimplex[j])]] = iter->second * lambdas[j]; } } } } observationProbabilitiesInAction[action] = actionObservationProbabilities; nextBelievesInAction[action] = actionObservationBelieves; + if (!transitionInActionBelief.empty()) { + transitionsInBelief.push_back(transitionInActionBelief); + } } - observationProbabilities.emplace( - std::make_pair(currId, observationProbabilitiesInAction)); + observationProbabilities.emplace(std::make_pair(currId, observationProbabilitiesInAction)); nextBelieves.emplace(std::make_pair(currId, nextBelievesInAction)); + if (transitionsInBelief.empty()) { + std::map transitionInActionBelief; + transitionInActionBelief[beliefStateMap[currId]] = storm::utility::one(); + transitionsInBelief.push_back(transitionInActionBelief); + } + mdpTransitions.push_back(transitionsInBelief); } } expansionTimer.stop(); @@ -187,6 +230,18 @@ namespace storm { STORM_PRINT("#Believes in List: " << beliefList.size() << std::endl) STORM_PRINT("Belief space expansion took " << expansionTimer << std::endl) + storm::models::sparse::StateLabeling mdpLabeling(mdpTransitions.size()); + mdpLabeling.addLabel("init"); + mdpLabeling.addLabel("target"); + mdpLabeling.addLabelToState("init", 0); + for (auto targetState : targetStates) { + mdpLabeling.addLabelToState("target", targetState); + } + + storm::storage::sparse::ModelComponents modelComponents(buildTransitionMatrix(mdpTransitions), mdpLabeling); + storm::models::sparse::Mdp overApproxMdp(modelComponents); + overApproxMdp.printModelInformationToStream(std::cout); + storm::utility::Stopwatch overApproxTimer(true); // Value Iteration while (!finished && iteration < maxIterations) { @@ -276,21 +331,34 @@ namespace storm { } overApproxTimer.stop(); - storm::utility::Stopwatch underApproxTimer(true); + ValueType underApprox = storm::utility::zero(); + /*storm::utility::Stopwatch underApproxTimer(true); ValueType underApprox = computeUnderapproximationWithMDP(pomdp, beliefList, beliefIsTarget, targetObservations, observationProbabilities, nextBelieves, result, chosenActions, gridResolution, initialBelief.id, min, false); - underApproxTimer.stop(); + underApproxTimer.stop();*/ - STORM_PRINT("Time Overapproximation: " << overApproxTimer - << std::endl - << "Time Underapproximation: " << underApproxTimer - << std::endl); + // 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); + //STORM_PRINT("Under-Approximation Result: " << underApprox << std::endl); - return std::make_unique>( - POMDPCheckResult{overApprox, underApprox}); + auto model = std::make_shared>(overApproxMdp); + auto modelPtr = std::static_pointer_cast>(model); + + + std::vector parameterNames; + storm::api::exportSparseModelAsDrn(modelPtr, "test", parameterNames); + + std::string propertyString = min ? "Pmin=? [F \"target\"]" : "Pmax=? [F \"target\"]"; + std::vector propertyVector = storm::api::parseProperties(propertyString); + std::shared_ptr property = storm::api::extractFormulasFromProperties(propertyVector).front(); + + std::unique_ptr res(storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, true))); + 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); + + return std::make_unique>(POMDPCheckResult{overApprox, underApprox}); }