stormvogel.stormpy_utils

Submodules

• stormvogel.stormpy_utils.convert_results
• stormvogel.stormpy_utils.magic
• stormvogel.stormpy_utils.mapping
• stormvogel.stormpy_utils.mec
• stormvogel.stormpy_utils.model_checking
• stormvogel.stormpy_utils.parametric_analysis
• stormvogel.stormpy_utils.stormpy_to_stormvogel
• stormvogel.stormpy_utils.stormvogel_to_stormpy

Functions

convert_scheduler_to_stormvogel(model, stormpy_scheduler)	Convert a stormpy scheduler to a stormvogel scheduler.
convert_model_checking_result(...)	Convert a stormpy model checking result to a stormvogel result.
map_result_to_original_model(→ stormvogel.result.Result)	Map a model checking result back to the original model states.
convert_pareto_result(→ stormvogel.result.ParetoResult)	Convert a stormpy Pareto curve result to a ParetoResult.
stormvogel_to_stormpy(model)	Convert a stormvogel model to a stormpy sparse model.
value_to_stormvogel(→ stormvogel.model.value.Value)	Convert a stormpy transition value to a stormvogel value.
stormpy_to_stormvogel(→ stormvogel.model.model.Model)	Convert a stormpy sparse model to a stormvogel model.
from_prism([prism_code])	Create a stormvogel model from a PRISM program.

Package Contents

stormvogel.stormpy_utils.convert_scheduler_to_stormvogel(model: stormvogel.model.Model, stormpy_scheduler: stormpy.storage.Scheduler)

Convert a stormpy scheduler to a stormvogel scheduler.

Parameters:

• model – The stormvogel model associated with the scheduler.

• stormpy_scheduler – The stormpy scheduler to convert.

Returns:

A stormvogel Scheduler.

stormvogel.stormpy_utils.convert_model_checking_result(model: stormvogel.model.Model, stormpy_result: stormpy.ExplicitQuantitativeCheckResult | stormpy.ExplicitQualitativeCheckResult | stormpy.ExplicitParametricQuantitativeCheckResult, with_scheduler: bool = True) → stormvogel.result.Result | None

Convert a stormpy model checking result to a stormvogel result.

Parameters:

• model – The stormvogel model associated with the result.

• stormpy_result – The stormpy model checking result.

• with_scheduler – Whether to include the scheduler in the result.

Returns:

The converted stormvogel result, or None if conversion fails.

Raises:

RuntimeError – If the result type is unsupported.

stormvogel.stormpy_utils.map_result_to_original_model(result: stormvogel.result.Result, original_model: stormvogel.model.Model, recreated_model: stormvogel.model.Model) → stormvogel.result.Result

Map a model checking result back to the original model states.

Remap state references from the recreated model to the original model to preserve object identities.

Parameters:

• result – The model checking result using recreated model states.

• original_model – The original stormvogel model.

• recreated_model – The recreated model whose states appear in the result.

Returns:

A new result with state references mapped to the original model.

stormvogel.stormpy_utils.convert_pareto_result(stormpy_result: stormpy.ExplicitParetoCurveCheckResultDouble, stormpy_property: stormpy.Property) → stormvogel.result.ParetoResult

Convert a stormpy Pareto curve result to a ParetoResult.

Parameters:

• stormpy_result – The stormpy Pareto curve check result.

• stormpy_property – The parsed property, used to extract objective labels.

Returns:

A ParetoResult with vertices and labels.

stormvogel.stormpy_utils.stormvogel_to_stormpy(model)

Convert a stormvogel model to a stormpy sparse model.

Parameters:

model – The stormvogel model to convert.

Returns:

The equivalent stormpy sparse model.

stormvogel.stormpy_utils.value_to_stormvogel(value, sparsemodel) → stormvogel.model.value.Value

Convert a stormpy transition value to a stormvogel value.

Parameters:

• value – The stormpy transition value.

• sparsemodel – The stormpy sparse model providing context.

Returns:

The converted stormvogel value.

stormvogel.stormpy_utils.stormpy_to_stormvogel(sparsemodel: stormpy.storage.SparseDtmc | stormpy.storage.SparseMdp | stormpy.storage.SparseCtmc | stormpy.storage.SparsePomdp | stormpy.storage.SparseMA) → stormvogel.model.model.Model

Convert a stormpy sparse model to a stormvogel model.

Parameters:

sparsemodel – The stormpy sparse model to convert.

Returns:

The equivalent stormvogel model.

Raises:

NotImplementedError – If the model type is not supported.

stormvogel.stormpy_utils.from_prism(prism_code='stormpy.storage.storage.PrismProgram')

Create a stormvogel model from a PRISM program.

Parameters:

prism_code – The PRISM program to build from.

Returns:

The converted stormvogel model.