stormvogel¶

The stormvogel package

Attributes¶

`EmptyAction`
`ChoicesShorthand`
`Number`
`Value`
`VariableDomain`
`VariableKey`

Classes¶

`Layout`	Store the layout and schema for a visualization.
`Action`	Represent an action, e.g., in MDPs.
`Choices`	Represent a choice, which maps actions to branches.
`Distribution`	A sparse distribution mapping support elements to probability values.
`ModelType`	The type of the model.
`Model`	Represent a model.
`State`	Represent a state in a Model.
`Interval`	Represent an interval value for interval models.
`Observation`	Represent an observation of a state (for POMDPs and HMMs).
`RewardModel`	Represent a reward model supporting state rewards and transition rewards.
`IntDomain`	A bounded integer domain [lo, hi].
`BoolDomain`	A boolean domain {False, True}.
`CategoricalDomain`	A finite categorical domain with an explicit ordered set of values.
`Variable`
`Predicate`	A named observable predicate with a required domain and an optional defining expression.
`Scheduler`	Specify what action to take in each state.
`Result`	Represent the model checking results for a given model.
`ParetoResult`	Result of a multiobjective Pareto model checking query.
`Path`	Represent a path created by a simulator on a certain model.
`JSVisualization`	Handles visualization of a Model using a Network from stormvogel.network.

Functions¶

