Renamed lower/upper bounds to under/over approximation in weightVectorCheckers

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

@@ -268,11 +268,11 @@ namespace storm {
                         errorAwayFromZero += digitizationError;
                     }
                     if (storm::solver::maximize(obj.optimizationDirection)) {
-                        this->offsetsToLowerBound[objIndex] = -errorTowardsZero;
-                        this->offsetsToUpperBound[objIndex] = errorAwayFromZero;
+                        this->offsetsToUnderApproximation[objIndex] = -errorTowardsZero;
+                        this->offsetsToOverApproximation[objIndex] = errorAwayFromZero;
                     } else {
-                        this->offsetsToLowerBound[objIndex] = errorAwayFromZero;
-                        this->offsetsToUpperBound[objIndex] = -errorTowardsZero;
+                        this->offsetsToUnderApproximation[objIndex] = errorAwayFromZero;
+                        this->offsetsToOverApproximation[objIndex] = -errorTowardsZero;
                     }
                 }
             } 

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h

@@ -106,7 +106,7 @@ namespace storm {
                 void digitize(SubModel& subModel, VT const& digitizationConstant) const;
                 
                 /* 
-                 * Fills the given map with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values
+                 * Fills the given map with the digitized time bounds. Also sets the offsetsToUnderApproximation / offsetsToOverApproximation values
                  * according to the digitization error
                  */
                 template <typename VT = ValueType, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>

src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp

@@ -47,8 +47,8 @@ namespace storm {
                         stepBoundIt->second.set(objIndex);
                         
                         // There is no error for the values of these objectives.
-                        this->offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
-                        this->offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
+                        this->offsetsToUnderApproximation[objIndex] = storm::utility::zero<ValueType>();
+                        this->offsetsToOverApproximation[objIndex] = storm::utility::zero<ValueType>();
                     }
                 }
                 

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp

@@ -94,12 +94,12 @@ namespace storm {
                 // Normalize the direction vector so that the entries sum up to one
                 storm::utility::vector::scaleVectorInPlace(direction, storm::utility::one<GeometryValueType>() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero<GeometryValueType>()));
                 weightVectorChecker->check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction));
-                STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getLowerBoundsOfInitialStateResults())));
+                STORM_LOG_DEBUG("weighted objectives checker result (under approximation) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getUnderApproximationOfInitialStateResults())));
                 RefinementStep step;
                 step.weightVector = direction;
-                step.lowerBoundPoint = storm::utility::vector::convertNumericVector<GeometryValueType>(weightVectorChecker->getLowerBoundsOfInitialStateResults());
-                step.upperBoundPoint = storm::utility::vector::convertNumericVector<GeometryValueType>(weightVectorChecker->getUpperBoundsOfInitialStateResults());
-                // For the minimizing objectives, we need to scale the corresponding entries with -1 in order to consider the downward closure
+                step.lowerBoundPoint = storm::utility::vector::convertNumericVector<GeometryValueType>(weightVectorChecker->getUnderApproximationOfInitialStateResults());
+                step.upperBoundPoint = storm::utility::vector::convertNumericVector<GeometryValueType>(weightVectorChecker->getOverApproximationOfInitialStateResults());
+                // For the minimizing objectives, we need to scale the corresponding entries with -1 as we want to consider the downward closure
                 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
                     if (storm::solver::minimize(this->objectives[objIndex].optimizationDirection)) {
                         step.lowerBoundPoint[objIndex] *= -storm::utility::one<GeometryValueType>();

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@@ -36,8 +36,8 @@ namespace storm {
                     discreteActionRewards(objectives.size()),
                     checkHasBeenCalled(false),
                     objectiveResults(objectives.size()),
-                    offsetsToLowerBound(objectives.size()),
-                    offsetsToUpperBound(objectives.size()) {
+                    offsetsToUnderApproximation(objectives.size()),
+                    offsetsToOverApproximation(objectives.size()) {
                 
                 // set data for unbounded objectives
                 for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
@@ -94,10 +94,9 @@ namespace storm {
                         break;
                     }
                 }
-                STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults())));
+                STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getUnderApproximationOfInitialStateResults())));
                 // Validate that the results are sufficiently precise
-                ValueType resultingWeightedPrecision = storm::utility::vector::dotProduct(getUpperBoundsOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getLowerBoundsOfInitialStateResults(), weightVector);
-                STORM_LOG_THROW(resultingWeightedPrecision >= storm::utility::zero<ValueType>(), storm::exceptions::UnexpectedException, "The distance between the lower and the upper result is negative.");
+                ValueType resultingWeightedPrecision = storm::utility::abs(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector));
                 resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector));
                 STORM_LOG_THROW(resultingWeightedPrecision <= weightedPrecision, storm::exceptions::UnexpectedException, "The desired precision was not reached");
             }
@@ -113,25 +112,25 @@ namespace storm {
             }
             
             template <class SparseModelType>
-            std::vector<typename SparsePcaaWeightVectorChecker<SparseModelType>::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::getLowerBoundsOfInitialStateResults() const {
+            std::vector<typename SparsePcaaWeightVectorChecker<SparseModelType>::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::getUnderApproximationOfInitialStateResults() const {
                 STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
                 uint_fast64_t initstate = *this->model.getInitialStates().begin();
                 std::vector<ValueType> res;
                 res.reserve(this->objectives.size());
                 for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
-                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToLowerBound[objIndex]);
+                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUnderApproximation[objIndex]);
                 }
                 return res;
             }
             
             template <class SparseModelType>
-            std::vector<typename SparsePcaaWeightVectorChecker<SparseModelType>::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::getUpperBoundsOfInitialStateResults() const {
+            std::vector<typename SparsePcaaWeightVectorChecker<SparseModelType>::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::getOverApproximationOfInitialStateResults() const {
                 STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
                 uint_fast64_t initstate = *this->model.getInitialStates().begin();
                 std::vector<ValueType> res;
                 res.reserve(this->objectives.size());
                 for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
-                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUpperBound[objIndex]);
+                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToOverApproximation[objIndex]);
                 }
                 return res;
             }
@@ -218,8 +217,8 @@ namespace storm {
                    for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) {
                        auto const& obj = objectives[objIndex];
                        if (objectivesWithNoUpperTimeBound.get(objIndex)) {
-                           offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
-                           offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
+                           offsetsToUnderApproximation[objIndex] = storm::utility::zero<ValueType>();
+                           offsetsToOverApproximation[objIndex] = storm::utility::zero<ValueType>();
                            storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
                            storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards);
                            // As maybestates we pick the states from which a state with reward is reachable

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

@@ -14,8 +14,8 @@ namespace storm {
             
             /*!
              * Helper Class that takes preprocessed Pcaa data and a weight vector and ...
-             * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
-             * - extracts the scheduler that induces this maximum
+             * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
+             * - extracts the scheduler that induces this optimum
              * - computes for each objective the value induced by this scheduler
              */
             template <class SparseModelType>
@@ -41,8 +41,8 @@ namespace storm {
                 virtual ~SparsePcaaWeightVectorChecker() = default;
                 
                 /*!
-                 * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
-                 * - extracts the scheduler that induces this maximum
+                 * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
+                 * - extracts the scheduler that induces this optimum
                  * - computes for each objective the value induced by this scheduler
                  */
                 void check(std::vector<ValueType> const& weightVector);
@@ -50,19 +50,19 @@ namespace storm {
                 /*!
                  * Retrieves the results of the individual objectives at the initial state of the given model.
                  * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown.
-                 * Also note that there is no guarantee that the lower/upper bounds are sound
+                 * Also note that there is no guarantee that the under/over approximation is in fact correct
                  * as long as the underlying solution methods are unsound (e.g., standard value iteration).
                  */
-                std::vector<ValueType> getLowerBoundsOfInitialStateResults() const;
-                std::vector<ValueType> getUpperBoundsOfInitialStateResults() const;
+                std::vector<ValueType> getUnderApproximationOfInitialStateResults() const;
+                std::vector<ValueType> getOverApproximationOfInitialStateResults() const;
                 
                 
                 /*!
                  * Sets the precision of this weight vector checker. After calling check() the following will hold:
                  * Let h_lower and h_upper be two hyperplanes such that
-                 * * the normal vector is the provided weight-vector
-                 * * getLowerBoundsOfInitialStateResults() lies on h_lower and
-                 * * getUpperBoundsOfInitialStateResults() lies on h_upper.
+                 * * the normal vector is the provided weight-vector where the entry for minimizing objectives is negated
+                 * * getUnderApproximationOfInitialStateResults() lies on h_lower and
+                 * * getOverApproximationOfInitialStateResults() lies on h_upper.
                  * Then the distance between the two hyperplanes is at most weightedPrecision
                  */
                 void setWeightedPrecision(ValueType const& weightedPrecision);
@@ -82,7 +82,7 @@ namespace storm {
             protected:
                 
                 /*!
-                 * Determines the scheduler that maximizes the weighted reward vector of the unbounded objectives
+                 * Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives
                  *
                  * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives)
                  */
@@ -134,12 +134,7 @@ namespace storm {
                 storm::storage::BitVector objectivesWithNoUpperTimeBound;
                 // stores the (discretized) state action rewards for each objective.
                 std::vector<std::vector<ValueType>> discreteActionRewards;
-                /* stores the precision of this weight vector checker. After calling check() the following will hold:
-                * Let h_lower and h_upper be two hyperplanes such that
-                * * the normal vector is the provided weight-vector
-                * * getLowerBoundsOfInitialStateResults() lies on h_lower and
-                * * getUpperBoundsOfInitialStateResults() lies on h_upper.
-                * Then the distance between the two hyperplanes is at most weightedPrecision */
+                // stores the precision of this weight vector checker.
                 ValueType weightedPrecision;
                 // Memory for the solution of the most recent call of check(..)
                 // becomes true after the first call of check(..)
@@ -148,11 +143,11 @@ namespace storm {
                 std::vector<ValueType> weightedResult;
                 // The results for the individual objectives (w.r.t. all states of the model)
                 std::vector<std::vector<ValueType>> objectiveResults;
-                // Stores for each objective the distance between the computed result (w.r.t. the initial state) and a lower/upper bound for the actual result.
+                // Stores for each objective the distance between the computed result (w.r.t. the initial state) and an over/under approximation for the actual result.
                 // The distances are stored as a (possibly negative) offset that has to be added (+) to to the objectiveResults.
-                std::vector<ValueType> offsetsToLowerBound;
-                std::vector<ValueType> offsetsToUpperBound;
-                // The scheduler that maximizes the weighted rewards
+                std::vector<ValueType> offsetsToUnderApproximation;
+                std::vector<ValueType> offsetsToOverApproximation;
+                // The scheduler that optimizes the weighted rewards
                 storm::storage::TotalScheduler scheduler;
                 
             };