get_reachable_states¶

Warning

The stormpy developer API is internal and can be subject to change.

get_reachable_states( transition_matrix: stormpy.developer.storage._storage._SparseMatrix_Double, initial_states: stormpy.datastructures.BitVector, constraint_states: stormpy.datastructures.BitVector, target_states: stormpy.datastructures.BitVector, use_step_bound: bool = False, maximal_steps: SupportsInt | SupportsIndex = 0, choice_filter: stormpy.datastructures.BitVector | None = None, ) → stormpy.datastructures.BitVector¶

get_reachable_states( transition_matrix: stormpy.developer.storage._storage._SparseMatrix_Rational, initial_states: stormpy.datastructures.BitVector, constraint_states: stormpy.datastructures.BitVector, target_states: stormpy.datastructures.BitVector, use_step_bound: bool = False, maximal_steps: SupportsInt | SupportsIndex = 0, choice_filter: stormpy.datastructures.BitVector | None = None, ) → stormpy.datastructures.BitVector

get_reachable_states( transition_matrix: stormpy.developer.storage._storage._SparseMatrix_RationalFunction, initial_states: stormpy.datastructures.BitVector, constraint_states: stormpy.datastructures.BitVector, target_states: stormpy.datastructures.BitVector, use_step_bound: bool = False, maximal_steps: SupportsInt | SupportsIndex = 0, choice_filter: stormpy.datastructures.BitVector | None = None, ) → stormpy.datastructures.BitVector

Get states reachable from the initial states