stormvogel.teaching.mec¶

Teaching-facing MEC detection/elimination re-exports, plus exhaustive EC enumeration.

The MEC detection and elimination implementations live in stormvogel.stormpy_utils.mec and require stormpy. enumerate_ecs() is pure Python and has no stormpy dependency.

Attributes¶

_EC_CHOICE_THRESHOLD

Classes¶

EndComponent

An end component (EC) of an MDP.

Functions¶

`_state_name`(→ str)
`_reachable`(→ frozenset)
`_is_strongly_connected`(→ bool)
`enumerate_ecs`(→ list[EndComponent])	Return all end components of mdp.

Module Contents¶

stormvogel.teaching.mec._state_name(s: stormvogel.model.state.State) → str¶

class stormvogel.teaching.mec.EndComponent¶

An end component (EC) of an MDP.

Formally, a non-empty set of state-action pairs X ⊆ S × A such that:

Closure: for every (s, a) ∈ X and every s’ with δ(s, a)(s’) > 0, s’ ∈ S’ where S’ = {s | (s, a) ∈ X}.
Strong connectivity: the graph on S’ induced by X is strongly connected.

Parameters:: choices – The state-action pairs comprising this EC, as a frozenset of (State, Action) tuples.

choices: frozenset¶

property states: frozenset¶: The set of states S’ = {s | (s, a) ∈ choices}.

property actions: frozenset¶: The set of distinct actions used across all choices.

satisfies_buchi(target_states) → bool¶

Return True if this EC contains at least one Büchi target state.

Parameters:: target_states – An iterable of State objects that are Büchi states.

__repr__() → str¶

stormvogel.teaching.mec._reachable(start: stormvogel.model.state.State, adj: dict, within: frozenset) → frozenset¶

stormvogel.teaching.mec._is_strongly_connected(states: frozenset, adj: dict) → bool¶

stormvogel.teaching.mec._EC_CHOICE_THRESHOLD = 15¶

stormvogel.teaching.mec.enumerate_ecs(mdp: stormvogel.model.Model) → list[EndComponent]¶

Return all end components of mdp.

Uses an exhaustive bitmask search over all state-action pairs. For each candidate subset X the function checks closure and strong connectivity. The number of subsets is 2^n where n is the total number of state-action pairs (choices) in the MDP — this is only tractable for small teaching examples.

Parameters:: mdp – A stormvogel MDP.
Returns:: All end components as EndComponent objects.