stormvogel.extensions.ec_elimination

Attributes

stormpy

Functions

map_state_labels(m, res)

Create a new state labeling based on the result of EC elimination.

map_choice_labels(m_old, m_new, res)

Create a new choice labeling based on the result of EC elimination.

simple_ec_elimination(m)

Perform End Component elimination on a stormpy model while preserving labels.

stormvogel_get_maximal_end_components(...)

Get the maximal end components of this model.

choice_mapping(sv_model, sp_model)

Return a bijective mapping between stormvogel state-action pairs and stormpy choice indices.

Module Contents

stormvogel.extensions.ec_elimination.stormpy = None
stormvogel.extensions.ec_elimination.map_state_labels(m, res)

Create a new state labeling based on the result of EC elimination.

Label sets of merged states are unified so the new model preserves all original labels.

Parameters:

  • m – stormpy model.

  • res – EC elimination result.

stormvogel.extensions.ec_elimination.map_choice_labels(m_old, m_new, res)

Create a new choice labeling based on the result of EC elimination.

Action labels are preserved when the number of choices is unchanged.

Parameters:

  • m_old – Old stormpy model.

  • m_new – New stormpy model based on res.

  • res – EC elimination result.

stormvogel.extensions.ec_elimination.simple_ec_elimination(m)

Perform End Component elimination on a stormpy model while preserving labels.

Label sets of merged states are unified. Action labels are preserved when possible.

Parameters:

m – stormpy model.

stormvogel.extensions.ec_elimination.stormvogel_get_maximal_end_components(sv_model: stormvogel.model.Model) → list[Tuple[set[int], set[stormvogel.model.Action]]]

Get the maximal end components of this model.

Return a list of tuples where the first element is a set of states, and the second is a set of actions.

Parameters:

sv_model – Stormvogel model to decompose.

Returns:

List of (states, actions) tuples.

stormvogel.extensions.ec_elimination.choice_mapping(sv_model, sp_model)

Return a bijective mapping between stormvogel state-action pairs and stormpy choice indices.

Warning

This function will be deprecated later. It might also be faulty.

Parameters:

  • sv_model – Stormvogel model.

  • sp_model – Corresponding stormpy model.

Returns:

A bidict mapping (State, Action) to choice index.