BaierUpperRewardBoundsComputer.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <functional>
#include <vector>
 
namespace storm {
namespace storage {
template<typename ValueType>
class SparseMatrix;
}
 
namespace modelchecker {
namespace helper {
 
template<typename ValueType>
class BaierUpperRewardBoundsComputer {
   public:
    BaierUpperRewardBoundsComputer(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& oneStepTargetProbabilities,
                                   std::function<uint64_t(uint64_t)> const& stateToScc = {});

    BaierUpperRewardBoundsComputer(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                   storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepTargetProbabilities,
                                   std::function<uint64_t(uint64_t)> const& stateToScc = {});
 
    struct Bounds {
        ValueType lower;
        ValueType upper;
    };

    Bounds computeTotalRewardBounds(std::vector<ValueType> const& rewards);

    static std::vector<ValueType> computeUpperBoundOnExpectedVisitingTimes(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                                           storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                                           std::vector<ValueType> const& oneStepTargetProbabilities);

    static std::vector<ValueType> computeUpperBoundOnExpectedVisitingTimes(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                                           std::vector<ValueType> const& oneStepTargetProbabilities);

    static std::vector<ValueType> computeUpperBoundOnExpectedVisitingTimes(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                                           storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                                           std::vector<ValueType> const& oneStepTargetProbabilities,
                                                                           std::function<uint64_t(uint64_t)> const& stateToScc);
 
   private:
    storm::storage::SparseMatrix<ValueType> const& transitionMatrix;
    storm::storage::SparseMatrix<ValueType> const* backwardTransitions;
    std::function<uint64_t(uint64_t)> stateToScc;
    std::vector<ValueType> const& oneStepTargetProbabilities;
};
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm