stormvogel.stormpy_utils.model_checking

Attributes

stormpy

mdp

Functions

model_checking(→ stormvogel.result.Result | None)

Perform model checking on a stormvogel model using stormpy.

Module Contents

stormvogel.stormpy_utils.model_checking.stormpy = None
stormvogel.stormpy_utils.model_checking.model_checking(model: stormvogel.model.Model, prop: str | None = None, scheduler: bool = True) → stormvogel.result.Result | None

Perform model checking on a stormvogel model using stormpy.

Convert the model to stormpy, run model checking, and convert the result back. If no property string is provided, a widget for building one is displayed.

Parameters:

  • model – The stormvogel model to check.

  • prop – A property string to check, or None to display a property builder widget.

  • scheduler – Whether to extract a scheduler from the result.

Returns:

The model checking result, or None if no property was provided.

Raises:

RuntimeError – If the model is not stochastic.

stormvogel.stormpy_utils.model_checking.mdp