stormvogel.stormpy_utils.stormvogel_to_stormpy¶

Attributes¶

stormpy

Functions¶

`value_to_stormpy`(...)	Convert a stormvogel transition value to a stormpy value.
`build_matrix`(→ stormpy.storage.SparseMatrix)	Build a stormpy sparse matrix from a stormvogel model.
`build_choice_labeling`(model)	Build a stormpy choice labeling object from a stormvogel model.
`build_state_labeling`(→ stormpy.storage.StateLabeling)	Build a stormpy state labeling object from a stormvogel model.
`build_reward_models`(→ dict[str, stormpy.SparseRewardModel])	Build stormpy reward models from a stormvogel model.
`build_state_valuations`(...)	Build a stormpy state valuations object from a stormvogel model.
`_apply_state_valuations`(→ None)	Assign state valuations to a stormpy component, if present.
`build_observations`(→ list[int])	Build the observation class mapping for a POMDP.
`build_markovian_states_bitvector`(→ stormpy.BitVector)	Build a bitvector indicating which states are Markovian.
`build_dtmc`(model, matrix, state_labeling, ...)	Build a stormpy sparse DTMC from components.
`build_mdp`(model, matrix, choice_labeling, ...)	Build a stormpy sparse MDP from components.
`build_ctmc`(model, matrix, state_labeling, ...)	Build a stormpy sparse CTMC from components.
`build_pomdp`(model, matrix, choice_labeling, ...)	Build a stormpy sparse POMDP from components.
`build_ma`(model, matrix, choice_labeling, ...)	Build a stormpy sparse MA from components.
`_all_non_init_states_incoming_transition`(→ bool)	Check whether all non-initial states have an incoming transition.
`_all_states_outgoing_transition`(→ bool)	Check whether all states have at least one choice.
`stormvogel_to_stormpy`(model)	Convert a stormvogel model to a stormpy sparse model.

Module Contents¶

stormvogel.stormpy_utils.stormvogel_to_stormpy.stormpy = None¶

stormvogel.stormpy_utils.stormvogel_to_stormpy.value_to_stormpy(value: stormvogel.model.value.Value, variables: list[stormpy.pycarl.Variable], model: stormvogel.model.model.Model) → stormpy.pycarl.cln.FactorizedRationalFunction | stormpy.pycarl.Interval | Value¶

Convert a stormvogel transition value to a stormpy value.

Parametric values are delegated to the active parametric backend’s to_pycarl() hook; the pycarl variables are passed in as a mapping from parameter name to pycarl.Variable so that the backend does not have to (re-)create them.

Parameters:

value – The stormvogel value to convert.
variables – The list of pycarl variables for parametric models, aligned with model.parameter_symbols() by index.
model – The stormvogel model providing context.

Returns:

The converted stormpy value.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_matrix(model: stormvogel.model.model.Model, choice_labeling, variables: list) → stormpy.storage.SparseMatrix¶

Build a stormpy sparse matrix from a stormvogel model.

Also populate the choice labeling by reference.

Parameters:

model – The stormvogel model.
choice_labeling – The choice labeling object to populate (mutated in place).
variables – The list of pycarl variables for parametric models.

Returns:

The constructed stormpy sparse matrix.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_choice_labeling(model: stormvogel.model.model.Model)¶

Build a stormpy choice labeling object from a stormvogel model.

Parameters:: model – The stormvogel model.
Returns:: The constructed choice labeling.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_state_labeling(model: stormvogel.model.model.Model) → stormpy.storage.StateLabeling¶

Build a stormpy state labeling object from a stormvogel model.

Parameters:: model – The stormvogel model.
Returns:: The constructed state labeling.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_reward_models(model: stormvogel.model.model.Model) → dict[str, stormpy.SparseRewardModel]¶

Build stormpy reward models from a stormvogel model.

Parameters:: model – The stormvogel model.
Returns:: A dictionary mapping reward model names to stormpy reward models.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_state_valuations(model: stormvogel.model.model.Model) → stormpy.storage.StateValuation | None¶

Build a stormpy state valuations object from a stormvogel model.

Only variables with a declared domain are exported. Variables without a domain are skipped. Returns None when no domain-bearing variables exist, in which case the caller should omit components.state_valuations.

