diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp index d134d8ff0..d26b67b54 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp @@ -31,6 +31,26 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler generation is not supported in this setting."); } + template + boost::optional PcaaWeightVectorChecker::computeWeightedResultBound(bool lower, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter) const { + + ValueType result = storm::utility::zero(); + for (auto const& objIndex : objectiveFilter) { + boost::optional const& objBound = (lower == storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) ? this->objectives[objIndex].upperResultBound : this->objectives[objIndex].lowerResultBound; + if (objBound) { + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { + result -= objBound.get() * weightVector[objIndex]; + } else { + result += objBound.get() * weightVector[objIndex]; + } + } else { + // If there is an objective without the corresponding bound we can not give guarantees for the weighted sum + return boost::none; + } + } + return result; + } + template template>::value, int>::type> std::unique_ptr> WeightVectorCheckerFactory::create(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h index 6d547de58..aefa139b8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h @@ -69,6 +69,14 @@ namespace storm { protected: + + + /*! + * Computes the weighted lower or upper bounds for the provided set of objectives. + * @param lower if true, lower result bounds are computed. otherwise upper result bounds + * @param weightVector the weight vector ooof the current check + */ + boost::optional computeWeightedResultBound(bool lower, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter) const; // The (preprocessed) objectives std::vector> objectives; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 024b71730..44059d110 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -15,6 +15,7 @@ #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/UncheckedRequirementException.h" namespace storm { namespace modelchecker { @@ -52,7 +53,7 @@ namespace storm { template void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData) { auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); - updateCachedData(epochModel, cachedData); + updateCachedData(epochModel, cachedData, weightVector); ++numCheckedEpochs; swEqBuilding.start(); @@ -137,6 +138,16 @@ namespace storm { } std::vector& x = cachedData.xLinEq[objIndex]; assert(x.size() == choices.size()); + auto req = cachedData.linEqSolver->getRequirements(); + if (this->objectives[objIndex].lowerResultBound) { + req.clearLowerBounds(); + cachedData.linEqSolver->setLowerBound(*this->objectives[objIndex].lowerResultBound); + } + if (this->objectives[objIndex].upperResultBound) { + cachedData.linEqSolver->setUpperBound(*this->objectives[objIndex].upperResultBound); + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); swEqBuilding.stop(); swLinEqSolving.start(); cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq); @@ -154,7 +165,7 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData) { + void SparseMdpRewardBoundedPcaaWeightVectorChecker::updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector) { if (epochModel.epochMatrixChanged) { swDataUpdate.start(); @@ -163,9 +174,23 @@ namespace storm { cachedData.xMinMax.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; cachedData.minMaxSolver = minMaxSolverFactory.create(epochModel.epochMatrix); - cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); cachedData.minMaxSolver->setTrackScheduler(true); cachedData.minMaxSolver->setCachingEnabled(true); + auto req = cachedData.minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); + req.clearNoEndComponents(); + boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true)); + if (lowerBound) { + cachedData.minMaxSolver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); + } + boost::optional upperBound = this->computeWeightedResultBound(false, weightVector, storm::storage::BitVector(weightVector.size(), true)); + if (upperBound) { + cachedData.minMaxSolver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met."); + cachedData.minMaxSolver->setRequirementsChecked(true); + cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); // Set the scheduler choices to invalid choice indices so that an update of the linEqSolver is enforced cachedData.schedulerChoices.assign(epochModel.epochMatrix.getRowGroupCount(), std::numeric_limits::max()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index 20ae60474..36cba968d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -79,7 +79,7 @@ namespace storm { void computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData); - void updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData); + void updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector); storm::utility::Stopwatch swAll, swDataUpdate, swEqBuilding, swLinEqSolving, swMinMaxSolving, swAux1, swAux2, swAux3; uint64_t numSchedChanges, numCheckedEpochs; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index b6251254b..1b5b51937 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -158,27 +158,6 @@ namespace storm { return result; } - template - boost::optional SparsePcaaWeightVectorChecker::computeWeightedResultBound(bool lower, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter) const { - - ValueType result = storm::utility::zero(); - for (auto const& objIndex : objectiveFilter) { - boost::optional const& objBound = (lower == storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) ? this->objectives[objIndex].upperResultBound : this->objectives[objIndex].lowerResultBound; - if (objBound) { - if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { - result -= objBound.get() * weightVector[objIndex]; - } else { - result += objBound.get() * weightVector[objIndex]; - } - } else { - // If there is an objective without the corresponding bound we can not give guarantees for the weighted sum - return boost::none; - } - } - return result; - } - - template void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, std::vector const& weightVector) { @@ -197,12 +176,12 @@ namespace storm { solver->setTrackScheduler(true); auto req = solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); req.clearNoEndComponents(); - boost::optional lowerBound = computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound); + boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound); if (lowerBound) { solver->setLowerBound(lowerBound.get()); req.clearLowerBounds(); } - boost::optional upperBound = computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound); + boost::optional upperBound = this->computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound); if (upperBound) { solver->setUpperBound(upperBound.get()); req.clearUpperBounds(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index d03538169..6365ad2dc 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -66,14 +66,7 @@ namespace storm { void initialize(SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0; - - /*! - * Computes the weighted lower and upper bounds for the provided set of objectives. - * @param lower if true, lower result bounds are computed. otherwise upper result bounds - * @param weightVector the weight vector ooof the current check - */ - boost::optional computeWeightedResultBound(bool lower, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter) const; - + /*! * Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives * diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index a000b2e66..6a7fbab1b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -94,6 +94,11 @@ namespace storm { minMaxSolver->setCachingEnabled(true); minMaxSolver->setLowerBound(storm::utility::zero()); minMaxSolver->setUpperBound(storm::utility::one()); + auto req = minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath, dir); + req.clearNoEndComponents(); + req.clearBounds(); + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "A solver requirement is not satisfied."); + minMaxSolver->setRequirementsChecked(); } // Prepare the right hand side of the equation system