Browse Source

LpChecker: Fixed validation of lp results where an objective has weight zero.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
e71033e0e0
  1. 8
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp

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

@ -104,7 +104,8 @@ namespace storm {
lpModel->optimize(); lpModel->optimize();
swCheckWeightVectors.stop(); swCheckWeightVectors.stop();
++numLpQueries; ++numLpQueries;
STORM_LOG_TRACE("\t Done checking a vertex...");
//STORM_PRINT_AND_LOG("Writing model to file '" << std::to_string(numLpQueries) << ".lp'" << std::endl;);
//lpModel->writeModelToFile(std::to_string(numLpQueries) + ".lp");
boost::optional<Point> result; boost::optional<Point> result;
if (!lpModel->isInfeasible()) { if (!lpModel->isInfeasible()) {
STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded."); STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded.");
@ -113,6 +114,7 @@ namespace storm {
swValidate.stop(); swValidate.stop();
} }
lpModel->pop(); lpModel->pop();
STORM_LOG_TRACE("\t Done checking a vertex...");
swAll.stop(); swAll.stop();
return result; return result;
} }
@ -687,11 +689,13 @@ namespace storm {
inducedValue = -inducedValue; inducedValue = -inducedValue;
} }
inducedPoint.push_back(inducedValue); inducedPoint.push_back(inducedValue);
// If this objective has weight zero, the lp solution is not necessarily correct
if (!storm::utility::isZero(currentWeightVector[objIndex])) {
ValueType lpValue = lpModel->getContinuousValue(currentObjectiveVariables[objIndex]); ValueType lpValue = lpModel->getContinuousValue(currentObjectiveVariables[objIndex]);
double diff = storm::utility::convertNumber<double>(storm::utility::abs<ValueType>(inducedValue - lpValue)); double diff = storm::utility::convertNumber<double>(storm::utility::abs<ValueType>(inducedValue - lpValue));
STORM_LOG_WARN_COND(diff <= 1e-4 * std::abs(storm::utility::convertNumber<double>(inducedValue)), "Imprecise value for objective " << objIndex << ": LP says " << lpValue << " but scheduler induces " << inducedValue << " (difference is " << diff << ")"); STORM_LOG_WARN_COND(diff <= 1e-4 * std::abs(storm::utility::convertNumber<double>(inducedValue)), "Imprecise value for objective " << objIndex << ": LP says " << lpValue << " but scheduler induces " << inducedValue << " (difference is " << diff << ")");
} }
}
return inducedPoint; return inducedPoint;
} }

Loading…
Cancel
Save