stormvogel.stormpy_utils

Submodules

• stormvogel.stormpy_utils.convert_results
• stormvogel.stormpy_utils.magic
• stormvogel.stormpy_utils.mapping
• stormvogel.stormpy_utils.model_checking

Attributes

stormpy
stormpy

Functions

convert_scheduler_to_stormvogel(model, stormpy_scheduler)	Converts a stormpy scheduler to a stormvogel scheduler
convert_model_checking_result(...)	Takes a model checking result from stormpy and its associated model and converts it to a stormvogel representation
value_to_stormpy(...)	converts a stormvogel transition value to a stormpy (pycarl) value
stormvogel_to_stormpy(...)
value_to_stormvogel(→ stormvogel.model.Value)	Converts a stormpy transition value to a stormvogel one
stormpy_to_stormvogel(→ stormvogel.model.Model | None)
from_prism([prism_code])	Create a model from prism.

Package Contents

stormvogel.stormpy_utils.stormpy = None

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

Converts a stormpy scheduler to 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

Takes a model checking result from stormpy and its associated model and converts it to a stormvogel representation

stormvogel.stormpy_utils.stormpy = None

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

converts a stormvogel transition value to a stormpy (pycarl) value

stormvogel.stormpy_utils.stormvogel_to_stormpy(model: stormvogel.model.Model) → stormpy.storage.SparseDtmc | stormpy.storage.SparseMdp | stormpy.storage.SparseCtmc | stormpy.storage.SparsePomdp | None

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

Converts a stormpy transition value to a stormvogel one

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 | None

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

Create a model from prism.