stormvogel.extensions.visual_algos

Simple implementations of two model checking algorithms in stormvogel, along with a function to display the workings of the algorithms.

Functions

naive_value_iteration(→ list[list[stormvogel.model.Value]])	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.

Module Contents

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

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.visual_algos.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.visual_algos.invert_2d_list(li: list[list[Any]]) → list[list[Any]]

stormvogel.extensions.visual_algos.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.visual_algos.arg_max(funcs, args)

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

stormvogel.extensions.visual_algos.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.