HybridCtmcCslHelper.h

Go to the documentation of this file.

#ifndef STORM_MODELCHECKER_HYBRID_CTMC_CSL_MODELCHECKER_HELPER_H_
#define STORM_MODELCHECKER_HYBRID_CTMC_CSL_MODELCHECKER_HELPER_H_
 
#include <memory>
 
#include "storm/models/symbolic/Ctmc.h"
 
#include "storm/modelchecker/results/CheckResult.h"
 
#include "storm/solver/LinearEquationSolver.h"
 
#include "storm/utility/NumberTraits.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
namespace helper {
 
class HybridCtmcCslHelper {
   public:
    template<storm::dd::DdType DdType, typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    static std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                         bool onlyInitialStatesRelevant, storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                         storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                         storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates,
                                                                         bool qualitative, double lowerBound, double upperBound);
 
    template<storm::dd::DdType DdType, typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    static std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                         bool onlyInitialStatesRelevant, storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                         storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                         storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates,
                                                                         bool qualitative, double lowerBound, double upperBound);
 
    template<storm::dd::DdType DdType, typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    static std::unique_ptr<CheckResult> computeInstantaneousRewards(
        Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
        storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector,
        typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel, double timeBound);
 
    template<storm::dd::DdType DdType, typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    static std::unique_ptr<CheckResult> computeInstantaneousRewards(
        Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
        storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector,
        typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel, double timeBound);
 
    template<storm::dd::DdType DdType, typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    static std::unique_ptr<CheckResult> computeCumulativeRewards(Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                 bool onlyInitialStatesRelevant, storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                 storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                 typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel,
                                                                 double timeBound);
 
    template<storm::dd::DdType DdType, typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
    static std::unique_ptr<CheckResult> computeCumulativeRewards(Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                 bool onlyInitialStatesRelevant, storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                 storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                 typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel,
                                                                 double timeBound);
 
    template<storm::dd::DdType DdType, typename ValueType>
    static std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                  storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                  storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                  storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates,
                                                                  bool qualitative);
 
    template<storm::dd::DdType DdType, typename ValueType>
    static std::unique_ptr<CheckResult> computeReachabilityRewards(
        Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix,
        storm::dd::Add<DdType, ValueType> const& exitRateVector, typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel,
        storm::dd::Bdd<DdType> const& targetStates, bool qualitative);
 
    template<storm::dd::DdType DdType, typename ValueType>
    static std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                 storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                 storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                 storm::dd::Bdd<DdType> const& nextStates);
 
    template<storm::dd::DdType DdType, typename ValueType>
    static storm::dd::Add<DdType, ValueType> computeProbabilityMatrix(storm::dd::Add<DdType, ValueType> const& rateMatrix,
                                                                      storm::dd::Add<DdType, ValueType> const& exitRateVector);
 
    template<storm::dd::DdType DdType, typename ValueType>
    static storm::dd::Add<DdType, ValueType> computeUniformizedMatrix(storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
                                                                      storm::dd::Add<DdType, ValueType> const& transitionMatrix,
                                                                      storm::dd::Add<DdType, ValueType> const& exitRateVector,
                                                                      storm::dd::Bdd<DdType> const& maybeStates, ValueType uniformizationRate);
};
 
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm
 
#endif /* STORM_MODELCHECKER_HYBRID_CTMC_CSL_MODELCHECKER_HELPER_H_ */