better time bounds

Former-commit-id: 57140de514

src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp

@@ -19,7 +19,7 @@ namespace storm {
             SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker<SparseMaModelType>(data) {
                 // Set the (discretized) state action rewards.
                 this->discreteActionRewards.resize(data.objectives.size());
-                for(auto objIndex : this->unboundedObjectives) {
+                for(auto objIndex : this->objectivesWithNoUpperTimeBound) {
                     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>());
@@ -62,7 +62,7 @@ namespace storm {
                 linEq.b.resize(PS.getNumberOfStates());
                 
                 // Stores the objectives for which we need to compute values in the current time epoch.
-                storm::storage::BitVector consideredObjectives = this->unboundedObjectives;
+                storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound;
                 
                 auto lowerTimeBoundIt = lowerTimeBounds.begin();
                 auto upperTimeBoundIt = upperTimeBounds.begin();
@@ -119,7 +119,7 @@ namespace storm {
                 for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
                     std::vector<ValueType>& objVector = result.objectiveRewardVectors[objIndex];
                     objVector = std::vector<ValueType>(result.weightedRewardVector.size(), storm::utility::zero<ValueType>());
-                    if(this->unboundedObjectives.get(objIndex)) {
+                    if(this->objectivesWithNoUpperTimeBound.get(objIndex)) {
                         storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]);
                     } else {
                         typename SparseMaModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName);
@@ -154,22 +154,18 @@ namespace storm {
                 
                 // Initialize some data for fast and easy access
                 VT const maxRate = this->data.preprocessedModel.getMaximalExitRate();
-                std::vector<std::pair<VT, VT>> lowerUpperBounds;
+                std::vector<std::pair<VT, VT>> boundPairs;
                 std::vector<std::pair<VT, VT>> eToPowerOfMinusMaxRateTimesBound;
                 for(auto const& obj : this->data.objectives) {
-                    if(obj.timeBounds) {
-                        if(obj.timeBounds->which() == 0) {
-                            lowerUpperBounds.emplace_back(storm::utility::zero<VT>(), storm::utility::convertNumber<VT>(boost::get<uint_fast64_t>(*obj.timeBounds)));
-                            eToPowerOfMinusMaxRateTimesBound.emplace_back(storm::utility::one<VT>(), std::exp(-maxRate * lowerUpperBounds.back().second));
-                        } else {
-                            auto const& pair = boost::get<std::pair<double, double>>(*obj.timeBounds);
-                            lowerUpperBounds.emplace_back(storm::utility::convertNumber<VT>(pair.first), storm::utility::convertNumber<VT>(pair.second));
-                            eToPowerOfMinusMaxRateTimesBound.emplace_back(std::exp(-maxRate * lowerUpperBounds.back().first), std::exp(-maxRate * lowerUpperBounds.back().second));
-                        }
+                    if(obj.lowerTimeBound || obj.upperTimeBound) {
+                        boundPairs.emplace_back(obj.lowerTimeBound ? (*obj.lowerTimeBound) : storm::utility::zero<VT>(),
+                                                obj.upperTimeBound ? (*obj.upperTimeBound) : storm::utility::zero<VT>());
+                        eToPowerOfMinusMaxRateTimesBound.emplace_back(std::exp(-maxRate * boundPairs.back().first),
+                                                                      std::exp(-maxRate * boundPairs.back().second));
                     }
                 }
                 VT smallestNonZeroBound = storm::utility::zero<VT>();
-                for (auto const& bounds : lowerUpperBounds) {
+                for (auto const& bounds : boundPairs) {
                     if(!storm::utility::isZero(bounds.first)) {
                         smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? bounds.first : std::min(smallestNonZeroBound, bounds.first);
                     } else if (!storm::utility::isZero(bounds.second)) {
@@ -189,7 +185,7 @@ namespace storm {
                 VT delta = smallestNonZeroBound / smallestStepBound;
                 while(true) {
                     bool deltaValid = true;
-                    for(auto const& bounds : lowerUpperBounds) {
+                    for(auto const& bounds : boundPairs) {
                         if(bounds.first/delta  != std::floor(bounds.first/delta) ||
                            bounds.second/delta != std::floor(bounds.second/delta)) {
                             deltaValid = false;
@@ -197,9 +193,9 @@ namespace storm {
                         }
                     }
                     if(deltaValid) {
-                        for(uint_fast64_t i = 0; i<lowerUpperBounds.size(); ++i) {
-                            VT precisionOfObj = storm::utility::one<VT>() - (eToPowerOfMinusMaxRateTimesBound[i].first * storm::utility::pow(storm::utility::one<VT>() + maxRate * delta, lowerUpperBounds[i].first / delta) );
-                            precisionOfObj += storm::utility::one<VT>() - (eToPowerOfMinusMaxRateTimesBound[i].second * storm::utility::pow(storm::utility::one<VT>() + maxRate * delta, lowerUpperBounds[i].second / delta) );
+                        for(uint_fast64_t i = 0; i<boundPairs.size(); ++i) {
+                            VT precisionOfObj = storm::utility::one<VT>() - (eToPowerOfMinusMaxRateTimesBound[i].first * storm::utility::pow(storm::utility::one<VT>() + maxRate * delta, boundPairs[i].first / delta) );
+                            precisionOfObj += storm::utility::one<VT>() - (eToPowerOfMinusMaxRateTimesBound[i].second * storm::utility::pow(storm::utility::one<VT>() + maxRate * delta, boundPairs[i].second / delta) );
                             if(precisionOfObj > this->maximumLowerUpperBoundGap) {
                                 deltaValid = false;
                                 break;
@@ -259,35 +255,22 @@ namespace storm {
                 VT const maxRate = this->data.preprocessedModel.getMaximalExitRate();
                 for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
                     auto const& obj = this->data.objectives[objIndex];
-                    if(obj.timeBounds) {
-                        boost::optional<VT> objLowerBound, objUpperBound;
-                        if(obj.timeBounds->which() == 0) {
-                            objUpperBound = storm::utility::convertNumber<VT>(boost::get<uint_fast64_t>(obj.timeBounds.get()));
-                        } else {
-                            auto const& pair = boost::get<std::pair<double, double>>(obj.timeBounds.get());
-                            if(!storm::utility::isZero(pair.first)) {
-                                objLowerBound = storm::utility::convertNumber<VT>(pair.first);
-                            }
-                            objUpperBound = storm::utility::convertNumber<VT>(pair.second);
-                        }
-                        if(objLowerBound) {
-                            uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*objLowerBound)/digitizationConstant);
+                    if(obj.lowerTimeBound) {
+                        uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*obj.lowerTimeBound)/digitizationConstant);
                         auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
                         timeBoundIt->second.set(objIndex);
                         VT digitizationError = storm::utility::one<VT>();
-                            digitizationError -= std::exp(-maxRate * (*objLowerBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
+                        digitizationError -= std::exp(-maxRate * (*obj.lowerTimeBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
                         this->offsetsToLowerBound[objIndex] = -digitizationError;
-                            
                     } else {
                         this->offsetsToLowerBound[objIndex] = storm::utility::zero<VT>();
                     }
-                        
-                        if(objUpperBound) {
-                            uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*objUpperBound)/digitizationConstant);
+                    if(obj.upperTimeBound) {
+                        uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*obj.upperTimeBound)/digitizationConstant);
                         auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
                         timeBoundIt->second.set(objIndex);
                         VT digitizationError = storm::utility::one<VT>();
-                            digitizationError -= std::exp(-maxRate * (*objUpperBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
+                        digitizationError -= std::exp(-maxRate * (*obj.upperTimeBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
                         this->offsetsToUpperBound[objIndex] = digitizationError;
                     } else {
                         this->offsetsToUpperBound[objIndex] = storm::utility::zero<VT>();
@@ -295,7 +278,6 @@ namespace storm {
                     STORM_LOG_ASSERT(this->offsetsToUpperBound[objIndex] - this->offsetsToLowerBound[objIndex] <= this->maximumLowerUpperBoundGap, "Precision not sufficient.");
                 }
             } 
-            }
             
             template <class SparseMaModelType>
             template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type>

src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp

@@ -33,27 +33,16 @@ namespace storm {
                 std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> upperTimeBounds;
                 for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
                     auto const& obj = this->data.objectives[objIndex];
-                    if(obj.timeBounds) {
-                        boost::optional<uint_fast64_t> objLowerBound, objUpperBound;
-                        if(obj.timeBounds->which() == 0) {
-                            objUpperBound = boost::get<uint_fast64_t>(obj.timeBounds.get());
-                        } else {
-                            auto const& pair = boost::get<std::pair<double, double>>(obj.timeBounds.get());
-                            if(!storm::utility::isZero(pair.first)) {
-                                objLowerBound = storm::utility::convertNumber<uint_fast64_t>(pair.first);
-                                STORM_LOG_WARN_COND(storm::utility::isZero(pair.first - (*objLowerBound)), "Rounded non-integral bound " << pair.first << " to " << *objLowerBound << ".");
-                            }
-                            objUpperBound = storm::utility::convertNumber<uint_fast64_t>(pair.second);
-                            STORM_LOG_WARN_COND(storm::utility::isZero(pair.second - (*objUpperBound)), "Rounded non-integral bound " << pair.second << " to " << *objUpperBound << ".");
-                        }
-                        if(objLowerBound) {
-                            auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(*objLowerBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
+                    if(obj.lowerTimeBound) {
+                        auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(storm::utility::convertNumber<uint_fast64_t>(*obj.lowerTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first;
+                        STORM_LOG_WARN_COND(storm::utility::convertNumber<ValueType>(timeBoundIt->first) == (*obj.lowerTimeBound), "Rounded non-integral bound " << *obj.lowerTimeBound << " to " << timeBoundIt->first  << ".");
                         timeBoundIt->second.set(objIndex);
                     }
-                        if(objUpperBound) {
-                            auto timeBoundIt = upperTimeBounds.insert(std::make_pair(*objUpperBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
+                    if(obj.upperTimeBound) {
+                        auto timeBoundIt = upperTimeBounds.insert(std::make_pair(storm::utility::convertNumber<uint_fast64_t>(*obj.upperTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first;
+                        STORM_LOG_WARN_COND(storm::utility::convertNumber<ValueType>(timeBoundIt->first) == (*obj.upperTimeBound), "Rounded non-integral bound " << *obj.upperTimeBound << " to " << timeBoundIt->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>();
@@ -61,7 +50,7 @@ namespace storm {
                 }
                 
                 // Stores the objectives for which we need to compute values in the current time epoch.
-                storm::storage::BitVector consideredObjectives = this->unboundedObjectives;
+                storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound;
                 
                 // Stores objectives for which the current epoch passed their lower bound
                 storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false);

src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h

@@ -32,8 +32,8 @@ namespace storm {
                 bool thresholdIsStrict = false;
                 
                 // The time bound(s) for the formula (if given by the originalFormula)
-                // If only a discrete bound is given, it is interpreted as an upper bound
-                boost::optional<boost::variant<uint_fast64_t, std::pair<double, double>>> timeBounds;
+                boost::optional<ValueType> lowerTimeBound;
+                boost::optional<ValueType> upperTimeBound;
                 
                 // Stores whether reward finiteness has been checked for this objective.
                 bool rewardFinitenessChecked;
@@ -51,13 +51,15 @@ namespace storm {
                     out << " \t";
                     out << "intern reward model: " << std::setw(10) << rewardModelName;
                     out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t";
-                    out << "time bound:";
-                    if(timeBounds) {
-                        if(timeBounds->which() == 0 ) {
-                            out << "<=" << std::setw(5) << (boost::get<uint_fast64_t>(timeBounds.get()));
+                    out << "time bounds:";
+                    if(lowerTimeBound) {
+                        if(upperTimeBound) {
+                            out << "[" << *lowerTimeBound << ", " <<  *upperTimeBound << "]";
                         } else {
-                            out << "[" << boost::get<std::pair<double, double>>(timeBounds.get()).first << ", " <<  boost::get<std::pair<double, double>>(timeBounds.get()).second << "]";
+                            out << ">=" << std::setw(5) << *lowerTimeBound;
                         }
+                    } else if (upperTimeBound) {
+                        out << "<=" << std::setw(5) << *upperTimeBound;
                     } else {
                         out << " none";
                     }

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp

@@ -190,7 +190,7 @@ namespace storm {
                 storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
                 storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
                 
-                if(!(psiStates & data.preprocessedModel.getInitialStates()).empty()) {
+                if(!(psiStates & data.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) {
                     // The probability is always one
                     data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
                     data.solutionsFromPreprocessing[data.objectives.size()-1].second = currentObjective.rewardsArePositive ? storm::utility::one<ValueType>() : -storm::utility::one<ValueType>();
@@ -258,24 +258,21 @@ namespace storm {
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 
-                if(data.originalModel.isOfType(storm::models::ModelType::Mdp)) {
-                    STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with a discrete time bound but got " << formula << ".");
-                    STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula with time bound 0. This is not supported.");
-                    currentObjective.timeBounds = formula.getDiscreteTimeBound();
-                    preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
-                    
-                } else if(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
                 if(formula.hasDiscreteTimeBound()) {
-                        STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula with time bound 0. This is not supported.");
-                        currentObjective.timeBounds = formula.getDiscreteTimeBound();
+                    currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getDiscreteTimeBound());
                 } else {
-                        STORM_LOG_THROW(formula.getIntervalBounds().first<formula.getIntervalBounds().second, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula where the lower time bound is not strictly smaller than the upper time bound. This is not supported.");
-                        currentObjective.timeBounds = formula.getIntervalBounds();
-                    }
-                    preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
+                    if(data.originalModel.isOfType(storm::models::ModelType::Mdp)) {
+                        STORM_LOG_THROW(formula.getIntervalBounds().first == std::round(formula.getIntervalBounds().first), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete lower time bound but got " << formula << ".");
+                        STORM_LOG_THROW(formula.getIntervalBounds().second == std::round(formula.getIntervalBounds().second), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete upper time bound but got " << formula << ".");
                     } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type.");
+                        STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type.");
+                    }
+                    if(!storm::utility::isZero(formula.getIntervalBounds().first)) {
+                        currentObjective.lowerTimeBound = storm::utility::convertNumber<ValueType>(formula.getIntervalBounds().first);
                     }
+                    currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getIntervalBounds().second);
+                }
+                preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
             }
             
             template<typename SparseModelType>
@@ -360,10 +357,14 @@ namespace storm {
             
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
-                STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for Markov automata.");
+                STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type.");
                 STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << ".");
-                STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a cumulativeRewardFormula with time bound 0. This is not supported.");
-                currentObjective.timeBounds = formula.getDiscreteTimeBound();
+                if(formula.getDiscreteTimeBound()==0) {
+                    data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
+                    data.solutionsFromPreprocessing[data.objectives.size()-1].second = storm::utility::zero<ValueType>();
+                    return;
+                }
+                currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getDiscreteTimeBound());
                 
                 RewardModelType objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
                 objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false);

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@@ -22,11 +22,11 @@ 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()), offsetsToLowerBound(data.objectives.size()), offsetsToUpperBound(data.objectives.size()) {
+            SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), objectivesWithNoUpperTimeBound(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) {
-                    unboundedObjectives.set(objIndex, !data.objectives[objIndex].timeBounds);
+                    objectivesWithNoUpperTimeBound.set(objIndex, !data.objectives[objIndex].upperTimeBound);
                 }
                 // Enlarge the set of prob1 states to the states that are only reachable via prob1 states
                 statesThatAreAllowedToBeVisitedInfinitelyOften = ~storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getInitialStates(), ~data.preprocessedModel.getStates(data.prob1StatesLabel), storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false));
@@ -38,14 +38,14 @@ namespace storm {
                 checkHasBeenCalled=true;
                 STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::convertNumericVector<double>(weightVector));
                 std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
-                for(auto objIndex : unboundedObjectives) {
+                for(auto objIndex : objectivesWithNoUpperTimeBound) {
                     storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]);
                 }
                 unboundedWeightedPhase(weightedRewardVector);
                 unboundedIndividualPhase(weightVector);
                 // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound
                 for(auto const& obj : this->data.objectives) {
-                    if(obj.timeBounds) {
+                    if(obj.lowerTimeBound || obj.upperTimeBound) {
                         boundedPhase(weightVector, weightedRewardVector);
                         break;
                     }
@@ -91,14 +91,14 @@ namespace storm {
             storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const {
                 STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
                 for(auto const& obj : this->data.objectives) {
-                    STORM_LOG_THROW(!obj.timeBounds, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
+                    STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
                 }
                 return scheduler;
             }
             
             template <class SparseModelType>
             void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector) {
-                if(this->unboundedObjectives.empty()) {
+                if(this->objectivesWithNoUpperTimeBound.empty()) {
                     this->weightedResult = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>());
                     this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates());
                     return;
@@ -136,7 +136,7 @@ namespace storm {
                 //Also only compute values for objectives with weightVector != zero,
                 //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)){
+                    if(objectivesWithNoUpperTimeBound.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]);

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h

@@ -100,8 +100,8 @@ namespace storm {
                 
                 // stores the considered information of the multi-objective model checking problem
                 PreprocessorData const& data;
-                // stores the indices of the objectives for which there is no time bound
-                storm::storage::BitVector unboundedObjectives;
+                // stores the indices of the objectives for which there is no upper time bound
+                storm::storage::BitVector objectivesWithNoUpperTimeBound;
                 // stores the (discretized) state action rewards for each objective.
                 std::vector<std::vector<ValueType>>discreteActionRewards;