diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 6debaf5a0..2955bdb7f 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -2,7 +2,6 @@ #include - #include "storm/utility/ConstantsComparator.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -105,7 +104,7 @@ namespace storm { boost::optional> overApproximationMap, boost::optional> underApproximationMap) { STORM_PRINT("Use On-The-Fly Grid Generation" << std::endl) - auto result = computeRefinementFirstStep(pomdp, targetObservations, min, observationResolutionVector, computeRewards, explorationThreshold, overApproximationMap, + auto result = computeFirstRefinementStep(pomdp, targetObservations, min, observationResolutionVector, computeRewards, explorationThreshold, overApproximationMap, underApproximationMap); return std::make_unique>(POMDPCheckResult{result->overApproxValue, result->underApproxValue}); } @@ -113,7 +112,7 @@ namespace storm { template std::unique_ptr> - ApproximatePOMDPModelchecker::computeRefinementFirstStep(storm::models::sparse::Pomdp const &pomdp, + ApproximatePOMDPModelchecker::computeFirstRefinementStep(storm::models::sparse::Pomdp const &pomdp, std::set const &targetObservations, bool min, std::vector &observationResolutionVector, bool computeRewards, double explorationThreshold, @@ -133,7 +132,7 @@ namespace storm { //Use caching to avoid multiple computation of the subsimplices and lambdas std::map>> subSimplexCache; std::map> lambdaCache; - std::map beliefStateMap; + bsmap_type beliefStateMap; std::deque beliefsToBeExpanded; @@ -151,8 +150,7 @@ namespace storm { beliefList.push_back(initialBelief); beliefIsTarget.push_back(targetObservations.find(initialBelief.observation) != targetObservations.end()); - // These are the components to build the MDP from the grid TODO make a better structure to allow for fast reverse lookups (state-->belief) as it is a bijective function (boost:bimap?) - + // These are the components to build the MDP from the grid // Reserve states 0 and 1 as always sink/goal states std::vector>> mdpTransitions = {{{{0, storm::utility::one()}}}, {{{1, storm::utility::one()}}}}; @@ -161,7 +159,7 @@ namespace storm { std::vector targetStates = {1}; uint64_t mdpStateId = 2; - beliefStateMap[initialBelief.id] = mdpStateId; + beliefStateMap.insert(bsmap_type::value_type(initialBelief.id, mdpStateId)); ++mdpStateId; // Map to save the weighted values resulting from the preprocessing for the beliefs / indices in beliefSpace @@ -173,7 +171,7 @@ namespace storm { observationResolutionVector[initialBelief.observation]); std::vector> initSubSimplex = initTemp.first; std::vector initLambdas = initTemp.second; - if(cacheSubsimplices){ + if (cacheSubsimplices) { subSimplexCache[0] = initSubSimplex; lambdaCache[0] = initLambdas; } @@ -225,7 +223,7 @@ namespace storm { hintVector.push_back(targetObservations.find(initialBelief.observation) != targetObservations.end() ? storm::utility::one() : storm::utility::zero()); - beliefStateMap[nextId] = mdpStateId; + beliefStateMap.insert(bsmap_type::value_type(nextId, mdpStateId)); initTransitionInActionBelief[mdpStateId] = initLambdas[j]; ++nextId; ++mdpStateId; @@ -261,9 +259,9 @@ namespace storm { // Depending on whether we compute rewards, we select the right initial result // MDP stuff std::vector> transitionsInBelief; - targetStates.push_back(beliefStateMap[currId]); + targetStates.push_back(beliefStateMap.left.at(currId)); std::map transitionInActionBelief; - transitionInActionBelief[beliefStateMap[currId]] = storm::utility::one(); + transitionInActionBelief[beliefStateMap.left.at(currId)] = storm::utility::one(); transitionsInBelief.push_back(transitionInActionBelief); mdpTransitions.push_back(transitionsInBelief); } else { @@ -332,12 +330,13 @@ namespace storm { : storm::utility::zero()); } beliefsToBeExpanded.push_back(nextId); - beliefStateMap[nextId] = mdpStateId; + beliefStateMap.insert(bsmap_type::value_type(nextId, mdpStateId)); transitionInActionBelief[mdpStateId] = iter->second * lambdas[j]; ++nextId; ++mdpStateId; } else { - transitionInActionBelief[beliefStateMap[getBeliefIdInVector(beliefGrid, observation, subSimplex[j])]] = iter->second * lambdas[j]; + transitionInActionBelief[beliefStateMap.left.at(getBeliefIdInVector(beliefGrid, observation, subSimplex[j]))] = + iter->second * lambdas[j]; } } } @@ -361,7 +360,7 @@ namespace storm { if (transitionsInBelief.empty()) { std::map transitionInActionBelief; - transitionInActionBelief[beliefStateMap[currId]] = storm::utility::one(); + transitionInActionBelief[beliefStateMap.left.at(currId)] = storm::utility::one(); transitionsInBelief.push_back(transitionInActionBelief); } mdpTransitions.push_back(transitionsInBelief); @@ -374,7 +373,7 @@ namespace storm { storm::models::sparse::StateLabeling mdpLabeling(mdpTransitions.size()); mdpLabeling.addLabel("init"); mdpLabeling.addLabel("target"); - mdpLabeling.addLabelToState("init", beliefStateMap[initialBelief.id]); + mdpLabeling.addLabelToState("init", beliefStateMap.left.at(initialBelief.id)); for (auto targetState : targetStates) { mdpLabeling.addLabelToState("target", targetState); } @@ -382,7 +381,7 @@ namespace storm { storm::models::sparse::Mdp overApproxMdp(modelComponents); if (computeRewards) { storm::models::sparse::StandardRewardModel mdpRewardModel(boost::none, std::vector(modelComponents.transitionMatrix.getRowCount())); - for (auto const &iter : beliefStateMap) { + for (auto const &iter : beliefStateMap.left) { auto currentBelief = beliefList[iter.first]; auto representativeState = pomdp.getStatesWithObservation(currentBelief.observation).front(); for (uint64_t action = 0; action < overApproxMdp.getNumberOfChoices(iter.second); ++action) { @@ -415,7 +414,7 @@ namespace storm { STORM_LOG_ASSERT(res, "Result not exist."); res->filter(storm::modelchecker::ExplicitQualitativeCheckResult(storm::storage::BitVector(overApproxMdp.getNumberOfStates(), true))); auto overApproxResultMap = res->asExplicitQuantitativeCheckResult().getValueMap(); - auto overApprox = overApproxResultMap[beliefStateMap[initialBelief.id]]; + auto overApprox = overApproxResultMap[beliefStateMap.left.at(initialBelief.id)]; STORM_PRINT("Time Overapproximation: " << overApproxTimer << std::endl) auto underApprox = weightedSumUnderMap[initialBelief.id]; @@ -423,9 +422,10 @@ namespace storm { STORM_PRINT("Under-Approximation Result: " << underApprox << std::endl); // Transfer the underapproximation results from the belief id space to the MDP id space - std::map underApproxResultMap; + std::map underApproxResultMap = {{0, storm::utility::zero()}, + {1, storm::utility::one()}}; for (auto const &belief : beliefGrid) { - underApproxResultMap[beliefStateMap[belief.id]] = weightedSumUnderMap[belief.id]; + underApproxResultMap[beliefStateMap.left.at(belief.id)] = weightedSumUnderMap[belief.id]; } return std::make_unique>( diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index f61c0f9a6..ab85b2cc1 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h @@ -3,12 +3,15 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/utility/logging.h" #include "storm-pomdp/storage/Belief.h" +#include #include "storm/storage/jani/Property.h" namespace storm { namespace pomdp { namespace modelchecker { + typedef boost::bimap bsmap_type; + template struct POMDPCheckResult { ValueType overApproxValue; @@ -73,7 +76,7 @@ namespace storm { * @return */ std::unique_ptr> - computeRefinementFirstStep(storm::models::sparse::Pomdp const &pomdp, + computeFirstRefinementStep(storm::models::sparse::Pomdp const &pomdp, std::set const &targetObservations, bool min, std::vector &observationResolutionVector, bool computeRewards, double explorationThreshold, boost::optional> overApproximationMap = boost::none, boost::optional> underApproximationMap = boost::none);