diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index f965d9794..eefd43d95 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -152,10 +152,11 @@ namespace storm { prec = storm::utility::convertNumber(env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()).first.get()); relative = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()).second.get(); } + prec *= factor; if (relative) { - return std::make_pair((value * (1/(prec + 1))) * factor, (value * (1 + prec/(prec +1))) * factor); + return std::make_pair(value * (1/(prec + 1)), value * (1 + prec/(prec +1))); } else { - return std::make_pair((value - prec) * factor, (value + prec) * factor); + return std::make_pair(value - prec, value + prec); } } @@ -197,11 +198,13 @@ namespace storm { // Translate the result by applying the scaling factors and permutation. std::vector permutation; for (auto const& v : quantileFormula.getBoundVariables()) { + uint64_t openDim = 0; for (auto const& dim : getOpenDimensions()) { if (getVariableForDimension(dim) == v) { - permutation.push_back(dim); + permutation.push_back(openDim); break; } + ++openDim; } } assert(permutation.size() == getOpenDimensions().getNumberOfSetBits());