`choices_from_shorthand`(...)	Create a `Choices` object from a `ChoicesShorthand`.
`new_dtmc`(→ Model)	Create a DTMC.
`new_mdp`(→ Model)	Create an MDP.
`new_ctmc`(→ Model)	Create a CTMC.
`new_pomdp`(→ Model)	Create a POMDP.
`new_hmm`(→ Model)	Create an HMM.
`new_ma`(→ Model)	Create a MA.
`new_model`(→ Model)	Create a model of the given type.
`is_zero`(→ bool)	Returns whether a value is zero.
`value_to_string`(→ str)	Convert a `Value` to a string.
`build_property_string`(model)	Let the user build a property string using a widget.
`random_scheduler`(→ Scheduler)	Create a random scheduler for the provided model.
`plot_pareto_result`(result[, ax, labels, bbox_pad])	Plot the under- and over-approximation of a 2-objective Pareto model checking result.
`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.
`show`(...)	Create and show a visualization of a Model using a visjs Network.
`step`(→ tuple[stormvogel.model.State, ...)	Simulate one step from the given state.
`simulate_path`(→ Path)	Simulate the model and return the path created by the process.
`simulate`(→ stormvogel.model.Model)	Simulate the model over multiple runs.
`get_action_at_state`(→ stormvogel.model.Action)	Obtain the chosen action in a state by a scheduler.
`model_checking`(...)	Perform model checking on a stormvogel model using stormpy.
`is_in_notebook`()

Package Contents¶

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

Store the layout and schema for a visualization.

Upon creation, the layout and schema dicts are loaded from layouts/default.json and layouts/schema.json, unless specified otherwise. Load a custom layout file by setting either path or path_relative, or provide a custom layout dict instead.

Parameters:

path – Path to a custom layout file. Leave as None for the default layout.
path_relative – If True, stormvogel looks for a custom layout file relative to the current working directory.
layout_dict – If set, this dictionary is used as the layout instead of the file specified in path. Missing keys are filled from layouts/default.json.

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 layout and schema respectively.

Parameters:

path – Path to the layout file, or None for the default layout.
path_relative – If True, path is resolved relative to the current working directory.

add_active_group(group: str) → None¶

Make a group active if it is not already.

The user can specify which groups of states can be edited separately. Such groups are referred to as active groups.

Parameters:: group – Name of the group to activate.

remove_active_group(group: str) → None¶

Make a group inactive if it is not already.

Parameters:: group – Name of the group to deactivate.

set_possible_groups(groups: set[str]) → None¶

Set the groups of states that the user can choose to make active.

These appear under edit_groups in the layout editor.

Parameters:: groups – Set of group names to make available.

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

Save this layout as a JSON file.

Parameters:

path – Path to the layout file. Must end in .json.
path_relative – If True, path is resolved relative to the current working directory.

Raises:

RuntimeError – If the filename does not end in .json.
OSError – If the file cannot be written.

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.

Parameters:

path – List of keys forming the path to the value.
value – The value to set.

__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, scale: float = 500) → Self¶

Apply NetworkX layout positions to this layout and disable physics.

Parameters:

pos – Dictionary of node positions from a NetworkX graph.
scale – Scaling factor for the positions.

Returns:

This Layout instance, for chaining.

class stormvogel.Action¶

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

The action object is independent of its corresponding branch; their relation is managed by Choices. Two actions with the same label are considered equal.

Parameters:: label – The label of this action. Corresponds to a Storm label.

label: str | None¶

__post_init__()¶

__lt__(other)¶

__repr__()¶

__str__¶

stormvogel.EmptyAction¶

class stormvogel.Choices[ValueType: stormvogel.model.value.Value](choices: dict[stormvogel.model.action.Action, stormvogel.model.distribution.Distribution[ValueType, State[ValueType]]])¶

Represent a choice, which maps actions to branches.

An EmptyAction may be used for a non-action choice. A single Choices instance might correspond to multiple ‘arrows’.

Parameters:: choices – The choice dictionary. For each available action, a branch containing the transitions.

_choices: dict[stormvogel.model.action.Action, stormvogel.model.distribution.Distribution[ValueType, State[ValueType]]]¶

property actions: list[stormvogel.model.action.Action]¶: Return the actions for the choices.

__str__()¶

has_empty_action() → bool¶

is_stochastic(epsilon=1e-06) → bool¶

Check whether the probabilities in the branches sum to 1.

Parameters:: epsilon – Tolerance for floating-point comparison.
Returns:: True if all branches are stochastic within epsilon.

has_zero_transition() → bool¶

Check whether any of the branches contains a zero-probability transition.

Returns:: True if a zero-probability transition exists.

add(other_choices: Self | ChoicesShorthand)¶

Add another Choices to this one in-place.

Parameters:: other – The choices to merge in.
Raises:: RuntimeError – If the two choices have incompatible or overlapping actions.

__add__(other: Self | ChoicesShorthand) → Choices[ValueType]¶

__iter__()¶

__len__() → int¶

__setitem__(key, value)¶

__getitem__(item)¶

__delitem__(key)¶

stormvogel.ChoicesShorthand¶

stormvogel.choices_from_shorthand(shorthand: ChoicesShorthand) → Choices[stormvogel.model.value.Value]¶

Create a Choices object from a ChoicesShorthand.

Two shorthand modes are supported:

A list of (probability, target_state) tuples (implies the default action when in an MDP).
A list of (action, target_state) tuples (implies probability 1).
A dict mapping actions to lists of (probability, target_state) tuples.

Parameters:: shorthand – The shorthand representation to convert.
Returns:: A new Choices instance.

class stormvogel.Distribution[ValueType: stormvogel.model.value.Value, SupportType](distribution: dict[SupportType, ValueType] | list[tuple[ValueType, SupportType]] | Distribution[ValueType, SupportType] | None = None)¶

A sparse distribution mapping support elements to probability values.

_distribution: dict[SupportType, ValueType]¶

property support: set[SupportType]¶: Returns the support of this distribution (elements with non-zero probability).

property probabilities: list[ValueType]¶: Returns the probability values of this distribution.

is_stochastic(epsilon: float = 1e-06) → bool¶

Returns whether this distribution sums to 1.

For interval and parametric distributions we always return True.

__eq__(other: object) → bool¶

__repr__() → str¶

__str__¶

__add__(other: Distribution[ValueType, SupportType]) → Distribution[ValueType, SupportType]¶

__iter__()¶

__len__() → int¶

__getitem__(key: SupportType) → ValueType¶

__setitem__(key: SupportType, value: ValueType)¶

__contains__(key: SupportType) → bool¶

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.Model[ValueType: stormvogel.model.value.Value](model_type: ModelType, create_initial_state: bool = True)¶

Represent a model.

Parameters:

model_type – The model type.
states – The states of the model.
transitions – The transitions of this model. The keys are State objects.
state_valuations – The state valuations of this model, mapping states to variable-value pairs.
friendly_names – Optional mapping from states to friendly names for easier debugging and visualization.
rewards – The reward models of this model.
observation_aliases – The mapping from observations to their aliases (empty for non-observation models).
observation_valuations – The mapping from observations to variable-value pairs (empty for non-observation models).
state_observations – The mapping from states to their observations (empty for non-observation models).
markovian_states – The set of states that are markovian (only for Markov automata).

model_type: ModelType¶

states: list[stormvogel.model.state.State[ValueType]]¶

transitions: dict[stormvogel.model.state.State[ValueType], stormvogel.model.choices.Choices]¶

state_valuations: dict[stormvogel.model.state.State[ValueType], dict[stormvogel.model.variable.Variable, Any]]¶

state_labels: dict[str, set[stormvogel.model.state.State[ValueType]]]¶

friendly_names: dict[stormvogel.model.state.State[ValueType], str | None]¶

rewards: list[stormvogel.model.reward_model.RewardModel]¶

observation_aliases: dict[stormvogel.model.observation.Observation, str]¶

observation_valuations: dict[stormvogel.model.observation.Observation, dict[stormvogel.model.variable.VariableKey, Any]]¶

state_observations: dict[stormvogel.model.state.State[ValueType], stormvogel.model.observation.Observation | stormvogel.model.distribution.Distribution[ValueType, stormvogel.model.observation.Observation]]¶

markovian_states: set[stormvogel.model.state.State[ValueType]]¶

_is_interval: bool | None = None¶

_state_index_cache: dict[stormvogel.model.state.State, int] | None = None¶

_parameters: dict[str, stormvogel.parametric.Parametric]¶

property actions: Iterable[stormvogel.model.action.Action]¶

Extract the actions from a model that supports actions.

Raises:: RuntimeError – If the model does not support actions.

property observations: Iterable[stormvogel.model.observation.Observation]¶

Extract the observations from a model that supports observations.

Raises:: RuntimeError – If the model does not support observations.

property parameters: tuple[str, Ellipsis]¶

Return the declared parameters of this model in insertion order.

The order is stable: it reflects the order in which parameters were first declared (either explicitly via declare_parameter() or implicitly by appearing in a transition). Downstream tools such as the pycarl/stormpy bridge depend on this ordering.

declare_parameter(name: str, **kwargs) → stormvogel.parametric.Parametric¶

Declare a parameter of this model.

If a parameter with this name has already been declared the existing backend-native symbol is returned unchanged; otherwise a new symbol is created via the active parametric backend and registered on the model. **kwargs are forwarded to the backend’s symbol factory (e.g. positive=True for sympy assumptions).

Parameters:: name – The parameter name.
Returns:: The backend-native symbol representing the parameter.

property parameter_symbols: tuple[stormvogel.parametric.Parametric, Ellipsis]¶

Return the declared parameters as backend-native symbols, in order.

Mirrors parameters but returns the actual backend objects instead of their names. This is what backend bridges (e.g. the pycarl converter) should consume, as it guarantees symbol identity is preserved for assumption-carrying backends such as sympy.

find_unused_parameters() → set[str]¶

Return declared parameters that do not appear in any transition.

This walks all transitions and collects free symbol names; the set difference with parameters is returned. Use prune_parameters() to actually remove them.

prune_parameters() → set[str]¶

Drop declared parameters that (no longer) occur in any transition.

Returns the set of parameter names that were removed. This is an explicit, on-demand operation: the model never prunes automatically on mutation.

property initial_state: stormvogel.model.state.State¶

Get the initial state (the state with label "init").

Raises:: RuntimeError – If the model does not have exactly one initial state.

property variables: set[stormvogel.model.variable.Variable]¶: Get the set of all variables present in this model (corresponding to state valuations).

property nr_states: int¶

Return the number of states in this model.

Note that not all states need to be reachable.

property nr_choices: int¶: Return the number of choices in the model (summed over all states).

property sorted_states¶

supports_actions() → bool¶: Return whether this model supports actions.

supports_rates() → bool¶: Return whether this model supports rates.

supports_observations() → bool¶: Return whether this model supports observations.

is_interval_model() → bool¶: Return whether this model is an interval model, i.e., contains interval values.

is_parametric() → bool¶: Return whether this model has parameters declared.

is_affine_parametric() → bool¶

Return whether all parametric transition probabilities and rewards are affine.

A model is affine parametric if every symbolic value has total polynomial degree ≤ 1. Non-parametric (constant) values are trivially affine. A non-parametric model always returns True.

has_fixed_graph() → bool¶

Return whether the set of reachable transitions is fixed (graph-independent of choices).

For constant (non-parametric, non-interval) models: always True.
For parametric models: raises ValueError because the graph depends on parameter values and cannot be determined symbolically.
For interval models: True if every interval lower bound is strictly positive (every edge always exists regardless of nature’s choice); False if any lower bound is zero (nature may remove that edge entirely).

Raises:: ValueError – If the model is parametric.

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

Check whether the model is stochastic.

For discrete models, check that all sums of outgoing transition probabilities for all states equal 1, with at most epsilon rounding error. For continuous models, check that each outgoing rate is positive.

Parameters:: epsilon – Maximum allowed rounding error for probability sums.
Returns:: True if the model is stochastic, False otherwise, or True trivially for parametric / interval models.

new_state(labels: list[str] | str | None = None, valuations: dict[stormvogel.model.variable.Variable, Any] | None = None, observation: stormvogel.model.observation.Observation | stormvogel.model.distribution.Distribution[ValueType, stormvogel.model.observation.Observation] | None = None, friendly_name: str | None = None) → stormvogel.model.state.State¶

Create a new state and return it.

Parameters:

labels – Labels to assign to the new state.
valuations – Variable-value pairs to assign as valuations.
observation – Observation to assign (required for models that support observations).
friendly_name – Optional human-readable name for the state.

Returns:

The newly created state.

Raises:

RuntimeError – If the model supports observations but none is provided, or if an observation is provided but not supported.

remove_state(state: stormvogel.model.state.State, normalize: bool = True, suppress_warning: bool = False)¶

Remove a state from the model.

Removes all incoming and outgoing transitions, labels, reward entries, and markovian-state membership for the given state.

Parameters:

state – The state to remove.
normalize – Whether to normalize the model after removal.
suppress_warning – If True, suppress the warning about existing references to states by id.

Raises:

RuntimeError – If the state is not part of this model.

get_state_index(state: stormvogel.model.state.State) → int¶

Return the index of the given state in the model, with O(1) amortized lookup.

Parameters:: state – The state to look up.
Returns:: The index of the state, or -1 if not found.

add_label(label: str)¶

Add a label to the model.

Parameters:: label – The label to add.

get_states_with_label(label: str) → set[stormvogel.model.state.State]¶

Get all states with a given label.

Parameters:: label – The label to search for.
Returns:: The set of states that carry the label.

get_state_by_id(state_id: uuid.UUID) → stormvogel.model.state.State¶

Get a state by its UUID.

Parameters:: state_id – The UUID of the state.
Returns:: The matching state.
Raises:: RuntimeError – If no state with the given id is found.

compute_predecessors() → dict[State, list[State]]¶

Build and return the full predecessor map for every state.

This is an O(states × transitions) operation; call it once and reuse the result rather than calling it in a loop.

Returns:: A dict mapping each state to the list of states that have a direct transition to it.

new_observation(alias: str, valuations: dict[stormvogel.model.variable.VariableKey, Any] | None = None) → stormvogel.model.observation.Observation¶

Create a new observation and return it.

Parameters:

alias – The alias for the new observation.
valuations – Variable-value pairs to assign as valuations.

Returns:

The newly created observation.

Raises:

RuntimeError – If the model does not support observations, or if an observation with the given alias already exists.
ValueError – If any value is outside its variable’s domain.

get_observation(alias: str) → stormvogel.model.observation.Observation¶

Get an existing observation with the given alias.

Parameters:: alias – The alias of the observation.
Returns:: The matching observation.
Raises:: RuntimeError – If the model does not support observations, or if no observation with the given alias is found.

compute_states_per_observation() → dict[Observation, set[State]]¶

Build and return a mapping from every observation to its set of states.

This is an O(states) operation; call it once and reuse the result rather than calling it in a loop.

Returns:: A dict mapping each Observation to the set of states assigned to it.
Raises:: RuntimeError – If the model does not support observations.

observation(alias: str) → stormvogel.model.observation.Observation¶: Makes a new observation if the given alias does not exist and returns it, otherwise returns the existing observation with the given alias.

make_observations_deterministic()¶

Make observations deterministic by splitting states with multiple observations.

In case of POMDPs or HMMs, split each state that has a distribution over observations into multiple states with single observations.

Raises:: RuntimeError – If the model does not support observations.

make_fully_observable() → Model¶

Remove observations and convert this model to its fully-observable counterpart.

POMDP → MDP and HMM → DTMC. All observation data (state_observations, observation_aliases, observation_valuations) is cleared. The model is mutated in place and returned for chaining.

Returns:: self, with model type updated and observations removed.
Raises:: ValueError – If the model is not a POMDP or HMM.

new_action(label: str) → stormvogel.model.action.Action¶

Create a new action with the given label.

Parameters:: label – The label for the new action.
Returns:: The newly created action.

action(label: str) → stormvogel.model.action.Action¶: Alias of new_action.

add_markovian_state(markovian_state: stormvogel.model.state.State)¶

Add a state to the markovian states.

Parameters:: markovian_state – The state to mark as markovian.
Raises:: RuntimeError – If the model is not a Markov automaton.

set_choices(s: stormvogel.model.state.State, choices: stormvogel.model.choices.Choices | stormvogel.model.choices.ChoicesShorthand) → None¶

Set the choices for a state.

Parameters:

s – The state to set choices for.
choices – The choices to assign.

Raises:

RuntimeError – If any transition probability is zero.

add_choices(s: stormvogel.model.state.State, choices: stormvogel.model.choices.Choices | stormvogel.model.choices.ChoicesShorthand) → None¶

Add new choices from a state to the model.

If no choice currently exists, the result is the same as set_choices().

Parameters:

s – The state to add choices to.
choices – The choices to add.

Raises:

RuntimeError – If any transition probability is zero.

_validate_parametric_choices(choices: stormvogel.model.choices.Choices) → bool¶

Check that all free symbols in parametric transitions are declared.

Returns True if any parametric value was found and False otherwise

Raises:: ValueError – If a transition references a symbol not in parameters. Call declare_parameter() first.

add_self_loops() → None¶: Add self-loops to all states that do not have an outgoing transition.

get_successor_states(state: stormvogel.model.state.State) → set[stormvogel.model.state.State]¶

Return the set of successor states of the given state.

Parameters:: state – The state whose successors to retrieve.
Returns:: The set of successor states.

get_distribution(state: stormvogel.model.state.State) → stormvogel.model.distribution.Distribution[ValueType, stormvogel.model.state.State[ValueType]]¶

Get the distribution at the given state.

Only intended for distribution with EmptyAction; raises an error otherwise.

Parameters:: state – The state to retrieve branches for.
Returns:: The branches for the empty action at this state.
Raises:: RuntimeError – If the state has non-empty choices.

iterate_transitions() → Iterator[tuple[ValueType, stormvogel.model.state.State]]¶: Iterate through all transitions in all choices of the model.

has_zero_transition() → bool¶: Check whether the model has transitions with probability zero.

new_reward_model(name: str) → stormvogel.model.reward_model.RewardModel¶

Create a reward model with the specified name, add it, and return it.

Parameters:: name – The name for the new reward model.
Returns:: The newly created reward model.
Raises:: RuntimeError – If a reward model with the given name already exists.

get_default_rewards() → stormvogel.model.reward_model.RewardModel¶

Get the default reward model.

Returns:: The first reward model.
Raises:: RuntimeError – If there are no reward models.

get_rewards(name: str) → stormvogel.model.reward_model.RewardModel¶

Get the reward model with the specified name.

Parameters:: name – The name of the reward model.
Returns:: The matching reward model.
Raises:: RuntimeError – If no reward model with the given name exists.

summary()¶: Give a short summary of the model.

normalize()¶

Normalize the model.

For states where outgoing transition probabilities do not sum to 1, divide each probability by the sum. For rate-based models, only add self-loops.

Raises:: RuntimeError – If the model is parametric or an interval model.

copy() → Model¶

Return a deep copy of this model, preserving all state UUIDs.

Each state in the copy shares the same state_id as its original, so callers can cross-reference states via new_model.get_state_by_id(s.state_id).

Implemented via copy.deepcopy(), so all current and future fields are included automatically. Sympy expressions (parametric transition probabilities) are immutable and shared by reference.

Returns:: A new Model with identical structure.

get_sub_model(states: Iterable[stormvogel.model.state.State], normalize: bool = True) → Model¶

Return a submodel containing only the given states.

Parameters:

states – The states to keep in the submodel.
normalize – Whether to normalize the submodel after construction.

Returns:

A new model containing only the specified states.

get_instantiated_model(values: dict[str, stormvogel.model.value.Number]) → Model¶

Substitute parameter values in all transitions and return a new model.

Partial substitutions are supported: parameters absent from values remain free and the resulting model is still parametric. When every declared parameter is substituted the returned model is effectively a regular Markov model with concrete probabilities.

Parameters:: values – Mapping from parameter names to their numeric values. Keys that do not correspond to a declared parameter are ignored.
Returns:: A new model with the listed parameters substituted.

add_valuation_at_remaining_states(variables: list[stormvogel.model.variable.Variable] | None = None, value: Any = 0)¶

Set a dummy value for variables in all states where they are unassigned.

Parameters:

variables – List of variable names to set. If None, all variables in the model are used.
value – The value to assign to unassigned variables.

unassigned_variables() → Iterator[tuple[stormvogel.model.state.State, stormvogel.model.variable.Variable]]¶: Yield tuples of state-variable pairs that are unassigned.

validate() → stormvogel.model.validation.ValidationResult¶

to_dot() → str¶: Generate a dot representation of this model.

__str__() → str¶

__getitem__(state_index: int)¶

__iter__()¶

get_type() → ModelType¶: Get the type of this model.

get_initial_state() → stormvogel.model.state.State¶: Get the initial state of this model.

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

Create a DTMC.

Parameters:: create_initial_state – Whether to create an initial state.
Returns:: A new DTMC model.

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

Create an MDP.

Parameters:: create_initial_state – Whether to create an initial state.
Returns:: A new MDP model.

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

Create a CTMC.

Parameters:: create_initial_state – Whether to create an initial state.
Returns:: A new CTMC model.

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

Create a POMDP.

Parameters:: create_initial_state – Whether to create an initial state.
Returns:: A new POMDP model.

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

Create an HMM.

Parameters:: create_initial_state – Whether to create an initial state.
Returns:: A new HMM model.

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

Create a MA.

Parameters:: create_initial_state – Whether to create an initial state.
Returns:: A new Markov automaton model.

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

Create a model of the given type.

Parameters:

modeltype – The type of model to create.
create_initial_state – Whether to create an initial state.

Returns:

A new model of the specified type.

class stormvogel.State[ValueType: stormvogel.model.value.Value]¶

Represent a state in a Model.

Parameters:

model – The model this state belongs to.
state_id – The unique identifier of this state.

model: Model[ValueType]¶

state_id: uuid.UUID¶

property labels: Iterable[str]¶: Return an iterator over the state’s labels.

set_friendly_name(friendly_name: str | None) → None¶

property friendly_name: str | None¶: Returns the friendly name of this state.

set_labels(labels: set[str])¶

Set the labels of this state, adding and removing as needed.

Parameters:: labels – The complete set of labels this state should have.

has_label(label: str)¶

Check whether this state has the given label.

Parameters:: label – The label to check for.
Returns:: True if the label is present.

add_label(label: str)¶

Add a new label to this state.

Parameters:: label – The label to add.

property observation: stormvogel.model.observation.Observation | stormvogel.model.distribution.Distribution[ValueType, stormvogel.model.observation.Observation] | None¶

Return the observation associated with this state.

Raises:: RuntimeError – If the model does not support observations.

property choices: Choices[ValueType]¶

Return the choices for this state.

Raises:: RuntimeError – If no choices exist for this state.

property unique_branch: Distribution[ValueType, State[ValueType]]¶

Return the single branch of this state.

Raises:: RuntimeError – If the state does not have exactly one choice.

property unique_choice: tuple[Action, Distribution[ValueType, State[ValueType]]]¶

Return the single (action, branch) pair of this state.

Raises:: RuntimeError – If the state does not have exactly one choice.

set_choices(choices: stormvogel.model.choices.Choices | stormvogel.model.choices.ChoicesShorthand)¶

Set the choices for this state.

Parameters:: choices – The choices to set.

add_choices(choices: stormvogel.model.choices.Choices | stormvogel.model.choices.ChoicesShorthand)¶

Add choices to this state.

Parameters:: choices – The choices to add.

has_choices() → bool¶: Check whether this state has choices.

property nr_choices: int¶: The number of choices in this state.

property valuations: dict[stormvogel.model.variable.Variable, Any]¶: The valuations of this state.

add_valuation(variable: stormvogel.model.variable.Variable, value: Any)¶

Add a valuation to this state.

Parameters:

variable – The variable name.
value – The value for the variable.

get_valuation(variable: stormvogel.model.variable.Variable) → Any¶

Return the valuation for the given variable.

Parameters:: variable – The variable name.
Returns:: The value associated with the variable.

available_actions() → list[stormvogel.model.action.Action]¶: Return the list of available actions in this state.

get_branches(action: stormvogel.model.action.Action | None = None) → stormvogel.model.distribution.Distribution[ValueType, State[ValueType]]¶

Get the branches of this state for a specific action.

Parameters:: action – The action to get branches for.
Returns:: The branches.
Raises:: RuntimeError – If the requested action does not exist for this state.

get_outgoing_transitions(action: stormvogel.model.action.Action | None = None) → stormvogel.model.distribution.Distribution[ValueType, State[ValueType]] | None¶

Get the outgoing transitions of this state for a specific action.

Parameters:: action – The action to get transitions for.
Returns:: The distribution over successor states, or None if not found.
Raises:: RuntimeError – If the model supports actions but none is provided.

is_absorbing() → bool¶: Check whether this state is absorbing (no nonzero transitions to other states).

has_selfloop() → bool¶

Check whether this state has a self-loop.

Returns True if any action has a transition back to this state with positive probability. For interval models a transition counts as positive when its upper bound is non-zero; for parametric models when the expression is not syntactically zero.

Returns:: True if a self-loop exists, False otherwise.

is_initial()¶: Check whether this state is the initial state.

__repr__()¶

__str__¶

stormvogel.Number¶

class stormvogel.Interval¶

Represent an interval value for interval models.

Parameters:

bottom – The bottom (left) element of the interval.
top – The top (right) element of the interval.

lower: Number¶

upper: Number¶

__lt__(other)¶

__str__()¶

stormvogel.Value¶

stormvogel.is_zero(value: Value) → bool¶: Returns whether a value is zero.

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.

Parameters:

n – The value to convert.
use_fractions – If True, represent numbers as fractions.
round_digits – Number of decimal places when not using fractions.
denom_limit – Maximum denominator when limiting fractions.

Returns:

String representation of the value.

class stormvogel.Observation¶

Represent an observation of a state (for POMDPs and HMMs).

Parameters:

alias – Human-readable name for the observation.
observation_id – Unique identifier for the observation.
valuations – Optional mapping of variable names to observed values.

model: stormvogel.model.Model¶

observation_id: uuid.UUID¶

property valuations: dict[stormvogel.model.variable.VariableKey, Any]¶: Return the variable- and predicate-value pairs observed in this observation.

property alias: str¶: Return the alias of this observation.

display()¶: Format the observation for visualizations.

__repr__()¶

__str__¶

class stormvogel.RewardModel[ValueType: stormvogel.model.value.Value]¶

Represent a reward model supporting state rewards and transition rewards.

Parameters:

name – Name of the reward model.
model – The model this reward model belongs to.
rewards – Mapping from states to their state reward values.
transition_rewards – Sparse mapping from (source, action, target) triples to reward values collected on that specific transition.

name: str¶

model: stormvogel.model.model.Model¶

rewards: dict[stormvogel.model.state.State, ValueType]¶

transition_rewards: dict[tuple[stormvogel.model.state.State, stormvogel.model.action.Action, stormvogel.model.state.State], ValueType]¶

set_from_rewards_vector(vector: list[ValueType], state_action: bool = False) → None¶

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

Parameters:

vector – The reward values.
state_action – If True, the vector has one entry per (state, action) pair; only the first entry for each state is used.

get_state_reward(state: stormvogel.model.state.State) → ValueType | None¶

Get the reward at the given state.

Parameters:: state – The state to look up.
Returns:: The reward value, or None if no reward is present.

set_state_reward(state: stormvogel.model.state.State, value: ValueType)¶

Set the reward at the given state.

Parameters:

state – The state to set the reward for.
value – The reward value to assign.

set_unset_rewards(value: ValueType)¶

Fill up rewards that were not set yet with the specified value.

Parameters:: value – The default reward value to assign to unset states.

has_transition_rewards() → bool¶: Return True if any nonzero transition reward is present.

set_transition_reward(s: stormvogel.model.state.State, a: stormvogel.model.action.Action, s_next: stormvogel.model.state.State, value: ValueType) → None¶: Set the reward collected when transitioning from s via a to s_next.

get_transition_reward(s: stormvogel.model.state.State, a: stormvogel.model.action.Action, s_next: stormvogel.model.state.State) → ValueType¶: Return the transition reward for (s, a, s_next), or 0 if absent.

__iter__()¶

get_reward_vector() → list[float]¶

Return a list of all rewards ordered appropriately.

Returns:: A flat list of reward values as floats.

class stormvogel.IntDomain¶

A bounded integer domain [lo, hi].

Parameters:

lo – Lower bound (inclusive).
hi – Upper bound (inclusive).
allow_none – Whether None is a valid value.

lo: int¶

hi: int¶

allow_none: bool = False¶

contains(value: Any) → bool¶

__repr__()¶

class stormvogel.BoolDomain¶

A boolean domain {False, True}.

Parameters:: allow_none – Whether None is a valid value.

allow_none: bool = False¶

contains(value: Any) → bool¶

__repr__()¶

class stormvogel.CategoricalDomain¶

A finite categorical domain with an explicit ordered set of values.

Parameters:

values – All valid values, as a tuple to preserve order.
allow_none – Whether None is a valid value.

values: tuple[Any, Ellipsis]¶

allow_none: bool = False¶

contains(value: Any) → bool¶

__repr__()¶

stormvogel.VariableDomain¶

class stormvogel.Variable¶

label: str¶

domain: VariableDomain | None = None¶

__lt__(other)¶

check_valuation(value: Any) → None¶: Raise ValueError if value is outside this variable’s declared domain.

__repr__()¶

__str__¶

class stormvogel.Predicate¶

A named observable predicate with a required domain and an optional defining expression.

Parameters:

label – Human-readable name for the predicate.
domain – The domain of values this predicate can take.
expr – Optional callable f(valuations) -> value that computes the predicate value from a state’s {Variable: value} dict. None when the predicate was imported from an external tool and the expression is not available.

label: str¶

domain: VariableDomain¶

expr: collections.abc.Callable[[dict[Variable, Any]], Any] | None = None¶

check_valuation(value: Any) → None¶: Raise ValueError if value is outside this predicate’s domain.

__repr__()¶

__str__¶

stormvogel.VariableKey¶

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

Let the user build a property string using a widget.

Parameters:: model – The model to build a property string for.

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

Specify what action to take in each state.

All schedulers are nondeterministic and memoryless.

Parameters:

model – Model associated with the scheduler (must support actions).
taken_actions – For each state, the action chosen in that state.

model: stormvogel.model.Model¶

taken_actions: dict[stormvogel.model.State, stormvogel.model.Action]¶

get_action_at_state(state: stormvogel.model.State) → stormvogel.model.Action¶

Return the action in the scheduler for the given state.

Parameters:: state – The state to look up.
Returns:: The action chosen for the given state.
Raises:: RuntimeError – If the state is not a part of the model.

generate_induced_dtmc(drop_unreachable: bool = True) → stormvogel.model.Model¶

Resolve the nondeterminacy of the MDP and return the scheduler-induced DTMC.

Copies the MDP (preserving state UUIDs), changes the model type to DTMC, and replaces each state’s choices with only the scheduled action’s branch.

Parameters:: drop_unreachable – When True (default), states not reachable from the initial state under the scheduler are pruned from the result. Set to False to keep the full state space.
Returns:: The induced DTMC.
Raises:: ValueError – If the model is not an MDP or POMDP.

__str__() → str¶

__eq__(other) → bool¶

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

Create a random scheduler for the provided model.

Parameters:: model – The model to create a scheduler for.
Returns:: A new Scheduler with randomly chosen actions.

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

Represent the model checking results for a given model.

Parameters:

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, optionally store a scheduler.

model: stormvogel.model.Model¶

values: dict[stormvogel.model.State, stormvogel.model.Value]¶

scheduler: Scheduler | None¶

at(state: stormvogel.model.State) → stormvogel.model.Value¶

Return the model checking result for a given state.

Parameters:: state – The state to look up.
Returns:: The model checking result value for the state.
Raises:: RuntimeError – If the state is not a part of the model.

at_init() → stormvogel.model.Value¶: Return the model checking result for the initial state.

get_result_of_state(state: stormvogel.model.State) → stormvogel.model.Value¶

filter(value_predicate: Callable[[stormvogel.model.Value], bool]) → list[stormvogel.model.State]¶

filter_true()¶: Obtain the set of states S’ where the result for each s in S’ is true.

__str__() → str¶

maximum_result() → stormvogel.model.Value¶

Return the maximum result.

Returns:: The maximum value across all states.
Raises:: RuntimeError – If the model uses interval or parametric values.

__eq__(other) → bool¶

__iter__()¶

class stormvogel.ParetoResult¶

Result of a multiobjective Pareto model checking query.

Holds the under- and over-approximation of the Pareto front as vertex lists. Each point is a list of floats with one entry per objective. The number of objectives is unrestricted, but plotting is limited to 2 objectives.

Parameters:

lower_points – Vertices of the under-approximation (known achievable region).
upper_points – Vertices of the over-approximation.
property_labels – One label per objective, auto-extracted from the formula.

lower_points: list[list[float]]¶

upper_points: list[list[float]]¶

property_labels: list[str] | None = None¶

plot(ax=None, labels: tuple[str, str] | None = None)¶

Plot the Pareto front. Only 2-objective results are supported.

Parameters:

ax – Target axes; creates a new figure if None.
labels – Override axis labels; defaults to property_labels.

Returns:

The populated axes.

stormvogel.plot_pareto_result(result: ParetoResult, ax=None, labels: tuple[str, str] | None = None, bbox_pad: float = 0.2)¶

Plot the under- and over-approximation of a 2-objective Pareto model checking result.

Renders: - Green filled polygon: under-approximation (known achievable region) - Blue dashed outline: over-approximation (upper bound on achievable region) - Black dots: vertices of the under-approximation

Parameters:

result – A ParetoResult from multiobjective model checking.
ax – Target axes; creates a new figure if None.
labels – Override axis labels; defaults to property_labels.
bbox_pad – Fractional padding around the points for axis limits.

Returns:

The populated axes.

Raises:

ValueError – If result does not contain exactly 2-dimensional points.

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.

Parameters:

model – The stormvogel model to be displayed.
result – A result associated 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.
engine – 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 – 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.bfs_layout seems to work great for models with a directed acyclic graph structure.
pos_function_scaling – Scaling factor for the positions when using networkx positions.
scheduler – 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 used for the visualization.
show_editor – For interactive visualization. Show an interactive layout editor.
debug_output – For interactive visualization. Output widget that can be used to debug interactive features.
use_iframe – For interactive visualization. Wrap the generated HTML inside of an IFrame. In some environments, the visualization works better with this enabled.
do_init_server – 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 – If the model has more states, then the network is not displayed.
max_physics_states – If the model has more states, then physics are disabled.

Returns:

A JSVisualization or MplVisualization object, or None on error.

Raises:

ValueError – If the engine is not recognized.

stormvogel.show_bird() → stormvogel.visualization.JSVisualization¶: Show a simple model with a bird state.

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

Parameters:

model – The stormvogel model to be displayed.
result – A result associated 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.
engine – 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 – 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.bfs_layout seems to work great for models with a directed acyclic graph structure.
pos_function_scaling – Scaling factor for the positions when using networkx positions.
scheduler – 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 used for the visualization.
show_editor – For interactive visualization. Show an interactive layout editor.
debug_output – For interactive visualization. Output widget that can be used to debug interactive features.
use_iframe – For interactive visualization. Wrap the generated HTML inside of an IFrame. In some environments, the visualization works better with this enabled.
do_init_server – 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 – If the model has more states, then the network is not displayed.
max_physics_states – If the model has more states, then physics are disabled.

Returns:

A JSVisualization or MplVisualization object, or None on error.

Raises:

ValueError – If the engine is not recognized.

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

Represent a path created by a simulator on a certain model.

Parameters:

path – The path itself is a list where we either store for each step a state or a state-action pair, depending on whether 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¶

Return the state discovered in the given step in the path.

Parameters:: step – The step index to look up.
Returns:: The state at the given step, or None.

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

Return the action discovered in the given step in the path.

Parameters:: step – The step index to look up.
Returns:: The action at the given step, or None.

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

Return the state or state-action pair discovered in the given step.

Parameters:: step – The step index to look up.
Returns:: The state or state-action pair at the given step.

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

Convert a Path to a list containing actions and states.

Returns:: A flat list of actions and states from this path.

__str__() → str¶

__len__()¶

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

Simulate one step from the given state.

Rewards are always the state-exit rewards of the current state. Missing rewards default to 0.

Parameters:

state – The current state to step from.
action – The action to take, or None for models without actions.
seed – Seed for the random state selection. Random if not provided.

Returns:

A tuple of (next_state, state-exit rewards, next_state labels).

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¶

Simulate the model and return the path created by the process.

Parameters:

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. A callable from states to actions can also be provided.
seed – The seed for the random state selection. Random if not provided.

Returns:

A path object representing the simulated trajectory.

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¶

Simulate the model over multiple runs.

Parameters:

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. A callable from states to actions can also be provided.
seed – The seed for the random state selection. Random if not provided.

Returns:

The partial model discovered by all the runs of the simulator together.

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

Obtain the chosen action in a state by a scheduler.

Parameters:

state – The state to get the action for.
scheduler – A scheduler or callable that maps states to actions.

Returns:

The action chosen by the scheduler at the given state.

Raises:

TypeError – If scheduler is not a Scheduler or callable.

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¶

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.

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

Perform model checking on a stormvogel model using stormpy.

Convert the model to stormpy, run model checking, and convert the result back. If no property string is provided, a widget for building one is displayed.

For multiobjective properties of the form multi(Pmax=? [...], ...) a ParetoResult is returned instead of a Result.

Parameters:

model – The stormvogel model to check.
prop – A property string to check, or None to display a property builder widget.
scheduler – Whether to extract a scheduler from the result (ignored for multiobjective).

Returns:

The model checking result, or None if no property was provided.

Raises:

RuntimeError – If the model is not stochastic.

stormvogel.is_in_notebook()¶

stormvogel¶

Submodules¶

Attributes¶

Classes¶

Functions¶

Package Contents¶