From 7dd5c9e2c51e842ba8146d907a727a50999b1779 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 3 May 2017 16:41:44 +0200 Subject: [PATCH] actually fixed the issue with timed reachability --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 47f90851e..7f4c5ff31 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -267,8 +267,13 @@ namespace storm { digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } - this->offsetsToLowerBound[objIndex] = -errorTowardsZero; - this->offsetsToUpperBound[objIndex] = errorAwayFromZero; + if (storm::solver::maximize(obj.optimizationDirection)) { + this->offsetsToLowerBound[objIndex] = -errorTowardsZero; + this->offsetsToUpperBound[objIndex] = errorAwayFromZero; + } else { + this->offsetsToLowerBound[objIndex] = errorAwayFromZero; + this->offsetsToUpperBound[objIndex] = -errorTowardsZero; + } } }