VisitingTimesHelper.h

Go to the documentation of this file.

#pragma once
 
#include <vector>
 
namespace storm::storage {
class BitVector;
class MaximalEndComponent;
template<typename ValueType>
class SparseMatrix;
}  // namespace storm::storage
 
namespace storm::modelchecker::multiobjective {
 
template<typename ValueType>
class VisitingTimesHelper {
   public:
    static ValueType computeMecTraversalLowerBound(storm::storage::MaximalEndComponent const& mec, storm::storage::SparseMatrix<ValueType> const& transitions,
                                                   bool assumeOptimalTransitionProbabilities = false);
 
    static ValueType computeMecVisitsUpperBound(storm::storage::MaximalEndComponent const& mec, storm::storage::SparseMatrix<ValueType> const& transitions,
                                                bool assumeOptimalTransitionProbabilities = false);
 
    static std::vector<ValueType> computeUpperBoundsOnExpectedVisitingTimes(storm::storage::BitVector const& subsystem,
                                                                            storm::storage::SparseMatrix<ValueType> const& transitions,
                                                                            storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
};
}  // namespace storm::modelchecker::multiobjective