SparseDeterministicInfiniteHorizonHelper.h

Go to the documentation of this file.

#pragma once
#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h"
 
namespace storm {
 
namespace modelchecker {
namespace helper {
 
template<typename ValueType>
class SparseDeterministicInfiniteHorizonHelper : public SparseInfiniteHorizonHelper<ValueType, false> {
   public:
    typedef typename SparseInfiniteHorizonHelper<ValueType, true>::ValueGetter ValueGetter;
 
    SparseDeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    SparseDeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates);
 
    virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                             storm::storage::StronglyConnectedComponent const& component) override;
 
    std::vector<ValueType> computeLongRunAverageStateDistribution(Environment const& env);
    std::vector<ValueType> computeLongRunAverageStateDistribution(Environment const& env, uint64_t const& initialState);
    std::vector<ValueType> computeLongRunAverageStateDistribution(Environment const& env, ValueGetter const& initialDistributionGetter);
 
   protected:
    virtual void createDecomposition() override;
 
    std::vector<ValueType> computeBsccReachabilityProbabilities(Environment const& env, ValueGetter const& initialDistributionGetter);
    std::vector<ValueType> computeBsccReachabilityProbabilitiesClassic(Environment const& env, ValueGetter const& initialDistributionGetter);
    std::vector<ValueType> computeBsccReachabilityProbabilitiesEVTs(Environment const& env, ValueGetter const& initialDistributionGetter);
 
    std::vector<ValueType> computeSteadyStateDistrForBscc(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc);
    std::vector<ValueType> computeSteadyStateDistrForBsccEqSys(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc);
    std::vector<ValueType> computeSteadyStateDistrForBsccEVTs(Environment const& env, storm::storage::StronglyConnectedComponent const& bscc);
 
    std::pair<bool, ValueType> computeLraForTrivialBscc(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                                        storm::storage::StronglyConnectedComponent const& bscc);
 
    ValueType computeLraForBsccVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                  storm::storage::StronglyConnectedComponent const& bscc);
 
    std::pair<ValueType, std::vector<ValueType>> computeLraForBsccGainBias(Environment const& env, ValueGetter const& stateValuesGetter,
                                                                           ValueGetter const& actionValuesGetter,
                                                                           storm::storage::StronglyConnectedComponent const& bscc);
 
    std::pair<ValueType, std::vector<ValueType>> computeLraForBsccSteadyStateDistr(Environment const& env, ValueGetter const& stateValuesGetter,
                                                                                   ValueGetter const& actionValuesGetter,
                                                                                   storm::storage::StronglyConnectedComponent const& bscc);
 
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> buildSspMatrixVector(std::vector<ValueType> const& bsccLraValues,
                                                                                                    std::vector<uint64_t> const& inputStateToBsccIndexMap,
                                                                                                    storm::storage::BitVector const& statesNotInComponent,
                                                                                                    bool asEquationSystem);
 
    virtual std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues) override;
};
 
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm