From 5de96cc170d894baaded19106f268747b5006c29 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 11 Oct 2019 10:59:45 +0200 Subject: [PATCH] Modified implementation to speed up the subsimplex computation --- .../ApproximatePOMDPModelchecker.cpp | 38 ++++++++----------- 1 file changed, 15 insertions(+), 23 deletions(-) diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 351694c27..69e9bea80 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -697,14 +697,14 @@ namespace storm { std::vector probabilities, uint64_t resolution) { // This is the Freudenthal Triangulation as described in Lovejoy (a whole lotta math) // Variable names are based on the paper - - std::vector x(probabilities.size(), storm::utility::zero()); - std::vector v(probabilities.size(), storm::utility::zero()); - std::vector d(probabilities.size(), storm::utility::zero()); + std::vector x(probabilities.size()); + std::vector v(probabilities.size()); + std::vector d(probabilities.size()); + auto convResolution = storm::utility::convertNumber(resolution); for (size_t i = 0; i < probabilities.size(); ++i) { for (size_t j = i; j < probabilities.size(); ++j) { - x[i] += storm::utility::convertNumber(resolution) * probabilities[j]; + x[i] += convResolution * probabilities[j]; } v[i] = storm::utility::floor(x[i]); d[i] = x[i] - v[i]; @@ -712,37 +712,29 @@ namespace storm { auto p = storm::utility::vector::getSortedIndices(d); - std::vector> qs; + std::vector> qs(probabilities.size(), std::vector(probabilities.size())); for (size_t i = 0; i < probabilities.size(); ++i) { - std::vector q(probabilities.size(), storm::utility::zero()); if (i == 0) { for (size_t j = 0; j < probabilities.size(); ++j) { - q[j] = v[j]; + qs[i][j] = v[j]; } - qs.push_back(q); } else { for (size_t j = 0; j < probabilities.size(); ++j) { if (j == p[i - 1]) { - q[j] = qs[i - 1][j] + storm::utility::one(); + qs[i][j] = qs[i - 1][j] + storm::utility::one(); } else { - q[j] = qs[i - 1][j]; + qs[i][j] = qs[i - 1][j]; } } - qs.push_back(q); } } - - std::vector> subSimplex; - for (auto q : qs) { - std::vector node; - for (size_t i = 0; i < probabilities.size(); ++i) { - if (i != probabilities.size() - 1) { - node.push_back((q[i] - q[i + 1]) / storm::utility::convertNumber(resolution)); - } else { - node.push_back(q[i] / storm::utility::convertNumber(resolution)); - } + std::vector> subSimplex(qs.size(), std::vector(probabilities.size())); + for (size_t j = 0; j < qs.size(); ++j) { + for (size_t i = 0; i < probabilities.size() - 1; ++i) { + subSimplex[j][i] = (qs[j][i] - qs[j][i + 1]) / convResolution; } - subSimplex.push_back(node); + + subSimplex[j][probabilities.size() - 1] = qs[j][probabilities.size() - 1] / convResolution; } std::vector lambdas(probabilities.size(), storm::utility::zero());