From d351bd64550c730a482ab07f409a450538db9e78 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 25 Sep 2020 16:06:31 +0200 Subject: [PATCH] WeightVectorChecker: Integrated lra objectives also in the individual phase --- .../StandardMaPcaaWeightVectorChecker.cpp | 12 +- .../pcaa/StandardMaPcaaWeightVectorChecker.h | 4 +- .../StandardMdpPcaaWeightVectorChecker.cpp | 10 +- .../pcaa/StandardMdpPcaaWeightVectorChecker.h | 4 +- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 117 ++++++++++-------- .../pcaa/StandardPcaaWeightVectorChecker.h | 9 +- 6 files changed, 88 insertions(+), 68 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 0da73ad35..628862cca 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -64,14 +64,16 @@ namespace storm { } template - storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper StandardMaPcaaWeightVectorChecker::createNondetInfiniteHorizonHelper() const { - return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(this->transitionMatrix, this->markovianStates, this->exitRates); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper StandardMaPcaaWeightVectorChecker::createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const { + STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix."); + return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(transitions, this->markovianStates, this->exitRates); } template - storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper StandardMaPcaaWeightVectorChecker::createDetInfiniteHorizonHelper() const { - // Right now, one would have to pick the nondeterministic helper. - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Deterministic infinite horizon solvers for 'deterministic' Markov automata are not implemented"); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper StandardMaPcaaWeightVectorChecker::createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const { + STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix."); + // TODO: Right now, there is no dedicated support for "deterministic" Markov automata so we have to pick the nondeterministic one. + return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(transitions, this->markovianStates, this->exitRates); } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h index bc9e2b3c4..d928d6eb6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h @@ -30,8 +30,8 @@ namespace storm { protected: virtual void initializeModelTypeSpecificData(SparseMaModelType const& model) override; - virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper() const override; - virtual storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper createDetInfiniteHorizonHelper() const override; + virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const override; + virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const override; private: diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp index 74736f700..cadd5f217 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp @@ -47,13 +47,15 @@ namespace storm { } template - storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper StandardMdpPcaaWeightVectorChecker::createNondetInfiniteHorizonHelper() const { - return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(this->transitionMatrix); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper StandardMdpPcaaWeightVectorChecker::createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const { + STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix."); + return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(transitions); } template - storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper StandardMdpPcaaWeightVectorChecker::createDetInfiniteHorizonHelper() const { - return storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper(this->transitionMatrix); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper StandardMdpPcaaWeightVectorChecker::createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const { + STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix."); + return storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper(transitions); } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h index 8d29cefc0..7dcf7ea28 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h @@ -38,8 +38,8 @@ namespace storm { protected: virtual void initializeModelTypeSpecificData(SparseMdpModelType const& model) override; - virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper() const override; - virtual storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper createDetInfiniteHorizonHelper() const override; + virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const override; + virtual storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const override; private: diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 943f533ca..4dafaeec4 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -179,7 +179,7 @@ namespace storm { storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeScheduler() const { STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); for (auto const& obj : this->objectives) { - STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::NotImplementedException, "Scheduler retrival is only implemented for objectives without time-bound."); + STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isLongRunAverageRewardFormula(), storm::exceptions::NotImplementedException, "Scheduler retrival is only implemented for objectives without time-bound."); } storm::storage::Scheduler result(this->optimalChoices.size()); @@ -291,7 +291,7 @@ namespace storm { void StandardPcaaWeightVectorChecker::infiniteHorizonWeightedPhase(Environment const& env, std::vector const& weightedActionRewardVector, boost::optional> const& weightedStateRewardVector) { // Compute the optimal (weighted) lra value for each mec, keeping track of the optimal choices STORM_LOG_ASSERT(lraMecDecomposition, "Mec decomposition for lra computations not initialized."); - storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper = createNondetInfiniteHorizonHelper(); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper = createNondetInfiniteHorizonHelper(this->transitionMatrix); helper.provideLongRunComponentDecomposition(lraMecDecomposition->mecs); helper.setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); helper.setProduceScheduler(true); @@ -392,11 +392,14 @@ namespace storm { } } } else { - storm::storage::SparseMatrix deterministicMatrix = transitionMatrix.selectRowsFromRowGroups(this->optimalChoices, true); + storm::storage::SparseMatrix deterministicMatrix = transitionMatrix.selectRowsFromRowGroups(this->optimalChoices, true); // TODO: why diagonal entries? storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); - std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); + std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); // allocate here storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + auto infiniteHorizonHelper = createDetInfiniteHorizonHelper(deterministicMatrix); + infiniteHorizonHelper.provideBackwardTransitions(deterministicBackwardTransitions); + // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far. // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i. std::vector weightedSumOfUncheckedObjectives = weightedResult; @@ -407,58 +410,68 @@ namespace storm { if (objectivesWithNoUpperTimeBound.get(objIndex)) { offsetsToUnderApproximation[objIndex] = storm::utility::zero(); offsetsToOverApproximation[objIndex] = storm::utility::zero(); - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, transitionMatrix.getRowGroupIndices(), actionRewards[objIndex]); - storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); - // As maybestates we pick the states from which a state with reward is reachable - storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); - - // Compute the estimate for this objective - if (!storm::utility::isZero(weightVector[objIndex])) { - objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; - ValueType scalingFactor = storm::utility::one() / sumOfWeightsOfUncheckedObjectives; - if (storm::solver::minimize(obj.formula->getOptimalityType())) { - scalingFactor *= -storm::utility::one(); - } - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor); - storm::utility::vector::clip(objectiveResults[objIndex], obj.lowerResultBound, obj.upperResultBound); - } - // Make sure that the objectiveResult is initialized correctly - objectiveResults[objIndex].resize(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - - if (!maybeStates.empty()) { - bool needEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - storm::storage::SparseMatrix submatrix = deterministicMatrix.getSubmatrix( - true, maybeStates, maybeStates, needEquationSystem); - if (needEquationSystem) { - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix.convertToEquationSystem(); + if (lraObjectives.get(objIndex)) { + auto actionValueGetter = [&] (uint64_t const& a) { return actionRewards[objIndex][transitionMatrix.getRowGroupIndices()[a] + this->optimalChoices[a]]; }; + typename storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper::ValueGetter stateValueGetter; + if (stateRewards[objIndex].empty()) { + stateValueGetter = [] (uint64_t const&) { return storm::utility::zero(); }; + } else { + stateValueGetter = [&] (uint64_t const& s) { return stateRewards[objIndex][s]; }; } - - // Prepare solution vector and rhs of the equation system. - std::vector x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates); - std::vector b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates); - - // Now solve the resulting equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, submatrix); - auto req = solver->getRequirements(env); - solver->clearBounds(); - storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates; - submatrixRowsWithSumLessOne.complement(); - this->setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b); - if (solver->hasLowerBound()) { - req.clearLowerBounds(); + objectiveResults[objIndex] = infiniteHorizonHelper.computeLongRunAverageValues(env, stateValueGetter, actionValueGetter); + } else { // i.e. a total reward objective + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, transitionMatrix.getRowGroupIndices(), actionRewards[objIndex]); + storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); + // As maybestates we pick the states from which a state with reward is reachable + storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); + + // Compute the estimate for this objective + if (!storm::utility::isZero(weightVector[objIndex])) { + objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; + ValueType scalingFactor = storm::utility::one() / sumOfWeightsOfUncheckedObjectives; + if (storm::solver::minimize(obj.formula->getOptimalityType())) { + scalingFactor *= -storm::utility::one(); + } + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor); + storm::utility::vector::clip(objectiveResults[objIndex], obj.lowerResultBound, obj.upperResultBound); } - if (solver->hasUpperBound()) { - req.clearUpperBounds(); + // Make sure that the objectiveResult is initialized correctly + objectiveResults[objIndex].resize(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + + if (!maybeStates.empty()) { + bool needEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + storm::storage::SparseMatrix submatrix = deterministicMatrix.getSubmatrix( + true, maybeStates, maybeStates, needEquationSystem); + if (needEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } + + // Prepare solution vector and rhs of the equation system. + std::vector x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates); + std::vector b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates); + + // Now solve the resulting equation system. + std::unique_ptr> solver = linearEquationSolverFactory.create(env, submatrix); + auto req = solver->getRequirements(env); + solver->clearBounds(); + storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates; + submatrixRowsWithSumLessOne.complement(); + this->setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b); + if (solver->hasLowerBound()) { + req.clearLowerBounds(); + } + if (solver->hasUpperBound()) { + req.clearUpperBounds(); + } + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); + solver->solveEquations(env, x, b); + // Set the result for this objective accordingly + storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); } - STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); - solver->solveEquations(env, x, b); - // Set the result for this objective accordingly - storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); + storm::utility::vector::setVectorValues(objectiveResults[objIndex], ~maybeStates, storm::utility::zero()); } - storm::utility::vector::setVectorValues(objectiveResults[objIndex], ~maybeStates, storm::utility::zero()); - // Update the estimate for the next objectives. if (!storm::utility::isZero(weightVector[objIndex])) { storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index 72d96d8ff..b59cd1336 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h @@ -28,7 +28,10 @@ namespace storm { class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker { public: typedef typename SparseModelType::ValueType ValueType; - + using DeterministicInfiniteHorizonHelperType = typename std::conditional>::value, + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper, + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper>::type; + /* * Creates a weight vextor checker. * @@ -68,8 +71,8 @@ namespace storm { void initialize(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0; - virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper() const = 0; - virtual storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper createDetInfiniteHorizonHelper() const = 0; + virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const = 0; + virtual DeterministicInfiniteHorizonHelperType createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const = 0; void infiniteHorizonWeightedPhase(Environment const& env, std::vector const& weightedActionRewardVector, boost::optional> const& weightedStateRewardVector);