SparseCtmcCslHelper.h

Go to the documentation of this file.

#ifndef STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_
#define STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_
 
#include "storm/storage/BitVector.h"
 
#include "storm/logic/OperatorFormula.h"
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/SolveGoal.h"
 
#include "storm/utility/NumberTraits.h"
 
#include "storm/storage/sparse/StateType.h"
 
namespace storm {
 
class Environment;
 
namespace storage {
class StronglyConnectedComponent;
}
 
namespace modelchecker {
namespace helper {
class SparseCtmcCslHelper {
   public:
    template<typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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, double lowerBound,
                                                                   double upperBound);
 
    template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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, double lowerBound,
                                                                   double 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, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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,
                                                              double timeBound);
 
    template<typename ValueType, typename RewardModelType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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,
                                                              double timeBound);
 
    template<typename ValueType, typename RewardModelType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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, double timeBound);
 
    template<typename ValueType, typename RewardModelType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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, double timeBound);
 
    template<typename ValueType, typename RewardModelType>
    static std::vector<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<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<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, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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,
                                                                   double timeBound);
    template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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,
                                                                   double timeBound);
 
    template<typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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,
             typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    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 helper
}  // namespace modelchecker
}  // namespace storm
 
#endif /* STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_ */