LraViHelper.h

Go to the documentation of this file.

#pragma once
 
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/multiplier/Multiplier.h"
#include "storm/storage/SparseMatrix.h"
 
namespace storm {
class Environment;
 
namespace modelchecker {
namespace helper {
namespace internal {
 
enum class LraViTransitionsType {
    DetTsNoIs,      
    DetTsNondetIs,  
    DetTsDetIs,     
    NondetTsNoIs    
};
 
template<typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
class LraViHelper {
   public:
    typedef std::function<ValueType(uint64_t)> ValueGetter;
 
    LraViHelper(ComponentType const& component, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, ValueType const& aperiodicFactor,
                storm::storage::BitVector const* timedStates = nullptr, std::vector<ValueType> const* exitRates = nullptr);
 
    ValueType performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter,
                                    std::vector<ValueType> const* exitRates = nullptr, storm::solver::OptimizationDirection const* dir = nullptr,
                                    std::vector<uint64_t>* choices = nullptr);
 
   private:
    void initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates = nullptr);
 
    void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector<uint64_t>* choices = nullptr);
 
    struct ConvergenceCheckResult {
        bool isPrecisionAchieved;
        ValueType currentValue;
    };
 
    ConvergenceCheckResult checkConvergence(bool relative, ValueType precision) const;
 
    void prepareNextIteration(Environment const& env);
 
    void prepareSolversAndMultipliers(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr);
 
    void setInputModelChoices(std::vector<uint64_t>& choices, std::vector<uint64_t> const& localMecChoices, bool setChoiceZeroToMarkovianStates = false,
                              bool setChoiceZeroToProbabilisticStates = false) const;
 
    bool isTimedState(uint64_t const& inputModelStateIndex) const;
 
    std::vector<ValueType>& xNew();
    std::vector<ValueType> const& xNew() const;
 
    std::vector<ValueType>& xOld();
    std::vector<ValueType> const& xOld() const;
 
    bool nondetTs() const;
 
    bool nondetIs() const;
 
    void setComponent(ComponentType component);
 
    // We need to make sure that states/choices will be processed in ascending order
    typedef std::map<uint64_t, std::set<uint64_t>> InternalComponentType;
 
    InternalComponentType _component;
    storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
    storm::storage::BitVector const* _timedStates;  // e.g. Markovian states of a Markov automaton.
    bool _hasInstantStates;
    ValueType _uniformizationRate;
    storm::storage::SparseMatrix<ValueType> _TsTransitions, _TsToIsTransitions, _IsTransitions, _IsToTsTransitions;
    std::vector<ValueType> _Tsx1, _Tsx2, _TsChoiceValues;
    bool _Tsx1IsCurrent;
    std::vector<ValueType> _Isx, _Isb, _IsChoiceValues;
    std::unique_ptr<storm::solver::Multiplier<ValueType>> _TsMultiplier, _TsToIsMultiplier, _IsToTsMultiplier;
    std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> _NondetIsSolver;
    std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> _DetIsSolver;
    std::unique_ptr<storm::Environment> _IsSolverEnv;
};
}  // namespace internal
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm