Browse Source

DeterministicSchedsLpChecker: Resolved two issues in the encoding.

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
commit
56dbbdabb4
  1. 8
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp

8
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp

@ -171,7 +171,7 @@ namespace storm {
if (numChoices == 1) { if (numChoices == 1) {
stateValue = choiceValue; stateValue = choiceValue;
} else { } else {
auto choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression();
auto choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), storm::utility::zero<ValueType>(), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression();
uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice; uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice;
storm::expressions::Expression upperValueBoundAtChoice = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)); storm::expressions::Expression upperValueBoundAtChoice = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state));
if (objectiveHelper[objIndex].minimizing()) { if (objectiveHelper[objIndex].minimizing()) {
@ -191,10 +191,16 @@ namespace storm {
//lpModel->addConstraint("", choiceValVar - stateVars[state] <= maxDiff); //lpModel->addConstraint("", choiceValVar - stateVars[state] <= maxDiff);
} }
} }
if (objectiveHelper[objIndex].minimizing()) {
lpModel->addConstraint("", stateVars[state] >= stateValue);
} else {
lpModel->addConstraint("", stateVars[state] <= stateValue); lpModel->addConstraint("", stateVars[state] <= stateValue);
} }
} }
}
swAux.start();
lpModel->update(); lpModel->update();
swAux.stop();
} }
template <typename ModelType, typename GeometryValueType> template <typename ModelType, typename GeometryValueType>

Loading…
Cancel
Save