stormpy.analysis

Graph and numerical analyses of probabilistic models.

Includes maximal end components, shortest paths, qualitative reachability, expected visiting times and steady-state distributions.

Functions

compute_expected_number_of_visits(model, *)	Compute the expected number of visits of each state, starting from the initial states.
compute_prob01_states(model, property)	Compute the states satisfying a reachability or until property with probability 0 and with probability 1.
compute_steady_state_distribution(model, *)	Compute the steady-state (aka stationary) distribution.
get_maximal_end_components(model)	Compute the maximal end components of a nondeterministic sparse model.
shortest_path(model, target, *[, k])	Compute the k-th most probable path from an initial state to a target.
topological_sort(model, *[, forward, initial])	Sort the states of a sparse model topologically.

Classes

MaximalEndComponent	Maximal end component
MaximalEndComponentDecomposition	Decomposition of maximal end components
Path	Entry of the shortest path tree: the k-th shortest path to a state via its predecessor and the path's probability