ShortestPathsGenerator

Warning

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

class ShortestPathsGenerator[ValueType]

Computes the k most probable paths from the initial states to a set of target states

Template arguments:

  • ValueType (type)

Available specializations:

  • ShortestPathsGenerator[float]

  • ShortestPathsGenerator[stormpy.numbers.Rational]

Construction

The specialization can be inferred from the first positional constructor argument (alternatively, the model or transition_matrix or maybe_transition_matrix keyword argument).

Constructor signatures vary by specialization:

  • ShortestPathsGenerator[float](model: stormpy.models.SparseModel[float], target_bv: stormpy.datastructures.BitVector)

  • ShortestPathsGenerator[float](model: stormpy.models.SparseModel[float], single_target: typing.SupportsInt | typing.SupportsIndex)

  • ShortestPathsGenerator[float](model: stormpy.models.SparseModel[float], target_list: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex])

  • ShortestPathsGenerator[float](model: stormpy.models.SparseModel[float], target_label: str = 'target')

  • ShortestPathsGenerator[float](transition_matrix: stormpy.datastructures.SparseMatrix[float], target_prob_vector: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex], initial_states: stormpy.datastructures.BitVector, matrix_format: stormpy.developer.utility.MatrixFormat)

  • ShortestPathsGenerator[float](maybe_transition_matrix: stormpy.datastructures.SparseMatrix[float], target_prob_map: collections.abc.Mapping[typing.SupportsInt | typing.SupportsIndex, typing.SupportsFloat | typing.SupportsIndex], initial_states: stormpy.datastructures.BitVector, matrix_format: stormpy.developer.utility.MatrixFormat)

  • ShortestPathsGenerator[stormpy.numbers.Rational](model: stormpy.models.SparseModel[stormpy.numbers.Rational], target_bv: stormpy.datastructures.BitVector)

  • ShortestPathsGenerator[stormpy.numbers.Rational](model: stormpy.models.SparseModel[stormpy.numbers.Rational], single_target: typing.SupportsInt | typing.SupportsIndex)

  • ShortestPathsGenerator[stormpy.numbers.Rational](model: stormpy.models.SparseModel[stormpy.numbers.Rational], target_list: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex])

  • ShortestPathsGenerator[stormpy.numbers.Rational](model: stormpy.models.SparseModel[stormpy.numbers.Rational], target_label: str = 'target')

  • ShortestPathsGenerator[stormpy.numbers.Rational](transition_matrix: stormpy.datastructures.SparseMatrix[stormpy.numbers.Rational], target_prob_vector: collections.abc.Sequence[stormpy.numbers.Rational], initial_states: stormpy.datastructures.BitVector, matrix_format: stormpy.developer.utility.MatrixFormat)

  • ShortestPathsGenerator[stormpy.numbers.Rational](maybe_transition_matrix: stormpy.datastructures.SparseMatrix[stormpy.numbers.Rational], target_prob_map: collections.abc.Mapping[typing.SupportsInt | typing.SupportsIndex, stormpy.numbers.Rational], initial_states: stormpy.datastructures.BitVector, matrix_format: stormpy.developer.utility.MatrixFormat)

Members

ShortestPathsGenerator.get_distance(
self: stormpy.developer.utility.ShortestPathsGenerator[ValueType],
k: SupportsInt | SupportsIndex,
) → ValueType

Get the probability of the k-th shortest path

ShortestPathsGenerator.get_path_as_list(
self: stormpy.developer.utility.ShortestPathsGenerator[ValueType],
k: SupportsInt | SupportsIndex,
) → list[int]

Get the states of the k-th shortest path as back-to-front traversal

ShortestPathsGenerator.get_states(
self: stormpy.developer.utility.ShortestPathsGenerator[ValueType],
k: SupportsInt | SupportsIndex,
) → stormpy.datastructures.BitVector

Get the states occurring in the k-th shortest path