towards bounded reachability: added the ability to have a lower/upper bound for the weightVectorChecker result

Former-commit-id: 413c2dee0a

src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp

@@ -16,12 +16,12 @@ namespace storm {
                 // Set the (discretized) state action rewards.
                 this->discreteActionRewards.resize(data.objectives.size());
                 for(auto objIndex : this->unboundedObjectives) {
-                    STORM_LOG_ASSERT(!this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName).hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected.");
-                    this->discreteActionRewards[objIndex] = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName).getStateActionRewardVector();
-                    if(this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName).hasStateRewards()) {
-                        auto const& stateRewards = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName).getStateRewardVector();
+                    typename SparseMaModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName);
+                    STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected.");
+                    this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector<ValueType>(this->data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
+                    if(rewModel.hasStateRewards()) {
                         for(auto markovianState : this->data.getMarkovianStatesOfPreprocessedModel()) {
-                            this->discreteActionRewards[objIndex][this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += stateRewards[markovianState] / this->data.preprocessedModel.getExitRate(markovianState);
+                            this->discreteActionRewards[objIndex][this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->data.preprocessedModel.getExitRate(markovianState);
                         }
                     }
                     
@@ -43,6 +43,9 @@ namespace storm {
                     uint_fast64_t timeBound = boost::get<uint_fast64_t>(this->data.objectives[objIndex].timeBounds.get());
                     auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
                     timeBoundIt->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>();
                 }
                 storm::storage::BitVector objectivesAtCurrentEpoch = this->unboundedObjectives;
                 auto timeBoundIt = timeBounds.begin();
@@ -64,7 +67,7 @@ namespace storm {
                     // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results.
                     for(auto objIndex : objectivesAtCurrentEpoch) {
                         std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex];
-                        std::vector<ValueType> objectiveRewards = getObjectiveRewardAsDiscreteActionRewards(objIndex);
+                        std::vector<ValueType> objectiveRewards = this->discreteActionRewards[objIndex];
                         auto rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin();
                         auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin();
                         for(ValueType& stateValue : temporaryResult){
@@ -79,7 +82,7 @@ namespace storm {
                         objectiveResult.swap(temporaryResult);
                     }
                 }
-                 */
+*/
             }
 
             template class SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;

src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp

@@ -14,9 +14,10 @@ namespace storm {
             template <class SparseMdpModelType>
             SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker<SparseMdpModelType>(data) {
                 // set the state action rewards
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    STORM_LOG_ASSERT(!this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName).hasTransitionRewards(), "Reward model has transition rewards which is not expected.");
-                    this->discreteActionRewards[objIndex] = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName).getTotalRewardVector(this->data.preprocessedModel.getTransitionMatrix());
+                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
+                    typename SparseMdpModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName);
+                    STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected.");
+                    this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->data.preprocessedModel.getTransitionMatrix());
                 }
             }
             
@@ -33,6 +34,9 @@ namespace storm {
                     uint_fast64_t timeBound = boost::get<uint_fast64_t>(this->data.objectives[objIndex].timeBounds.get());
                     auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
                     timeBoundIt->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>();
                 }
                 storm::storage::BitVector objectivesAtCurrentEpoch = this->unboundedObjectives;
                 auto timeBoundIt = timeBounds.begin();

src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp

@@ -9,6 +9,7 @@
 #include "src/utility/vector.h"
 #include "src/settings//SettingsManager.h"
 #include "src/settings/modules/MultiObjectiveSettings.h"
+#include "src/settings/modules/GeneralSettings.h"
 
 #include "src/exceptions/UnexpectedException.h"
 
