diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index ae788a31f..1a354c0c2 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -666,13 +666,9 @@ namespace storm { polytopeTree.clear(); } else { STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded."); -#ifndef NDEBUG - validateCurrentModel(env); -#endif - Point newPoint; - for (auto const& objVar : currentObjectiveVariables) { - newPoint.push_back(storm::utility::convertNumber(lpModel->getContinuousValue(objVar))); - } + swValidate.start(); + Point newPoint = validateCurrentModel(env); + swValidate.stop(); std::vector newPoints = {newPoint}; if (gurobiLpModel && useNonOptimalSolutions()) { // gurobi might have other good solutions. @@ -696,6 +692,10 @@ namespace storm { // Gurobi gives us the gap between the found solution and the known bound. offset += storm::utility::convertNumber(gurobiLpModel->getMILPGap(false)); } + // we might want to shift the halfspace to guarantee that our point is included. + for (auto const& p : newPoints) { + offset = std::max(offset, storm::utility::vector::dotProduct(currentWeightVector, p)); + } auto halfspace = storm::storage::geometry::Halfspace(currentWeightVector, offset).invert(); infeasableAreas.push_back(polytopeTree.getPolytope()->intersection(halfspace)); if (infeasableAreas.back()->isEmpty()) { @@ -738,7 +738,7 @@ namespace storm { } template - void DeterministicSchedsLpChecker::validateCurrentModel(Environment const& env) const { + typename DeterministicSchedsLpChecker::Point DeterministicSchedsLpChecker::validateCurrentModel(Environment const& env) const { storm::storage::Scheduler scheduler(model.getNumberOfStates()); for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { uint64_t numChoices = model.getNumberOfChoices(state); @@ -764,16 +764,19 @@ namespace storm { } } auto inducedModel = model.applyScheduler(scheduler)->template as(); + Point inducedPoint; for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) { - ValueType expectedValue = lpModel->getContinuousValue(currentObjectiveVariables[objIndex]); + ValueType inducedValue = objectiveHelper[objIndex].evaluateOnModel(env, *inducedModel); if (objectiveHelper[objIndex].minimizing()) { - expectedValue = -expectedValue; + inducedValue = -inducedValue; } - ValueType actualValue = objectiveHelper[objIndex].evaluateOnModel(env, *inducedModel); - double diff = storm::utility::convertNumber(storm::utility::abs(expectedValue - actualValue)); - STORM_PRINT_AND_LOG("Validating Lp solution for objective " << objIndex << ": LP" << storm::utility::convertNumber(expectedValue) << " InducedScheduler=" << storm::utility::convertNumber(actualValue) << " (difference is " << diff << ")" << std::endl); - STORM_LOG_WARN_COND(diff <= 1e-4 * std::abs(storm::utility::convertNumber(actualValue)), "Invalid value for objective " << objIndex << ": expected " << expectedValue << " but got " << actualValue << " (difference is " << diff << ")"); + inducedPoint.push_back(inducedValue); + ValueType lpValue = lpModel->getContinuousValue(currentObjectiveVariables[objIndex]); + double diff = storm::utility::convertNumber(storm::utility::abs(inducedValue - lpValue)); + STORM_LOG_WARN_COND(diff <= 1e-4 * std::abs(storm::utility::convertNumber(inducedValue)), "Imprecise value for objective " << objIndex << ": LP says " << lpValue << " but scheduler induces " << inducedValue << " (difference is " << diff << ")"); } + + return inducedPoint; } template class DeterministicSchedsLpChecker, storm::RationalNumber>; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index e97a99efc..10237d308 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -50,7 +50,7 @@ namespace storm { void initializeLpModel(Environment const& env); // Builds the induced markov chain of the current model and checks whether the resulting value coincide with the result of the lp solver. - void validateCurrentModel(Environment const& env) const; + Point validateCurrentModel(Environment const& env) const; void checkRecursive(storm::Environment const& env, storm::storage::geometry::PolytopeTree& polytopeTree, Point const& eps, std::vector& foundPoints, std::vector& infeasableAreas, uint64_t const& depth);