stormvogel

The stormvogel package

Submodules

• stormvogel.autoscale_svg
• stormvogel.bird
• stormvogel.communication_server
• stormvogel.dict_editor
• stormvogel.displayable
• stormvogel.examples
• stormvogel.extensions
• stormvogel.graph
• stormvogel.html_generation
• stormvogel.layout
• stormvogel.layout_editor
• stormvogel.model
• stormvogel.parametric
• stormvogel.property_builder
• stormvogel.rdict
• stormvogel.result
• stormvogel.show
• stormvogel.simulator
• stormvogel.stormpy_utils
• stormvogel.visualization

Attributes

Number
DEPRECATED_NAMES
Value
EmptyAction
ChoiceShorthand
EmptyAction
stormpy
mdp

Classes

Layout	Create a Layout object that stores the layout and schema.
Interval	represents an interval value for interval models
ModelType	The type of the model.
Observation	Represents an observation of a state (for POMDPs and HMMs)
Action	Represents an action, e.g., in MDPs.
State	Represents a state in a Model.
Branches	Represents branches, which is a distribution over states.
Choices	Represents a choice, which map actions to branches.
RewardModel	Represents a state-exit reward model.
Model	Represents a model.
Scheduler	Scheduler object specifies what action to take in each state.
Result	Result object represents the model checking results for a given model
Layout	Create a Layout object that stores the layout and schema.
JSVisualization	Handles visualization of a Model using a Network from stormvogel.network.
MplVisualization	Matplotlib-based visualization for Stormvogel models.
Path	Path object that represents a path created by a simulator on a certain model.
JSVisualization	Handles visualization of a Model using a Network from stormvogel.network.

Functions

__getattr__(name)
value_to_string(→ str)	Convert a Value to a string.
_to_state_id(→ int)
choice_from_shorthand(...)	Get a Choice object from a ChoiceShorthand. Use for all choices in DTMCs and for empty actions in MDPs.
new_dtmc(→ Model)	Creates a DTMC.
new_mdp(→ Model)	Creates an MDP.
new_ctmc(→ Model)	Creates a CTMC.
new_pomdp(→ Model)	Creates a POMDP.
new_hmm(→ Model)	Creates a HMM.
new_ma(→ Model)	Creates a MA.
new_model(→ Model)	More general model creation function
build_property_string(model)	Lets the user build a property string using a widget.
random_scheduler(→ Scheduler)	Create a random scheduler for the provided model.
DEFAULT()
SV()
show(...)	Create and show a visualization of a Model using a visjs Network
show_bird(→ stormvogel.visualization.JSVisualization)	Show a simple model with a bird state.
get_action_at_state(→ stormvogel.model.Action)	Helper function to obtain the chosen action in a state by a scheduler.
step(→ tuple[int, list[stormvogel.model.Number], ...)	given a state, action and seed we simulate a step and return information on the state we discover
simulate_path(→ Path)	Simulates the model and returns the path created by the process.
simulate(→ stormvogel.model.Model | None)	Simulates the model.
model_checking(→ stormvogel.result.Result | None)	Instead of calling this function, the storm model checker can be used.
is_in_notebook()

Package Contents

class stormvogel.Layout(path: str | None = None, path_relative: bool = True, layout_dict: dict | None = None)

Create a Layout object that stores the layout and schema. Upon creation, the layout and schema dicts are loaded from “layouts/default.json” and “layouts/schema.json”, unless specified otherwise. You can load a custom layout file by setting either path or relative_path, or provide a custom layout dict instead.

Args:

path (str, optional): Path to a custom layout file.

Leave to None for a default layout. Defaults to None.

path_relative (bool, optional): If set to True, then stormvogel will look for a custom layout

file relative to the current working directory. Defaults to True.

layout_dict (dict, optional): If set, this dictionary is used as the layout instead of the

file specified in path. Whenever keys are not present here, their default values from “layouts/default.json” are used.

default_dict: dict

load_schema() → None

Load in the schema. Used for the layout editor. Stored as self.schema.

load(path: str | None = None, path_relative: bool = True) → None

Load the layout and schema file at the specified path. They are stored as self.layout and self.schema respectively.

add_active_group(group: str) → None

The user can specify which groups of states can be edited seperately. We refer to such groups as active groups. Make a group active if it is not already.

remove_active_group(group: str) → None

Make a group inactive if it is not already.

set_possible_groups(groups: set[str]) → None

Set the groups of states that the user can choose to make active, under edit_groups in the layout editor.

save(path: str, path_relative: bool = True) → None

Save this layout as a json file. Raises runtime error if a filename does not end in json, and OSError if file not found.

Args:

path (str): Path to your layout file. path_relative (bool, optional): If set to true, then stormvogel will create a custom layout

file relative to the current working directory. Defaults to True.

set_value(path: list[str], value: Any) → None

Set a value in the layout. Also works if a key in the path does not exist.

__str__() → str

copy_settings() → None

Copy some settings from one place in the layout to another place in the layout. They differ because visjs requires for them to be arranged a certain way which is not nice for an editor.

set_nx_pos(pos: dict[int, numpy.typing.NDArray], scale: float = 500) → Self

Apply NetworkX layout positions to this layout and set physics to false.

Args:

pos (dict[int, NDArray]): A dictionary of node positions from a NetworkX graph. scale (float): Scaling factor for the positions. Defaults to 500.

stormvogel.Number

stormvogel.DEPRECATED_NAMES = [('Choice', 'Choices'), ('Branch', 'Branches')]

stormvogel.__getattr__(name)

class stormvogel.Interval(bottom: Number, top: Number)

represents an interval value for interval models

Args:

bottom: the bottom (left) element of the interval top: the top (right) element of the interval

bottom: Number

top: Number

__getitem__(idx)

__lt__(other)

__str__()

stormvogel.Value

stormvogel.value_to_string(n: Value, use_fractions: bool = True, round_digits: int = 4, denom_limit: int = 1000) → str

Convert a Value to a string.

class stormvogel.ModelType(*args, **kwds)

Bases: enum.Enum

The type of the model.

DTMC = 1

MDP = 2

CTMC = 3

POMDP = 4

MA = 5

HMM = 6

class stormvogel.Observation

Represents an observation of a state (for POMDPs and HMMs)

Args:

observation: the observation of a state as an integer

observation: int

valuations: dict[str, int | float | bool] | None = None

format()

__str__()

stormvogel._to_state_id(state_or_id: State | int) → int

class stormvogel.Action

Represents an action, e.g., in MDPs.

Note that this action object is completely independent of its corresponding branch. Their relation is managed by Choices. Two actions with the same labels are considered equal.

Args:

label: The label of this action. Corresponds to Storm label.

label: str | None

__post_init__()

__lt__(other)

__str__()

stormvogel.EmptyAction

class stormvogel.State(labels: list[str], valuations: dict[str, int | float | bool], id: int, model, observation: Observation | list[tuple[ValueType, Observation]] | None = None, name: str | None = None)

Represents a state in a Model.

Args:

labels: The labels of this state. Corresponds to Storm labels. valuations: The valuations of this state. Corresponds to Storm valuations/features. id: The id of this state. model: The model this state belongs to. observation: the observation of this state in case the model is a POMDP or HMM. name: the name of this state. (unique identifier in case ids change)

labels: list[str]

valuations: dict[str, int | float | bool]

id: int

model: Model[ValueType]

observation: Observation | list[tuple[State.ValueType, Observation]] | None

name: str

add_label(label: str)

adds a new label to the state

set_observation(observation: Observation | list[tuple[ValueType, Observation]]) → Observation | list[tuple[ValueType, Observation]]

sets the observation for this state

get_observation() → Observation | list[tuple[ValueType, Observation]]

gets the observation

set_choice(choice: Choices | ChoiceShorthand)

Set the choice for this state.

add_choice(choices: Choices | ChoiceShorthand)

Add choices to this state.

has_choices() → bool

nr_choices() → int

The number of choices in this state.

get_choice() → Choices | None

get_choices() → Choices | None

Gets the choices of this state.

add_valuation(variable: str, value: int | bool | float)

Adds a valuation to the state.

get_valuation(variable: str) → int | bool | float

available_actions() → list[Action]

returns the list of all available actions in this state

get_outgoing_transitions(action: Action | None = None) → list[tuple[ValueType, State[ValueType]]] | None

gets the outgoing transitions of this state (after a specific action)

is_absorbing() → bool

returns whether the state has a nonzero transition going to another state or not

is_initial()

Returns whether this state is initial.

__str__()

__eq__(other)

__lt__(other)

class stormvogel.Branches(*args)

Represents branches, which is a distribution over states.

Args:

branch: The branch as a list of tuples representing the transitions.

The first element is the probability value and the second element is the target state.

branch: list[tuple[Branches.ValueType, State[Branches.ValueType]]]

get_successors() → set[int]

sort_states()

sorts the branch list by states

__str__()

__eq__(other)

__add__(other)

sum_probabilities() → Number

__iter__()

class stormvogel.Choices(choice: dict[Action, Branches[ValueType]])

Represents a choice, which map actions to branches.

Note that an EmptyAction may be used if we want a non-action choice. Note that a single Choices might correspond to multiple ‘arrows’.

Args:

choice: The choice dictionary. For each available action, we have a branch containing the transitions.

choice: dict[Action, Branches[Choices.ValueType]]

actions() → list[Action]

Returns the actions for the choices

__str__()

has_empty_action() → bool

__eq__(other)

sum_probabilities(action: Action) → Number

is_stochastic(epsilon: Number) → bool

returns whether the probabilities in the branches sum to 1

has_zero_transition() → bool

__getitem__(item)

__iter__()

__len__() → int

stormvogel.ChoiceShorthand

stormvogel.choice_from_shorthand(shorthand: ChoiceShorthand, model: Model[ValueType]) → Choices[choice_from_shorthand.ValueType]

Get a Choice object from a ChoiceShorthand. Use for all choices in DTMCs and for empty actions in MDPs.

There are two possible ways to define a ChoiceShorthand. - using only the probability and the target state (implies default action when in an MDP). - using only the action and the target state (implies probability=1).

class stormvogel.RewardModel(name: str, model: Model, rewards: dict[Tuple[int, Action], ValueType])

Represents a state-exit reward model. Args:

name: Name of the reward model. model: The model this rewardmodel belongs to. rewards: The rewards, the keys state action pairs.

name: str

model: Model

rewards: dict[Tuple[int, Action], RewardModel.ValueType]

Rewards dict. Hashed by state id and Action. The function update_rewards can be called to update rewards. After this, rewards will correspond to intermediate_rewards. Note that in models without actions, EmptyAction will be used here.

set_from_rewards_vector(vector: list[ValueType]) → None

Set the rewards of this model according to a (stormpy) rewards vector.

get_state_reward(state: State) → ValueType | None

Gets the reward at said state or state action pair. Return None if no reward is present.

get_state_action_reward(state: State, action: Action) → ValueType | None

Gets the reward at said state or state action pair. Returns None if no reward was found.

set_state_reward(state: State, value: ValueType)

Sets the reward at said state. If the model has actions, try to use the empty state.

set_state_action_reward(state: State, action: Action, value: ValueType)

sets the reward at said state action pair (in case of models with actions). If you disable auto_update_rewards, you will need to call update_intermediate_to

get_reward_vector() → list[ValueType]

Return the rewards in a (stormpy) vector format.

set_unset_rewards(value: ValueType)

Fills up rewards that were not set yet with the specified value. Use this if converting (to stormpy) doesn’t work because the reward vector does not have the expected length.

__lt__(other) → bool

__eq__(other) → bool

__iter__()

class stormvogel.Model(model_type: ModelType, create_initial_state: bool = True)

Represents a model.

Args:

type: The model type. states: The states of the model. The keys are the state’s ids. choices: The choices of this model. The keys are the state ids. actions: The actions of the model, if this is a model that supports actions. rewards: The rewardsmodels of this model. exit_rates: The exit rates of the model, optional if this model supports rates. markovian_states: list of markovian states in the case of a ma.

type: ModelType

states: dict[int, State[Model.ValueType]]

choices: dict[int, Choices[Model.ValueType]]

actions: set[Action] | None

observations: list[Observation] | None

rewards: list[RewardModel]

exit_rates: dict[int, Model.ValueType] | None

markovian_states: list[State[Model.ValueType]] | None

parametric: bool | None

interval: bool | None

used_names

id_counter = 0

observation_id = 0

summary()

Give a short summary of the model.

get_actions() → set[Action] | None

Return the actions of the model. Returns None if actions are not supported.

supports_actions() → bool

Returns whether this model supports actions.

supports_rates() → bool

Returns whether this model supports rates.

supports_observations() → bool

Returns whether this model supports observations.

iterate_transitions() → list[tuple[ValueType, State]]

iterates through all transitions in all choices of the model

is_interval_model() → bool

Returns whether this model is an interval model, i.e., containts interval values)

is_parametric() → bool

Returns whether this model contains parametric transition values

is_stochastic(epsilon: Number = 1e-06) → bool | None

For discrete models: Checks if all sums of outgoing transition probabilities for all states equal 1, with at most epsilon rounding error. For continuous models: Checks if all sums of outgoing rates sum to 0

normalize()

Normalizes a model (for states where outgoing transition probabilities don’t sum to 1, we divide each probability by the sum)

get_sub_model(states: list[State], normalize: bool = True) → Model

Returns a submodel of the model based on a collection of states. The states in the collection are the states that stay in the model.

parameter_valuation(values: dict[str, Number]) → Model

evaluates all parametric transitions with the given values and returns the induced model

get_choice_id(state: State[ValueType], action: Action) → int | None

We calculate the appropriate choice id for a given state and action. This choice id corresponds to the row of the matrix in the underlying matrix.

get_state_action_id(state: State[ValueType], action: Action) → int | None

get_state_action_pair(id: int) → tuple[State[ValueType], Action] | None

Given an state action id, we return the corresponding state action pair Each state action pair corresponds to an id (which also corresponds to the row of the matrix).

add_self_loops()

adds self loops to all states that do not have an outgoing transition

add_valuation_at_remaining_states(variables: list[str] | None = None, value: int | bool | float = 0)

sets (dummy) value to variables in all states where they don’t have a value yet

unassigned_variables() → list[tuple[State[ValueType], str]]

we return a list of tuples of state variable pairs that are unassigned

all_states_outgoing_transition() → bool

checks if all states have a choice

all_non_init_states_incoming_transition() → bool

checks if all states except the initial state have an incoming transition

has_zero_transition() → bool

checks if the model has transitions with probability zero

add_markovian_state(markovian_state: State)

adds a state to the markovian states (in case of markov automatas)

set_choice(s: State, choices: Choices[ValueType] | ChoiceShorthand) → None

Set the choice for a state.

add_choice(s: State, choices: Choices[ValueType] | ChoiceShorthand) → None

Add new choices from a state to the model. If no choice currently exists, the result will be the same as set_choice.

get_successor_states(state_or_id: State[ValueType] | int) → set[int]

Returns the set of successors of state_or_id.

get_choices(state_or_id: State[ValueType] | int) → Choices[ValueType]

Get the choices at state s. Throws a KeyError if not present.

get_choice(state_or_id: State[ValueType] | int) → Choices[ValueType]

get_branches(state_or_id: State | int) → Branches[ValueType]

Get the branch at state s. Only intended for emtpy choices, otherwise a RuntimeError is thrown.

get_branch(state_or_id: State[ValueType] | int) → Branches[ValueType]

Get the branch at state s. Only intended for emtpy choices, otherwise a RuntimeError is thrown.

get_action_with_label(label: str | None) → Action | None

Get the action with provided label

reassign_ids()

Reassigns the ids of states, choices and rates to be in order again. Mainly useful to keep consistent with storm.

remove_state(state: State, normalize: bool = True, reassign_ids: bool = False)

Properly removes a state, it can optionally normalize the model and reassign ids automatically.

remove_transitions_between_states(state0: State, state1: State, normalize: bool = True)

Remove the transition(s) that start in state0 and go to state1. Only works on models that don’t support actions.

new_action(label: str | None = None) → Action

Creates a new action and returns it.

get_action(name: str) → Action

Gets an existing action.

action(label: str | None) → Action

New action or get action if it exists.

new_observation(valuations: dict[str, int | float | bool] | None = None, observation_id: int | None = None) → Observation

get_observation(observation_id: int) → Observation | None

observation(observation_id: int | None = None, valuations: dict[str, int | float | bool] | None = None) → Observation

New observation or get observation if it exists.

new_state(labels: list[str] | str | None = None, valuations: dict[str, int | bool | float] | None = None, observation: Observation | list[tuple[ValueType, Observation]] | None = None, name: str | None = None) → State[ValueType]

Creates a new state and returns it.

has_only_number_values() → bool

Checks whether all transition values, observation probabilities, exit rates, markovian states in this model are numbers.

make_observations_deterministic(reassign_ids: bool = False)

In case of POMDPs or HMMs, makes the observations deterministic by splitting states with multiple observations into multiple states with single observations.

get_states_with_label(label: str) → list[State]

Get all states with a given label.

get_state_by_id(state_id: int) → State

Get a state by its id.

get_state_by_name(state_name) → State | None

Get a state by its name.

