stormvogel.stormpy_utils.mec

MEC detection and elimination for MDPs.

Uses stormpy for the heavy lifting; exposes a stormvogel-native API.

Attributes

stormpy

Functions

_sv_state_name(→ str)

_relabel_actions(→ None)

Restore meaningful action labels on sv_new after MEC elimination.

detect_mecs(→ list[frozenset[stormvogel.model.State]])

Return the maximal end components of mdp as frozensets of stormvogel states.

eliminate_mecs(→ tuple[stormvogel.model.Model, ...)

Eliminate all end components from mdp and return the resulting model.

Module Contents

stormvogel.stormpy_utils.mec.stormpy = None
stormvogel.stormpy_utils.mec._sv_state_name(s: stormvogel.model.State, sp_id: int) → str
stormvogel.stormpy_utils.mec._relabel_actions(sv_new: stormvogel.model.Model, mdp: stormvogel.model.Model, new_id_to_old_sp_ids: dict[int, list[int]], sp_id_to_sv_old: dict[int, stormvogel.model.State]) → None

Restore meaningful action labels on sv_new after MEC elimination.

Pass-through states get their original labels back (matched by position). MEC representatives get exit choices labelled {action}_{origstate} (the textbook $a_s$ notation); the stormpy-added self-loop is labelled stay.

stormvogel.stormpy_utils.mec.detect_mecs(mdp: stormvogel.model.Model) → list[frozenset[stormvogel.model.State]]

Return the maximal end components of mdp as frozensets of stormvogel states.

Each MEC is returned as a frozenset of State objects from the original model. Trivial MECs (single states with a self-loop only) are included.

Parameters:

mdp – A stormvogel MDP.

Returns:

List of MECs, each represented as a frozenset of states.

Raises:

RuntimeError – If stormpy is not available.

stormvogel.stormpy_utils.mec.eliminate_mecs(mdp: stormvogel.model.Model, remove_representative_selfloops: bool = False, make_representatives_absorbing: bool = False) → tuple[stormvogel.model.Model, dict[stormvogel.model.State, stormvogel.model.State]]

Eliminate all end components from mdp and return the resulting model.

Each MEC is collapsed to a single representative state that inherits the union of labels from all states that were merged into it.

Two mutually exclusive post-processing options control how representative states (those produced by merging a non-trivial MEC) are treated:

  • remove_representative_selfloops=True: strip the stormpy-added self-loop from any representative that still has exit actions. Useful for maximum reachability IVI so the upper bound can descend.

  • make_representatives_absorbing=True: strip all exit actions from each representative, leaving only the self-loop. Useful for minimum reachability: the representative becomes a trap (value 0), reflecting that the scheduler can choose to stay in the MEC forever.

Parameters:

  • mdp – A stormvogel MDP.

  • remove_representative_selfloops – Remove self-loop choices from representative states that have at least one exit action.

  • make_representatives_absorbing – Remove all non-self-loop choices from representative states, making them absorbing sinks.

Returns:

A pair (new_mdp, state_map) where state_map maps every state of mdp to its corresponding state in new_mdp.

Raises:

  • RuntimeError – If stormpy is not available.

  • ValueError – If both post-processing options are requested.