From 654f705d2ee8e958c1621dcb3b957be3df09bdb6 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 7 Nov 2019 15:37:50 +0100
Subject: [PATCH] DetSchedsLpChecker: Glpk does not allow point intervals as
bounds for variables.
---
.../DeterministicSchedsLpChecker.cpp | 27 ++++++++++++++++---
1 file changed, 23 insertions(+), 4 deletions(-)
diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
index 836817e5f..8704a40c4 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
@@ -453,7 +453,15 @@ namespace storm {
}
}
}
- auto objValueVariable = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex), objectiveHelper[objIndex].getLowerValueBoundAtState(env, initialState), objectiveHelper[objIndex].getUpperValueBoundAtState(env, initialState));
+ ValueType lowerBound = objectiveHelper[objIndex].getLowerValueBoundAtState(env, initialState);
+ ValueType upperBound = objectiveHelper[objIndex].getUpperValueBoundAtState(env, initialState);
+ storm::expressions::Expression objValueVariable;
+ if (lowerBound == upperBound) {
+ // GLPK does not like point-intervals......
+ objValueVariable = lpModel->getConstant(lowerBound);
+ } else {
+ objValueVariable = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex), lowerBound, upperBound).getExpression();
+ }
if (objValue.empty()) {
lpModel->addConstraint("", objValueVariable == zero);
} else {
@@ -472,10 +480,21 @@ namespace storm {
for (uint64_t state = 0; state < numStates; ++state) {
auto valIt = schedulerIndependentStates.find(state);
if (valIt == schedulerIndependentStates.end()) {
- if (objectiveHelper[objIndex].minimizing()) {
- stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), -objectiveHelper[objIndex].getUpperValueBoundAtState(env, state), -objectiveHelper[objIndex].getLowerValueBoundAtState(env, state)).getExpression());
+ ValueType lowerBound = objectiveHelper[objIndex].getLowerValueBoundAtState(env, state);
+ ValueType upperBound = objectiveHelper[objIndex].getUpperValueBoundAtState(env, state);
+ if (lowerBound == upperBound) {
+ // glpk does not like variables with point-interval bounds...
+ if (objectiveHelper[objIndex].minimizing()) {
+ stateVars.push_back(lpModel->getConstant(-lowerBound));
+ } else {
+ stateVars.push_back(lpModel->getConstant(lowerBound));
+ }
} else {
- stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression());
+ if (objectiveHelper[objIndex].minimizing()) {
+ stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), -upperBound, -lowerBound).getExpression());
+ } else {
+ stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), lowerBound, upperBound).getExpression());
+ }
}
} else {
ValueType value = valIt->second;