SparseCtmcCslHelper.h

Go to the documentation of this file.

#pragma once
 
#include <optional>
 
#include "storm/storage/BitVector.h"
 
#include "storm/logic/OperatorFormula.h"
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/SolveGoal.h"
#include "storm/utility/ExtendedNumber.h"
 
#include "storm/utility/NumberTraits.h"
 
#include "storm/storage/sparse/StateType.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker::helper {
class SparseCtmcCslHelper {
   public:
    template<typename ValueType>
        requires storm::NumberTraits<ValueType>::SupportsExponential
    static std::vector<ValueType> computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
                                                                   storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                                   storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                                   storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates,
                                                                   std::vector<ValueType> const& exitRates, bool qualitative, ValueType lowerBound,
                                                                   std::optional<ValueType> const& upperBound);
 
    template<typename ValueType>
    static std::vector<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
                                                            storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                            storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                            std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates,
                                                            storm::storage::BitVector const& psiStates, bool qualitative);
 
    template<typename ValueType>
    static std::vector<ValueType> computeAllUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
                                                               storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                               std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates,
                                                               storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
 
    template<typename ValueType>
    static std::vector<ValueType> computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                           std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates);
 
    template<typename ValueType, typename RewardModelType>
        requires storm::NumberTraits<ValueType>::SupportsExponential
    static std::vector<ValueType> computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
                                                              storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                              std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel,
                                                              ValueType timeBound);
 
    template<typename ValueType, typename RewardModelType>
        requires storm::NumberTraits<ValueType>::SupportsExponential
    static std::vector<ValueType> computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
                                                           storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                           std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel,
                                                           ValueType timeBound);
 
    template<typename ValueType, typename RewardModelType>
    static std::vector<storm::utility::ExtendedValueType<ValueType>> computeReachabilityRewards(
        Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix,
        storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel,
        storm::storage::BitVector const& targetStates, bool qualitative);
 
    template<typename ValueType, typename RewardModelType>
    static std::vector<storm::utility::ExtendedValueType<ValueType>> computeTotalRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
                                                                                         storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                                                         storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                                                         std::vector<ValueType> const& exitRateVector,
                                                                                         RewardModelType const& rewardModel, bool qualitative);
 
    template<typename ValueType>
    static std::vector<storm::utility::ExtendedValueType<ValueType>> computeReachabilityTimes(
        Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix,
        storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector,
        storm::storage::BitVector const& targetStates, bool qualitative);
 
    template<typename ValueType>
        requires storm::NumberTraits<ValueType>::SupportsExponential
    static std::vector<ValueType> computeAllTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                                   storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates,
                                                                   storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates,
                                                                   ValueType timeBound);

    template<typename ValueType>
        requires storm::NumberTraits<ValueType>::SupportsExponential
    static storm::storage::SparseMatrix<ValueType> computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                                            storm::storage::BitVector const& maybeStates, ValueType uniformizationRate,
                                                                            std::vector<ValueType> const& exitRates);

    template<typename ValueType, bool useMixedPoissonProbabilities = false>
        requires storm::NumberTraits<ValueType>::SupportsExponential
    static std::vector<ValueType> computeTransientProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix,
                                                                std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate,
                                                                std::vector<ValueType> values, ValueType epsilon);

    template<typename ValueType>
    static storm::storage::SparseMatrix<ValueType> computeProbabilityMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                                            std::vector<ValueType> const& exitRates);

    template<typename ValueType>
    static storm::storage::SparseMatrix<ValueType> computeGeneratorMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix,
                                                                          std::vector<ValueType> const& exitRates);

    template<typename ValueType>
    static bool checkAndUpdateTransientProbabilityEpsilon(storm::Environment const& env, ValueType& epsilon, std::vector<ValueType> const& resultVector,
                                                          storm::storage::BitVector const& relevantPositions);
};
}  // namespace modelchecker::helper
}  // namespace storm