stormvogel.umbi¶

Submodules¶

stormvogel.umbi.translate

Attributes¶

_UMBI_AVAILABLE

Classes¶

Model

Represent a model.

Functions¶

`translate_to_umbi`(→ umbi.ats.simple_ats.SimpleAts)	Export a stormvogel Model to a UMBI SimpleAts.
`translate_to_stormvogel`(→ stormvogel.model.model.Model)	Import a UMBI SimpleAts as a stormvogel Model.
`write_to_umb`(→ None)	Translate a stormvogel Model and write it to a .umb file.
`read_from_umb`(→ stormvogel.model.model.Model)	Read a .umb file and return it as a stormvogel Model.

Package Contents¶

stormvogel.umbi._UMBI_AVAILABLE = True¶

stormvogel.umbi.translate_to_umbi(model: stormvogel.model.model.Model, ignore_unsupported_rewards: bool = False) → umbi.ats.simple_ats.SimpleAts¶

Export a stormvogel Model to a UMBI SimpleAts.

Args:: model: a stormvogel Model (DTMC, CTMC, MDP, or POMDP) ignore_unsupported_rewards: if True, silently skip transition reward models

instead of raising an error.

Returns: a umbi.ats.SimpleAts

stormvogel.umbi.translate_to_stormvogel(ats: umbi.ats.simple_ats.SimpleAts, ignore_unsupported_rewards: bool = False, ignore_choice_annotations: bool = False, ignore_branch_annotations: bool = False) → stormvogel.model.model.Model¶

Import a UMBI SimpleAts as a stormvogel Model.

Args:

ats: a umbi.ats.SimpleAts ignore_unsupported_rewards: if True, silently skip reward annotations that have

only choice- or branch-level values (not supported by stormvogel state rewards) instead of raising an error.

ignore_choice_annotations: if True, silently skip choice-level variable valuations: instead of raising an error.
ignore_branch_annotations: if True, silently skip branch-level variable valuations: instead of raising an error.

Returns: a stormvogel Model

class stormvogel.umbi.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.umbi.write_to_umb(model: stormvogel.model.model.Model, path: str | pathlib.Path, ignore_unsupported_rewards: bool = False) → None¶: Translate a stormvogel Model and write it to a .umb file.

stormvogel.umbi.read_from_umb(path: str | pathlib.Path, ignore_unsupported_rewards: bool = False, ignore_choice_annotations: bool = False, ignore_branch_annotations: bool = False) → stormvogel.model.model.Model¶: Read a .umb file and return it as a stormvogel Model.