get_initial_state() → State

Gets the initial state (contains label “init”, or has id 0).

get_ordered_labels() → list[list[str]]

Get all the labels of this model, ordered by id. IMPORTANT: If a state has no label, then a value ‘’ is inserted!

get_labels() → set[str]

Get all labels in states of this Model.

get_variables() → set[str]

gets the set of all variables present in this model (corresponding to valuations

get_default_rewards() → RewardModel

Gets the default reward model, throws a RuntimeError if there is none.

get_rewards(name: str) → RewardModel

Gets the reward model with the specified name. Throws a RuntimeError if said model does not exist.

get_parameters() → set[str]

Returns the set of parameters of this model

get_states() → list[State]

new_reward_model(name: str) → RewardModel

Creates a reward model with the specified name, adds it and returns it.

get_rate(state: State) → ValueType

Gets the rate of a state.

set_rate(state: State, rate: ValueType)

Sets the rate of a state.

get_type() → ModelType

Gets the type of this model

property nr_states: int

Returns the number of states in this model. Note that not all states need to be reachable.

property nr_choices: int

Returns the number of choices in the model (summed over all states).

to_dot() → str

Generates a dot representation of this model.

__str__() → str

__eq__(other) → bool

__getitem__(state_id: int)

__iter__()

stormvogel.new_dtmc(create_initial_state: bool = True) → Model

Creates a DTMC.

stormvogel.new_mdp(create_initial_state: bool = True) → Model

Creates an MDP.

stormvogel.new_ctmc(create_initial_state: bool = True) → Model

Creates a CTMC.

stormvogel.new_pomdp(create_initial_state: bool = True) → Model

Creates a POMDP.

stormvogel.new_hmm(create_initial_state: bool = True) → Model

Creates a HMM.

stormvogel.new_ma(create_initial_state: bool = True) → Model

Creates a MA.

stormvogel.new_model(modeltype: ModelType, create_initial_state: bool = True) → Model

More general model creation function

stormvogel.build_property_string(model: stormvogel.model.Model)

Lets the user build a property string using a widget.

class stormvogel.Scheduler(model: stormvogel.model.Model, taken_actions: dict[int, stormvogel.model.Action])

Scheduler object specifies what action to take in each state. All schedulers are nondeterminstic and memoryless.

Args:

model: model associated with the scheduler (has to support actions). taken_actions: for each state the action we choose in that state.

model: stormvogel.model.Model

taken_actions: dict[int, stormvogel.model.Action]

get_action_at_state(state: stormvogel.model.State | int) → stormvogel.model.Action

returns the action in the scheduler for the given state if present in the model

generate_induced_dtmc() → stormvogel.model.Model | None

This function resolves the nondeterminacy of the mdp and returns the scheduler induced dtmc

__str__() → str

__eq__(other) → bool

stormvogel.random_scheduler(model: stormvogel.model.Model) → Scheduler

Create a random scheduler for the provided model.

class stormvogel.Result(model: stormvogel.model.Model, values: dict[int, stormvogel.model.Value], scheduler: Scheduler | None = None)

Result object represents the model checking results for a given model

Args:

model: stormvogel representation of the model associated with the results values: for each state the model checking result scheduler: in case the model is an mdp we can optionally store a scheduler

model: stormvogel.model.Model

values: dict[int, stormvogel.model.Value]

scheduler: Scheduler | None

get_result_of_state(state: stormvogel.model.State | int) → stormvogel.model.Value | None

returns the model checking result for a given state

__str__() → str

maximum_result() → stormvogel.model.Value

Return the maximum result.

__eq__(other) → bool

__iter__()

class stormvogel.Layout(path: str | None = None, path_relative: bool = True, layout_dict: dict | None = None)

Create a Layout object that stores the layout and schema. Upon creation, the layout and schema dicts are loaded from “layouts/default.json” and “layouts/schema.json”, unless specified otherwise. You can load a custom layout file by setting either path or relative_path, or provide a custom layout dict instead.

Args:

path (str, optional): Path to a custom layout file.

Leave to None for a default layout. Defaults to None.

path_relative (bool, optional): If set to True, then stormvogel will look for a custom layout

file relative to the current working directory. Defaults to True.

layout_dict (dict, optional): If set, this dictionary is used as the layout instead of the

file specified in path. Whenever keys are not present here, their default values from “layouts/default.json” are used.

default_dict: dict

load_schema() → None

Load in the schema. Used for the layout editor. Stored as self.schema.

load(path: str | None = None, path_relative: bool = True) → None

Load the layout and schema file at the specified path. They are stored as self.layout and self.schema respectively.

add_active_group(group: str) → None

The user can specify which groups of states can be edited seperately. We refer to such groups as active groups. Make a group active if it is not already.

remove_active_group(group: str) → None

Make a group inactive if it is not already.

set_possible_groups(groups: set[str]) → None

Set the groups of states that the user can choose to make active, under edit_groups in the layout editor.

save(path: str, path_relative: bool = True) → None

Save this layout as a json file. Raises runtime error if a filename does not end in json, and OSError if file not found.

Args:

path (str): Path to your layout file. path_relative (bool, optional): If set to true, then stormvogel will create a custom layout

file relative to the current working directory. Defaults to True.

set_value(path: list[str], value: Any) → None

Set a value in the layout. Also works if a key in the path does not exist.

__str__() → str

copy_settings() → None

Copy some settings from one place in the layout to another place in the layout. They differ because visjs requires for them to be arranged a certain way which is not nice for an editor.

set_nx_pos(pos: dict[int, numpy.typing.NDArray], scale: float = 500) → Self

Apply NetworkX layout positions to this layout and set physics to false.

Args:

pos (dict[int, NDArray]): A dictionary of node positions from a NetworkX graph. scale (float): Scaling factor for the positions. Defaults to 500.

stormvogel.DEFAULT()

stormvogel.SV()

class stormvogel.JSVisualization(model: stormvogel.model.Model, name: str | None = None, result: stormvogel.result.Result | None = None, scheduler: stormvogel.result.Scheduler | None = None, layout: stormvogel.layout.Layout = stormvogel.layout.DEFAULT(), output: ipywidgets.Output | None = None, debug_output: ipywidgets.Output | None = None, use_iframe: bool = False, do_init_server: bool = True, max_states: int = 1000, max_physics_states: int = 500)

Bases: VisualizationBase

Handles visualization of a Model using a Network from stormvogel.network.

EXTRA_PIXELS: int = 20

name: str = ''

use_iframe: bool = False

max_states: int = 1000

max_physics_states: int = 500

do_init_server: bool = True

network_wrapper: str = ''

new_nodes_hidden: bool = False

_generate_node_js() → str

Generate the required js script for node definition

_generate_edge_js() → str

Generate the required js script for edge definition

_get_options() → str

Returns the current layout configuration as a JSON-formatted string.

This method serializes the layout dictionary used for visualization into a readable JSON format with indentation for clarity.

Returns:

str: A pretty-printed JSON string representing the current layout configuration.

set_options(options: str) → None

Sets the layout configuration from a JSON-formatted string.

This method replaces the current layout with a new one defined by the given JSON string. It should be called only before visualization is rendered (i.e., before calling show()), as it reinitializes the layout.

Args:

options (str): A JSON-formatted string representing the layout configuration.

generate_html() → str

Generate an html page representing the current state of the ModelGraph

generate_iframe() → str

Generate an iframe for the network, using the html.

generate_svg(width: int = 800) → str

Generate an svg rendering for the network.

enable_exploration_mode(initial_node_id: int)

Enables exploration mode starting from a specified initial state.

This method activates interactive exploration mode in the visualization and sets the starting point for exploration to the given state ID. show() needs to be called after this method is executed to have an effect.

Args:

initial_node_id (int): The ID of the state from which exploration should begin.

get_positions() → dict[int, dict[str, int]]

Get the current positions of the nodes on the canvas. Returns empty dict if unsuccessful. Example result: {0: {“x”: 5, “y”: 10}}

show(hidden: bool = False) → None

update() → None

Updates the visualization with the current layout options.

This method sends updated layout configuration to the frontend visualization by injecting JavaScript code. It is typically used to reflect changes made to layout settings after the initial rendering.

Note:

This should be called after modifying layout properties if the visualization has already been shown, to apply those changes interactively.

set_node_color(node_id: int, color: str | None) → None

Sets the color of a specific node in the visualization.

This method updates the visual appearance of a node by changing its color via JavaScript. It only takes effect once the network has been fully loaded in the frontend.

Args:

node_id (int): The ID of the node whose color should be changed. color (str | None): The color to apply (e.g., “#ff0000” for red).

If None, the node color is reset or cleared.

Note:

This function requires that the visualization is already rendered (i.e., show() has been called and completed asynchronously).

highlight_state(state_id: int, color: str | None = 'red')

Highlights a single state in the model by changing its color.

This method changes the color of the specified state node in the visualization. Pass None to reset or clear the highlight.

Args:

state_id (int): The ID of the state to highlight. color (str | None, optional): The color to use for highlighting (e.g., “red”, “#00ff00”).

Defaults to “red”.

Raises:

AssertionError: If the state ID does not exist in the model graph.

highlight_action(state_id: int, action: stormvogel.model.Action, color: str | None = 'red')

Highlights a single action in the model by changing its color.

This method changes the color of the node representing a specific action taken from a given state. Pass None to remove the highlight.

Args:

state_id (int): The ID of the state from which the action originates. action (stormvogel.model.Action): The action to highlight. color (str | None, optional): The color to use for highlighting. Defaults to “red”.

Warns:

UserWarning: If the specified (state, action) pair is not found in the model graph.

highlight_state_set(state_ids: set[int], color: str | None = 'blue')

Highlights a set of states in the model by changing their color.

Iterates over each state ID in the provided set and applies the given color. Pass None to clear highlighting for all specified states.

Args:

state_ids (set[int]): A set of state IDs to highlight. color (str | None, optional): The color to apply. Defaults to “blue”.

highlight_action_set(state_action_set: set[tuple[int, stormvogel.model.Action]], color: str = 'red')

Highlights a set of actions in the model by changing their color.

Applies the specified color to all (state, action) pairs in the given set. Pass None as the color to clear the current highlighting.

Args:

state_action_set (set[tuple[int, stormvogel.model.Action]]): A set of

(state ID, action) pairs to highlight.

color (str, optional): The color to apply. Defaults to “red”.

highlight_decomposition(decomp: list[tuple[set[int], set[tuple[int, stormvogel.model.Action]]]], colors: list[str] | None = None)

Highlight a set of tuples of (states and actions) in the model by changing their color. Args:

decomp: A list of tuples (states, actions) colors (optional): A list of colors for the decompositions. Random colors are picked by default.

clear_highlighting()

Clear all highlighting that is currently active, returning all states to their original colors.

highlight_path(path: stormvogel.simulator.Path, color: str, delay: float = 1, clear: bool = True) → None

Highlight the path that is provided as an argument in the model. Args:

path (simulator.Path): The path to highlight. color (str | None): The color that the highlighted states should get (in HTML color standard).

Set to None, in order to clear existing highlights on this path.

delay (float): If not None, there will be a pause of a specified time before highlighting the next state in the path. clear (bool): Clear the highlighting of a state after it was highlighted. Only works if delay is not None.

This is particularly useful for highlighting paths with loops.

export(output_format: str, filename: str = 'export') → None

Export the visualization to your preferred output format. The appropriate file extension will be added automatically.

Parameters:

output_format (str): Desired export format. filename (str): Base name for the exported file.

Supported output formats (not case-sensitive):

“HTML” → An interactive .html file (e.g., draggable nodes) “IFrame” → Exports as an <iframe> wrapped HTML in a .html file “PDF” → Exports to .pdf (via conversion from SVG) “SVG” → Exports to .svg vector image

class stormvogel.MplVisualization(model: stormvogel.model.Model, layout: stormvogel.layout.Layout = stormvogel.layout.DEFAULT(), result: stormvogel.result.Result | None = None, scheduler: stormvogel.result.Scheduler | None = None, title: str | None = None, interactive: bool = False, hover_node: collections.abc.Callable[[matplotlib.collections.PathCollection, matplotlib.collections.PathCollection, matplotlib.backend_bases.MouseEvent, matplotlib.axes.Axes], None] | None = None)

Bases: VisualizationBase

Matplotlib-based visualization for Stormvogel models.

Extends the base visualization class to render the model, results, and scheduler using Matplotlib. Supports interactive features like node highlighting and custom hover behavior.

This class manages figure creation, state and edge highlighting, and optionally allows interaction callbacks when hovering over nodes.

Args:

model (stormvogel.model.Model): The model to visualize. layout (stormvogel.layout.Layout, optional): Layout configuration for

the visualization. Defaults to stormvogel.layout.DEFAULT().

result (stormvogel.result.Result | None, optional): The result of a model

checking operation, which may contain a scheduler. Defaults to None.

scheduler (stormvogel.result.Scheduler | None, optional): Explicit scheduler

defining actions to take in each state. Defaults to None.

title (str | None, optional): Title of the visualization figure. Defaults to None. interactive (bool, optional): Whether to enable interactive features such

as node hover callbacks. Defaults to False.

hover_node (Callable | None, optional): Callback function invoked when

hovering over nodes. Receives parameters (PathCollection, PathCollection, MouseEvent, Axes). Defaults to None.

title = ''

interactive = False

hover_node = None

_highlights: dict[int, str]

_edge_highlights: dict[tuple[int, int], str]

_fig = None

highlight_state(state: stormvogel.model.State | int, color: str = 'red') → None

Highlights a state node in the visualization by setting its color.

Args:

state (stormvogel.model.State | int): The state object or state ID to highlight. color (str, optional): The color to apply. Defaults to “red”.

Raises:

AssertionError: If the state node is not present in the model graph.

highlight_action(state: stormvogel.model.State | int, action: stormvogel.model.Action, color: str = 'red') → None

Highlights an action node associated with a state by setting its color.

Args:

state (stormvogel.model.State | int): The state object or state ID from which the action originates. action (stormvogel.model.Action): The action to highlight. color (str, optional): The color to apply. Defaults to “red”.

Raises:

AssertionError: If the state node is not present in the model graph.

highlight_edge(from_: int, to_: int, color: str = 'red') → None

Highlights an edge between two nodes by setting its color.

Args:

from_ (int): The source node ID of the edge. to_ (int): The target node ID of the edge. color (str, optional): The color to apply. Defaults to “red”.

clear_highlighting() → None

Clear all nodes that are marked for highlighting in the visualization

highlight_scheduler(scheduler: stormvogel.result.Scheduler) → None

Highlights states, actions, and edges according to the given scheduler.

Applies a specific highlight color defined by the layout to all states and actions specified by the scheduler’s taken actions, as well as the edges connecting them. The color is derived from the layout’s configured group colors for scheduled actions.

Args:

scheduler (stormvogel.result.Scheduler): The scheduler containing

state-action mappings to highlight.

add_to_ax(ax, node_size: int | dict[int, int] = 300, node_kwargs: dict[str, Any] | None = None, edge_kwargs: dict[str, Any] | None = None) → tuple[Any, Any]

Draws the model graph onto a given Matplotlib Axes.

This method renders nodes and edges of the model graph on the provided Matplotlib ax object. It uses layout positions, colors from the current layout configuration, and any highlights applied to nodes or edges. Node sizes can be specified either as a fixed integer or as a dictionary mapping node IDs to sizes.

Args:

ax (matplotlib.axes.Axes): The Matplotlib axes to draw the graph on. node_size (int or dict[int, int], optional): Size(s) of nodes. If an

int is given, all nodes are drawn with that size. If a dictionary, it must provide sizes for all nodes. Defaults to 300.

node_kwargs (dict[str, Any], optional): Additional keyword arguments

passed to nx.draw_networkx_nodes(). Defaults to None.

edge_kwargs (dict[str, Any], optional): Additional keyword arguments

passed to nx.draw_networkx_edges(). Defaults to None.

Returns:

tuple: A tuple (nodes, edges) where nodes is the

matplotlib.collections.PathCollection of drawn nodes and edges is the matplotlib.collections.LineCollection of drawn edges.

update(node_size: int | dict[int, int] = 300, node_kwargs: dict[str, Any] | None = None, edge_kwargs: dict[str, Any] | None = None)

Updates or creates the Matplotlib figure displaying the model graph.

This method sets up the figure size based on layout settings, draws the graph nodes and edges using add_to_ax, and applies highlights and titles. If interactive is enabled, it connects a hover event handler to update the plot title dynamically when the mouse moves over nodes.

Args:

node_size (int or Sequence[int], optional): Size(s) for the nodes. Can be

a single integer or a sequence of sizes for each node. Defaults to 300.

node_kwargs (dict[str, Any], optional): Additional keyword arguments

passed to nx.draw_networkx_nodes(). Defaults to None.

edge_kwargs (dict[str, Any], optional): Additional keyword arguments

passed to nx.draw_networkx_edges(). Defaults to None.

Returns:

matplotlib.figure.Figure: The Matplotlib figure object containing the visualization.

show() → None

stormvogel.show(model: stormvogel.model.Model, result: stormvogel.result.Result | None = None, engine: str = 'js', pos_function: Callable[[stormvogel.graph.ModelGraph], dict[int, Any]] | None = None, pos_function_scaling: int = 750, scheduler: stormvogel.result.Scheduler | None = None, layout: stormvogel.layout.Layout | None = None, show_editor: bool = False, debug_output: ipywidgets.Output | None = None, use_iframe: bool = False, do_init_server: bool = True, max_states: int = 1000, max_physics_states: int = 500) → stormvogel.visualization.JSVisualization | stormvogel.visualization.MplVisualization | None

Create and show a visualization of a Model using a visjs Network

Args:

model (Model): The stormvogel model to be displayed. engine (str): The engine that should be used for the visualization.

Can be either “js” for the interactive html/JavaScript visualization, or “mpl” for matplotlib.

pos_function (Callable | None): Function that takes a ModelGraph and maps it to a dictionary of node positions.

It is often useful to import these from networkx, see https://networkx.org/documentation/stable/_modules/networkx/drawing/layout.html for some examples. In particular, nx.nx.bfs_layout seems to work great for models with a directed acyclic graph structure. Defaults to None.

pos_function_scaling (int): Scaling factor for the positions when using networkx positions. Defaults to 500. result (Result, optional): A result associatied with the model.

The results are displayed as numbers on a state. Enable the layout editor for options. If this result has a scheduler, then the scheduled actions will have a different color etc. based on the layout

scheduler (Scheduler, optional): The scheduled actions will have a different color etc. based on the layout

If both result and scheduler are set, then scheduler takes precedence.

layout (Layout): Layout used for the visualization. show_editor (bool): For interactive visualizaiton. Show an interactive layout editor. debug_output (widgets.Output): For interactive visualization. Output widget that can be used to debug interactive features. use_iframe(bool): For interactive visualziation. Wrap the generated html inside of an IFrame.

In some environments, the visualization works better with this enabled.

do_init_server(bool): For interactive visualization. Initialize a local server that is used for communication between Javascript and Python.

If this is set to False, then exporting network node positions and svg/pdf/latex is impossible.

max_states (int): If the model has more states, then the network is not displayed. max_physics_states (int): If the model has more states, then physics are disabled.

Returns:

JSVisualization or MlpVisualzition object.

stormvogel.show_bird() → stormvogel.visualization.JSVisualization

Show a simple model with a bird state.

stormvogel.EmptyAction

class stormvogel.Path(path: list[tuple[stormvogel.model.Action, stormvogel.model.State]] | list[stormvogel.model.State], model: stormvogel.model.Model)

Path object that represents a path created by a simulator on a certain model.

Args:

path: The path itself is a dictionary where we either store for each step a state or a state action pair, depending on if we are working with a dtmc or an mdp. model: model that the path traverses through

path: list[tuple[stormvogel.model.Action, stormvogel.model.State]] | list[stormvogel.model.State]

model: stormvogel.model.Model

get_state_in_step(step: int) → stormvogel.model.State | None

returns the state discovered in the given step in the path

get_action_in_step(step: int) → stormvogel.model.Action | None

returns the action discovered in the given step in the path

get_step(step: int) → tuple[stormvogel.model.Action, stormvogel.model.State] | stormvogel.model.State

returns the state or state action pair discovered in the given step

to_state_action_sequence() → list[stormvogel.model.Action | stormvogel.model.State]

Convert a Path to a list containing actions and states.

__str__() → str

__eq__(other)

__len__()

stormvogel.get_action_at_state(state: stormvogel.model.State, scheduler: stormvogel.result.Scheduler | Callable[[stormvogel.model.State], stormvogel.model.Action]) → stormvogel.model.Action

Helper function to obtain the chosen action in a state by a scheduler.

stormvogel.step(state: stormvogel.model.State, action: stormvogel.model.Action | None = None, seed: int | None = None) → tuple[int, list[stormvogel.model.Number], list[str]]

given a state, action and seed we simulate a step and return information on the state we discover

stormvogel.simulate_path(model: stormvogel.model.Model, steps: int = 1, scheduler: stormvogel.result.Scheduler | Callable[[stormvogel.model.State], stormvogel.model.Action] | None = None, seed: int | None = None) → Path

Simulates the model and returns the path created by the process. Args:

model: The stormvogel model that the simulator should run on. steps: The number of steps the simulator walks through the model. scheduler: A stormvogel scheduler to determine what actions should be taken. Random if not provided.

(instead of a stormvogel scheduler, a function from states to actions can also be provided.)

seed: The seed for the function that determines for each state what the next state will be. Random seed if not provided.

Returns a path object.

stormvogel.simulate(model: stormvogel.model.Model, steps: int = 1, runs: int = 1, scheduler: stormvogel.result.Scheduler | Callable[[stormvogel.model.State], stormvogel.model.Action] | None = None, seed: int | None = None) → stormvogel.model.Model | None

Simulates the model. Args:

model: The stormvogel model that the simulator should run on steps: The number of steps the simulator walks through the model runs: The number of times the model gets simulated. scheduler: A stormvogel scheduler to determine what actions should be taken. Random if not provided.

(instead of a stormvogel scheduler, a function from states to actions can also be provided.)

seed: The seed for the function that determines for each state what the next state will be. Random seed if not provided.

Returns the partial model discovered by all the runs of the simulator together

class stormvogel.JSVisualization(model: stormvogel.model.Model, name: str | None = None, result: stormvogel.result.Result | None = None, scheduler: stormvogel.result.Scheduler | None = None, layout: stormvogel.layout.Layout = stormvogel.layout.DEFAULT(), output: ipywidgets.Output | None = None, debug_output: ipywidgets.Output | None = None, use_iframe: bool = False, do_init_server: bool = True, max_states: int = 1000, max_physics_states: int = 500)

Bases: VisualizationBase

Handles visualization of a Model using a Network from stormvogel.network.

EXTRA_PIXELS: int = 20

name: str = ''

use_iframe: bool = False

max_states: int = 1000

max_physics_states: int = 500

do_init_server: bool = True

network_wrapper: str = ''

new_nodes_hidden: bool = False

_generate_node_js() → str

Generate the required js script for node definition

_generate_edge_js() → str

Generate the required js script for edge definition

_get_options() → str

Returns the current layout configuration as a JSON-formatted string.

This method serializes the layout dictionary used for visualization into a readable JSON format with indentation for clarity.

Returns:

str: A pretty-printed JSON string representing the current layout configuration.

set_options(options: str) → None

Sets the layout configuration from a JSON-formatted string.

This method replaces the current layout with a new one defined by the given JSON string. It should be called only before visualization is rendered (i.e., before calling show()), as it reinitializes the layout.

Args:

options (str): A JSON-formatted string representing the layout configuration.

generate_html() → str

Generate an html page representing the current state of the ModelGraph

generate_iframe() → str

Generate an iframe for the network, using the html.

generate_svg(width: int = 800) → str

Generate an svg rendering for the network.

enable_exploration_mode(initial_node_id: int)

Enables exploration mode starting from a specified initial state.

This method activates interactive exploration mode in the visualization and sets the starting point for exploration to the given state ID. show() needs to be called after this method is executed to have an effect.

Args:

initial_node_id (int): The ID of the state from which exploration should begin.

get_positions() → dict[int, dict[str, int]]

Get the current positions of the nodes on the canvas. Returns empty dict if unsuccessful. Example result: {0: {“x”: 5, “y”: 10}}

show(hidden: bool = False) → None

update() → None

Updates the visualization with the current layout options.

This method sends updated layout configuration to the frontend visualization by injecting JavaScript code. It is typically used to reflect changes made to layout settings after the initial rendering.

Note:

This should be called after modifying layout properties if the visualization has already been shown, to apply those changes interactively.

set_node_color(node_id: int, color: str | None) → None

Sets the color of a specific node in the visualization.

This method updates the visual appearance of a node by changing its color via JavaScript. It only takes effect once the network has been fully loaded in the frontend.

Args:

node_id (int): The ID of the node whose color should be changed. color (str | None): The color to apply (e.g., “#ff0000” for red).

If None, the node color is reset or cleared.

Note:

This function requires that the visualization is already rendered (i.e., show() has been called and completed asynchronously).

highlight_state(state_id: int, color: str | None = 'red')

Highlights a single state in the model by changing its color.

This method changes the color of the specified state node in the visualization. Pass None to reset or clear the highlight.

Args:

state_id (int): The ID of the state to highlight. color (str | None, optional): The color to use for highlighting (e.g., “red”, “#00ff00”).

Defaults to “red”.

Raises:

AssertionError: If the state ID does not exist in the model graph.

highlight_action(state_id: int, action: stormvogel.model.Action, color: str | None = 'red')

Highlights a single action in the model by changing its color.

This method changes the color of the node representing a specific action taken from a given state. Pass None to remove the highlight.

Args:

state_id (int): The ID of the state from which the action originates. action (stormvogel.model.Action): The action to highlight. color (str | None, optional): The color to use for highlighting. Defaults to “red”.

Warns:

UserWarning: If the specified (state, action) pair is not found in the model graph.

highlight_state_set(state_ids: set[int], color: str | None = 'blue')

Highlights a set of states in the model by changing their color.

Iterates over each state ID in the provided set and applies the given color. Pass None to clear highlighting for all specified states.

Args:

state_ids (set[int]): A set of state IDs to highlight. color (str | None, optional): The color to apply. Defaults to “blue”.

highlight_action_set(state_action_set: set[tuple[int, stormvogel.model.Action]], color: str = 'red')

Highlights a set of actions in the model by changing their color.

Applies the specified color to all (state, action) pairs in the given set. Pass None as the color to clear the current highlighting.

Args:

state_action_set (set[tuple[int, stormvogel.model.Action]]): A set of

(state ID, action) pairs to highlight.

color (str, optional): The color to apply. Defaults to “red”.

highlight_decomposition(decomp: list[tuple[set[int], set[tuple[int, stormvogel.model.Action]]]], colors: list[str] | None = None)

Highlight a set of tuples of (states and actions) in the model by changing their color. Args:

decomp: A list of tuples (states, actions) colors (optional): A list of colors for the decompositions. Random colors are picked by default.

clear_highlighting()

Clear all highlighting that is currently active, returning all states to their original colors.

highlight_path(path: stormvogel.simulator.Path, color: str, delay: float = 1, clear: bool = True) → None

Highlight the path that is provided as an argument in the model. Args:

path (simulator.Path): The path to highlight. color (str | None): The color that the highlighted states should get (in HTML color standard).

Set to None, in order to clear existing highlights on this path.

delay (float): If not None, there will be a pause of a specified time before highlighting the next state in the path. clear (bool): Clear the highlighting of a state after it was highlighted. Only works if delay is not None.

This is particularly useful for highlighting paths with loops.

export(output_format: str, filename: str = 'export') → None

Export the visualization to your preferred output format. The appropriate file extension will be added automatically.

Parameters:

output_format (str): Desired export format. filename (str): Base name for the exported file.

Supported output formats (not case-sensitive):

“HTML” → An interactive .html file (e.g., draggable nodes) “IFrame” → Exports as an <iframe> wrapped HTML in a .html file “PDF” → Exports to .pdf (via conversion from SVG) “SVG” → Exports to .svg vector image

stormvogel.stormpy = None

stormvogel.model_checking(model: stormvogel.model.Model, prop: str | None = None, scheduler: bool = True) → stormvogel.result.Result | None

Instead of calling this function, the storm model checker can be used. In order to to that, convert this model using the mapping and then do storm model checking. After that, map it back.

This function just performs this procedure automatically.

stormvogel.mdp

stormvogel.is_in_notebook()