stormvogel.extensions

Submodules

• stormvogel.extensions.ec_elimination
• stormvogel.extensions.gifs
• stormvogel.extensions.gym_grid
• stormvogel.extensions.gym_sampling
• 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.
arg_max(funcs, args)	Takes a list of callables and arguments and return the argument that yields the highest value.
policy_iteration(, delay, clear)	Performs policy iteration on the given mdp.
sample_gym(env[, no_samples, sample_length, ...])	Sample the gym environment and convert it to a Stormvogel MDP.

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.

stormvogel.extensions.arg_max(funcs, args)

Takes a list of callables and arguments and return the argument that yields the highest value.

stormvogel.extensions.policy_iteration(model: stormvogel.model.Model, prop: str, visualize: bool = True, layout: stormvogel.layout.Layout = stormvogel.layout.DEFAULT(), delay: int = 2, clear: bool = True) → stormvogel.Result

Performs policy iteration on the given mdp. Args:

model (Model): MDP. prop (str): PRISM property string to maximize. Rembember that this is a property on the induced DTMC, not the MDP. visualize (bool): Whether the intermediate and final results should be visualized. Defaults to True. layout (Layout): Layout to use to show the intermediate results. delay (int): Seconds to wait between each iteration. clear (bool): Whether to clear the visualization of each previous iteration.

stormvogel.extensions.sample_gym(env: gymnasium.Env, no_samples: int = 10, sample_length: int = 20, gymnasium_scheduler: Callable[[Any], int] | None = None, convert_obs: Callable[[Any], Any] = lambda x: ..., max_size: int = 10000)

Sample the gym environment and convert it to a Stormvogel MDP. In reality, gym environments are POMDPs, and gymnasium only allows us to access the observation. The result is an MDP where states with the same observations (and termination) are lumped together. Probablities are frequentist estimates. Their accuracy depends on how often each “state” is visited.

Args:

env (gym.Env): Gymnasium env. no_samples (int): Total number of samples (starting at an initial state).

To resolve multiple initial states, a new, single initial state is added if necessary.

sample_length (int): The maximum length of a single sample. gymnasium_scheduler (Callable[[any], int] | None): A function from states to action numbers. convert_obs (Callable[[any], any]): Converts the observations to a hashable type. You can also apply rounding here.