stormvogel.extensions

Submodules

• stormvogel.extensions.ec_elimination
• stormvogel.extensions.gifs
• stormvogel.extensions.gym_grid
• stormvogel.extensions.helpers
• stormvogel.extensions.visual_algos

Attributes

stormpy
GRID_ACTION_LABEL_MAP
stormpy

Functions

choice_mapping(sv_model, sp_model)	Return a bijective mapping between the stormvogel state-action pairs and the stormvogel model.
map_state_labels(m, res)	Based on the result of EC elimination, create a new state labeling that can be used for a new model that captures the result.
map_choice_labels(m_old, m_new, res)	Based on the result of EC elimination, create a new choice labeling that can be used for a new model that captures the result.
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.
render_model_gif(→ str)	Render a stormvogel model to a gif, using the gymnasium_scheduler (A map from state numbers to action numbers) to pick an action.
embed_gif(filename)	Hacky way to embed a gif in a jupyter notebook so that it also works with sphinx docs.
gymnasium_grid_to_stormvogel(env[, action_label_map])	Convert a FrozenLake, Taxi, or Cliffwalking gymnasium environment to an explicit stormvogel model.
to_coordinate(s, env)	Calculate the state's coordinates. Works for FrozenLake, Cliffwalking, and Taxi
to_state(x, y, env)	Calculate the state index from coordinates. Works for FrozenLake, CliffWalking, and Taxi.
get_target_state(env)	Calculate the target state for an env. Works for FrozenLake and Cliffwalking
to_gymnasium_scheduler(→ Callable[[int], int])	Convert a stormvogel scheduler to a gymnasium scheduler (for a model that was converted using gymnasium_grid_to_stormvogel).
gymnasium_render_model_gif(→ str)	Render a gymnasium model to a gif, using the gymnasium_scheduler (A map from state numbers to action numbers) to pick an action.
choice_mapping(sv_model, sp_model)	Return a bijective mapping between the stormvogel state-action pairs and the stormvogel model.
to_bit_vector(state_set, model)
naive_value_iteration(...)	Run naive value iteration. The result is a 2D list where result[n][m] is the probability to be in state m at step n.
dtmc_evolution(→ list[list[float]])	Run DTMC evolution. The result is a 2D list where result[n][m] is the probability to be in state m at step n.
invert_2d_list(→ list[list[Any]])
display_value_iteration_result(res, hor_size, labels)	Display a value iteration results using matplotlib.

Package Contents

stormvogel.extensions.stormpy = None

stormvogel.extensions.choice_mapping(sv_model, sp_model)

Return a bijective mapping between the stormvogel state-action pairs and the stormvogel model. WARNING: This function will be depricated later. It might also be faulty, I don’t know :))

stormvogel.extensions.map_state_labels(m, res)

Based on the result of EC elimination, create a new state labeling that can be used for a new model that captures the result. Args:

m: stormpy model res (EndComponentEliminatorReturnTypeDouble): EC result

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

Based on the result of EC elimination, create a new choice labeling that can be used for a new model that captures the result. Args:

m_old: old stormpy model m_new: new strompy model that is based on res res (EndComponentEliminatorReturnTypeDouble): EC result

stormvogel.extensions.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. Args:

m: stormpy model

stormvogel.extensions.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. They are returned as a list of tuples where the first element is a set of state ids, and the second a set of actions.

stormvogel.extensions.render_model_gif(model: stormvogel.model.Model, state_to_image: Callable[[stormvogel.model.State], PIL.Image.Image], scheduler: stormvogel.result.Scheduler | Callable[[stormvogel.model.State], stormvogel.model.Action] | None = None, path: stormvogel.simulator.Path | None = None, filename: str = 'my_gif', max_length: int = 50, fps: int = 2, loop: int = 0) → str

Render a stormvogel model to a gif, using the gymnasium_scheduler (A map from state numbers to action numbers) to pick an action. Leave as None for a random action.

Args:

