diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp index 7fd8b8769..b9509bfeb 100644 --- a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp @@ -19,7 +19,7 @@ namespace storm { SparseMaMultiObjectiveWeightVectorChecker::SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker(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(this->data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); @@ -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& objVector = result.objectiveRewardVectors[objIndex]; objVector = std::vector(result.weightedRewardVector.size(), storm::utility::zero()); - 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> lowerUpperBounds; + std::vector> boundPairs; std::vector> eToPowerOfMinusMaxRateTimesBound; for(auto const& obj : this->data.objectives) { - if(obj.timeBounds) { - if(obj.timeBounds->which() == 0) { - lowerUpperBounds.emplace_back(storm::utility::zero(), storm::utility::convertNumber(boost::get(*obj.timeBounds))); - eToPowerOfMinusMaxRateTimesBound.emplace_back(storm::utility::one(), std::exp(-maxRate * lowerUpperBounds.back().second)); - } else { - auto const& pair = boost::get>(*obj.timeBounds); - lowerUpperBounds.emplace_back(storm::utility::convertNumber(pair.first), storm::utility::convertNumber(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(), + obj.upperTimeBound ? (*obj.upperTimeBound) : storm::utility::zero()); + eToPowerOfMinusMaxRateTimesBound.emplace_back(std::exp(-maxRate * boundPairs.back().first), + std::exp(-maxRate * boundPairs.back().second)); } } VT smallestNonZeroBound = storm::utility::zero(); - 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() - (eToPowerOfMinusMaxRateTimesBound[i].first * storm::utility::pow(storm::utility::one() + maxRate * delta, lowerUpperBounds[i].first / delta) ); - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[i].second * storm::utility::pow(storm::utility::one() + maxRate * delta, lowerUpperBounds[i].second / delta) ); + for(uint_fast64_t i = 0; i() - (eToPowerOfMinusMaxRateTimesBound[i].first * storm::utility::pow(storm::utility::one() + maxRate * delta, boundPairs[i].first / delta) ); + precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[i].second * storm::utility::pow(storm::utility::one() + maxRate * delta, boundPairs[i].second / delta) ); if(precisionOfObj > this->maximumLowerUpperBoundGap) { deltaValid = false; break; @@ -259,43 +255,29 @@ 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 objLowerBound, objUpperBound; - if(obj.timeBounds->which() == 0) { - objUpperBound = storm::utility::convertNumber(boost::get(obj.timeBounds.get())); - } else { - auto const& pair = boost::get>(obj.timeBounds.get()); - if(!storm::utility::isZero(pair.first)) { - objLowerBound = storm::utility::convertNumber(pair.first); - } - objUpperBound = storm::utility::convertNumber(pair.second); - } - if(objLowerBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*objLowerBound)/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(); - digitizationError -= std::exp(-maxRate * (*objLowerBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); - this->offsetsToLowerBound[objIndex] = -digitizationError; - - } else { - this->offsetsToLowerBound[objIndex] = storm::utility::zero(); - } - - if(objUpperBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*objUpperBound)/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(); - digitizationError -= std::exp(-maxRate * (*objUpperBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); - this->offsetsToUpperBound[objIndex] = digitizationError; - } else { - this->offsetsToUpperBound[objIndex] = storm::utility::zero(); - } - STORM_LOG_ASSERT(this->offsetsToUpperBound[objIndex] - this->offsetsToLowerBound[objIndex] <= this->maximumLowerUpperBoundGap, "Precision not sufficient."); + if(obj.lowerTimeBound) { + uint_fast64_t digitizedBound = storm::utility::convertNumber((*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(); + digitizationError -= std::exp(-maxRate * (*obj.lowerTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); + this->offsetsToLowerBound[objIndex] = -digitizationError; + } else { + this->offsetsToLowerBound[objIndex] = storm::utility::zero(); + } + if(obj.upperTimeBound) { + uint_fast64_t digitizedBound = storm::utility::convertNumber((*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(); + digitizationError -= std::exp(-maxRate * (*obj.upperTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); + this->offsetsToUpperBound[objIndex] = digitizationError; + } else { + this->offsetsToUpperBound[objIndex] = storm::utility::zero(); } + STORM_LOG_ASSERT(this->offsetsToUpperBound[objIndex] - this->offsetsToLowerBound[objIndex] <= this->maximumLowerUpperBoundGap, "Precision not sufficient."); } - } + } template template ::SupportsExponential, int>::type> diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp index fecec0071..229535235 100644 --- a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp @@ -33,27 +33,16 @@ namespace storm { std::map> 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 objLowerBound, objUpperBound; - if(obj.timeBounds->which() == 0) { - objUpperBound = boost::get(obj.timeBounds.get()); - } else { - auto const& pair = boost::get>(obj.timeBounds.get()); - if(!storm::utility::isZero(pair.first)) { - objLowerBound = storm::utility::convertNumber(pair.first); - STORM_LOG_WARN_COND(storm::utility::isZero(pair.first - (*objLowerBound)), "Rounded non-integral bound " << pair.first << " to " << *objLowerBound << "."); - } - objUpperBound = storm::utility::convertNumber(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; - timeBoundIt->second.set(objIndex); - } - if(objUpperBound) { - auto timeBoundIt = upperTimeBounds.insert(std::make_pair(*objUpperBound, storm::storage::BitVector(this->data.objectives.size(), false))).first; - timeBoundIt->second.set(objIndex); - } + if(obj.lowerTimeBound) { + auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.lowerTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first; + STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.lowerTimeBound), "Rounded non-integral bound " << *obj.lowerTimeBound << " to " << timeBoundIt->first << "."); + timeBoundIt->second.set(objIndex); + } + if(obj.upperTimeBound) { + auto timeBoundIt = upperTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.upperTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first; + STORM_LOG_WARN_COND(storm::utility::convertNumber(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(); this->offsetsToUpperBound[objIndex] = storm::utility::zero(); @@ -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); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h index 5814bca3c..8d37a6786 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h +++ b/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>> timeBounds; + boost::optional lowerTimeBound; + boost::optional 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(timeBounds.get())); + out << "time bounds:"; + if(lowerTimeBound) { + if(upperTimeBound) { + out << "[" << *lowerTimeBound << ", " << *upperTimeBound << "]"; } else { - out << "[" << boost::get>(timeBounds.get()).first << ", " << boost::get>(timeBounds.get()).second << "]"; + out << ">=" << std::setw(5) << *lowerTimeBound; } + } else if (upperTimeBound) { + out << "<=" << std::setw(5) << *upperTimeBound; } else { out << " none"; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 0e87c9dbf..90f030d59 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/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() : -storm::utility::one(); @@ -258,24 +258,21 @@ namespace storm { template void SparseMultiObjectivePreprocessor::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(); + if(formula.hasDiscreteTimeBound()) { + currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); + } else { + 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(formula.getIntervalBounds().first(formula.getIntervalBounds().first); + } + currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getIntervalBounds().second); } + preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false); } template @@ -360,10 +357,14 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional 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(); + return; + } + currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); RewardModelType objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index 3d9ef373c..6b9c21fa4 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -22,11 +22,11 @@ namespace storm { template - SparseMultiObjectiveWeightVectorChecker::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::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(weightVector)); std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - 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::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 void SparseMultiObjectiveWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector) { - if(this->unboundedObjectives.empty()) { + if(this->objectivesWithNoUpperTimeBound.empty()) { this->weightedResult = std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); 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(); offsetsToUpperBound[objIndex] = storm::utility::zero(); storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h index 0267ac1c0..3022769d7 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h +++ b/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>discreteActionRewards;