SparseDeterministicVisitingTimesHelper.h

Go to the documentation of this file.

#pragma once
#include <vector>
 
#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/utility/OptionalRef.h"
 
namespace storm {
class Environment;
 
namespace modelchecker {
namespace helper {
 
template<typename ValueType>
class SparseDeterministicVisitingTimesHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
   public:
    typedef std::function<ValueType(uint64_t)> ValueGetter;
 
    SparseDeterministicVisitingTimesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    SparseDeterministicVisitingTimesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates);
 
    void provideBackwardTransitions(storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
 
    void provideSCCDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& decomposition);
 
    std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, storm::storage::BitVector const& initialStates);
 
    std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, uint64_t initialState);
 
    std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, ValueGetter const& initialStateValueGetter);
 
    void computeExpectedVisitingTimes(Environment const& env, std::vector<ValueType>& stateValues);
 
    std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, storm::storage::BitVector const& subsystem,
                                                        std::vector<ValueType> const& initialValues) const;
 
   private:
    bool isContinuousTime() const;
 
    void createBackwardTransitions();
 
    void createDecomposition(Environment const& env);
 
    void createNonBsccStateVector();
 
    std::vector<ValueType> computeUpperBounds(storm::storage::BitVector const& stateSetAsBitVector) const;
 
    storm::Environment getEnvironmentForSolver(storm::Environment const& env, bool topological = false) const;
 
    storm::Environment getEnvironmentForTopologicalSolver(storm::Environment const& env) const;
 
    void processSingletonScc(uint64_t sccState, std::vector<ValueType>& stateValues) const;
 
    std::vector<ValueType> computeValueForStateSet(storm::Environment const& env, storm::storage::BitVector const& stateSetAsBitVector,
                                                   std::vector<ValueType> const& stateValues) const;
 
    storm::storage::SparseMatrix<ValueType> const& transitionMatrix;
    storm::OptionalRef<std::vector<ValueType> const> exitRates;
 
    storm::OptionalRef<storm::storage::SparseMatrix<ValueType> const> backwardTransitions;
    std::unique_ptr<storm::storage::SparseMatrix<ValueType>> computedBackwardTransitions;
 
    storm::OptionalRef<storm::storage::StronglyConnectedComponentDecomposition<ValueType> const> sccDecomposition;
    std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> computedSccDecomposition;
 
    storm::storage::BitVector nonBsccStates;
};
 
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm