From 38121c28cb0a2acb053216827a10e37c28fad693 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 13 Mar 2019 18:02:13 +0100 Subject: [PATCH] quantiles: permute point entries if the order of quantile variable definitions is not the same as the order of occurrence on a cost bound. --- .../helper/rewardbounded/QuantileHelper.cpp | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index d2f6c1c80..7fc19c5ab 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -208,15 +208,23 @@ namespace storm { // Call the internal recursive function auto internalResult = computeQuantile(envCpy, getOpenDimensions(), false); - // Translate the result by applying the scaling factors. + // Translate the result by applying the scaling factors and permutation. + std::vector permutation; + for (auto const& v : quantileFormula.getBoundVariables()) { + for (auto const& dim : getOpenDimensions()) { + if (getVariableForDimension(dim) == v) { + permutation.push_back(dim); + break; + } + } + } + assert(permutation.size() == getOpenDimensions().getNumberOfSetBits()); for (auto const& costLimits : internalResult.first.getGenerator()) { - std::vector resultPoint(costLimits.size()); - storm::utility::vector::applyPointwise(costLimits, internalResult.second, resultPoint, [](CostLimit const& costLimit, ValueType const& factor) -> ValueType { - if (costLimit.isInfinity()) { - return storm::utility::infinity(); - } else { - return storm::utility::convertNumber(costLimit.get()) * factor; - }}); + std::vector resultPoint; + for (auto const& dim : permutation) { + CostLimit const& cl = costLimits[dim]; + resultPoint.push_back(cl.isInfinity() ? storm::utility::infinity() : storm::utility::convertNumber(cl.get()) * internalResult.second[dim]); + } result.push_back(resultPoint); } if (storm::settings::getModule().isShowStatisticsSet()) {