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(env.modelchecker().multi().getPrecision()); weightedPrecision /= storm::utility::sqrt(storm::utility::convertNumber(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 for the under-approximation and resp. + // for the over-approximation. Then, the over-approx. point 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(0.9); this->weightVectorChecker->setWeightedPrecision(weightedPrecision);