stormvogel.visualization

Contains the code responsible for model visualization.

Classes

VisualizationBase

Base class for visualizing a Stormvogel MDP model.

JSVisualization

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

MplVisualization

Matplotlib-based visualization for Stormvogel models.

Functions

_escape_js_template(→ str)

Escape a Python string for safe embedding inside a JS template literal (backticks).

_escape_js_dquote(→ str)

Escape a Python string for safe embedding inside a JS double-quoted string.

Module Contents

stormvogel.visualization._escape_js_template(s: str) str

Escape a Python string for safe embedding inside a JS template literal (backticks).

stormvogel.visualization._escape_js_dquote(s: str) str

Escape a Python string for safe embedding inside a JS double-quoted string.

class stormvogel.visualization.VisualizationBase(model: stormvogel.model.Model, layout: stormvogel.layout.Layout = stormvogel.layout.DEFAULT(), result: stormvogel.result.Result | None = None, scheduler: stormvogel.result.Scheduler | None = None)

Base class for visualizing a Stormvogel MDP model.

This class sets up a visual representation of a Stormvogel model, optionally incorporating the result of a model checking operation and a scheduler (i.e., a strategy for selecting actions). It constructs an internal graph of the model and manages visual layout settings, such as active and possible display groups.

If a scheduler is not explicitly provided but is available in the model checking result, it will be used automatically. When a scheduler is set, the “scheduled_actions” group is activated in the layout; otherwise, it is deactivated.

Parameters:
  • model – The MDP model to visualize.

  • layout – Layout settings for the visualization.

  • result – The result of a model checking operation, which may contain a scheduler.

  • scheduler – An explicit scheduler defining actions to take in each state.

Variables:
  • model – The MDP model being visualized.

  • layout – The layout configuration for the visualization.

  • result – The result of a model checking operation.

  • scheduler – A scheduler representing a path through the model.

  • G – The internal graph structure representing the model.

model
layout
result = None
scheduler = None
static _und(x: str) str

Replace spaces by underscores.

static _random_word(k: int) str

Generate a random word of length k.

static _random_color() str

Return a random HEX color.

static _blend_colors(c1: str, c2: str, factor: float) str

Blend two colors in HEX format (#RRGGBB).

Parameters:
  • c1 – Color 1 in HEX format #RRGGBB.

  • c2 – Color 2 in HEX format #RRGGBB.

  • factor – The fraction of the resulting color that should come from c1.

recreate()

Recreate the ModelGraph and set the edit groups.

_format_number(n: stormvogel.model.Value) str

Format a number using the settings specified in the layout object.

_format_result(s: stormvogel.model.State) str

Create a string that shows the result for this state.

Start with a newline. If results are not enabled, return the empty string.

_format_observations(s: stormvogel.model.State) str

Create a string that shows the observation for this state (for POMDPs).

Start with a newline.

_group_state(s: stormvogel.model.State, default: str) str

Determine the group of a state.

The group is the label of s that has the highest priority, as specified by the user under edit_groups.

_group_action(state: stormvogel.model.State, a: stormvogel.model.Action, default: str) str

Return the group of this action. Only relevant for scheduling.

_format_rewards(s: stormvogel.model.State, a: stormvogel.model.Action) str

Create a string that contains the state reward. Actions no longer have individual rewards.

_create_state_properties(state: stormvogel.model.State) dict

Generate visualization properties for a given state in the model.

Create the visual representation of a state, including its label, group assignment, color (based on model checking results), and other textual annotations like rewards and observations. These properties are used when constructing the ModelGraph for visualization.

If result coloring is enabled and a model checking result is available, the state’s color is interpolated between two configured colors based on the state’s result value relative to the maximum result.

Parameters:

state – The model state for which to generate properties.

Returns:

A dictionary containing the state’s visualization properties with keys "label", "group", and "color".

_create_action_properties(state: stormvogel.model.State, action: stormvogel.model.Action) dict

Generate visualization properties for a given action in the model.

Create a label for the action, optionally including any associated reward, and include the original Action object for use in the visualization or interaction.

Parameters:
  • state – The state from which the action originates.

  • action – The action being evaluated.

Returns:

A dictionary containing the action’s visualization properties with keys "label" and "model_action".

_create_transition_properties(state, action, next_state) dict

Generate visualization properties for a transition between states.

Find the transition probability for a specific state-action-next-state triplet and format it as a label. If the transition exists, the formatted probability is included; otherwise, an empty dictionary is returned.

Parameters:
  • state – The source state of the transition.

  • action – The action taken from the source state.

  • next_state – The target state of the transition.

Returns:

A dictionary containing the transition’s visualization properties.

class stormvogel.visualization.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
initial_state
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.

_STORMVOGEL_LAYOUT_KEYS
_get_options() str

Return the vis.js-compatible layout configuration as a JSON-formatted string.

Strips stormvogel-specific keys so that only recognized vis.js options are forwarded to the network.

Returns:

A pretty-printed JSON string representing the vis.js options.

set_options(options: str) None

Set the layout configuration from a JSON-formatted string.

Replace the current layout with a new one defined by the given JSON string. Call only before visualization is rendered (i.e., before calling show()), as it reinitializes the layout.

Parameters:

options – A JSON-formatted string representing the layout configuration.

generate_html(height: int | str | None = None) str

Generate an HTML page representing the current state of the ModelGraph.

Parameters:

height – Override the layout height. Either an integer (pixels) or a CSS string like "100%". If None, the layout height is used.

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_state: stormvogel.model.State)

Enable exploration mode starting from a specified initial state.

Activate interactive exploration mode in the visualization and set the starting point for exploration to the given state. show() needs to be called after this method to have an effect.

Parameters:

initial_state – The state from which exploration should begin.

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

Get the current positions of the nodes on the canvas.

Returns:

A dict mapping node keys to position dicts, e.g. {"uuid-string": {"x": 5, "y": 10}}. Return empty dict if unsuccessful.

Raises:

TimeoutError – If the server is not initialized or communication times out.

show(hidden: bool = False) None
update() None

Update the visualization with the current layout options.

Send updated layout configuration to the frontend visualization by injecting JavaScript code. Typically used to reflect changes made to layout settings after the initial rendering.

Note

Call this after modifying layout properties if the visualization has already been shown, to apply those changes interactively.

set_node_color(obj: stormvogel.model.State | tuple[stormvogel.model.State, stormvogel.model.Action], color: str | None) None

Set the color of a specific node in the visualization.

Update the visual appearance of a node by changing its color via JavaScript. Only takes effect once the network has been fully loaded in the frontend.

Parameters:
  • obj – The state or (state, action) pair whose node color should be changed.

  • color – The color to apply (e.g., "#ff0000" for red). If None, the node color is reset.

Note

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

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

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

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

Parameters:
  • state – The state to highlight.

  • color – The color to use for highlighting (e.g., "red", "#00ff00").

Raises:

AssertionError – If the state does not exist in the model graph.

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

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

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

Parameters:
  • state – The state from which the action originates.

  • action – The action to highlight.

  • color – The color to use for highlighting.

Raises:

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

highlight_state_set(states: set[stormvogel.model.State], color: str | None = 'blue')

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

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

Parameters:
  • states – A set of states to highlight.

  • color – The color to apply.

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

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

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

Parameters:
  • state_action_set – A set of (state, action) pairs to highlight.

  • color – The color to apply.

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

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

Parameters:
  • decomp – A list of tuples (states, actions).

  • colors – A list of colors for the decompositions. Random colors are picked by default.

clear_highlighting()

Clear all highlighting that is currently active, returning all nodes 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.

Parameters:
  • path – The path to highlight.

  • color – The color that the highlighted states should get (in HTML color standard). Set to None to clear existing highlights on this path.

  • delay – Pause for the specified time before highlighting the next state in the path.

  • clear – Clear the highlighting of a state after it was highlighted. Only works if delay is not None. Particularly useful for highlighting paths with loops.

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

Export the visualization to the preferred output format.

The appropriate file extension will be added automatically.

Parameters:
  • output_format – Desired export format. Supported values (not case-sensitive): "HTML", "IFrame", "PDF", "SVG", "LaTeX".

  • filename – Base name for the exported file.

Raises:

RuntimeError – If the export format is not supported.

class stormvogel.visualization.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.

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

Parameters:
  • model – The model to visualize.

  • layout – Layout configuration for the visualization.

  • result – The result of a model checking operation, which may contain a scheduler.

  • scheduler – Explicit scheduler defining actions to take in each state.

  • title – Title of the visualization figure.

  • interactive – Whether to enable interactive features such as node hover callbacks.

  • hover_node – Callback function invoked when hovering over nodes. Receives parameters (PathCollection, PathCollection, MouseEvent, Axes).

title = ''
interactive = False
hover_node = None
_highlights: dict[stormvogel.model.State | tuple[stormvogel.model.State, stormvogel.model.Action], str]
_edge_highlights: dict[tuple[stormvogel.model.State | tuple[stormvogel.model.State, stormvogel.model.Action], stormvogel.model.State | tuple[stormvogel.model.State, stormvogel.model.Action]], str]
_fig = None
highlight_state(state: stormvogel.model.State, color: str = 'red') None

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

Parameters:
  • state – The state to highlight.

  • color – The color to apply.

Raises:

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

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

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

Parameters:
  • state – The state from which the action originates.

  • action – The action to highlight.

  • color – The color to apply.

Raises:

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

highlight_edge(from_: stormvogel.model.State | tuple[stormvogel.model.State, stormvogel.model.Action], to_: stormvogel.model.State | tuple[stormvogel.model.State, stormvogel.model.Action], color: str = 'red') None

Highlight an edge between two nodes by setting its color.

Parameters:
  • from – The source node of the edge.

  • to – The target node of the edge.

  • color – The color to apply.

clear_highlighting() None

Clear all nodes that are marked for highlighting in the visualization.

highlight_scheduler(scheduler: stormvogel.result.Scheduler) None

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

Apply 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.

Parameters:

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]

Draw the model graph onto a given Matplotlib Axes.

Render nodes and edges of the model graph on the provided Matplotlib ax object. Use layout positions, colors from the current layout configuration, and any highlights applied to nodes or edges.

Parameters:
  • ax – The Matplotlib axes to draw the graph on.

  • node_size – 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.

  • node_kwargs – Additional keyword arguments passed to nx.draw_networkx_nodes().

  • edge_kwargs – Additional keyword arguments passed to nx.draw_networkx_edges().

Returns:

A tuple (nodes, edges) where nodes is the PathCollection of drawn nodes and edges is the 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)

Update or create the Matplotlib figure displaying the model graph.

Set up the figure size based on layout settings, draw the graph nodes and edges using add_to_ax, and apply highlights and titles. If interactive is enabled, connect a hover event handler to update the plot title dynamically when the mouse moves over nodes.

Parameters:
  • node_size – Size(s) for the nodes. Can be a single integer or a dictionary mapping nodes to sizes.

  • node_kwargs – Additional keyword arguments passed to nx.draw_networkx_nodes().

  • edge_kwargs – Additional keyword arguments passed to nx.draw_networkx_edges().

Returns:

The Matplotlib figure object containing the visualization.

show() None