stormvogel.examples

Submodules

• stormvogel.examples.atva20
• stormvogel.examples.atva20_z0
• stormvogel.examples.car
• stormvogel.examples.cheese_maze
• stormvogel.examples.condensed_monty_hall
• stormvogel.examples.debugging
• stormvogel.examples.die
• stormvogel.examples.end_components
• stormvogel.examples.four_state_reachability
• stormvogel.examples.knuth_yao_imc
• stormvogel.examples.knuth_yao_pmc
• stormvogel.examples.lion
• stormvogel.examples.minitown
• stormvogel.examples.mixed_mec
• stormvogel.examples.mixedpolicymo
• stormvogel.examples.monty_hall
• stormvogel.examples.monty_hall_pomdp
• stormvogel.examples.monty_hall_should
• stormvogel.examples.nuclear_fusion_ctmc
• stormvogel.examples.parker
• stormvogel.examples.six_state_reachability
• stormvogel.examples.stormpy_examples
• stormvogel.examples.study
• stormvogel.examples.sup_not_attained_pomdp
• stormvogel.examples.two_state_commitment_pomdp

Functions

create_car_mdp()
create_debugging_mdp()
create_die_dtmc()
generate_dice_image(→ PIL.Image.Image)	Generates a 128x128 PIL image with a question mark for 0
create_end_components_mdp()
create_mixed_mec_mdp()	MDP illustrating trivial MECs, non-trivial MECs, and non-MEC cycling.
create_lion_mdp()
create_monty_hall_mdp()
create_monty_hall_pomdp()
create_monty_hall_mdp2()
create_nuclear_fusion_ctmc()
create_knuth_yao_pmc()	Build the Knuth--Yao dice as a parametric DTMC.
create_knuth_yao_pmc_twocoins()	Build the Knuth--Yao dice as a parametric DTMC.
create_parker_mdp()	Return the Parker MDP, a small MDP used in the lecture notes by David Parker.
example_building_ctmcs_01()
example_building_dtmcs_01()
example_building_mas_01()
create_study_mdp()
create_cheese_maze([num_corridors, vcorridor_length, ...])	Build the cheese maze POMDP using the bird API.
create_condensed_monty_hall(→ stormvogel.model.Model)	Return the condensed Monty Hall POMDP.
create_4state_reachability_pomdp(...)	Return the 4-state reachability POMDP.
create_4state_reachability_pomdp_variantb(...)	Return the 4-state reachability POMDP.
create_6state_reachability_pomdp(...)	Return the 6-state reachability POMDP.
create_6state_reachability_pomdp_variantb(...)	Return the 6-state reachability POMDP, variant b (three actions).
create_two_state_commitment_pomdp(...)	Return the two-state commitment POMDP.
create_sup_not_attained_pomdp(→ stormvogel.model.Model)	Return the "supremum not attained" POMDP.
create_atva20_pomdp(→ stormvogel.model.Model)	Return the ATVA 2020 POMDP example.
create_atva20_z0_pomdp(→ stormvogel.model.Model)	Return the simplified ATVA z0-cluster POMDP.

Package Contents

stormvogel.examples.create_car_mdp()

stormvogel.examples.create_debugging_mdp()

stormvogel.examples.create_die_dtmc()

stormvogel.examples.generate_dice_image(number: int) → PIL.Image.Image

Generates a 128x128 PIL image with a question mark for 0 or a dice face (1-6) with the corresponding number of dots.

stormvogel.examples.create_end_components_mdp()

stormvogel.examples.create_mixed_mec_mdp()

MDP illustrating trivial MECs, non-trivial MECs, and non-MEC cycling.

States

s0 : entry state; routes to each region s1 : cycle with stochastic exit — NOT a MEC (notmec1) s2 : cycle with stochastic exit — NOT a MEC; labeled “target” (notmec2) s3 : non-trivial MEC via “loop”; “escape” exits to s1 (mec1) s4 : non-trivial MEC via “loop”; “self” self-loops (mec2) s5 : absorbing self-loop — trivial MEC (sink)

Extra actions on s3/s4 highlight that being in an EC is about the existence of a scheduler that stays forever, not that every scheduler does.

stormvogel.examples.create_lion_mdp()

stormvogel.examples.create_monty_hall_mdp()

stormvogel.examples.create_monty_hall_pomdp()

stormvogel.examples.create_monty_hall_mdp2()

stormvogel.examples.create_nuclear_fusion_ctmc()

stormvogel.examples.create_knuth_yao_pmc()

Build the Knuth–Yao dice as a parametric DTMC.

The parameter x is the success probability of the underlying coin. Probabilities are expressed as ordinary sympy expressions, so 1 - x is literally 1 - x — no special constructors needed.

stormvogel.examples.create_knuth_yao_pmc_twocoins()

Build the Knuth–Yao dice as a parametric DTMC.

stormvogel.examples.create_parker_mdp()

Return the Parker MDP, a small MDP used in the lecture notes by David Parker.

States s0–s3; s0 and s3 have two actions (a, b), the rest only action a. s2 is an absorbing target state.

stormvogel.examples.example_building_ctmcs_01()

stormvogel.examples.example_building_dtmcs_01()

stormvogel.examples.example_building_mas_01()

stormvogel.examples.create_study_mdp()

stormvogel.examples.create_cheese_maze(num_corridors: int = 3, vcorridor_length: int = 2, slippery: float = 0.0)

Build the cheese maze POMDP using the bird API.

The maze has a horizontal corridor (top row) of width 2*num_corridors-1 connected to num_corridors vertical corridors. Each vertical corridor ends at the bottom row, where the middle corridor holds the cheese and the rest hold dragons.

Observations are determined by which directions are open (walls / grid boundaries), except for the bottom row and the special start state.

Parameters:

• num_corridors – Number of vertical corridors. Must be odd and >= 3.

• vcorridor_length – Number of blue cells in each vertical corridor (rows between horizontal corridor and bottom row).

• slippery – Probability that an action is a no-op (agent stays in place). Must be in [0, 1). Default 0 gives fully deterministic moves. Has no effect when the intended move would already stay in place (wall or boundary), since both outcomes coincide.

stormvogel.examples.create_condensed_monty_hall() → stormvogel.model.Model

Return the condensed Monty Hall POMDP.

The model has 10 states. Observations do not distinguish prize location (d1/d2/d3), nor whether the initial pick was correct (g vs b), nor the post-reveal state (g’ vs b’). Switching is the optimal final action.

Returns:

A stormvogel POMDP model.

stormvogel.examples.create_4state_reachability_pomdp(p: Fraction | float = Fraction(1, 2)) → stormvogel.model.Model

Return the 4-state reachability POMDP.

Parameters:

p – Initial probability of being in s1 (must be in (0, 1)).

Returns:

A stormvogel POMDP model.

Raises:

ValueError – If p is not in (0, 1).

stormvogel.examples.create_4state_reachability_pomdp_variantb(p: Fraction | float = Fraction(1, 2)) → stormvogel.model.Model

Return the 4-state reachability POMDP.

Parameters:

p – Initial probability of being in s1 (must be in (0, 1)).

Returns:

A stormvogel POMDP model.

Raises:

ValueError – If p is not in (0, 1).

stormvogel.examples.create_6state_reachability_pomdp(p: Fraction | float = Fraction(1, 2)) → stormvogel.model.Model

Return the 6-state reachability POMDP.

The initial distribution puts weight p on s3 and 1 − p on s4.

Transitions at the outer level (obs z2):

s3  --a-->  s1 (7/10),  s2 (3/10)
s3  --b-->  s3 (8/10),  s4 (2/10)
s4  --a-->  s1 (2/10),  s2 (8/10)
s4  --b-->  s3 (3/10),  s4 (7/10)

Transitions at the inner level (obs z) are identical to the 4-state model:

s1  --a-->  target (7/10),  sink (3/10)
s1  --b-->  s1 (8/10),     s2 (2/10)
s2  --a-->  target (2/10),  sink (8/10)
s2  --b-->  s1 (3/10),     s2 (7/10)

Parameters:

p – Initial probability of being in s3 (must be in (0, 1)).

Returns:

A stormvogel POMDP model.

Raises:

ValueError – If p is not in (0, 1).

stormvogel.examples.create_6state_reachability_pomdp_variantb(p: Fraction | float = Fraction(1, 2)) → stormvogel.model.Model

Return the 6-state reachability POMDP, variant b (three actions).

