Browse Source

quantiles: permute point entries if the order of quantile variable definitions is not the same as the order of occurrence on a cost bound.

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
commit
38121c28cb
  1. 24
      src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp

24
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<uint64_t> 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<ValueType> resultPoint(costLimits.size());
storm::utility::vector::applyPointwise<CostLimit, ValueType, ValueType>(costLimits, internalResult.second, resultPoint, [](CostLimit const& costLimit, ValueType const& factor) -> ValueType {
if (costLimit.isInfinity()) {
return storm::utility::infinity<ValueType>();
} else {
return storm::utility::convertNumber<ValueType>(costLimit.get()) * factor;
}});
std::vector<ValueType> resultPoint;
for (auto const& dim : permutation) {
CostLimit const& cl = costLimits[dim];
resultPoint.push_back(cl.isInfinity() ? storm::utility::infinity<ValueType>() : storm::utility::convertNumber<ValueType>(cl.get()) * internalResult.second[dim]);
}
result.push_back(resultPoint);
}
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {

Loading…
Cancel
Save