diff --git a/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.cpp b/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.cpp index 9241e2e87..1b51f0f50 100644 --- a/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.cpp +++ b/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.cpp @@ -13,15 +13,12 @@ namespace storm { namespace helper { template - BaierUpperRewardBoundsComputer::BaierUpperRewardBoundsComputer(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& rewards, std::vector const& oneStepTargetProbabilities) : transitionMatrix(transitionMatrix), rewards(rewards), oneStepTargetProbabilities(oneStepTargetProbabilities) { + BaierUpperRewardBoundsComputer::BaierUpperRewardBoundsComputer(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& rewards, std::vector const& oneStepTargetProbabilities) : _transitionMatrix(transitionMatrix), _rewards(rewards), _oneStepTargetProbabilities(oneStepTargetProbabilities) { // Intentionally left empty. } - + template - ValueType BaierUpperRewardBoundsComputer::computeUpperBound() { - STORM_LOG_TRACE("Computing upper reward bounds using variant-2 of Baier et al."); - std::chrono::high_resolution_clock::time_point start = std::chrono::high_resolution_clock::now(); - + std::vector BaierUpperRewardBoundsComputer::computeUpperBoundOnExpectedVisitingTimes(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& oneStepTargetProbabilities) { std::vector stateToScc(transitionMatrix.getRowGroupCount()); { // Start with an SCC decomposition of the system. @@ -106,18 +103,28 @@ namespace storm { remainingStates.set(newStates.begin(), newStates.end(), false); newStates.clear(); } - - for (uint64_t state = 0; state < result.size(); ++state) { - ValueType maxReward = storm::utility::zero(); - for (auto row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { - maxReward = std::max(maxReward, rewards[row]); - } - result[state] = storm::utility::one() / result[state] * maxReward; + // Transform the d_t to an upper bound for zeta(t) + for (auto& r : result) { + r = storm::utility::one() / r; } + return result; + } + + + template + ValueType BaierUpperRewardBoundsComputer::computeUpperBound() { + STORM_LOG_TRACE("Computing upper reward bounds using variant-2 of Baier et al."); + std::chrono::high_resolution_clock::time_point start = std::chrono::high_resolution_clock::now(); + + auto expVisits = computeUpperBoundOnExpectedVisitingTimes(_transitionMatrix, _oneStepTargetProbabilities); ValueType upperBound = storm::utility::zero(); - for (auto const& e : result) { - upperBound += e; + for (uint64_t state = 0; state < expVisits.size(); ++state) { + ValueType maxReward = storm::utility::zero(); + for (auto row = _transitionMatrix.getRowGroupIndices()[state], endRow = _transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { + maxReward = std::max(maxReward, _rewards[row]); + } + upperBound += expVisits[state] * maxReward; } STORM_LOG_TRACE("Baier algorithm for reward bound computation (variant 2) computed bound " << upperBound << "."); diff --git a/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h b/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h index a9b343d2e..cf47c4c5a 100644 --- a/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h +++ b/src/storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h @@ -29,10 +29,18 @@ namespace storm { */ ValueType computeUpperBound(); + /*! + * Computes for each state an upper bound for the maximal expected times each state is visited. + * @param transitionMatrix The matrix defining the transitions of the system without the transitions + * that lead directly to the goal state. + * @param oneStepTargetProbabilities For each choice the probability to go to a goal state in one step. + */ + static std::vector computeUpperBoundOnExpectedVisitingTimes(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& oneStepTargetProbabilities); + private: - storm::storage::SparseMatrix const& transitionMatrix; - std::vector const& rewards; - std::vector const& oneStepTargetProbabilities; + storm::storage::SparseMatrix const& _transitionMatrix; + std::vector const& _rewards; + std::vector const& _oneStepTargetProbabilities; }; } }