stormvogel.teaching.dtmc_evaluation

Exact reachability evaluation for DTMCs via sympy linear system solving.

Intended for teaching: results are exact rationals, and the intermediate linear system can be displayed in a notebook.

Functions

_check_dtmc(→ None)

_state_variables(→ dict[stormvogel.model.State, ...)

_to_expr(→ sympy.Expr)

Convert val to a sympy expression.

compute_zero_states(→ set[stormvogel.model.State])

Return states from which no one_state is reachable in dtmc.

compute_one_states(→ set[stormvogel.model.State])

Return states that reach target_states with probability 1 in dtmc.

equations_reachability(→ list[sympy.Expr])

Return the sympy residuals for the reachability linear system in a DTMC.

equations_expected_reward() → list[sympy.Expr])

Return the sympy residuals for the expected-reward linear system in a DTMC.

solve_expected_reward() → dict[stormvogel.model.State, ...)

Solve the expected reward system exactly and return per-state values.

solve_reachability(→ dict[stormvogel.model.State, ...)

Solve the reachability linear system exactly and return per-state values.

Module Contents

stormvogel.teaching.dtmc_evaluation._check_dtmc(dtmc: stormvogel.model.Model) → None
stormvogel.teaching.dtmc_evaluation._state_variables(dtmc: stormvogel.model.Model) → dict[stormvogel.model.State, sympy.Symbol]
stormvogel.teaching.dtmc_evaluation._to_expr(val) → sympy.Expr

Convert val to a sympy expression.

Passes through values that are already sympy.Expr (parametric models store probabilities and rewards as sympy expressions directly). Numeric values (int, float, fractions.Fraction) are converted to exact rationals via sympy.nsimplify().

stormvogel.teaching.dtmc_evaluation.compute_zero_states(dtmc: stormvogel.model.Model, one_states: Iterable[stormvogel.model.State]) → set[stormvogel.model.State]

Return states from which no one_state is reachable in dtmc.

Backward BFS from one_states; any state not reached has reachability probability 0. The one_states may belong to a different model — they are matched against dtmc by state_id.

Parameters:

  • dtmc – A stormvogel DTMC.

  • one_states – States with reachability probability 1.

Returns:

Set of states in dtmc with reachability probability 0.

stormvogel.teaching.dtmc_evaluation.compute_one_states(dtmc: stormvogel.model.Model, target_states: Iterable[stormvogel.model.State]) → set[stormvogel.model.State]

Return states that reach target_states with probability 1 in dtmc.

Uses the Prob1 algorithm:

  1. Compute Sno via compute_zero_states().

  2. Backward BFS from Sno, treating target_states as absorbing (paths do not continue through them). The result is the set of states that can reach Sno with positive probability — i.e. states with reachability strictly less than 1.

  3. Syes = all states states that can reach Sno.

Parameters:

  • dtmc – A stormvogel DTMC.

  • target_states – States to reach.

Returns:

Set of states with reachability probability exactly 1.

stormvogel.teaching.dtmc_evaluation.equations_reachability(dtmc: stormvogel.model.Model, one_states: Iterable[stormvogel.model.State], zero_states: Iterable[stormvogel.model.State] | None = None) → list[sympy.Expr]

Return the sympy residuals for the reachability linear system in a DTMC.

Each residual equals zero when the system is satisfied. States in one_states contribute x_s - 1; states in zero_states contribute x_s; all other states contribute x_s - Σ P(s,s') x_{s'}.

Works for both plain DTMCs (numeric probabilities) and parametric DTMCs (probabilities that are sympy expressions over declared parameters). For parametric models, solving the returned system with sympy.linsolve() yields reachability as a rational function in the parameters.

The zero-state auto-detection is graph-based and assumes parameters are strictly positive (no edge is degenerate for the given parameter range).

Parameters:

  • dtmc – A stormvogel DTMC (plain or parametric).

  • one_states – States with reachability probability 1.

  • zero_states – States with reachability probability 0, or None to auto-detect from the graph structure.

Returns:

List of sympy expressions (residuals), one per state in dtmc.sorted_states.

stormvogel.teaching.dtmc_evaluation.equations_expected_reward(dtmc: stormvogel.model.Model, reward_model: stormvogel.model.RewardModel, terminal_states: Iterable[stormvogel.model.State], discount: sympy.Expr = sp.Integer(1)) → list[sympy.Expr]

Return the sympy residuals for the expected-reward linear system in a DTMC.

Each residual equals zero when the system is satisfied. Terminal states contribute x_s; non-terminal states contribute x_s - r_s - γ Σ P(s,s') x_{s'}.

Works for both plain and parametric DTMCs; probabilities and rewards that are sympy expressions are used directly, yielding a parametric solution when the system is solved.

For undiscounted problems (discount = 1) the system is ill-defined when a non-terminal state cannot reach any terminal state, because the expected reward would be infinite. A ValueError is raised in that case rather than producing a wrong answer.

For discounted problems (discount < 1) the system always has a unique solution and no reachability check is needed.

Parameters:

  • dtmc – A stormvogel DTMC (plain or parametric).

  • reward_model – Per-state rewards; missing states are treated as 0.

  • terminal_states – States fixed to value 0 (reward collection stops).

  • discount – Discount factor γ ∈ (0, 1]. Must be a sympy expression or a value that sympy.nsimplify() can convert.

Raises:

ValueError – If discount > 1, or if discount = 1 and any non-terminal state cannot reach a terminal state.

stormvogel.teaching.dtmc_evaluation.solve_expected_reward(dtmc: stormvogel.model.Model, reward_model: stormvogel.model.RewardModel, terminal_states: Iterable[stormvogel.model.State], discount: sympy.Expr = sp.Integer(1)) → dict[stormvogel.model.State, sympy.Expr]

Solve the expected reward system exactly and return per-state values.

Parameters:

  • dtmc – A stormvogel DTMC.

  • reward_model – Per-state rewards; missing states are treated as 0.

  • terminal_states – States fixed to value 0.

  • discount – Discount factor γ ∈ (0, 1].

Returns:

Mapping from state to exact sympy expected reward.

Raises:

ValueError – See equations_expected_reward().

stormvogel.teaching.dtmc_evaluation.solve_reachability(dtmc: stormvogel.model.Model, one_states: Iterable[stormvogel.model.State], zero_states: Iterable[stormvogel.model.State] | None = None) → dict[stormvogel.model.State, sympy.Expr]

Solve the reachability linear system exactly and return per-state values.

Parameters:

  • dtmc – A stormvogel DTMC.

  • one_states – States with reachability probability 1.

  • zero_states – States with reachability probability 0, or None to auto-detect via compute_zero_states().

Returns:

Mapping from state to exact rational reachability probability.

Raises:

ValueError – If the system has no unique solution.