@@ -22,7 +23,6 @@ namespace storm {
                 ResultData resultData;
                 resultData.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
                 resultData.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
-                
                 if(!checkIfPreprocessingWasConclusive(preprocessorData)) {
                     switch(preprocessorData.queryType) {
                         case PreprocessorData::QueryType::Achievability:
@@ -57,6 +57,9 @@ namespace storm {
             
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) {
+                //Set the maximum gap between lower and upper bound of the weightVectorChecker result we initially allow for this query type.
+                weightVectorChecker->setMaximumLowerUpperBoundGap(storm::utility::convertNumber<SparseModelValueType>(0.1)); // TODO try other values?
+                // Get a point that represents the thresholds
                 Point thresholds;
                 thresholds.reserve(preprocessorData.objectives.size());
                 storm::storage::BitVector strictThresholds(preprocessorData.objectives.size());
@@ -64,11 +67,11 @@ namespace storm {
                     thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*preprocessorData.objectives[objIndex].threshold));
                     strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict);
                 }
-                
+                // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx.
                 storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true);
                 do {
                     WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
-                    performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
+                    performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                     if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){
                         resultData.setThresholdsAreAchievable(false);
                     }
@@ -81,6 +84,9 @@ namespace storm {
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) {
                 STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Detected numerical query but index of optimizing objective is not set.");
+                // Set the maximum gap between lower and upper bound of the weightVectorChecker result we initially allow for this query type.
+                weightVectorChecker->setMaximumLowerUpperBoundGap(storm::utility::convertNumber<SparseModelValueType>(0.1)); // TODO try other values?
+                // initialize some data
                 uint_fast64_t optimizingObjIndex = *preprocessorData.indexOfOptimizingObjective;
                 Point thresholds;
                 thresholds.reserve(preprocessorData.objectives.size());
@@ -108,9 +114,9 @@ namespace storm {
                 individualObjectivesToBeChecked.set(optimizingObjIndex, false);
                 do {
                     WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
-                    performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
+                    performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                     //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded
-                    thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], resultData.refinementSteps().back().getPoint()[optimizingObjIndex]);
+                    thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], resultData.refinementSteps().back().getLowerBoundPoint()[optimizingObjIndex]);
                     if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){
                         resultData.setThresholdsAreAchievable(false);
                     }