CategoricalDomain variables are encoded as integers (index into domain.values); the categorical labels are not preserved in stormpy.

Parameters:: model – The stormvogel model.
Returns:: The constructed state valuations, or None.
Raises:: ValueError – If a state is missing a value for a domain-bearing variable, or if a variable has a None value (not supported by stormpy).

stormvogel.stormpy_utils.stormvogel_to_stormpy._apply_state_valuations(components, state_valuations) → None¶: Assign state valuations to a stormpy component, if present.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_observations(model: stormvogel.model.model.Model) → list[int]¶

Build the observation class mapping for a POMDP.

Parameters:

model – The stormvogel POMDP model.

Returns:

A list of observation class indices per state.

Raises:

RuntimeError – If any state lacks an observation.
NotImplementedError – If probabilistic observations are used.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_markovian_states_bitvector(model: stormvogel.model.model.Model) → stormpy.BitVector¶

Build a bitvector indicating which states are Markovian.

Parameters:: model – The stormvogel MA model.
Returns:: A stormpy bitvector of Markovian state indices.
Raises:: RuntimeError – If the model has no Markovian states defined.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_dtmc(model: stormvogel.model.model.Model, matrix, state_labeling, reward_models, state_valuations)¶

Build a stormpy sparse DTMC from components.

Parameters:

model – The stormvogel model.
matrix – The sparse transition matrix.
state_labeling – The state labeling.
reward_models – The reward models dictionary.
state_valuations – The state valuations.

Returns:

The constructed stormpy DTMC.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_mdp(model: stormvogel.model.model.Model, matrix, choice_labeling, state_labeling, reward_models, state_valuations)¶

Build a stormpy sparse MDP from components.

Parameters:

model – The stormvogel model.
matrix – The sparse transition matrix.
choice_labeling – The choice labeling.
state_labeling – The state labeling.
reward_models – The reward models dictionary.
state_valuations – The state valuations.

Returns:

The constructed stormpy MDP.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_ctmc(model: stormvogel.model.model.Model, matrix, state_labeling, reward_models, state_valuations)¶

Build a stormpy sparse CTMC from components.

Parameters:

model – The stormvogel model.
matrix – The sparse transition matrix.
state_labeling – The state labeling.
reward_models – The reward models dictionary.
state_valuations – The state valuations.

Returns:

The constructed stormpy CTMC.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_pomdp(model: stormvogel.model.model.Model, matrix, choice_labeling, state_labeling, observations, reward_models, state_valuations)¶

Build a stormpy sparse POMDP from components.

Parameters:

model – The stormvogel model.
matrix – The sparse transition matrix.
choice_labeling – The choice labeling.
state_labeling – The state labeling.
observations – The observation class indices per state.
reward_models – The reward models dictionary.
state_valuations – The state valuations.

Returns:

The constructed stormpy POMDP.

stormvogel.stormpy_utils.stormvogel_to_stormpy.build_ma(model: stormvogel.model.model.Model, matrix, choice_labeling, state_labeling, markovian_states_bitvector, reward_models, state_valuations)¶

Build a stormpy sparse MA from components.

Parameters:

model – The stormvogel model.
matrix – The sparse transition matrix.
choice_labeling – The choice labeling.
state_labeling – The state labeling.
markovian_states_bitvector – The bitvector of Markovian states.
reward_models – The reward models dictionary.
state_valuations – The state valuations.

Returns:

The constructed stormpy MA.

stormvogel.stormpy_utils.stormvogel_to_stormpy._all_non_init_states_incoming_transition(model) → bool¶

Check whether all non-initial states have an incoming transition.

Parameters:: model – The stormvogel model to check.
Returns:: True if every non-initial state has at least one incoming transition.

stormvogel.stormpy_utils.stormvogel_to_stormpy._all_states_outgoing_transition(model) → bool¶: Check whether all states have at least one choice.

stormvogel.stormpy_utils.stormvogel_to_stormpy.stormvogel_to_stormpy(model: stormvogel.model.model.Model)¶

Convert a stormvogel model to a stormpy sparse model.

Parameters:

model – The stormvogel model to convert.

Returns:

The equivalent stormpy sparse model.

Raises:

RuntimeError – If the model has states without outgoing transitions, unassigned variables, multiple states without incoming transitions, or zero-probability transitions.
NotImplementedError – If the model type is not supported.