SparseNondeterministicInfiniteHorizonHelper.h

Go to the documentation of this file.

#pragma once
#include <optional>
#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::optional<ValueType> computeLraForTrivialMec(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter,
                                                     storm::storage::MaximalEndComponent const& mec);
    std::optional<ValueType> computeLraForZeroMec(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