@@ -125,6 +131,11 @@ namespace storm {
                     // Note that we do not have to care whether a threshold is strict anymore, because the resulting optimum should be
                     // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict
                     // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds.
+                    // The euclidean distance between the lower and upper bounds of the results of the weightVectorChecker should be less than the precision given in the settings
+                    SparseModelValueType gap = storm::utility::convertNumber<SparseModelValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
+                    gap -=  storm::utility::convertNumber<SparseModelValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+                    gap /= storm::utility::sqrt(static_cast<SparseModelValueType>(preprocessorData.objectives.size()));
+                    weightVectorChecker->setMaximumLowerUpperBoundGap(gap); // TODO try other values?
                     while(true) {
                         std::pair<Point, bool> optimizationRes = resultData.underApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
                         STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty.");
@@ -142,18 +153,25 @@ namespace storm {
                             break;
                         }
                         WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
-                        performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
+                        performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                     }
                 }
             }
             
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) {
+                // Set the maximum gap between lower and upper bound of the weightVectorChecker result we initially allow for this query type.
+                // The euclidean distance between the lower and upper bounds of the results of the weightVectorChecker should be less than the precision given in the settings
+                SparseModelValueType gap = storm::utility::convertNumber<SparseModelValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
+                gap -=  storm::utility::convertNumber<SparseModelValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+                gap /= storm::utility::sqrt(static_cast<SparseModelValueType>(preprocessorData.objectives.size()));
+                weightVectorChecker->setMaximumLowerUpperBoundGap(gap); // TODO try other values?
+                
                 //First consider the objectives individually
                 for(uint_fast64_t objIndex = 0; objIndex<preprocessorData.objectives.size() && !maxStepsPerformed(resultData); ++objIndex) {
                     WeightVector direction(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
                     direction[objIndex] = storm::utility::one<RationalNumberType>();
-                    performRefinementStep(direction, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
+                    performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                 }
                 
                 while(true) {
@@ -177,7 +195,7 @@ namespace storm {
                         break;
                     }
                     WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector();
-                    performRefinementStep(direction, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
+                    performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                 }
             }
             
@@ -225,13 +243,41 @@ namespace storm {
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& result) {
-                weightVectorChecker->check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction));
-                STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getInitialStateResultOfObjectives()));
+            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector&& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& result) {
+                // Normalize the direction vector so that the entries sum up to one
+                storm::utility::vector::scaleVectorInPlace(direction, storm::utility::one<RationalNumberType>() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero<RationalNumberType>()));
+                // Check if we already did a refinement step with that direction vector. If this is the case, we increase the precision.
+                // We start with the most recent steps to consider the most recent result for this direction vector
+                boost::optional<SparseModelValueType> oldMaximumLowerUpperBoundGap;
+                for(auto stepIt = result.refinementSteps().rbegin(); stepIt != result.refinementSteps().rend(); ++stepIt) {
+                    if(stepIt->getWeightVector() == direction) {
+                        STORM_LOG_WARN("Performing multiple refinement steps with the same direction vector.");
+                        oldMaximumLowerUpperBoundGap = weightVectorChecker->getMaximumLowerUpperBoundGap();
+                        std::vector<RationalNumberType> lowerUpperDistances = stepIt->getUpperBoundPoint();
+                        storm::utility::vector::subtractVectors(lowerUpperDistances, stepIt->getLowerBoundPoint(), lowerUpperDistances);
+                        // shorten the distance between lower and upper bound for the new result by multiplying the current distance with 0.5
+                        // TODO: try other values/strategies?
+                        RationalNumberType distance = storm::utility::sqrt(storm::utility::vector::dotProduct(lowerUpperDistances, lowerUpperDistances));
+                        weightVectorChecker->setMaximumLowerUpperBoundGap(storm::utility::convertNumber<SparseModelValueType>(distance) + storm::utility::convertNumber<SparseModelValueType>(0.5));
+                        break;
+                    }
+                }
+                weightVectorChecker->check(storm::utility::vector::convertNumericVector<SparseModelValueType>(direction));
+                if(oldMaximumLowerUpperBoundGap) {
+                    // Reset the precision back to the previous values
+                    weightVectorChecker->setMaximumLowerUpperBoundGap(*oldMaximumLowerUpperBoundGap);
+                }
+                STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getLowerBoundsOfInitialStateResults()));
+                
                 if(saveScheduler) {
-                    result.refinementSteps().emplace_back(direction, weightVectorChecker->template getInitialStateResultOfObjectives<RationalNumberType>(), weightVectorChecker->getScheduler());
+                    result.refinementSteps().emplace_back(direction,
+                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getLowerBoundsOfInitialStateResults()),
+                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getUpperBoundsOfInitialStateResults()),
+                                                          weightVectorChecker->getScheduler());
                 } else {
-                    result.refinementSteps().emplace_back(direction, weightVectorChecker->template getInitialStateResultOfObjectives<RationalNumberType>());
+                    result.refinementSteps().emplace_back(direction,
+                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getLowerBoundsOfInitialStateResults()),
+                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getUpperBoundsOfInitialStateResults()));
                 }
                 updateOverApproximation(result.refinementSteps(), result.overApproximation());
                 updateUnderApproximation(result.refinementSteps(), result.underApproximation());
@@ -239,18 +285,18 @@ namespace storm {
             
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateOverApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation) {
-                storm::storage::geometry::Halfspace<RationalNumberType> h(refinementSteps.back().getWeightVector(), storm::utility::vector::dotProduct(refinementSteps.back().getWeightVector(), refinementSteps.back().getPoint()));
+                storm::storage::geometry::Halfspace<RationalNumberType> h(refinementSteps.back().getWeightVector(), storm::utility::vector::dotProduct(refinementSteps.back().getWeightVector(), refinementSteps.back().getUpperBoundPoint()));
                 
                 // Due to numerical issues, it might be the case that the updated overapproximation does not contain the underapproximation,
                 // e.g., when the new point is strictly contained in the underapproximation. Check if this is the case.
                 RationalNumberType maximumOffset = h.offset();
                 for(auto const& step : refinementSteps){
-                    maximumOffset = std::max(maximumOffset, storm::utility::vector::dotProduct(h.normalVector(), step.getPoint()));
+                    maximumOffset = std::max(maximumOffset, storm::utility::vector::dotProduct(h.normalVector(), step.getLowerBoundPoint()));
                 }
                 if(maximumOffset > h.offset()){
                     // We correct the issue by shifting the halfspace such that it contains the underapproximation
                     h.offset() = maximumOffset;
-                    STORM_LOG_WARN("Numerical issues: The overapproximation would not contain the underapproximation. Hence, a halfspace is shifted by " << storm::utility::convertNumber<double>(h.euclideanDistance(refinementSteps.back().getPoint())) << ".");
+                    STORM_LOG_WARN("Numerical issues: The overapproximation would not contain the underapproximation. Hence, a halfspace is shifted by " << storm::utility::convertNumber<double>(h.euclideanDistance(refinementSteps.back().getUpperBoundPoint())) << ".");
                 }
                 overApproximation = overApproximation->intersection(h);
                 STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true));
@@ -261,7 +307,7 @@ namespace storm {
                 std::vector<Point> paretoPoints;
                 paretoPoints.reserve(refinementSteps.size());
                 for(auto const& step : refinementSteps) {
-                    paretoPoints.push_back(step.getPoint());
+                    paretoPoints.push_back(step.getLowerBoundPoint());
                 }
                 underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createDownwardClosure(paretoPoints);
                 STORM_LOG_DEBUG("Updated UnderApproximation to " << underApproximation->toString(true));

src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h

@@ -16,6 +16,8 @@ namespace storm {
             template <class SparseModelType, typename RationalNumberType>
             class SparseMultiObjectiveHelper {
             public:
+                typedef typename SparseModelType::ValueType SparseModelValueType;
+                
                 typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
                 typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData;
                 typedef SparseMultiObjectiveRefinementStep<RationalNumberType> RefinementStep;
@@ -52,7 +54,7 @@ namespace storm {
                 /*
                  * Refines the current result w.r.t. the given direction vector
                  */
-                static void performRefinementStep(WeightVector const& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& resultData);
+                static void performRefinementStep(WeightVector&& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& resultData);
                 
                 /*
                  * Updates the overapproximation after a refinement step has been performed

src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp

@@ -170,7 +170,7 @@ namespace storm {
                 std::vector<std::vector<ValueType>> paretoOptimalPoints;
                 paretoOptimalPoints.reserve(resultData.refinementSteps().size());
                 for(auto const& step : resultData.refinementSteps()) {
-                    paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<ValueType>(transformToOriginalValues(step.getPoint(), preprocessorData)));
+                    paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<ValueType>(transformToOriginalValues(step.getLowerBoundPoint(), preprocessorData)));
                 }
                 return std::unique_ptr<CheckResult>(new ParetoCurveCheckResult<ValueType>(
                           initState,
@@ -220,7 +220,7 @@ namespace storm {
                 std::vector<std::vector<RationalNumberType>> paretoPoints;
                 paretoPoints.reserve(resultData.refinementSteps().size());
                 for(auto const& step : resultData.refinementSteps()) {
-                    paretoPoints.push_back(transformToOriginalValues(step.getPoint(), preprocessorData));
+                    paretoPoints.push_back(transformToOriginalValues(step.getLowerBoundPoint(), preprocessorData));
                     boundaries.enlarge(paretoPoints.back());
                 }
                 auto underApproxVertices = transformedUnderApprox->getVertices();

src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h

@@ -14,19 +14,19 @@ namespace storm {
             class SparseMultiObjectiveRefinementStep {
                 
             public:
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& lowerBoundPoint, std::vector<RationalNumberType> const& upperBoundPoint, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint), scheduler(scheduler) {
                     //Intentionally left empty
                 }
                 
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& lowerBoundPoint, std::vector<RationalNumberType>&& upperBoundPoint, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint), scheduler(scheduler) {
                     //Intentionally left empty
                 }
                 
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point) : weightVector(weightVector), point(point) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& lowerBoundPoint, std::vector<RationalNumberType> const& upperBoundPoint) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint) {
                     //Intentionally left empty
                 }
                 
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point) : weightVector(weightVector), point(point) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& lowerBoundPoint, std::vector<RationalNumberType>&& upperBoundPoint) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint) {
                     //Intentionally left empty
                 }
                 
@@ -34,8 +34,12 @@ namespace storm {
                     return weightVector;
                 }
                 
-                std::vector<RationalNumberType> const& getPoint() const {
-                    return point;
+                std::vector<RationalNumberType> const& getLowerBoundPoint() const {
+                    return lowerBoundPoint;
+                }
+                
+                std::vector<RationalNumberType> const& getUpperBoundPoint() const {
+                    return upperBoundPoint;
                 }
                 
                 bool hasScheduler() const {
@@ -48,7 +52,8 @@ namespace storm {
                 
             private:
                 std::vector<RationalNumberType> const weightVector;
-                std::vector<RationalNumberType> const point;
+                std::vector<RationalNumberType> const lowerBoundPoint;
+                std::vector<RationalNumberType> const upperBoundPoint;
                 boost::optional<storm::storage::TotalScheduler> const scheduler;
             };
         }

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@@ -22,7 +22,7 @@ namespace storm {
             
 
             template <class SparseModelType>
-            SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), unboundedObjectives(data.objectives.size()), discreteActionRewards(data.objectives.size()), checkHasBeenCalled(false), objectiveResults(data.objectives.size()){
+            SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), unboundedObjectives(data.objectives.size()), discreteActionRewards(data.objectives.size()), checkHasBeenCalled(false), objectiveResults(data.objectives.size()), offsetsToLowerBound(data.objectives.size()), offsetsToUpperBound(data.objectives.size()) {
                 
                 // set the unbounded objectives
                 for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
@@ -44,22 +44,42 @@ namespace storm {
                 unboundedWeightedPhase(weightedRewardVector);
                 STORM_LOG_DEBUG("Unbounded weighted phase result: " << weightedResult[data.preprocessedModel.getInitialStates().getNextSetIndex(0)] << " (value in initial state).");
                 unboundedIndividualPhase(weightVector);
-                STORM_LOG_DEBUG("Unbounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>());
                 if(!this->unboundedObjectives.full()) {
                     boundedPhase(weightVector, weightedRewardVector);
-                    STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>() << " ...WeightVectorChecker done.");
                 }
+                STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults()));
             }
             
             template <class SparseModelType>
-            template<typename TargetValueType>
-            std::vector<TargetValueType> SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getInitialStateResultOfObjectives() const {
+            void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::setMaximumLowerUpperBoundGap(ValueType const& value) {
+                this->maximumLowerUpperBoundGap = value;
+            }
+            
+            template <class SparseModelType>
+            typename SparseMultiObjectiveWeightVectorChecker<SparseModelType>::ValueType const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getMaximumLowerUpperBoundGap() const {
+                return this->maximumLowerUpperBoundGap;
+            }
+            
+            template <class SparseModelType>
+            std::vector<typename SparseMultiObjectiveWeightVectorChecker<SparseModelType>::ValueType> SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getLowerBoundsOfInitialStateResults() const {
                 STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
-                STORM_LOG_ASSERT(data.preprocessedModel.getInitialStates().getNumberOfSetBits()==1, "The considered model has multiple initial states");
-                std::vector<TargetValueType> res;
-                res.reserve(objectiveResults.size());
-                for(auto const& objResult : objectiveResults) {
-                    res.push_back(storm::utility::convertNumber<TargetValueType>(objResult[*data.preprocessedModel.getInitialStates().begin()]));
+                uint_fast64_t initstate = *this->data.preprocessedModel.getInitialStates().begin();
+                std::vector<ValueType> res;
+                res.reserve(this->data.objectives.size());
+                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
+                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToLowerBound[objIndex]);
+                }
+                return res;
+            }
+            
+            template <class SparseModelType>
+            std::vector<typename SparseMultiObjectiveWeightVectorChecker<SparseModelType>::ValueType> SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getUpperBoundsOfInitialStateResults() const {
+                STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
+                uint_fast64_t initstate = *this->data.preprocessedModel.getInitialStates().begin();
+                std::vector<ValueType> res;
+                res.reserve(this->data.objectives.size());
+                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
+                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUpperBound[objIndex]);
                 }
                 return res;
             }
@@ -147,6 +167,8 @@ namespace storm {
                 //one check can be omitted as the result can be computed back from the weighed result and the results from the remaining objectives
                 for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
                     if(unboundedObjectives.get(objIndex)){
+                        offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
+                        offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
                         storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
                         storm::storage::BitVector statesWithRewards =  ~storm::utility::vector::filterZero(deterministicStateRewards);
                         // As target states, we pick the states from which no reward is reachable.
@@ -166,19 +188,10 @@ namespace storm {
             }
             
             template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>;
-            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<double>() const;
             template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;
-            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getInitialStateResultOfObjectives<double>() const;
 #ifdef STORM_HAVE_CARL
-            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
-            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
-            
             template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
-            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>::getInitialStateResultOfObjectives<double>() const;
             template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
-            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getInitialStateResultOfObjectives<double>() const;
-            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
-            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
 #endif
             
         }

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h

@@ -33,13 +33,28 @@ namespace storm {
                 void check(std::vector<ValueType> const& weightVector);
                 
                 /*!
-                 * Getter methods for the results of the most recent call of check(..)
+                 * Sets the maximum gap that is allowed between the lower and upper bound of the result of some objective.
+                 */
+                void setMaximumLowerUpperBoundGap(ValueType const& value);
+                
+                /*!
+                 * Retrieves the maximum gap that is allowed between the lower and upper bound of the result of some objective.
+                 */
+                ValueType const& getMaximumLowerUpperBoundGap() const;
+                
+                /*!
+                 * 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
+                 * as long as the underlying solution methods are unsound (e.g., standard value iteration).
+                 */
+                std::vector<ValueType> getLowerBoundsOfInitialStateResults() const;
+                std::vector<ValueType> getUpperBoundsOfInitialStateResults() const;
+                
+                /*!
+                 * Retrieves a scheduler that induces the current values
+                 * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown.
                  */
-                // The results of the individual objectives at the initial state of the given model
-                template<typename TargetValueType = ValueType>
-                std::vector<TargetValueType> getInitialStateResultOfObjectives() const;
-                // A scheduler that induces the optimal values
                 storm::storage::TotalScheduler const& getScheduler() const;
                 
                 
@@ -85,10 +100,19 @@ namespace storm {
                 // becomes true after the first call of check(..)
                 bool checkHasBeenCalled;
                 
+                // stores the maximum gap that is allowed between the lower and upper bound of the result of some objective.
+                ValueType maximumLowerUpperBoundGap;
+                
                 // The result for the weighted reward vector (for all states of the model)
                 std::vector<ValueType> weightedResult;
-                // The results for the individual objectives (for all states of the model)
+                // The lower bounds of 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.
+                // The distances are stored as a (possibly negative) offset that has to be added to to the objectiveResults.
+                // Note that there is no guarantee that the lower/upper bounds are sound as long as the underlying solution method is not sound (e.g. standard value iteration).
+                std::vector<ValueType> offsetsToLowerBound;
+                std::vector<ValueType> offsetsToUpperBound;
+                
                 // The scheduler that maximizes the weighted rewards
                 storm::storage::TotalScheduler scheduler;
                 

src/modelchecker/results/ParetoCurveCheckResult.cpp

@@ -65,7 +65,7 @@ namespace storm {
             out << std::endl;
             out << "Underapproximation of achievable values: " << underApproximation->toString() << std::endl;
             out << "Overapproximation of achievable values: " << overApproximation->toString() << std::endl;
-            out << points.size() << " pareto optimal points found:" << std::endl;
+            out << points.size() << " pareto optimal points found (Note that these points are safe, i.e., contained in the underapproximation, but there is no guarantee for optimality):" << std::endl;
             for(auto const& p : points) {
                 out << "   (";
                 for(auto it = p.begin(); it != p.end(); ++it){