diff --git a/src/storm-pomdp/builder/BeliefMdpExplorer.h b/src/storm-pomdp/builder/BeliefMdpExplorer.h index 0fc6c9ba4..32adf985c 100644 --- a/src/storm-pomdp/builder/BeliefMdpExplorer.h +++ b/src/storm-pomdp/builder/BeliefMdpExplorer.h @@ -14,6 +14,7 @@ #include "storm/storage/SparseMatrix.h" #include "storm/utility/macros.h" #include "storm-pomdp/storage/BeliefManager.h" +#include "storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h" #include "storm/utility/SignalHandler.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -38,7 +39,7 @@ namespace storm { ModelChecked }; - BeliefMdpExplorer(std::shared_ptr beliefManager, std::vector const& pomdpLowerValueBounds, std::vector const& pomdpUpperValueBounds) : beliefManager(beliefManager), pomdpLowerValueBounds(pomdpLowerValueBounds), pomdpUpperValueBounds(pomdpUpperValueBounds), status(Status::Uninitialized) { + BeliefMdpExplorer(std::shared_ptr beliefManager, storm::pomdp::modelchecker::TrivialPomdpValueBounds const& pomdpValueBounds) : beliefManager(beliefManager), pomdpValueBounds(pomdpValueBounds), status(Status::Uninitialized) { // Intentionally left empty } BeliefMdpExplorer(BeliefMdpExplorer&& other) = default; @@ -544,16 +545,24 @@ namespace storm { return upperValueBounds[getCurrentMdpState()]; } - /// This requires that we either over-approximate the scheduler behavior in this direction (e.g. grid approximation for minimizing properties) - /// Or that the pomdpLowerValueBounds are based on a memoryless scheduler. Otherwise, such a triangulation would not be valid. ValueType computeLowerValueBoundAtBelief(BeliefId const& beliefId) const { - return beliefManager->getWeightedSum(beliefId, pomdpLowerValueBounds); + STORM_LOG_ASSERT(!pomdpValueBounds.lower.empty(), "Requested lower value bounds but none were available."); + auto it = pomdpValueBounds.lower.begin(); + ValueType result = beliefManager->getWeightedSum(beliefId, *it); + for (++it; it != pomdpValueBounds.lower.end(); ++it) { + result = std::max(result, beliefManager->getWeightedSum(beliefId, *it)); + } + return result; } - /// This requires that we either over-approximate the scheduler behavior in this direction (e.g. grid approximation for maximizing properties) - /// Or that the pomdpUpperValueBounds are based on a memoryless scheduler. Otherwise, such a triangulation would not be valid. ValueType computeUpperValueBoundAtBelief(BeliefId const& beliefId) const { - return beliefManager->getWeightedSum(beliefId, pomdpUpperValueBounds); + STORM_LOG_ASSERT(!pomdpValueBounds.upper.empty(), "Requested upper value bounds but none were available."); + auto it = pomdpValueBounds.upper.begin(); + ValueType result = beliefManager->getWeightedSum(beliefId, *it); + for (++it; it != pomdpValueBounds.upper.end(); ++it) { + result = std::min(result, beliefManager->getWeightedSum(beliefId, *it)); + } + return result; } void computeValuesOfExploredMdp(storm::solver::OptimizationDirection const& dir) { @@ -817,8 +826,7 @@ namespace storm { std::shared_ptr> exploredMdp; // Value and scheduler related information - std::vector const& pomdpLowerValueBounds; - std::vector const& pomdpUpperValueBounds; + storm::pomdp::modelchecker::TrivialPomdpValueBounds pomdpValueBounds; std::vector lowerValueBounds; std::vector upperValueBounds; std::vector values; // Contains an estimate during building and the actual result after a check has performed diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index fbbe017f8..b08eb8177 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -87,7 +87,8 @@ namespace storm { // Compute some initial bounds on the values for each state of the pomdp auto initialPomdpValueBounds = TrivialPomdpValueBoundsModelChecker>(pomdp).getValueBounds(formula, formulaInfo); - Result result(initialPomdpValueBounds.lower[pomdp.getInitialStates().getNextSetIndex(0)], initialPomdpValueBounds.upper[pomdp.getInitialStates().getNextSetIndex(0)]); + uint64_t initialPomdpState = pomdp.getInitialStates().getNextSetIndex(0); + Result result(initialPomdpValueBounds.getHighestLowerBound(initialPomdpState), initialPomdpValueBounds.getSmallestUpperBound(initialPomdpState)); STORM_PRINT_AND_LOG("Initial value bounds are [" << result.lowerBound << ", " << result.upperBound << "]" << std::endl); boost::optional rewardModelName; @@ -112,9 +113,9 @@ namespace storm { } if (options.refine) { - refineReachability(formulaInfo.getTargetStates().observations, formulaInfo.minimize(), rewardModelName, initialPomdpValueBounds.lower, initialPomdpValueBounds.upper, result); + refineReachability(formulaInfo.getTargetStates().observations, formulaInfo.minimize(), rewardModelName, initialPomdpValueBounds, result); } else { - computeReachabilityOTF(formulaInfo.getTargetStates().observations, formulaInfo.minimize(), rewardModelName, initialPomdpValueBounds.lower, initialPomdpValueBounds.upper, result); + computeReachabilityOTF(formulaInfo.getTargetStates().observations, formulaInfo.minimize(), rewardModelName, initialPomdpValueBounds, result); } // "clear" results in case they were actually not requested (this will make the output a bit more clear) if ((formulaInfo.minimize() && !options.discretize) || (formulaInfo.maximize() && !options.unfold)) { @@ -187,7 +188,7 @@ namespace storm { } template - void ApproximatePOMDPModelchecker::computeReachabilityOTF(std::set const &targetObservations, bool min, boost::optional rewardModelName, std::vector const& lowerPomdpValueBounds, std::vector const& upperPomdpValueBounds, Result& result) { + void ApproximatePOMDPModelchecker::computeReachabilityOTF(std::set const &targetObservations, bool min, boost::optional rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds const& pomdpValueBounds, Result& result) { if (options.discretize) { std::vector observationResolutionVector(pomdp.getNrObservations(), options.resolutionInit); @@ -195,7 +196,7 @@ namespace storm { if (rewardModelName) { manager->setRewardModel(rewardModelName); } - auto approx = std::make_shared(manager, lowerPomdpValueBounds, upperPomdpValueBounds); + auto approx = std::make_shared(manager, pomdpValueBounds); HeuristicParameters heuristicParameters; heuristicParameters.gapThreshold = options.gapThresholdInit; heuristicParameters.observationThreshold = options.obsThresholdInit; // Actually not relevant without refinement @@ -215,7 +216,7 @@ namespace storm { if (rewardModelName) { manager->setRewardModel(rewardModelName); } - auto approx = std::make_shared(manager, lowerPomdpValueBounds, upperPomdpValueBounds); + auto approx = std::make_shared(manager, pomdpValueBounds); HeuristicParameters heuristicParameters; heuristicParameters.gapThreshold = options.gapThresholdInit; heuristicParameters.optimalChoiceValueEpsilon = options.optimalChoiceValueThresholdInit; @@ -239,7 +240,7 @@ namespace storm { } template - void ApproximatePOMDPModelchecker::refineReachability(std::set const &targetObservations, bool min, boost::optional rewardModelName, std::vector const& lowerPomdpValueBounds, std::vector const& upperPomdpValueBounds, Result& result) { + void ApproximatePOMDPModelchecker::refineReachability(std::set const &targetObservations, bool min, boost::optional rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds const& pomdpValueBounds, Result& result) { statistics.refinementSteps = 0; // Set up exploration data @@ -253,7 +254,7 @@ namespace storm { if (rewardModelName) { overApproxBeliefManager->setRewardModel(rewardModelName); } - overApproximation = std::make_shared(overApproxBeliefManager, lowerPomdpValueBounds, upperPomdpValueBounds); + overApproximation = std::make_shared(overApproxBeliefManager, pomdpValueBounds); overApproxHeuristicPar.gapThreshold = options.gapThresholdInit; overApproxHeuristicPar.observationThreshold = options.obsThresholdInit; overApproxHeuristicPar.sizeThreshold = options.sizeThresholdInit == 0 ? std::numeric_limits::max() : options.sizeThresholdInit; @@ -277,7 +278,7 @@ namespace storm { if (rewardModelName) { underApproxBeliefManager->setRewardModel(rewardModelName); } - underApproximation = std::make_shared(underApproxBeliefManager, lowerPomdpValueBounds, upperPomdpValueBounds); + underApproximation = std::make_shared(underApproxBeliefManager, pomdpValueBounds); underApproxHeuristicPar.gapThreshold = options.gapThresholdInit; underApproxHeuristicPar.optimalChoiceValueEpsilon = options.optimalChoiceValueThresholdInit; underApproxHeuristicPar.sizeThreshold = options.sizeThresholdInit; diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index 44127e011..c9f46aa1f 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h @@ -16,6 +16,9 @@ namespace storm { namespace pomdp { namespace modelchecker { + template + struct TrivialPomdpValueBounds; + template class ApproximatePOMDPModelchecker { public: @@ -53,7 +56,7 @@ namespace storm { * @param maxUaModelSize the maximum size of the underapproximation model to be generated * @return A struct containing the overapproximation (overApproxValue) and underapproximation (underApproxValue) values */ - void computeReachabilityOTF(std::set const &targetObservations, bool min, boost::optional rewardModelName, std::vector const& lowerPomdpValueBounds, std::vector const& upperPomdpValueBounds, Result& result); + void computeReachabilityOTF(std::set const &targetObservations, bool min, boost::optional rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds const& pomdpValueBounds, Result& result); /** @@ -63,7 +66,7 @@ namespace storm { * @param min true if minimum probability is to be computed * @return A struct containing the final overapproximation (overApproxValue) and underapproximation (underApproxValue) values */ - void refineReachability(std::set const &targetObservations, bool min, boost::optional rewardModelName, std::vector const& lowerPomdpValueBounds, std::vector const& upperPomdpValueBounds, Result& result); + void refineReachability(std::set const &targetObservations, bool min, boost::optional rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds const& pomdpValueBounds, Result& result); struct HeuristicParameters { ValueType gapThreshold; diff --git a/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h b/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h index ca4c2192f..82bfd9e5b 100644 --- a/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h +++ b/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h @@ -15,26 +15,112 @@ namespace storm { namespace pomdp { namespace modelchecker { + + template + struct TrivialPomdpValueBounds { + std::vector> lower; + std::vector> upper; + ValueType getHighestLowerBound(uint64_t const& state) { + STORM_LOG_ASSERT(!lower.empty(), "requested a lower bound but none were available"); + auto it = lower.begin(); + ValueType result = (*it)[state]; + for (++it; it != lower.end(); ++it) { + result = std::max(result, (*it)[state]); + } + return result; + } + ValueType getSmallestUpperBound(uint64_t const& state) { + STORM_LOG_ASSERT(!upper.empty(), "requested an upper bound but none were available"); + auto it = upper.begin(); + ValueType result = (*it)[state]; + for (++it; it != upper.end(); ++it) { + result = std::min(result, (*it)[state]); + } + return result; + } + }; + template class TrivialPomdpValueBoundsModelChecker { public: typedef typename PomdpType::ValueType ValueType; + typedef TrivialPomdpValueBounds ValueBounds; TrivialPomdpValueBoundsModelChecker(PomdpType const& pomdp) : pomdp(pomdp) { // Intentionally left empty } - struct ValueBounds { - std::vector lower; - std::vector upper; - }; ValueBounds getValueBounds(storm::logic::Formula const& formula) { return getValueBounds(formula, storm::pomdp::analysis::getFormulaInformation(pomdp, formula)); } + std::vector getChoiceValues(std::vector const& stateValues, std::vector* actionBasedRewards) { + std::vector choiceValues((pomdp.getNumberOfChoices())); + pomdp.getTransitionMatrix().multiplyWithVector(stateValues, choiceValues, actionBasedRewards); + return choiceValues; + } + + std::vector computeValuesForGuessedScheduler(std::vector const& stateValues, std::vector* actionBasedRewards, storm::logic::Formula const& formula, storm::pomdp::analysis::FormulaInformation const& info, std::shared_ptr> underlyingMdp, ValueType const& scoreThreshold, bool relativeScore) { + // Create some positional scheduler for the POMDP + storm::storage::Scheduler pomdpScheduler(pomdp.getNumberOfStates()); + // For each state, we heuristically find a good distribution over output actions. + auto choiceValues = getChoiceValues(stateValues, actionBasedRewards); + auto const& choiceIndices = pomdp.getTransitionMatrix().getRowGroupIndices(); + std::vector> choiceDistributions(pomdp.getNrObservations()); + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + auto& choiceDistribution = choiceDistributions[pomdp.getObservation(state)]; + ValueType const& stateValue = stateValues[state]; + assert(stateValue >= storm::utility::zero()); + std::cout << state << ": " << stateValue << "\t t=" << scoreThreshold << " rel=" << relativeScore << std::endl; + for (auto choice = choiceIndices[state]; choice < choiceIndices[state + 1]; ++choice) { + ValueType const& choiceValue = choiceValues[choice]; + assert(choiceValue >= storm::utility::zero()); + std::cout << "\t" << (choice - choiceIndices[state]) << ": " << choiceValue << std::endl; + // Rate this choice by considering the relative difference between the choice value and the (optimal) state value + // A high score shall mean that the choice is "good" + if (storm::utility::isInfinity(stateValue)) { + // For infinity states, we simply distribute uniformly. + // FIXME: This case could be handled a bit more sensible + choiceDistribution.addProbability(choice - choiceIndices[state], scoreThreshold); + } else { + ValueType choiceScore = info.minimize() ? (choiceValue - stateValue) : (stateValue - choiceValue); + if (relativeScore) { + ValueType avg = (stateValue + choiceValue) / storm::utility::convertNumber(2); + if (!storm::utility::isZero(avg)) { + choiceScore /= avg; + } + } + choiceScore = storm::utility::one() - choiceScore; + if (choiceScore >= scoreThreshold) { + choiceDistribution.addProbability(choice - choiceIndices[state], choiceScore); + } + } + + } + STORM_LOG_ASSERT(choiceDistribution.size() > 0, "Empty choice distribution."); + } + // Normalize all distributions + for (auto& choiceDistribution : choiceDistributions) { + choiceDistribution.normalize(); + } + // Set the scheduler for all states + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + pomdpScheduler.setChoice(choiceDistributions[pomdp.getObservation(state)], state); + } + STORM_LOG_ASSERT(!pomdpScheduler.isPartialScheduler(), "Expected a fully defined scheduler."); + auto scheduledModel = underlyingMdp->applyScheduler(pomdpScheduler, false); + + auto resultPtr = storm::api::verifyWithSparseEngine(scheduledModel, storm::api::createTask(formula.asSharedPointer(), false)); + STORM_LOG_THROW(resultPtr, storm::exceptions::UnexpectedException, "No check result obtained."); + STORM_LOG_THROW(resultPtr->isExplicitQuantitativeCheckResult(), storm::exceptions::UnexpectedException, "Unexpected Check result Type"); + std::vector pomdpSchedulerResult = std::move(resultPtr->template asExplicitQuantitativeCheckResult().getValueVector()); + return pomdpSchedulerResult; + } + ValueBounds getValueBounds(storm::logic::Formula const& formula, storm::pomdp::analysis::FormulaInformation const& info) { STORM_LOG_THROW(info.isNonNestedReachabilityProbability() || info.isNonNestedExpectedRewardFormula(), storm::exceptions::NotSupportedException, "The property type is not supported for this analysis."); + // Compute the values on the fully observable MDP - // We need an actual MDP here so that the apply scheduler method below will work. + // We need an actual MDP so that we can apply schedulers below. // Also, the api call in the next line will require a copy anyway. auto underlyingMdp = std::make_shared>(pomdp.getTransitionMatrix(), pomdp.getStateLabeling(), pomdp.getRewardModels()); auto resultPtr = storm::api::verifyWithSparseEngine(underlyingMdp, storm::api::createTask(formula.asSharedPointer(), false)); @@ -42,70 +128,76 @@ namespace storm { STORM_LOG_THROW(resultPtr->isExplicitQuantitativeCheckResult(), storm::exceptions::UnexpectedException, "Unexpected Check result Type"); std::vector fullyObservableResult = std::move(resultPtr->template asExplicitQuantitativeCheckResult().getValueVector()); - // Create some positional scheduler for the POMDP - storm::storage::Scheduler pomdpScheduler(pomdp.getNumberOfStates()); - // For each state, we heuristically find a good distribution over output actions. - std::vector fullyObservableChoiceValues(pomdp.getNumberOfChoices()); + std::vector actionBasedRewards; + std::vector* actionBasedRewardsPtr = nullptr; if (info.isNonNestedExpectedRewardFormula()) { - std::vector actionBasedRewards = pomdp.getRewardModel(info.getRewardModelName()).getTotalRewardVector(pomdp.getTransitionMatrix()); - pomdp.getTransitionMatrix().multiplyWithVector(fullyObservableResult, fullyObservableChoiceValues, &actionBasedRewards); - } else { - pomdp.getTransitionMatrix().multiplyWithVector(fullyObservableResult, fullyObservableChoiceValues); + actionBasedRewards = pomdp.getRewardModel(info.getRewardModelName()).getTotalRewardVector(pomdp.getTransitionMatrix()); + actionBasedRewardsPtr = &actionBasedRewards; } - auto const& choiceIndices = pomdp.getTransitionMatrix().getRowGroupIndices(); - for (uint32_t obs = 0; obs < pomdp.getNrObservations(); ++obs) { - auto obsStates = pomdp.getStatesWithObservation(obs); - storm::storage::Distribution choiceDistribution; - for (auto const &state : obsStates) { - ValueType const& stateValue = fullyObservableResult[state]; - assert(stateValue >= storm::utility::zero()); - for (auto choice = choiceIndices[state]; choice < choiceIndices[state + 1]; ++choice) { - ValueType const& choiceValue = fullyObservableChoiceValues[choice]; - assert(choiceValue >= storm::utility::zero()); - // Rate this choice by considering the relative difference between the choice value and the (optimal) state value - ValueType choiceRating; - if (stateValue < choiceValue) { - choiceRating = choiceValue - stateValue; - if (!storm::utility::isZero(choiceValue)) { - choiceRating /= choiceValue; - } + std::vector> guessedSchedulerValues; + + std::vector> guessParameters({{0.875,false},{0.875,true},{0.75,false},{0.75,true}}); + for (auto const& pars : guessParameters) { + guessedSchedulerValues.push_back(computeValuesForGuessedScheduler(fullyObservableResult, actionBasedRewardsPtr, formula, info, underlyingMdp, storm::utility::convertNumber(pars.first), pars.second)); + } + + // compute the 'best' guess and do a few iterations on it + uint64_t bestGuess = 0; + ValueType bestGuessSum = std::accumulate(guessedSchedulerValues.front().begin(), guessedSchedulerValues.front().end(), storm::utility::zero()); + for (uint64_t guess = 1; guess < guessedSchedulerValues.size(); ++guess) { + ValueType guessSum = std::accumulate(guessedSchedulerValues[guess].begin(), guessedSchedulerValues[guess].end(), storm::utility::zero()); + if ((info.minimize() && guessSum < bestGuessSum) || (info.maximize() && guessSum > bestGuessSum)) { + bestGuess = guess; + bestGuessSum = guessSum; + } + } + guessedSchedulerValues.push_back(computeValuesForGuessedScheduler(guessedSchedulerValues[bestGuess], actionBasedRewardsPtr, formula, info, underlyingMdp, storm::utility::convertNumber(guessParameters[bestGuess].first), guessParameters[bestGuess].second)); + guessedSchedulerValues.push_back(computeValuesForGuessedScheduler(guessedSchedulerValues.back(), actionBasedRewardsPtr, formula, info, underlyingMdp, storm::utility::convertNumber(guessParameters[bestGuess].first), guessParameters[bestGuess].second)); + guessedSchedulerValues.push_back(computeValuesForGuessedScheduler(guessedSchedulerValues.back(), actionBasedRewardsPtr, formula, info, underlyingMdp, storm::utility::convertNumber(guessParameters[bestGuess].first), guessParameters[bestGuess].second)); + + // Check if one of the guesses is worse than one of the others (and potentially delete it) + // Avoid deleting entries during the loop to ensure that indices remain valid + storm::storage::BitVector keptGuesses(guessedSchedulerValues.size(), true); + for (uint64_t i = 0; i < guessedSchedulerValues.size() - 1; ++i) { + if (!keptGuesses.get(i)) { + continue; + } + for (uint64_t j = i + 1; j < guessedSchedulerValues.size(); ++j) { + if (!keptGuesses.get(j)) { + continue; + } + if (storm::utility::vector::compareElementWise(guessedSchedulerValues[i], guessedSchedulerValues[j], std::less_equal())) { + if (info.minimize()) { + // In this case we are guessing upper bounds (and smaller upper bounds are better) + keptGuesses.set(j, false); } else { - choiceRating = stateValue - choiceValue; - if (!storm::utility::isZero(stateValue)) { - choiceRating /= stateValue; - } + // In this case we are guessing lower bounds (and larger lower bounds are better) + keptGuesses.set(i, false); + break; } - assert(choiceRating <= storm::utility::one()); - assert(choiceRating >= storm::utility::zero()); - // choiceRating = 0 is a very good choice, choiceRating = 1 is a very bad choice - if (choiceRating <= storm::utility::convertNumber(0.5)) { - choiceDistribution.addProbability(choice - choiceIndices[state], storm::utility::one() - choiceRating); + } else if (storm::utility::vector::compareElementWise(guessedSchedulerValues[j], guessedSchedulerValues[i], std::less_equal())) { + if (info.minimize()) { + keptGuesses.set(i, false); + break; + } else { + keptGuesses.set(j, false); } } } - choiceDistribution.normalize(); - for (auto const& state : obsStates) { - pomdpScheduler.setChoice(choiceDistribution, state); - } } - STORM_LOG_ASSERT(!pomdpScheduler.isPartialScheduler(), "Expected a fully defined scheduler."); - auto scheduledModel = underlyingMdp->applyScheduler(pomdpScheduler, false); - - auto resultPtr2 = storm::api::verifyWithSparseEngine(scheduledModel, storm::api::createTask(formula.asSharedPointer(), false)); - STORM_LOG_THROW(resultPtr2, storm::exceptions::UnexpectedException, "No check result obtained."); - STORM_LOG_THROW(resultPtr2->isExplicitQuantitativeCheckResult(), storm::exceptions::UnexpectedException, "Unexpected Check result Type"); - std::vector pomdpSchedulerResult = std::move(resultPtr2->template asExplicitQuantitativeCheckResult().getValueVector()); + std::cout << "Keeping scheduler guesses " << keptGuesses << std::endl; + storm::utility::vector::filterVectorInPlace(guessedSchedulerValues, keptGuesses); // Finally prepare the result ValueBounds result; if (info.minimize()) { - result.lower = std::move(fullyObservableResult); - result.upper = std::move(pomdpSchedulerResult); + result.lower.push_back(std::move(fullyObservableResult)); + result.upper = std::move(guessedSchedulerValues); } else { - result.lower = std::move(pomdpSchedulerResult); - result.upper = std::move(fullyObservableResult); + result.lower = std::move(guessedSchedulerValues); + result.upper.push_back(std::move(fullyObservableResult)); } - STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(result.lower, result.upper, std::less_equal()), "Lower bound is larger than upper bound"); + STORM_LOG_WARN_COND_DEBUG(storm::utility::vector::compareElementWise(result.lower.front(), result.upper.front(), std::less_equal()), "Lower bound is larger than upper bound"); return result; }