stormvogel.stormpy_utils.convert_results

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.

Module Contents

stormvogel.stormpy_utils.convert_results.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_results.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.convert_results.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_results.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.