From 64ca58494db910fb775647f8b1b229b6d6d7e05a Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 28 Sep 2017 16:31:25 +0200 Subject: [PATCH] considered solver requirements for multiobjective model checking --- .../SparseMultiObjectivePreprocessor.cpp | 15 +++- .../SparseMultiObjectivePreprocessor.h | 3 + .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 21 +++++- .../pcaa/SparseMaPcaaWeightVectorChecker.h | 2 +- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 72 +++++++++++-------- .../pcaa/SparsePcaaWeightVectorChecker.h | 10 ++- 6 files changed, 85 insertions(+), 38 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index fb652cd28..7d44bd268 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -35,6 +35,7 @@ namespace storm { data.objectives.push_back(std::make_shared>()); data.objectives.back()->originalFormula = subFormula; data.finiteRewardCheckObjectives.resize(data.objectives.size(), false); + data.upperResultBoundObjectives.resize(data.objectives.size(), false); if (data.objectives.back()->originalFormula->isOperatorFormula()) { preprocessOperatorFormula(data.objectives.back()->originalFormula->asOperatorFormula(), data); } else { @@ -69,6 +70,16 @@ namespace storm { } preprocessedModel->restrictRewardModels(relevantRewardModels); + // Compute upper result bounds wherever this is necessarry + for (auto const& objIndex : data.upperResultBoundObjectives) { + auto const& formula = data.objectives[objIndex]->formula->asRewardOperatorFormula(); + auto const& rewModel = preprocessedModel->getRewardModel(formula.getRewardModelName()); + // BaierUpperRewardBoundsComputer baier(submatrix, choiceRewards, oneStepTargetProbabilities); + // hintInformation.upperResultBound = baier.computeUpperBound(); + } + + + // Build the actual result return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions); } @@ -330,13 +341,12 @@ namespace storm { auto totalRewardFormula = std::make_shared(); data.objectives.back()->formula = std::make_shared(totalRewardFormula, auxRewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + data.upperResultBoundObjectives.set(data.objectives.size() - 1, true); if (formula.isReachabilityRewardFormula()) { assert(optionalRewardModelName.is_initialized()); data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, optionalRewardModelName.get())); - data.finiteRewardCheckObjectives.set(data.objectives.size() - 1); } else if (formula.isReachabilityTimeFormula() && data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { - data.finiteRewardCheckObjectives.set(data.objectives.size() - 1); data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); @@ -358,6 +368,7 @@ namespace storm { auto totalRewardFormula = std::make_shared(); data.objectives.back()->formula = std::make_shared(totalRewardFormula, *optionalRewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + data.upperResultBoundObjectives.set(data.objectives.size() - 1, true); } template diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 7def811a1..5fc531677 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -41,6 +41,9 @@ namespace storm { // Indices of the objectives that require a check for finite reward storm::storage::BitVector finiteRewardCheckObjectives; + // Indices of the objectives for which we need to compute an upper bound for the result + storm::storage::BitVector upperResultBoundObjectives; + std::string memoryLabelPrefix; std::string rewardModelNamePrefix; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index a7ce425a5..61f995939 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -13,6 +13,7 @@ #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/UncheckedRequirementException.h" namespace storm { namespace modelchecker { @@ -72,7 +73,7 @@ namespace storm { // Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch // No EC elimination is necessary as we assume non-zenoness - std::unique_ptr minMax = initMinMaxSolver(PS); + std::unique_ptr minMax = initMinMaxSolver(PS, weightVector); // create a linear equation solver for the model induced by the optimal choice vector. // the solver will be updated whenever the optimal choice vector has changed. @@ -294,13 +295,27 @@ namespace storm { } template - std::unique_ptr::MinMaxSolverData> SparseMaPcaaWeightVectorChecker::initMinMaxSolver(SubModel const& PS) const { + std::unique_ptr::MinMaxSolverData> SparseMaPcaaWeightVectorChecker::initMinMaxSolver(SubModel const& PS, std::vector const& weightVector) const { std::unique_ptr result(new MinMaxSolverData()); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; result->solver = minMaxSolverFactory.create(PS.toPS); - result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); result->solver->setTrackScheduler(true); result->solver->setCachingEnabled(true); + auto req = result->solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); + req.clearNoEndComponents(); + boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true)); + if (lowerBound) { + result->solver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); + } + boost::optional upperBound = this->computeWeightedResultBound(false, weightVector, storm::storage::BitVector(weightVector.size(), true)); + if (upperBound) { + result->solver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met."); + result->solver->setRequirementsChecked(true); + result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); result->b.resize(PS.getNumberOfChoices()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index c2940612f..af8dd0e91 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -117,7 +117,7 @@ namespace storm { /*! * Initializes the data for the MinMax solver */ - std::unique_ptr initMinMaxSolver(SubModel const& PS) const; + std::unique_ptr initMinMaxSolver(SubModel const& PS, std::vector const& weightVector) const; /*! * Initializes the data for the LinEq solver diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 05f7318fb..b6251254b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -19,6 +19,7 @@ #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UncheckedRequirementException.h" namespace storm { namespace modelchecker { @@ -92,39 +93,17 @@ namespace storm { void SparsePcaaWeightVectorChecker::check(std::vector const& weightVector) { checkHasBeenCalled = true; STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); + std::vector weightedRewardVector(transitionMatrix.getRowCount(), storm::utility::zero()); - boost::optional weightedLowerResultBound = storm::utility::zero(); - boost::optional weightedUpperResultBound = storm::utility::zero(); for (auto objIndex : objectivesWithNoUpperTimeBound) { - auto const& obj = this->objectives[objIndex]; if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { - if (obj.lowerResultBound && weightedUpperResultBound) { - weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get(); - } else { - weightedUpperResultBound = boost::none; - } - if (obj.upperResultBound && weightedLowerResultBound) { - weightedLowerResultBound.get() -= weightVector[objIndex] * obj.upperResultBound.get(); - } else { - weightedLowerResultBound = boost::none; - } storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], -weightVector[objIndex]); } else { - if (obj.lowerResultBound && weightedLowerResultBound) { - weightedLowerResultBound.get() += weightVector[objIndex] * obj.lowerResultBound.get(); - } else { - weightedLowerResultBound = boost::none; - } - if (obj.upperResultBound && weightedUpperResultBound) { - weightedUpperResultBound.get() += weightVector[objIndex] * obj.upperResultBound.get(); - } else { - weightedUpperResultBound = boost::none; - } storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weightVector[objIndex]); } } - unboundedWeightedPhase(weightedRewardVector, weightedLowerResultBound, weightedUpperResultBound); + unboundedWeightedPhase(weightedRewardVector, weightVector); unboundedIndividualPhase(weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound @@ -180,7 +159,28 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { + boost::optional SparsePcaaWeightVectorChecker::computeWeightedResultBound(bool lower, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter) const { + + ValueType result = storm::utility::zero(); + for (auto const& objIndex : objectiveFilter) { + boost::optional const& objBound = (lower == storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) ? this->objectives[objIndex].upperResultBound : this->objectives[objIndex].lowerResultBound; + if (objBound) { + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { + result -= objBound.get() * weightVector[objIndex]; + } else { + result += objBound.get() * weightVector[objIndex]; + } + } else { + // If there is an objective without the corresponding bound we can not give guarantees for the weighted sum + return boost::none; + } + } + return result; + } + + + template + void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, std::vector const& weightVector) { if (this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) { this->weightedResult = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -194,14 +194,22 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory solverFactory; std::unique_ptr> solver = solverFactory.create(ecQuotient->matrix); - solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setTrackScheduler(true); - if (lowerResultBound) { - solver->setLowerBound(*lowerResultBound); + auto req = solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); + req.clearNoEndComponents(); + boost::optional lowerBound = computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound); + if (lowerBound) { + solver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); } - if (upperResultBound) { - solver->setUpperBound(*upperResultBound); + boost::optional upperBound = computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound); + if (upperBound) { + solver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met."); + solver->setRequirementsChecked(true); + solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); // Use the (0...0) vector as initial guess for the solution. std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero()); @@ -273,12 +281,16 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + auto req = solver->getRequirements(); if (obj.lowerResultBound) { + req.clearLowerBounds(); solver->setLowerBound(*obj.lowerResultBound); } if (obj.upperResultBound) { solver->setUpperBound(*obj.upperResultBound); + req.clearUpperBounds(); } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); solver->solveEquations(x, b); // Set the result for this objective accordingly diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index c4316d480..d03538169 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -66,18 +66,24 @@ namespace storm { void initialize(SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0; + + /*! + * Computes the weighted lower and upper bounds for the provided set of objectives. + * @param lower if true, lower result bounds are computed. otherwise upper result bounds + * @param weightVector the weight vector ooof the current check + */ + boost::optional computeWeightedResultBound(bool lower, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter) const; /*! * Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives * * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) */ - void unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound); + void unboundedWeightedPhase(std::vector const& weightedRewardVector, std::vector const& weightVector); /*! * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase * - * @param weightVector the weight vector of the current check */ void unboundedIndividualPhase(std::vector const& weightVector);