more solver requirements for multi-objective model checking

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 <class SparseModelType>
+            boost::optional<typename SparseModelType::ValueType> PcaaWeightVectorChecker<SparseModelType>::computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter) const {
+                
+                ValueType result = storm::utility::zero<ValueType>();
+                for (auto const& objIndex : objectiveFilter) {
+                    boost::optional<ValueType> 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 <typename ModelType>
             template<typename VT, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type>
             std::unique_ptr<PcaaWeightVectorChecker<ModelType>>  WeightVectorCheckerFactory<ModelType>::create(SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult) {

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<ValueType> computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter) const;
                 
                 // The (preprocessed) objectives
                 std::vector<Objective<ValueType>> objectives;

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 <class SparseMdpModelType>
             void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType, false>::Epoch const& epoch, std::vector<ValueType> 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<ValueType>& 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 <class SparseMdpModelType>
-            void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::updateCachedData(typename MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData) {
+            void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::updateCachedData(typename MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector) {
                 if (epochModel.epochMatrixChanged) {
                     swDataUpdate.start();
                 
@@ -163,9 +174,23 @@ namespace storm {
                     cachedData.xMinMax.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                     storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> 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<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true));
+                    if (lowerBound) {
+                        cachedData.minMaxSolver->setLowerBound(lowerBound.get());
+                        req.clearLowerBounds();
+                    }
+                    boost::optional<ValueType> 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<uint64_t>::max());

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h

@@ -79,7 +79,7 @@ namespace storm {
                 
                 void computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType, false>::Epoch const& epoch, std::vector<ValueType> const& weightVector, EpochCheckingData& cachedData);
                 
-                void updateCachedData(typename MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData);
+                void updateCachedData(typename MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector);
                 
                 storm::utility::Stopwatch swAll, swDataUpdate, swEqBuilding, swLinEqSolving, swMinMaxSolving, swAux1, swAux2, swAux3;
                 uint64_t numSchedChanges, numCheckedEpochs;

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@@ -158,27 +158,6 @@ namespace storm {
                 return result;
             }
             
-            template <class SparseModelType>
-            boost::optional<typename SparseModelType::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter) const {
-                
-                ValueType result = storm::utility::zero<ValueType>();
-                for (auto const& objIndex : objectiveFilter) {
-                    boost::optional<ValueType> 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 <class SparseModelType>
             void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector, std::vector<ValueType> const& weightVector) {
                 
@@ -197,12 +176,12 @@ namespace storm {
                 solver->setTrackScheduler(true);
                 auto req = solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
                 req.clearNoEndComponents();
-                boost::optional<ValueType> lowerBound = computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
+                boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
                 if (lowerBound) {
                     solver->setLowerBound(lowerBound.get());
                     req.clearLowerBounds();
                 }
-                boost::optional<ValueType> upperBound = computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound);
+                boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound);
                 if (upperBound) {
                     solver->setUpperBound(upperBound.get());
                     req.clearUpperBounds();

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

@@ -66,14 +66,7 @@ namespace storm {
                 
                 void initialize(SparseMultiObjectivePreprocessorResult<SparseModelType> 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<ValueType> computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter) const;
-                
+
                 /*!
                  * Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives
                  *

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -94,6 +94,11 @@ namespace storm {
                         minMaxSolver->setCachingEnabled(true);
                         minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
                         minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
+                        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