SparseNondeterministicInfiniteHorizonHelper.h

Go to the documentation of this file.

#pragma once
#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h"
 
namespace storm {
 
namespace storage {
template<typename VT>
class Scheduler;
}
 
namespace modelchecker {
namespace helper {
 
template<typename ValueType>
class SparseNondeterministicInfiniteHorizonHelper : public SparseInfiniteHorizonHelper<ValueType, true> {
   public:
    typedef typename SparseInfiniteHorizonHelper<ValueType, true>::ValueGetter ValueGetter;
 
    SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates);
 
    std::vector<uint64_t> const& getProducedOptimalChoices() const;
 
    std::vector<uint64_t>& getProducedOptimalChoices();
 
    storm::storage::Scheduler<ValueType> extractScheduler() const;
 
    virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                             storm::storage::MaximalEndComponent const& component) override;
 
   protected:
    virtual void createDecomposition() override;
 
    std::pair<bool, ValueType> computeLraForTrivialMec(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                                       storm::storage::MaximalEndComponent const& mec);
 
    ValueType computeLraForMecVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                 storm::storage::MaximalEndComponent const& mec);
 
    ValueType computeLraForMecLp(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                 storm::storage::MaximalEndComponent const& mec);
 
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> buildSspMatrixVector(
        std::vector<ValueType> const& mecLraValues, std::vector<uint64_t> const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent,
        uint64_t numberOfNonComponentStates, std::vector<std::pair<uint64_t, uint64_t>>* sspComponentExitChoicesToOriginalMap);
 
    void constructOptimalChoices(std::vector<uint64_t> const& sspChoices, storm::storage::SparseMatrix<ValueType> const& sspMatrix,
                                 std::vector<uint64_t> const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent,
                                 uint64_t numberOfNonComponentStates, std::vector<std::pair<uint64_t, uint64_t>> const& sspComponentExitChoicesToOriginalMap);
 
    virtual std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues) override;
};
 
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm