DsMpiUpperRewardBoundsComputer.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <vector>
 
namespace storm {
namespace storage {
template<typename ValueType>
class SparseMatrix;
}
 
namespace modelchecker {
namespace helper {
 
template<typename ValueType>
class DsMpiDtmcPriorityLess;
 
template<typename ValueType>
class DsMpiDtmcUpperRewardBoundsComputer {
   public:
    DsMpiDtmcUpperRewardBoundsComputer(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& rewards,
                                       std::vector<ValueType> const& oneStepTargetProbabilities);
 
    virtual ~DsMpiDtmcUpperRewardBoundsComputer() = default;
 
    std::vector<ValueType> computeUpperBounds();
 
   protected:
    virtual void sweep();
 
    virtual ValueType computeLambda() const;
 
    ValueType computeLambdaForChoice(uint64_t choice) const;
 
    virtual uint64_t getStateForChoice(uint64_t choice) const;
 
    // References to input data.
    storm::storage::SparseMatrix<ValueType> const& transitionMatrix;
    std::vector<ValueType> const& originalRewards;
    std::vector<ValueType> const& originalOneStepTargetProbabilities;
 
    // Derived from input data.
    storm::storage::SparseMatrix<ValueType> backwardTransitions;
 
    // Data that the algorithm uses internally.
    std::vector<ValueType> p;
    std::vector<ValueType> w;
    std::vector<ValueType> rewards;
    std::vector<ValueType> targetProbabilities;
 
    friend class DsMpiDtmcPriorityLess<ValueType>;
};
 
template<typename ValueType>
class DsMpiMdpPriorityLess;
 
template<typename ValueType>
class DsMpiMdpUpperRewardBoundsComputer : public DsMpiDtmcUpperRewardBoundsComputer<ValueType> {
   public:
    DsMpiMdpUpperRewardBoundsComputer(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& rewards,
                                      std::vector<ValueType> const& oneStepTargetProbabilities);
 
   private:
    virtual void sweep() override;
    virtual ValueType computeLambda() const override;
    virtual uint64_t getStateForChoice(uint64_t choice) const override;
    uint64_t getChoiceInState(uint64_t state) const;
    void setChoiceInState(uint64_t state, uint64_t choice);
 
    std::vector<uint64_t> choiceToState;
    std::vector<uint64_t> policy;
 
    friend class DsMpiMdpPriorityLess<ValueType>;
};
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm