SparseInfiniteHorizonHelper.h

Go to the documentation of this file.

#pragma once
#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
 
#include "storm/storage/Decomposition.h"
#include "storm/storage/MaximalEndComponent.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/StronglyConnectedComponent.h"
 
namespace storm {
class Environment;
 
namespace models {
namespace sparse {
template<typename VT>
class StandardRewardModel;
}
}  // namespace models
 
namespace modelchecker {
namespace helper {
 
template<typename ValueType, bool Nondeterministic>
class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
   public:
    using LongRunComponentType =
        typename std::conditional<Nondeterministic, storm::storage::MaximalEndComponent, storm::storage::StronglyConnectedComponent>::type;
 
    typedef std::function<ValueType(uint64_t)> ValueGetter;
 
    SparseInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    SparseInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& markovianStates,
                                std::vector<ValueType> const& exitRates);
 
    SparseInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates);
 
    void provideBackwardTransitions(storm::storage::SparseMatrix<ValueType> const& backwardsTransitions);
 
    void provideLongRunComponentDecomposition(storm::storage::Decomposition<LongRunComponentType> const& decomposition);
 
    std::vector<ValueType> computeLongRunAverageProbabilities(Environment const& env, storm::storage::BitVector const& psiStates);
 
    std::vector<ValueType> computeLongRunAverageRewards(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel);
 
    std::vector<ValueType> computeLongRunAverageValues(Environment const& env, std::vector<ValueType> const* stateValues = nullptr,
                                                       std::vector<ValueType> const* actionValues = nullptr);
 
    std::vector<ValueType> computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter);
 
    virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                             LongRunComponentType const& component) = 0;
 
   protected:
    bool isContinuousTime() const;
 
    void createBackwardTransitions();
 
    virtual void createDecomposition() = 0;
 
    virtual std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues) = 0;
 
    storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
    storm::storage::BitVector const* _markovianStates;
    std::vector<ValueType> const* _exitRates;
 
    storm::storage::SparseMatrix<ValueType> const* _backwardTransitions;
    storm::storage::Decomposition<LongRunComponentType> const* _longRunComponentDecomposition;
    std::unique_ptr<storm::storage::SparseMatrix<ValueType>> _computedBackwardTransitions;
    std::unique_ptr<storm::storage::Decomposition<LongRunComponentType>> _computedLongRunComponentDecomposition;
 
    boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
};
 
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm