diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 7f4c5ff31..a1a779bc3 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/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; } } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index 559882c9a..dcc12d8d6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/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 ::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index f41e4c621..01ea6f616 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/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(); - this->offsetsToUpperBound[objIndex] = storm::utility::zero(); + this->offsetsToUnderApproximation[objIndex] = storm::utility::zero(); + this->offsetsToOverApproximation[objIndex] = storm::utility::zero(); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index c85a22c5c..a7feb8ae6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/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() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero())); weightVectorChecker->check(storm::utility::vector::convertNumericVector(direction)); - STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()))); + STORM_LOG_DEBUG("weighted objectives checker result (under approximation) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVectorChecker->getUnderApproximationOfInitialStateResults()))); RefinementStep step; step.weightVector = direction; - step.lowerBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()); - step.upperBoundPoint = storm::utility::vector::convertNumericVector(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(weightVectorChecker->getUnderApproximationOfInitialStateResults()); + step.upperBoundPoint = storm::utility::vector::convertNumericVector(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(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index d944aa7c3..a5427ccd8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/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(getLowerBoundsOfInitialStateResults()))); + STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(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(), 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 - std::vector::ValueType> SparsePcaaWeightVectorChecker::getLowerBoundsOfInitialStateResults() const { + std::vector::ValueType> SparsePcaaWeightVectorChecker::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 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 - std::vector::ValueType> SparsePcaaWeightVectorChecker::getUpperBoundsOfInitialStateResults() const { + std::vector::ValueType> SparsePcaaWeightVectorChecker::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 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(); - offsetsToUpperBound[objIndex] = storm::utility::zero(); + offsetsToUnderApproximation[objIndex] = storm::utility::zero(); + offsetsToOverApproximation[objIndex] = storm::utility::zero(); 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 diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 314cec988..691b69fad 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/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 @@ -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 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 getLowerBoundsOfInitialStateResults() const; - std::vector getUpperBoundsOfInitialStateResults() const; + std::vector getUnderApproximationOfInitialStateResults() const; + std::vector 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> 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 weightedResult; // The results for the individual objectives (w.r.t. all states of the model) std::vector> 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 offsetsToLowerBound; - std::vector offsetsToUpperBound; - // The scheduler that maximizes the weighted rewards + std::vector offsetsToUnderApproximation; + std::vector offsetsToOverApproximation; + // The scheduler that optimizes the weighted rewards storm::storage::TotalScheduler scheduler; };