From 621aae1c4c779d6a376a0f89f903cbda7fab4d03 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 May 2019 10:36:06 +0200 Subject: [PATCH] DeterministicSchedsParetoExplorer: Selecting LP-based weight vector checkers in case of properties that are not supported by the standard weight vector checker. --- .../DeterministicSchedsParetoExplorer.cpp | 49 ++++++++++++------- .../pcaa/StandardPcaaWeightVectorChecker.h | 1 - .../SparseMultiObjectivePreprocessorResult.h | 10 ++++ 3 files changed, 41 insertions(+), 19 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 09a7506e0..b1e7398c2 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -283,7 +283,11 @@ namespace storm { objectiveHelper.emplace_back(*model, obj); } lpChecker = std::make_shared>(env, *model, objectiveHelper); - wvChecker = storm::modelchecker::multiobjective::WeightVectorCheckerFactory::create(preprocessorResult); + if (preprocessorResult.containsOnlyTotalRewardFormulas()) { + wvChecker = storm::modelchecker::multiobjective::WeightVectorCheckerFactory::create(preprocessorResult); + } else { + wvChecker = nullptr; + } } template @@ -395,14 +399,17 @@ namespace storm { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { std::vector weightVector(objectives.size(), storm::utility::zero()); weightVector[objIndex] = storm::utility::one(); - //negateMinObjectives(weightVector); - wvChecker->check(env, storm::utility::vector::convertNumericVector(weightVector)); - auto point = storm::utility::vector::convertNumericVector(wvChecker->getUnderApproximationOfInitialStateResults()); - //lpChecker->setCurrentWeightVector(weightVector); - //auto point = lpChecker->check(env, negateMinObjectives(this->overApproximation)); - //STORM_LOG_THROW(point.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation."); - //negateMinObjectives(weightVector); - negateMinObjectives(point); + std::vector point; + if (wvChecker) { + wvChecker->check(env, storm::utility::vector::convertNumericVector(weightVector)); + point = storm::utility::vector::convertNumericVector(wvChecker->getUnderApproximationOfInitialStateResults()); + negateMinObjectives(point); + } else { + lpChecker->setCurrentWeightVector(weightVector); + auto optionalPoint = lpChecker->check(env, negateMinObjectives(this->overApproximation)); + STORM_LOG_THROW(optionalPoint.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation."); + point = std::move(optionalPoint.get()); + } Point p(point); p.setOnFacet(); // Adapt the overapproximation @@ -483,20 +490,26 @@ namespace storm { // Invoke optimization and insert the explored points boost::optional optPointId; - wvChecker->check(env, storm::utility::vector::convertNumericVector(f.getHalfspace().normalVector())); - auto point = storm::utility::vector::convertNumericVector(wvChecker->getUnderApproximationOfInitialStateResults()); - //auto currentArea = negateMinObjectives(overApproximation->intersection(f.getHalfspace().invert())); - //auto point = lpChecker->check(env, currentArea); - // if (point.is_initialized()) { - negateMinObjectives(point); + std::vector point; + if (wvChecker) { + wvChecker->check(env, storm::utility::vector::convertNumericVector(f.getHalfspace().normalVector())); + point = storm::utility::vector::convertNumericVector(wvChecker->getUnderApproximationOfInitialStateResults()); + negateMinObjectives(point); + } else { + auto currentArea = negateMinObjectives(overApproximation->intersection(f.getHalfspace().invert())); + auto optionalPoint = lpChecker->check(env, currentArea); + if (optionalPoint.is_initialized()) { + point = std::move(optionalPoint.get()); + } else { + // As we did not find any feasable solution in the given area, we take a point that lies on the facet + point = pointset.getPoint(f.getPoints().front()).get(); + } + } Point p(point); p.setOnFacet(); GeometryValueType offset = storm::utility::vector::dotProduct(f.getHalfspace().normalVector(), p.get()); addHalfspaceToOverApproximation(env, f.getHalfspace().normalVector(), offset); optPointId = pointset.addPoint(env, std::move(p)); - //} else { - // addHalfspaceToOverApproximation(env, f.getHalfspace().normalVector(), f.getHalfspace().offset()); - //} // Potentially generate new facets if (optPointId) { diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index 70da1049b..3a6ac3c9f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h @@ -34,7 +34,6 @@ namespace storm { * @param possibleBottomStates The states for which it is posible to not collect further reward with prob. 1 * */ - StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); /*! diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h index cc185e821..9e87eec4d 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h @@ -38,6 +38,16 @@ namespace storm { // Intentionally left empty } + + bool containsOnlyTotalRewardFormulas() const { + for (auto const& obj : objectives) { + if (!obj.formula->isRewardOperatorFormula() || !obj.formula->getSubformula().isTotalRewardFormula()) { + return false; + } + } + return true; + } + bool containsOnlyTrivialObjectives() const { // Trivial objectives are either total reward formulas or single-dimensional step or time bounded cumulative reward formulas for (auto const& obj : objectives) {