fix for interval iteration in weight vector checkers

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

@@ -112,6 +112,7 @@ namespace storm {
                 swAux3.start();
                 assert(cachedData.bLinEq.size() == choices.size());
                 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
+                    auto const& obj = this->objectives[objIndex];
                     std::vector<ValueType> const& objectiveReward = epochModel.objectiveRewards[objIndex];
                     auto rowGroupIndexIt = epochModel.epochMatrix.getRowGroupIndices().begin();
                     auto choiceIt = choices.begin();
@@ -139,14 +140,25 @@ namespace storm {
                     std::vector<ValueType>& x = cachedData.xLinEq[objIndex];
                     assert(x.size() == choices.size());
                     auto req = cachedData.linEqSolver->getRequirements();
-                    if (this->objectives[objIndex].lowerResultBound) {
+                    if (storm::solver::minimize(obj.formula->getOptimalityType())) {
+                        if (obj.lowerResultBound) {
+                            req.clearUpperBounds();
+                            cachedData.linEqSolver->setUpperBound(-(*obj.lowerResultBound));
+                        }
+                        if (obj.upperResultBound) {
+                            req.clearLowerBounds();
+                            cachedData.linEqSolver->setLowerBound(-(*obj.upperResultBound));
+                        }
+                    } else {
+                        if (obj.lowerResultBound) {
                             req.clearLowerBounds();
-                        cachedData.linEqSolver->setLowerBound(*this->objectives[objIndex].lowerResultBound);
+                            cachedData.linEqSolver->setLowerBound(*obj.lowerResultBound);
                         }
-                    if (this->objectives[objIndex].upperResultBound) {
-                        cachedData.linEqSolver->setUpperBound(*this->objectives[objIndex].upperResultBound);
+                        if (obj.upperResultBound) {
+                            cachedData.linEqSolver->setUpperBound(*obj.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();

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

@@ -261,6 +261,16 @@ namespace storm {
                                // Now solve the resulting equation system.
                                std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
                                auto req = solver->getRequirements();
+                               if (storm::solver::minimize(obj.formula->getOptimalityType())) {
+                                   if (obj.lowerResultBound) {
+                                       req.clearUpperBounds();
+                                       solver->setUpperBound(-(*obj.lowerResultBound));
+                                   }
+                                   if (obj.upperResultBound) {
+                                       req.clearLowerBounds();
+                                       solver->setLowerBound(-(*obj.upperResultBound));
+                                   }
+                               } else {
                                    if (obj.lowerResultBound) {
                                        req.clearLowerBounds();
                                        solver->setLowerBound(*obj.lowerResultBound);
@@ -269,6 +279,7 @@ namespace storm {
                                        solver->setUpperBound(*obj.upperResultBound);
                                        req.clearUpperBounds();
                                    }
+                               }
                                STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met.");
                                solver->solveEquations(x, b);