From 1982dc0dbadf739e83fbeff09ea22de942614795 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 19 Nov 2020 17:29:28 +0100
Subject: [PATCH] SparsePcaaParetoQuery: Added a (hopefully explaining) comment

---
 .../modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp  | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
index f1c4145df..cc05a6697 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
@@ -29,6 +29,8 @@ namespace storm {
                 typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber<typename SparseModelType::ValueType>(env.modelchecker().multi().getPrecision());
                 weightedPrecision /= storm::utility::sqrt(storm::utility::convertNumber<typename SparseModelType::ValueType, uint_fast64_t>(this->objectives.size()));
                 // multiobjPrecision / sqrt(numObjectives) is the largest possible value for which termination is guaranteed.
+                // To see this, assume that for both weight vectors <1,0> and <0,1> we get the same point <a,b> for the under-approximation and <a+weightedPrecision,b> resp. <a,b+weightedPrecision>
+                // for the over-approximation. Then, the over-approx. point <a+weightedPrecision,b+weightedPrecision> has a distance to the under-approximation of weightedPrecision * sqrt(numObjectives).
                 // Lets be a little bit more precise to reduce the number of required iterations.
                 weightedPrecision *= storm::utility::convertNumber<typename SparseModelType::ValueType>(0.9);
                 this->weightVectorChecker->setWeightedPrecision(weightedPrecision);