Mirrors create_4state_reachability_pomdp_variantb(): the inner level uses three actions (a, b, c), and the outer level (s3/s4) mirrors the same structure with s1/s2 in place of target/sink.

Transitions at the outer level (obs z2):

s3  --a-->  s1 (1)
s3  --b-->  s3 (3/4),  s4 (1/4)
s3  --c-->  s1 (1/4),  s2 (3/4)
s4  --a-->  s2 (1)
s4  --b-->  s3 (2/3),  s4 (1/3)
s4  --c-->  s1 (4/5),  s2 (1/5)

Transitions at the inner level (obs z) are identical to the 4-state variant b:

s1  --a-->  target (1)
s1  --b-->  s1 (3/4),     s2 (1/4)
s1  --c-->  target (1/4), sink (3/4)
s2  --a-->  sink (1)
s2  --b-->  s1 (2/3),     s2 (1/3)
s2  --c-->  target (4/5), sink (1/5)

Parameters:

p – Initial probability of being in s3 (must be in (0, 1)).

Returns:

A stormvogel POMDP model.

Raises:

ValueError – If p is not in (0, 1).

stormvogel.examples.create_two_state_commitment_pomdp(p: Fraction | float = Fraction(1, 2)) → stormvogel.model.Model

Return the two-state commitment POMDP.

The initial distribution puts weight p on s1 and 1 − p on s2.

Transitions:

s1  --a1-->  g (1)
s1  --a2-->  f (1)
s1  --w -->  s1 (4/5),  f (1/5)

s2  --a1-->  f (1)
s2  --a2-->  g (1)
s2  --w -->  s2 (4/5),  f (1/5)

Analytical values at the uniform initial belief b_0 = {s1:1/2, s2:1/2}:

V_MDP(b_0)   = 1     (oracle always picks the correct action)
V_QMDP(b_0)  = 4/5   (w-alpha dominates; assumes revelation after one step)
V_POMDP(b_0) = 1/2   (commit immediately; waiting is never informative)

Parameters:

p – Initial probability of being in s1 (must be in (0, 1)).

Returns:

A stormvogel POMDP model.

Raises:

ValueError – If p is not in (0, 1).

stormvogel.examples.create_sup_not_attained_pomdp() → stormvogel.model.Model

Return the “supremum not attained” POMDP.

The start state distributes uniformly over L_l, R_l, L_r, R_r (probability 1/4 each), so the initial belief is {L: 1/2, R: 1/2} under either first observation.

Transitions:

L_l / L_r  --listen-->  L_l (9/10),  L_r (1/10)
R_l / R_r  --listen-->  R_l (1/10),  R_r (9/10)

L_l / L_r  --guessL-->  g (1)
L_l / L_r  --guessR-->  f (1)
R_l / R_r  --guessL-->  f (1)
R_l / R_r  --guessR-->  g (1)

Returns:

A stormvogel POMDP model.

stormvogel.examples.create_atva20_pomdp() → stormvogel.model.Model

Return the ATVA 2020 POMDP example.

Transitions:

s0  --a-->  s1 (3/5),  s2 (1/5),  s0 (1/5)
s0  --b-->  s5 (1/6),  s6 (1/3),  s0 (1/2)

s5  --a-->  s1 (1)
s5  --b-->  s5 (1/4),  s6 (3/4)

s6  --a-->  s2 (1)
s6  --b-->  s5 (2/3),  s6 (1/3)

s1  --a-->  s3 (1)
s1  --b-->  s3 (2/3),  s4 (1/3)

s2  --a-->  s3 (3/4),  s4 (1/4)
s2  --b-->  s4 (1)

s3  --a-->  goal (2/5),  fail (3/5)
s3  --b-->  goal (1)

s4  --a-->  goal (3/4),  fail (1/4)
s4  --b-->  fail (1)

Returns:

A stormvogel POMDP model.

stormvogel.examples.create_atva20_z0_pomdp() → stormvogel.model.Model

Return the simplified ATVA z0-cluster POMDP.

All three states share observation z0, so the belief over them forms a 2-simplex (triangle). The b action mixes within the cluster; the a action commits to an absorbing goal or fail state with probabilities that differ per state (s1 is the best state, s2 the worst).

Returns:

A stormvogel POMDP model.