Storm
A Modern Probabilistic Model Checker
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Public Member Functions | Public Attributes | List of all members
storm::storage::SccDecompositionResult Struct Reference

Holds the result data of the implemented SCC decomposition algorithm. More...

#include <StronglyConnectedComponentDecomposition.h>

Collaboration diagram for storm::storage::SccDecompositionResult:
Collaboration graph
[legend]

Public Member Functions

void initialize (uint64_t numStates, bool computeSccDepths)
 
bool stateHasScc (uint64_t stateIndex) const
 

Public Attributes

uint64_t sccCount
 True if an SCC is associated to the given state.
 
std::vector< uint64_t > stateToSccMapping
 Number of found SCCs.
 
storm::storage::BitVector nonTrivialStates
 Mapping from states to the SCC it belongs to.
 
std::optional< std::vector< uint64_t > > sccDepths
 Keep track of trivial states (singleton SCCs without selfloop).
 

Detailed Description

Holds the result data of the implemented SCC decomposition algorithm.

Definition at line 58 of file StronglyConnectedComponentDecomposition.h.

Member Function Documentation

◆ initialize()

void storm::storage::SccDecompositionResult::initialize ( uint64_t  numStates,
bool  computeSccDepths 
)

Definition at line 54 of file StronglyConnectedComponentDecomposition.cpp.

◆ stateHasScc()

bool storm::storage::SccDecompositionResult::stateHasScc ( uint64_t  stateIndex) const

Definition at line 70 of file StronglyConnectedComponentDecomposition.cpp.

Member Data Documentation

◆ nonTrivialStates

storm::storage::BitVector storm::storage::SccDecompositionResult::nonTrivialStates

Mapping from states to the SCC it belongs to.

Definition at line 63 of file StronglyConnectedComponentDecomposition.h.

◆ sccCount

uint64_t storm::storage::SccDecompositionResult::sccCount

True if an SCC is associated to the given state.

Definition at line 61 of file StronglyConnectedComponentDecomposition.h.

◆ sccDepths

std::optional<std::vector<uint64_t> > storm::storage::SccDecompositionResult::sccDepths

Keep track of trivial states (singleton SCCs without selfloop).

Definition at line 64 of file StronglyConnectedComponentDecomposition.h.

◆ stateToSccMapping

std::vector<uint64_t> storm::storage::SccDecompositionResult::stateToSccMapping

Number of found SCCs.

Definition at line 62 of file StronglyConnectedComponentDecomposition.h.

The documentation for this struct was generated from the following files: