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/ExtendedNumber.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;
 
    using ExtendedValueType = storm::utility::ExtendedValueType<ValueType>;

    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<ExtendedValueType> computeExpectedVisitingTimes(Environment const& env, storm::storage::BitVector const& initialStates);

    std::vector<ExtendedValueType> computeExpectedVisitingTimes(Environment const& env, uint64_t initialState);

    std::vector<ExtendedValueType> computeExpectedVisitingTimes(Environment const& env, ValueGetter const& initialStateValueGetter);

    void computeExpectedVisitingTimes(Environment const& env, std::vector<ExtendedValueType>& 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<ExtendedValueType>& stateValues) const;

    std::vector<ValueType> computeValueForStateSet(storm::Environment const& env, storm::storage::BitVector const& stateSetAsBitVector,
                                                   std::vector<ExtendedValueType> 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