StronglyConnectedComponentDecomposition.h

Go to the documentation of this file.

#pragma once
 
#include <optional>
#include <vector>
 
#include "storm/storage/BitVector.h"
#include "storm/storage/Decomposition.h"
#include "storm/storage/StronglyConnectedComponent.h"
#include "storm/utility/OptionalRef.h"
namespace storm {
 
namespace storage {
 
template<typename ValueType>
class SparseMatrix;
 
struct StronglyConnectedComponentDecompositionOptions {
    StronglyConnectedComponentDecompositionOptions& subsystem(storm::storage::BitVector const& subsystem);
 
    StronglyConnectedComponentDecompositionOptions& choices(storm::storage::BitVector const& choices);
 
    StronglyConnectedComponentDecompositionOptions& dropNaiveSccs(bool value = true);
 
    StronglyConnectedComponentDecompositionOptions& onlyBottomSccs(bool value = true);
 
    StronglyConnectedComponentDecompositionOptions& forceTopologicalSort(bool value = true);
 
    StronglyConnectedComponentDecompositionOptions& computeSccDepths(bool value = true);
 
    storm::OptionalRef<storm::storage::BitVector const> optSubsystem;
    storm::OptionalRef<storm::storage::BitVector const> optChoices;
    bool areNaiveSccsDropped = false;
    bool areOnlyBottomSccsConsidered = false;
    bool isTopologicalSortForced = false;
    bool isComputeSccDepthsSet = false;
};
 
struct SccDecompositionMemoryCache {
    void initialize(uint64_t numStates);
    bool hasPreorderNumber(uint64_t stateIndex) const;
    std::vector<uint64_t> preorderNumbers, recursionStateStack, s, p;
};
 
struct SccDecompositionResult {
    void initialize(uint64_t numStates, bool computeSccDepths);
    bool stateHasScc(uint64_t stateIndex) const;     
    uint64_t sccCount;                               
    std::vector<uint64_t> stateToSccMapping;         
    storm::storage::BitVector nonTrivialStates;      
    std::optional<std::vector<uint64_t>> sccDepths;  
};
 
template<typename ValueType>
void performSccDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options,
                             SccDecompositionResult& result);
 
template<typename ValueType>
void performSccDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options,
                             SccDecompositionResult& result, SccDecompositionMemoryCache& cache);
 
template<typename ValueType>
class StronglyConnectedComponentDecomposition : public Decomposition<StronglyConnectedComponent> {
   public:
    StronglyConnectedComponentDecomposition();
 
    StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                            StronglyConnectedComponentDecompositionOptions const& options = StronglyConnectedComponentDecompositionOptions());
 
    StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other);
 
    StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition const& other);
 
    StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other);
 
    StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other);
 
    bool hasSccDepth() const;
 
    uint_fast64_t getSccDepth(uint_fast64_t const& sccIndex) const;
 
    uint_fast64_t getMaxSccDepth() const;
 
    std::vector<uint64_t> computeStateToSccIndexMap(uint64_t numberOfStates) const;
 
   private:
    /*
     * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills
     * the vector of blocks of the decomposition.
     *
     * @param transitionMatrix The transition matrix of the system to decompose.
     */
    void performSccDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                 StronglyConnectedComponentDecompositionOptions const& options);
 
    std::optional<std::vector<uint_fast64_t>> sccDepths;
};
}  // namespace storage
}  // namespace storm