From 4da61d972c1f5f3196b69ab0ff48c59c8e9a56eb Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 5 Oct 2017 09:27:44 +0200
Subject: [PATCH] fixed correctly setting the result bounds for weight vector
checker
---
...dpRewardBoundedPcaaWeightVectorChecker.cpp | 25 ++++++-------------
.../pcaa/SparsePcaaWeightVectorChecker.cpp | 25 ++++++-------------
2 files changed, 14 insertions(+), 36 deletions(-)
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
index f2ce81b87..0bf69f67d 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
@@ -142,24 +142,13 @@ namespace storm {
std::vector<ValueType>& x = cachedData.xLinEq[objIndex];
assert(x.size() == choices.size());
auto req = cachedData.linEqSolver->getRequirements();
- 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(*obj.lowerResultBound);
- }
- if (obj.upperResultBound) {
- cachedData.linEqSolver->setUpperBound(*obj.upperResultBound);
- req.clearUpperBounds();
- }
+ if (obj.lowerResultBound) {
+ req.clearLowerBounds();
+ cachedData.linEqSolver->setLowerBound(*obj.lowerResultBound);
+ }
+ 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();
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
index e275cab37..1b5b51937 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
@@ -261,24 +261,13 @@ 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);
- }
- if (obj.upperResultBound) {
- solver->setUpperBound(*obj.upperResultBound);
- req.clearUpperBounds();
- }
+ if (obj.lowerResultBound) {
+ req.clearLowerBounds();
+ solver->setLowerBound(*obj.lowerResultBound);
+ }
+ if (obj.upperResultBound) {
+ 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);