From 11da1ddc14767aff8022146846104a4d265b5050 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 2 Oct 2017 12:22:34 +0200 Subject: [PATCH] upper bounds for expected reward objectives --- .../SparseMultiObjectivePreprocessor.cpp | 58 +++++++++++++++---- .../SparseMultiObjectivePreprocessor.h | 6 ++ 2 files changed, 54 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 7d44bd268..cb9948b37 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -7,6 +7,7 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/storage/memorystructure/MemoryStructureBuilder.h" @@ -70,16 +71,6 @@ 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); } @@ -387,6 +378,12 @@ namespace storm { setReward0States(result, backwardTransitions); checkRewardFiniteness(result, data.finiteRewardCheckObjectives, backwardTransitions); + // Compute upper result bounds wherever this is necessarry + for (auto const& objIndex : data.upperResultBoundObjectives) { + STORM_LOG_WARN("Computing upper result bound for an objective. TODO: this might not be necessary depending on the solution method."); + result.objectives[objIndex].upperResultBound = computeUpperResultBound(result, objIndex, backwardTransitions); + } + return result; } @@ -500,6 +497,47 @@ namespace storm { } + template + boost::optional SparseMultiObjectivePreprocessor::computeUpperResultBound(ReturnType const& result, uint64_t objIndex, storm::storage::SparseMatrix const& backwardTransitions) { + + if (result.objectives[objIndex].formula->isRewardOperatorFormula() && result.objectives[objIndex].formula->getSubformula().isTotalRewardFormula()) { + auto const& transitions = result.preprocessedModel->getTransitionMatrix(); + auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); + storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true); + + // Get the set of states from which no reward is reachable + auto nonZeroRewardStates = rewModel.getStatesWithZeroReward(transitions); + nonZeroRewardStates.complement(); + auto expRewGreater0EStates = storm::utility::graph::performProbGreater0E(backwardTransitions, allStates, nonZeroRewardStates); + auto expRew0AStates = ~expRewGreater0EStates; + + // An upper reward bound can only be computed if it is below infinity + if (storm::utility::graph::performProb1A(transitions, transitions.getRowGroupIndices(), backwardTransitions, allStates, expRew0AStates).full()) { + storm::storage::SparseMatrix submatrix = transitions.getSubmatrix(true, expRewGreater0EStates, expRewGreater0EStates); + std::vector rew0StateProbs; + rew0StateProbs.reserve(submatrix.getRowCount()); + std::vector rewards; + rewards.reserve(submatrix.getRowCount()); + for (auto const& state : expRewGreater0EStates) { + for (uint64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) { + rew0StateProbs.push_back(transitions.getConstrainedRowSum(choice, expRew0AStates)); + rewards.push_back(rewModel.getTotalStateActionReward(state, choice, transitions)); + } + } + + storm::modelchecker::helper::BaierUpperRewardBoundsComputer baier(submatrix, rewards, rew0StateProbs); + return baier.computeUpperBound(); + } + + } + + + // reaching this point means that we were not able to compute an upper bound + return boost::none; + + } + + template class SparseMultiObjectivePreprocessor>; template class SparseMultiObjectivePreprocessor>; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 5fc531677..00dd6201c 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -92,6 +92,12 @@ namespace storm { */ static void checkRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::SparseMatrix const& backwardTransitions); + /*! + * Finds an upper bound for the expected reward of the objective with the given index (assuming it considers an expected reward objective) + */ + static boost::optional computeUpperResultBound(ReturnType const& result, uint64_t objIndex, storm::storage::SparseMatrix const& backwardTransitions); + + }; } }