model (Model): stormvogel model. state_to_image (Callable[[State], Image]): Function that takes a state and returns an image. scheduler (Scheduler | Callable[[State], Action] | None): Scheduler to use for the simulation. path (Path | None): Path to use for the simulation. If both scheduler and path are set, path takes presedence. filename (str): The gif will be saved as gifs/filename.gif. max_length (int): The maximum amount of steps to simulate. fps (int): The frames per second of the gif. loop (int): The amount of times the gif will loop. 0 means infinite.

stormvogel.extensions.embed_gif(filename: str)

Hacky way to embed a gif in a jupyter notebook so that it also works with sphinx docs.

stormvogel.extensions.GRID_ACTION_LABEL_MAP

stormvogel.extensions.gymnasium_grid_to_stormvogel(env, action_label_map: dict[int, str] = GRID_ACTION_LABEL_MAP)

Convert a FrozenLake, Taxi, or Cliffwalking gymnasium environment to an explicit stormvogel model.

stormvogel.extensions.to_coordinate(s, env)

Calculate the state’s coordinates. Works for FrozenLake, Cliffwalking, and Taxi

stormvogel.extensions.to_state(x, y, env)

Calculate the state index from coordinates. Works for FrozenLake, CliffWalking, and Taxi.

stormvogel.extensions.get_target_state(env)

Calculate the target state for an env. Works for FrozenLake and Cliffwalking

stormvogel.extensions.to_gymnasium_scheduler(model: stormvogel.model.Model, scheduler: stormvogel.result.Scheduler | Callable[[stormvogel.model.State], stormvogel.model.Action], action_label_map: dict[int, str] = GRID_ACTION_LABEL_MAP) → Callable[[int], int]

Convert a stormvogel scheduler to a gymnasium scheduler (for a model that was converted using gymnasium_grid_to_stormvogel). Args:

model: Stormvogel model. scheduler: Stormvogel scheduler. action_label_map: Map that you also used for the call in gymnasium_grid_to_stormvogel.

Returns a gymnasium scheduler.

stormvogel.extensions.gymnasium_render_model_gif(env, gymnasium_scheduler: Callable[[int], int] | None = None, filename: str = 'my_gif', max_length: int = 50, fps: int = 2, loop: int = 0) → str

Render a gymnasium model to a gif, using the gymnasium_scheduler (A map from state numbers to action numbers) to pick an action. Leave as None for a random action.

Args:

env: The gymnasium environment. gymnasium_scheduler: A function that takes a state number and returns an action number. filename: The name of the gif file to save. max_length: The maximum number of frames to render. fps: Frames per second for the gif. loop: Number of times to loop the gif (0 means loop forever).

stormvogel.extensions.stormpy = None

stormvogel.extensions.choice_mapping(sv_model, sp_model)

Return a bijective mapping between the stormvogel state-action pairs and the stormvogel model. WARNING: This function will be depricated later. It might also be faulty, I don’t know :))

stormvogel.extensions.to_bit_vector(state_set: set[int], model: Any)

stormvogel.extensions.naive_value_iteration(model: stormvogel.model.Model, epsilon: float, target_state: stormvogel.model.State) → list[list[stormvogel.model.Number]]

Run naive value iteration. The result is a 2D list where result[n][m] is the probability to be in state m at step n.

Args:

model (stormvogel.model.Model): Target model. steps (int): Amount of steps. target_state (stormvogel.model.State): Target state of the model.

Returns:

list[list[float]]: The result is a 2D list where result[n][m] is the value of state m at iteration n.

stormvogel.extensions.dtmc_evolution(model: stormvogel.model.Model, steps: int) → list[list[float]]

Run DTMC evolution. The result is a 2D list where result[n][m] is the probability to be in state m at step n.

Args:

model (stormvogel.model.Model): Target model. steps (int): Amount of steps.

Returns:

list[list[float]]: The result is a 2D list where result[n][m] is the probability to be in state m at step n.

stormvogel.extensions.invert_2d_list(li: list[list[Any]]) → list[list[Any]]

stormvogel.extensions.display_value_iteration_result(res: list[list[float]], hor_size: int, labels: list[str])

Display a value iteration results using matplotlib.

Args:

res (list[list[float]]): 2D list where result[n][m] is the probability to be in state m at step n. hor_size (int): the horizontal size of the plot, in inches. labels (list[str]): the names of all the states.